FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[Ada] Proof of System.Val_Util utilities for 'Value support

Browse source 
gcc/ada/

	* libgnat/s-valboo.adb (First_Non_Space_Ghost): Move to
	utilities.
	(Value_Boolean): Prefix call to First_Non_Space_Ghost.
	* libgnat/s-valboo.ads (First_Non_Space_Ghost): Move to
	utilities.
	(Is_Boolean_Image_Ghost, Value_Boolean): Prefix call to
	First_Non_Space_Ghost.
	* libgnat/s-valuer.adb (Scan_Raw_Real): Adapt to change of
	function Scan_Exponent to procedure.
	* libgnat/s-valueu.adb (Scan_Raw_Unsigned): Adapt to change of
	function Scan_Exponent to procedure.
	* libgnat/s-valuti.adb (First_Non_Space_Ghost): Function moved
	here.
	(Last_Number_Ghost): New ghost query function.
	(Scan_Exponent): Change function with side-effects into
	procedure, to mark in SPARK. Prove procedure wrt contract.
	Change type of local P to avoid possible range check failure (it
	is not known whether this can be activated by callers).
	(Scan_Plus_Sign, Scan_Sign): Change type of local P to avoid
	possible range check failure. Add loop invariants and assertions
	for proof.
	(Scan_Trailing_Blanks): Add loop invariant.
	(Scan_Underscore): Remove SPARK_Mode Off.
	* libgnat/s-valuti.ads (First_Non_Space_Ghost): Function moved
	here.
	(Last_Number_Ghost, Only_Number_Ghost, Is_Natural_Format_Ghost,
	Scan_Natural_Ghost): New ghost query functions.
	(Scan_Plus_Sign, Scan_Sign, Scan_Exponent, Scan_Trailing_Blanks,
	Scan_Underscore): Add functional contracts.
This commit is contained in:
Yannick Moy 2021-11-19 10:34:21 +01:00 • committed by Pierre-Marie de Rodat
parent 6df3ec0e7e
commit 40b180995a
6 changed files with 307 additions and 71 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
gcc/ada/libgnat/s-valboo.adb
View file

@ -43,19 +43,6 @@ package body System.Val_Bool
with SPARK_Mode
is
function First_Non_Space_Ghost (S : String) return Positive is
begin
for J in S'Range loop
if S (J) /= ' ' then
return J;
end if;
pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
end loop;
raise Program_Error;
end First_Non_Space_Ghost;
-------------------
-- Value_Boolean --
-------------------
@ -68,7 +55,7 @@ is
begin
Normalize_String (S, F, L);
pragma Assert (F = First_Non_Space_Ghost (S));
pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S));
if S (F .. L) = "TRUE" then
return True;

16
gcc/ada/libgnat/s-valboo.ads
View file

