From 40b180995ab1b2b6748d5eb217d8fbfd21b4a51b Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Fri, 19 Nov 2021 10:34:21 +0100 Subject: [PATCH] [Ada] Proof of System.Val_Util utilities for 'Value support 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. --- gcc/ada/libgnat/s-valboo.adb | 15 +-- gcc/ada/libgnat/s-valboo.ads | 16 +-- gcc/ada/libgnat/s-valuer.adb | 5 +- gcc/ada/libgnat/s-valueu.adb | 2 +- gcc/ada/libgnat/s-valuti.adb | 139 ++++++++++++++++++------ gcc/ada/libgnat/s-valuti.ads | 201 +++++++++++++++++++++++++++++++++-- 6 files changed, 307 insertions(+), 71 deletions(-) diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb index edfa09af2d1..7559de38395 100644 --- a/gcc/ada/libgnat/s-valboo.adb +++ b/gcc/ada/libgnat/s-valboo.adb @@ -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; diff --git a/gcc/ada/libgnat/s-valboo.ads b/gcc/ada/libgnat/s-valboo.ads index d8bed1a3f89..c4448e47dfa 100644 --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -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; diff --git a/gcc/ada/libgnat/s-valuer.adb b/gcc/ada/libgnat/s-valuer.adb index ff78c4bfff1..a1793fa2c0e 100644 --- a/gcc/ada/libgnat/s-valuer.adb +++ b/gcc/ada/libgnat/s-valuer.adb @@ -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 diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index b385a9bc84d..5b77358d72a 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -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 diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb index e2ae9e35646..3e62d09b595 100644 --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -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; diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 3223707d5e1..388a884c8e8 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -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;