@ -47,22 +47,11 @@ package System.Val_Bool
is
pragma Preelaborate;
function First_Non_Space_Ghost (S : String) return Positive
with
Ghost,
Pre => not System.Val_Util.Only_Space_Ghost (S, S'First, S'Last),
Post => First_Non_Space_Ghost'Result in S'Range
and then S (First_Non_Space_Ghost'Result) /= ' '
and then System.Val_Util.Only_Space_Ghost
(S, S'First, First_Non_Space_Ghost'Result - 1);
-- Ghost function that returns the index of the first non-space character
-- in S, which necessarily exists given the precondition on S.
function Is_Boolean_Image_Ghost (Str : String) return Boolean is
(not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last)
and then
(declare
F : constant Positive := First_Non_Space_Ghost (Str);
F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str);
begin
(F <= Str'Last - 3
and then Str (F) in 't' | 'T'
@ -92,7 +81,8 @@ is
with
Pre => Is_Boolean_Image_Ghost (Str),
Post =>
Value_Boolean'Result = (Str (First_Non_Space_Ghost (Str)) in 't' | 'T');
Value_Boolean'Result =
(Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T');
-- Computes Boolean'Value (Str)
end System.Val_Bool;

5
gcc/ada/libgnat/s-valuer.adb
View file

@ -511,6 +511,8 @@ package body System.Value_R is
Value : Uns;
-- Mantissa as an Integer
Expon : Integer;
begin
-- The default base is 10
@ -643,7 +645,8 @@ package body System.Value_R is
-- Update pointer and scan exponent
Ptr.all := Index;
Scale := Scale + Scan_Exponent (Str, Ptr, Max, Real => True);
Scan_Exponent (Str, Ptr, Max, Expon, Real => True);
Scale := Scale + Expon;
-- Here is where we check for a bad based number

2
gcc/ada/libgnat/s-valueu.adb
View file

@ -234,7 +234,7 @@ package body System.Value_U is
-- Come here with scanned unsigned value in Uval. The only remaining
-- required step is to deal with exponent if one is present.
Expon := Scan_Exponent (Str, Ptr, Max);
Scan_Exponent (Str, Ptr, Max, Expon);
if Expon /= 0 and then Uval /= 0 then

139
gcc/ada/libgnat/s-valuti.adb
View file

@ -62,6 +62,41 @@ is
end if;
end Bad_Value;
---------------------------
-- First_Non_Space_Ghost --
---------------------------
function First_Non_Space_Ghost (S : String) return Positive is
begin
for J in S'Range loop
if S (J) /= ' ' then
return J;
end if;
pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' ');
end loop;
raise Program_Error;
end First_Non_Space_Ghost;
-----------------------
-- Last_Number_Ghost --
-----------------------
function Last_Number_Ghost (Str : String) return Positive is
begin
for J in Str'Range loop
if Str (J) not in '0' .. '9' | '_' then
return J - 1;
end if;
pragma Loop_Invariant
(for all K in Str'First .. J => Str (K) in '0' .. '9' | '_');
end loop;
return Str'Last;
end Last_Number_Ghost;
----------------------
-- Normalize_String --
----------------------
@ -119,15 +154,14 @@ is
-- Scan_Exponent --
-------------------
function Scan_Exponent
procedure Scan_Exponent
(Str : String;
Ptr : not null access Integer;
Max : Integer;
Real : Boolean := False) return Integer
with
SPARK_Mode => Off -- Function with side-effect through Ptr
Exp : out Integer;
Real : Boolean := False)
is
P : Natural := Ptr.all;
P : Integer := Ptr.all;
M : Boolean;
X : Integer;
@ -135,7 +169,8 @@ is
if P >= Max
or else (Str (P) /= 'E' and then Str (P) /= 'e')
then
return 0;
Exp := 0;
return;
end if;
-- We have an E/e, see if sign follows
@ -146,7 +181,8 @@ is
P := P + 1;
if P > Max then
return 0;
Exp := 0;
return;
else
M := False;
end if;
@ -155,7 +191,8 @@ is
P := P + 1;
if P > Max or else not Real then
return 0;
Exp := 0;
return;
else
M := True;
end if;
@ -165,7 +202,8 @@ is
end if;
if Str (P) not in '0' .. '9' then
return 0;
Exp := 0;
return;
end if;
-- Scan out the exponent value as an unsigned integer. Values larger
@ -176,28 +214,52 @@ is
X := 0;
loop
if X < (Integer'Last / 10) then
X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
end if;
declare
Rest : constant String := Str (P .. Max) with Ghost;
Last : constant Natural := Last_Number_Ghost (Rest) with Ghost;
P := P + 1;
begin
pragma Assert (Is_Natural_Format_Ghost (Rest));
exit when P > Max;
loop
pragma Assert (Str (P) = Rest (P));
pragma Assert (Str (P) in '0' .. '9');
if Str (P) = '_' then
Scan_Underscore (Str, P, Ptr, Max, False);
else
exit when Str (P) not in '0' .. '9';
end if;
end loop;
if X < (Integer'Last / 10) then
X := X * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
end if;
pragma Loop_Invariant (X >= 0);
pragma Loop_Invariant (P in P'Loop_Entry .. Last);
pragma Loop_Invariant (Str (P) in '0' .. '9');
pragma Loop_Invariant
(Scan_Natural_Ghost (Rest, P'Loop_Entry, 0)
= (if P = Max
or else Rest (P + 1) not in '0' .. '9' | '_'
or else X >= Integer'Last / 10
then
X
else
Scan_Natural_Ghost (Rest, P + 1, X)));
P := P + 1;
exit when P > Max;
if Str (P) = '_' then
Scan_Underscore (Str, P, Ptr, Max, False);
else
exit when Str (P) not in '0' .. '9';
end if;
end loop;
end;
if M then
X := -X;
end if;
Ptr.all := P;
return X;
Exp := X;
end Scan_Exponent;
--------------------
@ -209,10 +271,8 @@ is
Ptr : not null access Integer;
Max : Integer;
Start : out Positive)
with
SPARK_Mode => Off -- Not proved yet
is
P : Natural := Ptr.all;
P : Integer := Ptr.all;
begin
if P > Max then
@ -224,6 +284,12 @@ is
while Str (P) = ' ' loop
P := P + 1;
pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
pragma Loop_Invariant (P in Ptr.all .. Max);
pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
pragma Loop_Invariant
(for all J in Ptr.all .. P - 1 => Str (J) = ' ');
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@ -232,6 +298,8 @@ is
Start := P;
pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
-- Skip past an initial plus sign
if Str (P) = '+' then
@ -256,10 +324,8 @@ is
Max : Integer;
Minus : out Boolean;
Start : out Positive)
with
SPARK_Mode => Off -- Not proved yet
is
P : Natural := Ptr.all;
P : Integer := Ptr.all;
begin
-- Deal with case of null string (all blanks). As per spec, we raise
@ -274,6 +340,12 @@ is
while Str (P) = ' ' loop
P := P + 1;
pragma Loop_Invariant (Ptr.all = Ptr.all'Loop_Entry);
pragma Loop_Invariant (P in Ptr.all .. Max);
pragma Loop_Invariant (for some J in P .. Max => Str (J) /= ' ');
pragma Loop_Invariant
(for all J in Ptr.all .. P - 1 => Str (J) = ' ');
if P > Max then
Ptr.all := P;
Bad_Value (Str);
@ -282,6 +354,8 @@ is
Start := P;
pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max)));
-- Remember an initial minus sign
if Str (P) = '-' then
@ -315,15 +389,14 @@ is
-- Scan_Trailing_Blanks --
--------------------------
procedure Scan_Trailing_Blanks (Str : String; P : Positive)
with
SPARK_Mode => Off -- Not proved yet
is
procedure Scan_Trailing_Blanks (Str : String; P : Positive) is
begin
for J in P .. Str'Last loop
if Str (J) /= ' ' then
Bad_Value (Str);
end if;
pragma Loop_Invariant (for all K in P .. J => Str (K) = ' ');
end loop;
end Scan_Trailing_Blanks;
@ -337,8 +410,6 @@ is
Ptr : not null access Integer;
Max : Integer;
Ext : Boolean)
with
SPARK_Mode => Off -- Not proved yet
is
C : Character;

201
gcc/ada/libgnat/s-valuti.ads
View file

@ -47,6 +47,7 @@ with System.Case_Util;
package System.Val_Util
with SPARK_Mode, Pure
is
pragma Unevaluated_Use_Of_Old (Allow);
procedure Bad_Value (S : String)
with
@ -62,6 +63,17 @@ is
-- Ghost function that returns True if S has only space characters from
-- index From to index To.
function First_Non_Space_Ghost (S : String) return Positive
with
Ghost,
Pre => not Only_Space_Ghost (S, S'First, S'Last),
Post => First_Non_Space_Ghost'Result in S'Range
and then S (First_Non_Space_Ghost'Result) /= ' '
and then Only_Space_Ghost
(S, S'First, First_Non_Space_Ghost'Result - 1);
-- Ghost function that returns the index of the first non-space character
-- in S, which necessarily exists given the precondition on S.
procedure Normalize_String
(S : in out String;
F, L : out Integer)
@ -96,7 +108,27 @@ is
Ptr : not null access Integer;
Max : Integer;
Minus : out Boolean;
Start : out Positive);
Start : out Positive)
with
Pre =>
-- Ptr.all .. Max is either an empty range, or a valid range in Str
(Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
and then not Only_Space_Ghost (Str, Ptr.all, Max)
and then
(declare
F : constant Positive :=
First_Non_Space_Ghost (Str (Ptr.all .. Max));
begin
(if Str (F) in '+' | '-' then
F <= Max - 1 and then Str (F + 1) /= ' ')),
Post =>
(declare
F : constant Positive :=
First_Non_Space_Ghost (Str (Ptr.all'Old .. Max));
begin
Minus = (Str (F) = '-')
and then Ptr.all = (if Str (F) in '+' | '-' then F + 1 else F)
and then Start = F);
-- The Str, Ptr, Max parameters are as for the scan routines (Str is the
-- string to be scanned starting at Ptr.all, and Max is the index of the
-- last character in the string). Scan_Sign first scans out any initial
@ -121,17 +153,150 @@ is
(Str : String;
Ptr : not null access Integer;
Max : Integer;
Start : out Positive);
Start : out Positive)
with
Pre =>
-- Ptr.all .. Max is either an empty range, or a valid range in Str
(Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
and then not Only_Space_Ghost (Str, Ptr.all, Max)
and then
(declare
F : constant Positive :=
First_Non_Space_Ghost (Str (Ptr.all .. Max));
begin
(if Str (F) = '+' then
F <= Max - 1 and then Str (F + 1) /= ' ')),
Post =>
(declare
F : constant Positive :=
First_Non_Space_Ghost (Str (Ptr.all'Old .. Max));
begin
Ptr.all = (if Str (F) = '+' then F + 1 else F)
and then Start = F);
-- Same as Scan_Sign, but allows only plus, not minus. This is used for
-- modular types.
function Scan_Exponent
function Only_Number_Ghost (Str : String; From, To : Integer) return Boolean
is
(for all J in From .. To => Str (J) in '0' .. '9' | '_')
with
Ghost,
Pre => From > To or else (From >= Str'First and then To <= Str'Last);
-- Ghost function that returns True if S has only number characters from
-- index From to index To.
function Last_Number_Ghost (Str : String) return Positive
with
Ghost,
Pre => Str /= "" and then Str (Str'First) in '0' .. '9',
Post => Last_Number_Ghost'Result in Str'Range
and then (if Last_Number_Ghost'Result < Str'Last then
Str (Last_Number_Ghost'Result + 1) not in '0' .. '9' | '_')
and then Only_Number_Ghost (Str, Str'First, Last_Number_Ghost'Result);
-- Ghost function that returns the index of the last character in S that
-- is either a figure or underscore, which necessarily exists given the
-- precondition on S.
function Is_Natural_Format_Ghost (Str : String) return Boolean is
(Str /= ""
and then Str (Str'First) in '0' .. '9'
and then
(declare
L : constant Positive := Last_Number_Ghost (Str);
begin
Str (L) in '0' .. '9'
and then (for all J in Str'First .. L =>
(if Str (J) = '_' then Str (J + 1) /= '_'))))
with
Ghost;
-- Ghost function that determines if Str has the correct format for a
-- natural number, consisting in a sequence of figures possibly separated
-- by single underscores. It may be followed by other characters.
function Scan_Natural_Ghost
(Str : String;
P : Natural;
Acc : Natural)
return Natural
is
(if Str (P) = '_' then
Scan_Natural_Ghost (Str, P + 1, Acc)
else
(declare
Shift_Acc : constant Natural :=
Acc * 10 + (Character'Pos (Str (P)) - Character'Pos ('0'));
begin
(if P = Str'Last
or else Str (P + 1) not in '0' .. '9' | '_'
or else Shift_Acc >= Integer'Last / 10
then
Shift_Acc
else
Scan_Natural_Ghost (Str, P + 1, Shift_Acc))))
with
Ghost,
Subprogram_Variant => (Increases => P),
Pre => Is_Natural_Format_Ghost (Str)
and then P in Str'First .. Last_Number_Ghost (Str)
and then Acc < Integer'Last / 10;
-- Ghost function that recursively computes the natural number in Str, up
-- to the first number greater or equal to Natural'Last / 10, assuming Acc
-- has been scanned already and scanning continues at index P.
procedure Scan_Exponent
(Str : String;
Ptr : not null access Integer;
Max : Integer;
Real : Boolean := False) return Integer
Exp : out Integer;
Real : Boolean := False)
with
SPARK_Mode => Off; -- Function with side-effect through Ptr
Pre =>
-- Ptr.all .. Max is either an empty range, or a valid range in Str
(Ptr.all > Max or else (Ptr.all >= Str'First and then Max <= Str'Last))
and then
Max < Natural'Last
and then
(if Ptr.all < Max and then Str (Ptr.all) in 'E' | 'e' then
(declare
Plus_Sign : constant Boolean := Str (Ptr.all + 1) = '+';
Minus_Sign : constant Boolean := Str (Ptr.all + 1) = '-';
Sign : constant Boolean := Plus_Sign or Minus_Sign;
begin
(if Minus_Sign and not Real then True
elsif Sign
and then (Ptr.all > Max - 2
or else Str (Ptr.all + 2) not in '0' .. '9')
then True
else
(declare
Start : constant Natural :=
(if Sign then Ptr.all + 2 else Ptr.all + 1);
begin
Is_Natural_Format_Ghost (Str (Start .. Max)))))),
Post =>
(if Ptr.all'Old < Max and then Str (Ptr.all'Old) in 'E' | 'e' then
(declare
Plus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '+';
Minus_Sign : constant Boolean := Str (Ptr.all'Old + 1) = '-';
Sign : constant Boolean := Plus_Sign or Minus_Sign;
Unchanged : constant Boolean :=
Exp = 0 and Ptr.all = Ptr.all'Old;
begin
(if Minus_Sign and not Real then Unchanged
elsif Sign
and then (Ptr.all'Old > Max - 2
or else Str (Ptr.all'Old + 2) not in '0' .. '9')
then Unchanged
else
(declare
Start : constant Natural :=
(if Sign then Ptr.all'Old + 2 else Ptr.all'Old + 1);
Value : constant Natural :=
Scan_Natural_Ghost (Str (Start .. Max), Start, 0);
begin
Exp = (if Minus_Sign then -Value else Value))))
else
Exp = 0 and Ptr.all = Ptr.all'Old);
-- Called to scan a possible exponent. Str, Ptr, Max are as described above
-- for Scan_Sign. If Ptr.all < Max and Str (Ptr.all) = 'E' or 'e', then an
-- exponent is scanned out, with the exponent value returned in Exp, and
@ -146,18 +311,37 @@ is
-- This routine must not be called with Str'Last = Positive'Last. There is
-- no check for this case, the caller must ensure this condition is met.
procedure Scan_Trailing_Blanks (Str : String; P : Positive);
procedure Scan_Trailing_Blanks (Str : String; P : Positive)
with
Pre => P >= Str'First
and then Only_Space_Ghost (Str, P, Str'Last);
-- Checks that the remainder of the field Str (P .. Str'Last) is all
-- blanks. Raises Constraint_Error if a non-blank character is found.
pragma Warnings
(GNATprove, Off, """Ptr"" is not modified",
Reason => "Ptr is actually modified when raising an exception");
procedure Scan_Underscore
(Str : String;
P : in out Natural;
Ptr : not null access Integer;
Max : Integer;
Ext : Boolean);
Ext : Boolean)
with
Pre => P in Str'Range
and then Str (P) = '_'
and then Max in Str'Range
and then P < Max
and then
(if Ext then
Str (P + 1) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
else
Str (P + 1) in '0' .. '9'),
Post =>
P = P'Old + 1
and then Ptr.all = Ptr.all;
-- Called if an underscore is encountered while scanning digits. Str (P)
-- contains the underscore. Ptr it the pointer to be returned to the
-- contains the underscore. Ptr is the pointer to be returned to the
-- ultimate caller of the scan routine, Max is the maximum subscript in
-- Str, and Ext indicates if extended digits are allowed. In the case
-- where the underscore is invalid, Constraint_Error is raised with Ptr
@ -166,5 +350,6 @@ is
--
-- This routine must not be called with Str'Last = Positive'Last. There is
-- no check for this case, the caller must ensure this condition is met.
pragma Warnings (GNATprove, On, """Ptr"" is not modified");
end System.Val_Util;