From 649b3efae598aaf855b8cc453749695dded9fa95 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Wed, 15 Dec 2021 20:10:06 +0100 Subject: [PATCH] [Ada] Proof of System.Val_Uns at gold level gcc/ada/ * libgnat/a-tiinau.ads: Use a procedure for the Scan parameter instead of a function with side-effects. * libgnat/a-tiinau.adb: Idem. * libgnat/a-wtinau.ads: Idem. * libgnat/a-wtinau.adb: Idem. * libgnat/a-ztinau.ads: Idem. * libgnat/a-ztinau.adb: Idem. * libgnat/s-valint.ads: Change the function with side-effects Scan_Integer into a procedure * libgnat/s-vallli.ads: Idem. * libgnat/s-valllli.ads: Idem. * libgnat/s-vallllu.ads: Add SPARK_Mode and pragma to ignore assertions in instance. * libgnat/s-valllu.ads: Idem. * libgnat/s-valuns.ads: Idem. * libgnat/s-valuei.ads: Use a procedure for the Scan_Raw_Unsigned parameter instead of a function with side-effects and change the function with side-effects Scan_Integer into a procedure. * libgnat/s-valuei.adb: Idem. * libgnat/s-valuti.ads: Introduce a ghost function that scans an exponent and complete the postcondition of Scan_Exponent to also describe the value of Ptr after the call. Fix the postcondition of Scan_Underscore. Simplify the definition of Scan_Natural_Ghost. * libgnat/s-valuti.adb: Idem. * libgnat/s-valboo.ads, libgnat/s-valboo.adb: Update calls to First_Non_Space_Ghost. * libgnat/s-valueu.ads: Add functional contracts. * libgnat/s-valueu.adb: Idem. --- gcc/ada/libgnat/a-tiinau.adb | 4 +- gcc/ada/libgnat/a-tiinau.ads | 7 +- gcc/ada/libgnat/a-wtinau.adb | 4 +- gcc/ada/libgnat/a-wtinau.ads | 7 +- gcc/ada/libgnat/a-ztinau.adb | 4 +- gcc/ada/libgnat/a-ztinau.ads | 7 +- gcc/ada/libgnat/s-valboo.adb | 3 +- gcc/ada/libgnat/s-valboo.ads | 6 +- gcc/ada/libgnat/s-valint.ads | 5 +- gcc/ada/libgnat/s-vallli.ads | 5 +- gcc/ada/libgnat/s-valllli.ads | 5 +- gcc/ada/libgnat/s-vallllu.ads | 24 ++- gcc/ada/libgnat/s-valllu.ads | 24 ++- gcc/ada/libgnat/s-valuei.adb | 15 +- gcc/ada/libgnat/s-valuei.ads | 12 +- gcc/ada/libgnat/s-valueu.adb | 436 ++++++++++++++++++++++++++++++++++++++- gcc/ada/libgnat/s-valueu.ads | 462 +++++++++++++++++++++++++++++++++++++++++- gcc/ada/libgnat/s-valuns.ads | 24 ++- gcc/ada/libgnat/s-valuti.adb | 31 +-- gcc/ada/libgnat/s-valuti.ads | 96 +++++---- 20 files changed, 1066 insertions(+), 115 deletions(-) diff --git a/gcc/ada/libgnat/a-tiinau.adb b/gcc/ada/libgnat/a-tiinau.adb index f95d34a..100c5c4 100644 --- a/gcc/ada/libgnat/a-tiinau.adb +++ b/gcc/ada/libgnat/a-tiinau.adb @@ -54,7 +54,7 @@ package body Ada.Text_IO.Integer_Aux is Load_Integer (File, Buf, Stop); end if; - Item := Scan (Buf, Ptr'Access, Stop); + Scan (Buf, Ptr'Access, Stop, Item); Check_End_Of_Field (Buf, Stop, Ptr, Width); end Get; @@ -71,7 +71,7 @@ package body Ada.Text_IO.Integer_Aux is begin String_Skip (From, Pos); - Item := Scan (From, Pos'Access, From'Last); + Scan (From, Pos'Access, From'Last, Item); Last := Pos - 1; exception diff --git a/gcc/ada/libgnat/a-tiinau.ads b/gcc/ada/libgnat/a-tiinau.ads index d995f24..75eb915 100644 --- a/gcc/ada/libgnat/a-tiinau.ads +++ b/gcc/ada/libgnat/a-tiinau.ads @@ -38,8 +38,11 @@ private generic type Num is (<>); - with function Scan - (Str : String; Ptr : not null access Integer; Max : Integer) return Num; + with procedure Scan + (Str : String; + Ptr : not null access Integer; + Max : Integer; + Res : out Num); with procedure Set_Image (V : Num; S : in out String; P : in out Natural); with procedure Set_Image_Width diff --git a/gcc/ada/libgnat/a-wtinau.adb b/gcc/ada/libgnat/a-wtinau.adb index 3934d9b..0628cc6 100644 --- a/gcc/ada/libgnat/a-wtinau.adb +++ b/gcc/ada/libgnat/a-wtinau.adb @@ -54,7 +54,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is Load_Integer (File, Buf, Stop); end if; - Item := Scan (Buf, Ptr'Access, Stop); + Scan (Buf, Ptr'Access, Stop, Item); Check_End_Of_Field (Buf, Stop, Ptr, Width); end Get; @@ -71,7 +71,7 @@ package body Ada.Wide_Text_IO.Integer_Aux is begin String_Skip (From, Pos); - Item := Scan (From, Pos'Access, From'Last); + Scan (From, Pos'Access, From'Last, Item); Last := Pos - 1; exception diff --git a/gcc/ada/libgnat/a-wtinau.ads b/gcc/ada/libgnat/a-wtinau.ads index 97138b1..37ac2d1 100644 --- a/gcc/ada/libgnat/a-wtinau.ads +++ b/gcc/ada/libgnat/a-wtinau.ads @@ -38,8 +38,11 @@ private generic type Num is (<>); - with function Scan - (Str : String; Ptr : not null access Integer; Max : Integer) return Num; + with procedure Scan + (Str : String; + Ptr : not null access Integer; + Max : Integer; + Res : out Num); with procedure Set_Image (V : Num; S : in out String; P : in out Natural); with procedure Set_Image_Width diff --git a/gcc/ada/libgnat/a-ztinau.adb b/gcc/ada/libgnat/a-ztinau.adb index 9f4c4c8..d7df8ef 100644 --- a/gcc/ada/libgnat/a-ztinau.adb +++ b/gcc/ada/libgnat/a-ztinau.adb @@ -54,7 +54,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is Load_Integer (File, Buf, Stop); end if; - Item := Scan (Buf, Ptr'Access, Stop); + Scan (Buf, Ptr'Access, Stop, Item); Check_End_Of_Field (Buf, Stop, Ptr, Width); end Get; @@ -71,7 +71,7 @@ package body Ada.Wide_Wide_Text_IO.Integer_Aux is begin String_Skip (From, Pos); - Item := Scan (From, Pos'Access, From'Last); + Scan (From, Pos'Access, From'Last, Item); Last := Pos - 1; exception diff --git a/gcc/ada/libgnat/a-ztinau.ads b/gcc/ada/libgnat/a-ztinau.ads index 79374f4..c1871af 100644 --- a/gcc/ada/libgnat/a-ztinau.ads +++ b/gcc/ada/libgnat/a-ztinau.ads @@ -38,8 +38,11 @@ private generic type Num is (<>); - with function Scan - (Str : String; Ptr : not null access Integer; Max : Integer) return Num; + with procedure Scan + (Str : String; + Ptr : not null access Integer; + Max : Integer; + Res : out Num); with procedure Set_Image (V : Num; S : in out String; P : in out Natural); with procedure Set_Image_Width diff --git a/gcc/ada/libgnat/s-valboo.adb b/gcc/ada/libgnat/s-valboo.adb index 2bc1b15..54b1265 100644 --- a/gcc/ada/libgnat/s-valboo.adb +++ b/gcc/ada/libgnat/s-valboo.adb @@ -55,7 +55,8 @@ is begin Normalize_String (S, F, L); - pragma Assert (F = System.Val_Util.First_Non_Space_Ghost (S)); + pragma Assert (F = System.Val_Util.First_Non_Space_Ghost + (S, Str'First, Str'Last)); 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 3cd8538..a9afc45 100644 --- a/gcc/ada/libgnat/s-valboo.ads +++ b/gcc/ada/libgnat/s-valboo.ads @@ -51,7 +51,8 @@ is (not System.Val_Util.Only_Space_Ghost (Str, Str'First, Str'Last) and then (declare - F : constant Positive := System.Val_Util.First_Non_Space_Ghost (Str); + F : constant Positive := System.Val_Util.First_Non_Space_Ghost + (Str, Str'First, Str'Last); begin (F <= Str'Last - 3 and then Str (F) in 't' | 'T' @@ -82,7 +83,8 @@ is Pre => Is_Boolean_Image_Ghost (Str), Post => Value_Boolean'Result = - (Str (System.Val_Util.First_Non_Space_Ghost (Str)) in 't' | 'T'); + (Str (System.Val_Util.First_Non_Space_Ghost + (Str, Str'First, Str'Last)) in 't' | 'T'); -- Computes Boolean'Value (Str) end System.Val_Bool; diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads index d85fa75..4fef265 100644 --- a/gcc/ada/libgnat/s-valint.ads +++ b/gcc/ada/libgnat/s-valint.ads @@ -43,10 +43,11 @@ package System.Val_Int is package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned); - function Scan_Integer + procedure Scan_Integer (Str : String; Ptr : not null access Integer; - Max : Integer) return Integer + Max : Integer; + Res : out Integer) renames Impl.Scan_Integer; function Value_Integer (Str : String) return Integer diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index 79098b5..ce1d9ee 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -46,10 +46,11 @@ package System.Val_LLI is Long_Long_Unsigned, Val_LLU.Scan_Raw_Long_Long_Unsigned); - function Scan_Long_Long_Integer + procedure Scan_Long_Long_Integer (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Integer + Max : Integer; + Res : out Long_Long_Integer) renames Impl.Scan_Integer; function Value_Long_Long_Integer (Str : String) return Long_Long_Integer diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads index 3890ef3..176000a 100644 --- a/gcc/ada/libgnat/s-valllli.ads +++ b/gcc/ada/libgnat/s-valllli.ads @@ -46,10 +46,11 @@ package System.Val_LLLI is Long_Long_Long_Unsigned, Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned); - function Scan_Long_Long_Long_Integer + procedure Scan_Long_Long_Long_Integer (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Long_Integer + Max : Integer; + Res : out Long_Long_Long_Integer) renames Impl.Scan_Integer; function Value_Long_Long_Long_Integer diff --git a/gcc/ada/libgnat/s-vallllu.ads b/gcc/ada/libgnat/s-vallllu.ads index db74864..c6c9ece 100644 --- a/gcc/ada/libgnat/s-vallllu.ads +++ b/gcc/ada/libgnat/s-vallllu.ads @@ -32,26 +32,40 @@ -- This package contains routines for scanning modular Long_Long_Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Value_U; -package System.Val_LLLU is +package System.Val_LLLU with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; package Impl is new Value_U (Long_Long_Long_Unsigned); - function Scan_Raw_Long_Long_Long_Unsigned + procedure Scan_Raw_Long_Long_Long_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Long_Unsigned + Max : Integer; + Res : out Long_Long_Long_Unsigned) renames Impl.Scan_Raw_Unsigned; - function Scan_Long_Long_Long_Unsigned + procedure Scan_Long_Long_Long_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Long_Unsigned + Max : Integer; + Res : out Long_Long_Long_Unsigned) renames Impl.Scan_Unsigned; function Value_Long_Long_Long_Unsigned diff --git a/gcc/ada/libgnat/s-valllu.ads b/gcc/ada/libgnat/s-valllu.ads index 9c01152..0a5cb34 100644 --- a/gcc/ada/libgnat/s-valllu.ads +++ b/gcc/ada/libgnat/s-valllu.ads @@ -32,26 +32,40 @@ -- This package contains routines for scanning modular Long_Long_Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Value_U; -package System.Val_LLU is +package System.Val_LLU with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; package Impl is new Value_U (Long_Long_Unsigned); - function Scan_Raw_Long_Long_Unsigned + procedure Scan_Raw_Long_Long_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Unsigned + Max : Integer; + Res : out Long_Long_Unsigned) renames Impl.Scan_Raw_Unsigned; - function Scan_Long_Long_Unsigned + procedure Scan_Long_Long_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Long_Long_Unsigned + Max : Integer; + Res : out Long_Long_Unsigned) renames Impl.Scan_Unsigned; function Value_Long_Long_Unsigned diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb index b89443f..83828d3 100644 --- a/gcc/ada/libgnat/s-valuei.adb +++ b/gcc/ada/libgnat/s-valuei.adb @@ -37,10 +37,11 @@ package body System.Value_I is -- Scan_Integer -- ------------------ - function Scan_Integer + procedure Scan_Integer (Str : String; Ptr : not null access Integer; - Max : Integer) return Int + Max : Integer; + Res : out Int) is Uval : Uns; -- Unsigned result @@ -59,13 +60,13 @@ package body System.Value_I is Bad_Value (Str); end if; - Uval := Scan_Raw_Unsigned (Str, Ptr, Max); + Scan_Raw_Unsigned (Str, Ptr, Max, Uval); -- Deal with overflow cases, and also with largest negative number if Uval > Uns (Int'Last) then if Minus and then Uval = Uns (-(Int'First)) then - return Int'First; + Res := Int'First; else Bad_Value (Str); end if; @@ -73,12 +74,12 @@ package body System.Value_I is -- Negative values elsif Minus then - return -(Int (Uval)); + Res := -(Int (Uval)); -- Positive values else - return Int (Uval); + Res := Int (Uval); end if; end Scan_Integer; @@ -106,7 +107,7 @@ package body System.Value_I is V : Int; P : aliased Integer := Str'First; begin - V := Scan_Integer (Str, P'Access, Str'Last); + Scan_Integer (Str, P'Access, Str'Last, V); Scan_Trailing_Blanks (Str, P); return V; end; diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index 5d1140f..e0a34d9 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -38,19 +38,21 @@ generic type Uns is mod <>; - with function Scan_Raw_Unsigned + with procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Uns; + Max : Integer; + Res : out Uns); package System.Value_I is pragma Preelaborate; - function Scan_Integer + procedure Scan_Integer (Str : String; Ptr : not null access Integer; - Max : Integer) return Int; - -- This function scans the string starting at Str (Ptr.all) for a valid + Max : Integer; + Res : out Int); + -- This procedure scans the string starting at Str (Ptr.all) for a valid -- integer according to the syntax described in (RM 3.5(43)). The substring -- scanned extends no further than Str (Max). There are three cases for the -- return: diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index 819d132..991d4a5 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -29,18 +29,220 @@ -- -- ------------------------------------------------------------------------------ -with System.Val_Util; use System.Val_Util; - package body System.Value_U is + -- Ghost code, loop invariants and assertions in this unit are meant for + -- analysis only, not for run-time checking, as it would be too costly + -- otherwise. This is enforced by setting the assertion policy to Ignore. + + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore, + Assert_And_Cut => Ignore, + Subprogram_Variant => Ignore); + + -- Local lemmas + + procedure Lemma_Digit_Is_Before_Last + (Str : String; + P : Integer; + From : Integer; + To : Integer) + with Ghost, + Pre => Str'Last /= Positive'Last + and then From in Str'Range + and then To in From .. Str'Last + and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + and then P in From .. To + and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F', + Post => P /= Last_Hexa_Ghost (Str (From .. To)) + 1; + -- If the character at position P is a digit, P cannot be the position of + -- of the first non-digit in Str. + + procedure Lemma_End_Of_Scan + (Str : String; + From : Integer; + To : Integer; + Base : Uns; + Acc : Uns) + with Ghost, + Pre => Str'Last /= Positive'Last and then From > To, + Post => Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = + (False, Acc); + -- Unfold the definition of Scan_Based_Number_Ghost on an empty string + + procedure Lemma_Scan_Digit + (Str : String; + P : Integer; + Lst : Integer; + Digit : Uns; + Base : Uns; + Old_Acc : Uns; + Acc : Uns; + Scan_Val : Uns_Option; + Old_Overflow : Boolean; + Overflow : Boolean) + with Ghost, + Pre => Str'Last /= Positive'Last + and then Lst in Str'Range + and then P in Str'First .. Lst + and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + and then Digit = Hexa_To_Unsigned_Ghost (Str (P)) + and then Only_Hexa_Ghost (Str, P, Lst) + and then Base in 2 .. 16 + and then (if Digit < Base and then Old_Acc <= Uns'Last / Base + then Acc = Base * Old_Acc + Digit) + and then (if Digit >= Base + or else Old_Acc > Uns'Last / Base + or else (Old_Acc > (Uns'Last - Base + 1) / Base + and then Acc < Uns'Last / Base) + then Overflow + else Overflow = Old_Overflow) + and then + (if not Old_Overflow then + Scan_Val = Scan_Based_Number_Ghost + (Str, P, Lst, Base, Old_Acc)), + Post => + (if not Overflow then + Scan_Val = Scan_Based_Number_Ghost + (Str, P + 1, Lst, Base, Acc)) + and then + (if Overflow then Old_Overflow or else Scan_Val.Overflow); + -- Unfold the definition of Scan_Based_Number_Ghost when the string starts + -- with a digit. + + procedure Lemma_Scan_Underscore + (Str : String; + P : Integer; + From : Integer; + To : Integer; + Lst : Integer; + Base : Uns; + Acc : Uns; + Scan_Val : Uns_Option; + Overflow : Boolean; + Ext : Boolean) + with Ghost, + Pre => Str'Last /= Positive'Last + and then From in Str'Range + and then To in From .. Str'Last + and then Lst <= To + and then P in From .. Lst + 1 + and then P <= To + and then + (if Ext then + Is_Based_Format_Ghost (Str (From .. To)) + and then Lst = Last_Hexa_Ghost (Str (From .. To)) + else Is_Natural_Format_Ghost (Str (From .. To)) + and then Lst = Last_Number_Ghost (Str (From .. To))) + and then Str (P) = '_' + and then + (if not Overflow then + Scan_Val = Scan_Based_Number_Ghost (Str, P, Lst, Base, Acc)), + Post => P + 1 <= Lst + and then + (if Ext then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + else Str (P + 1) in '0' .. '9') + and then + (if not Overflow then + Scan_Val = Scan_Based_Number_Ghost (Str, P + 1, Lst, Base, Acc)); + -- Unfold the definition of Scan_Based_Number_Ghost when the string starts + -- with an underscore. + + ----------------------------- + -- Local lemma null bodies -- + ----------------------------- + + procedure Lemma_Digit_Is_Before_Last + (Str : String; + P : Integer; + From : Integer; + To : Integer) + is null; + + procedure Lemma_End_Of_Scan + (Str : String; + From : Integer; + To : Integer; + Base : Uns; + Acc : Uns) + is null; + + procedure Lemma_Scan_Underscore + (Str : String; + P : Integer; + From : Integer; + To : Integer; + Lst : Integer; + Base : Uns; + Acc : Uns; + Scan_Val : Uns_Option; + Overflow : Boolean; + Ext : Boolean) + is null; + + --------------------- + -- Last_Hexa_Ghost -- + --------------------- + + function Last_Hexa_Ghost (Str : String) return Positive is + begin + for J in Str'Range loop + if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then + return J - 1; + end if; + + pragma Loop_Invariant + (for all K in Str'First .. J => + Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_'); + end loop; + + return Str'Last; + end Last_Hexa_Ghost; + + ---------------------- + -- Lemma_Scan_Digit -- + ---------------------- + + procedure Lemma_Scan_Digit + (Str : String; + P : Integer; + Lst : Integer; + Digit : Uns; + Base : Uns; + Old_Acc : Uns; + Acc : Uns; + Scan_Val : Uns_Option; + Old_Overflow : Boolean; + Overflow : Boolean) + is + pragma Unreferenced (Str, P, Lst, Scan_Val, Overflow, Old_Overflow); + begin + if Digit >= Base then + null; + + elsif Old_Acc <= (Uns'Last - Base + 1) / Base then + pragma Assert (not Scan_Overflows_Ghost (Digit, Base, Old_Acc)); + + elsif Old_Acc > Uns'Last / Base then + null; + + else + pragma Assert + ((Acc < Uns'Last / Base) = + Scan_Overflows_Ghost (Digit, Base, Old_Acc)); + end if; + end Lemma_Scan_Digit; + ----------------------- -- Scan_Raw_Unsigned -- ----------------------- - function Scan_Raw_Unsigned + procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Uns + Max : Integer; + Res : out Uns) is P : Integer; -- Local copy of the pointer @@ -63,6 +265,40 @@ package body System.Value_U is Digit : Uns; -- Digit value + Ptr_Old : constant Integer := Ptr.all + with Ghost; + Last_Num_Init : constant Integer := + Last_Number_Ghost (Str (Ptr.all .. Max)) + with Ghost; + Init_Val : constant Uns_Option := + Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init) + with Ghost; + Starts_As_Based : constant Boolean := + Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + with Ghost; + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max)) + else Last_Num_Init) + with Ghost; + Is_Based : constant Boolean := + Starts_As_Based + and then Last_Num_Based < Max + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1) + with Ghost; + Based_Val : constant Uns_Option := + (if Starts_As_Based and then not Init_Val.Overflow + then Scan_Based_Number_Ghost + (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) + else Init_Val) + with Ghost; + First_Exp : constant Integer := + (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1) + with Ghost; + begin -- We do not tolerate strings with Str'Last = Positive'Last @@ -85,9 +321,20 @@ package body System.Value_U is Umax10 : constant Uns := Uns'Last / 10; -- Numbers bigger than Umax10 overflow if multiplied by 10 + Old_Uval : Uns with Ghost; + Old_Overflow : Boolean with Ghost; + begin -- Loop through decimal digits loop + pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Init + 1); + pragma Loop_Invariant + (if Overflow then Init_Val.Overflow); + pragma Loop_Invariant + (if not Overflow + then Init_Val = Scan_Based_Number_Ghost + (Str, P, Last_Num_Init, Acc => Uval)); + exit when P > Max; Digit := Character'Pos (Str (P)) - Character'Pos ('0'); @@ -96,6 +343,9 @@ package body System.Value_U is if Digit > 9 then if Str (P) = '_' then + Lemma_Scan_Underscore + (Str, P, Ptr_Old, Max, Last_Num_Init, 10, Uval, + Init_Val, Overflow, False); Scan_Underscore (Str, P, Ptr, Max, False); else exit; @@ -104,6 +354,9 @@ package body System.Value_U is -- Accumulate result, checking for overflow else + Old_Uval := Uval; + Old_Overflow := Overflow; + if Uval <= Umax then Uval := 10 * Uval + Digit; @@ -118,11 +371,22 @@ package body System.Value_U is end if; end if; + Lemma_Scan_Digit + (Str, P, Last_Num_Init, Digit, 10, Old_Uval, Uval, Init_Val, + Old_Overflow, Overflow); + P := P + 1; end if; end loop; + pragma Assert (P = Last_Num_Init + 1); + pragma Assert (Init_Val.Overflow = Overflow); end; + pragma Assert_And_Cut + (P = Last_Num_Init + 1 + and then Overflow = Init_Val.Overflow + and then (if not Overflow then Init_Val.Value = Uval)); + Ptr.all := P; -- Deal with based case. We recognize either the standard '#' or the @@ -153,10 +417,18 @@ package body System.Value_U is UmaxB : constant Uns := Uns'Last / Base; -- Numbers bigger than UmaxB overflow if multiplied by base + Old_Uval : Uns with Ghost; + Old_Overflow : Boolean with Ghost; + begin + pragma Assert + (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f' + then Is_Based_Format_Ghost (Str (P .. Max))); + -- Loop to scan out based integer value loop + -- We require a digit at this stage if Str (P) in '0' .. '9' then @@ -177,9 +449,32 @@ package body System.Value_U is else Uval := Base; + Base := 10; + pragma Assert (Ptr.all = Last_Num_Init + 1); + pragma Assert (if not Overflow then Uval = Init_Val.Value); exit; end if; + Lemma_Digit_Is_Before_Last (Str, P, Last_Num_Init + 2, Max); + + pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based); + pragma Loop_Invariant + (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + and then Digit = Hexa_To_Unsigned_Ghost (Str (P))); + pragma Loop_Invariant + (if Overflow'Loop_Entry then Overflow); + pragma Loop_Invariant + (if Overflow then + Overflow'Loop_Entry or else Based_Val.Overflow); + pragma Loop_Invariant + (if not Overflow + then Based_Val = Scan_Based_Number_Ghost + (Str, P, Last_Num_Based, Base, Uval)); + pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1); + + Old_Uval := Uval; + Old_Overflow := Overflow; + -- If digit is too large, just signal overflow and continue. -- The idea here is to keep scanning as long as the input is -- syntactically valid, even if we have detected overflow @@ -203,6 +498,10 @@ package body System.Value_U is end if; end if; + Lemma_Scan_Digit + (Str, P, Last_Num_Based, Digit, Base, Old_Uval, Uval, + Based_Val, Old_Overflow, Overflow); + -- If at end of string with no base char, not a based number -- but we signal Constraint_Error and set the pointer past -- the end of the field, since this is what the ACVC tests @@ -219,23 +518,62 @@ package body System.Value_U is if Str (P) = Base_Char then Ptr.all := P + 1; + pragma Assert (Ptr.all = Last_Num_Based + 2); + Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval); + pragma Assert (if not Overflow then Uval = Based_Val.Value); exit; -- Deal with underscore elsif Str (P) = '_' then + Lemma_Scan_Underscore + (Str, P, Last_Num_Init + 2, Max, Last_Num_Based, Base, + Uval, Based_Val, Overflow, True); Scan_Underscore (Str, P, Ptr, Max, True); + pragma Assert + (if not Overflow + then Based_Val = Scan_Based_Number_Ghost + (Str, P, Last_Num_Based, Base, Uval)); end if; - end loop; end; + pragma Assert + (if Starts_As_Based then P = Last_Num_Based + 1 + else P = Last_Num_Init + 2); + pragma Assert + (Overflow = + (Init_Val.Overflow + or else Init_Val.Value not in 2 .. 16 + or else (Starts_As_Based and then Based_Val.Overflow))); end if; + pragma Assert_And_Cut + (Overflow = + (Init_Val.Overflow + or else + (Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Init_Val.Value not in 2 .. 16) + or else (Starts_As_Based and then Based_Val.Overflow)) + and then + (if not Overflow then + (if Is_Based then Uval = Based_Val.Value + else Uval = Init_Val.Value)) + and then Ptr.all = First_Exp + and then Base in 2 .. 16 + and then + (if not Overflow then + (if Is_Based then Base = Init_Val.Value else Base = 10))); + -- Come here with scanned unsigned value in Uval. The only remaining -- required step is to deal with exponent if one is present. Scan_Exponent (Str, Ptr, Max, Expon); + pragma Assert + (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) + then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max))); + if Expon /= 0 and then Uval /= 0 then -- For non-zero value, scale by exponent value. No need to do this @@ -246,8 +584,24 @@ package body System.Value_U is UmaxB : constant Uns := Uns'Last / Base; -- Numbers bigger than UmaxB overflow if multiplied by base + Res_Val : constant Uns_Option := + Exponent_Unsigned_Ghost (Uval, Expon, Base) + with Ghost; begin for J in 1 .. Expon loop + pragma Loop_Invariant + (if Overflow'Loop_Entry then Overflow); + pragma Loop_Invariant + (if Overflow + then Overflow'Loop_Entry or else Res_Val.Overflow); + pragma Loop_Invariant + (if not Overflow + then Res_Val = Exponent_Unsigned_Ghost + (Uval, Expon - J + 1, Base)); + + pragma Assert + ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval)); + if Uval > UmaxB then Overflow := True; exit; @@ -255,15 +609,45 @@ package body System.Value_U is Uval := Uval * Base; end loop; + pragma Assert + (Overflow = (Init_Val.Overflow + or else + (Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Init_Val.Value not in 2 .. 16) + or else (Starts_As_Based and then Based_Val.Overflow) + or else Res_Val.Overflow)); + pragma Assert + (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max)); + pragma Assert + (Exponent_Unsigned_Ghost (Uval, 0, Base) = (False, Uval)); + pragma Assert + (if not Overflow then Uval = Res_Val.Value); + pragma Assert + (if not Overflow then + Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max)); end; end if; + pragma Assert + (if Expon = 0 or else Uval = 0 then + Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval)); + pragma Assert + (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max)); + pragma Assert + (if not Overflow then + Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max)); - -- Return result, dealing with sign and overflow + -- Return result, dealing with overflow if Overflow then Bad_Value (Str); + pragma Annotate + (GNATprove, Intentional, + "call to nonreturning subprogram might be executed", + "it is expected that Constraint_Error is raised in case of" + & " overflow"); else - return Uval; + Res := Uval; end if; end Scan_Raw_Unsigned; @@ -271,23 +655,30 @@ package body System.Value_U is -- Scan_Unsigned -- ------------------- - function Scan_Unsigned + procedure Scan_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Uns + Max : Integer; + Res : out Uns) is Start : Positive; -- Save location of first non-blank character begin + pragma Warnings + (Off, + """Start"" is set by ""Scan_Plus_Sign"" but not used after the call"); Scan_Plus_Sign (Str, Ptr, Max, Start); + pragma Warnings + (On, + """Start"" is set by ""Scan_Plus_Sign"" but not used after the call"); if Str (Ptr.all) not in '0' .. '9' then Ptr.all := Start; Bad_Value (Str); end if; - return Scan_Raw_Unsigned (Str, Ptr, Max); + Scan_Raw_Unsigned (Str, Ptr, Max, Res); end Scan_Unsigned; -------------------- @@ -313,9 +704,32 @@ package body System.Value_U is declare V : Uns; P : aliased Integer := Str'First; + + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last) + with Ghost; + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank) + with Ghost; begin - V := Scan_Unsigned (Str, P'Access, Str'Last); + pragma Assert + (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + + declare + P_Acc : constant not null access Integer := P'Access; + begin + Scan_Unsigned (Str, P_Acc, Str'Last, V); + end; + + pragma Assert + (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); + pragma Assert + (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)); + Scan_Trailing_Blanks (Str, P); + + pragma Assert + (Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), V)); return V; end; end if; diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads index 269eb24..b0e3b1e 100644 --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -32,6 +32,22 @@ -- This package contains routines for scanning modular Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); +pragma Warnings (Off, "postcondition does not mention function result"); +-- True postconditions are used to avoid inlining for GNATprove + +with System.Val_Util; use System.Val_Util; + generic type Uns is mod <>; @@ -39,10 +55,314 @@ generic package System.Value_U is pragma Preelaborate; - function Scan_Raw_Unsigned + type Uns_Option (Overflow : Boolean := False) is record + case Overflow is + when True => + null; + when False => + Value : Uns := 0; + end case; + end record with Ghost; + + function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean + is + (for all J in From .. To => + Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') + with + Ghost, + Pre => From > To or else (From >= Str'First and then To <= Str'Last); + -- Ghost function that returns True if S has only hexadecimal characters + -- from index From to index To. + + function Last_Hexa_Ghost (Str : String) return Positive + with + Ghost, + Pre => Str /= "" + and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F', + Post => Last_Hexa_Ghost'Result in Str'Range + and then (if Last_Hexa_Ghost'Result < Str'Last then + Str (Last_Hexa_Ghost'Result + 1) not in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_') + and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result); + -- Ghost function that returns the index of the last character in S that + -- is either an hexadecimal digit or an underscore, which necessarily + -- exists given the precondition on Str. + + function Is_Based_Format_Ghost (Str : String) return Boolean + is + (Str /= "" + and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + and then + (declare + L : constant Positive := Last_Hexa_Ghost (Str); + begin + Str (L) /= '_' + 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 + -- based number, consisting in a sequence of hexadecimal digits possibly + -- separated by single underscores. It may be followed by other characters. + + function Hexa_To_Unsigned_Ghost (X : Character) return Uns is + (case X is + when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'), + when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10, + when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10, + when others => raise Program_Error) + with + Ghost, + Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + -- Ghost function that computes the value corresponding to an hexadecimal + -- digit. + + function Scan_Overflows_Ghost + (Digit : Uns; + Base : Uns; + Acc : Uns) return Boolean + is + (Digit >= Base + or else Acc > Uns'Last / Base + or else Uns'Last - Digit < Base * Acc) + with Ghost; + -- Ghost function which returns True if Digit + Base * Acc overflows or + -- Digit is greater than Base, as this is used by the algorithm for the + -- test of overflow. + + function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) return Uns_Option + with + Ghost, + Subprogram_Variant => (Increases => From), + Pre => Str'Last /= Positive'Last + and then + (From > To or else (From >= Str'First and then To <= Str'Last)) + and then Only_Hexa_Ghost (Str, From, To); + -- Ghost function that recursively computes the based number in Str, + -- assuming Acc has been scanned already and scanning continues at index + -- From. + + function Exponent_Unsigned_Ghost + (Value : Uns; + Exp : Natural; + Base : Uns := 10) return Uns_Option + with + Ghost, + Subprogram_Variant => (Decreases => Exp); + -- Ghost function that recursively computes Value * Base ** Exp + + function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is + (Is_Natural_Format_Ghost (Str) + and then + (declare + Last_Num_Init : constant Integer := Last_Number_Ghost (Str); + Starts_As_Based : constant Boolean := + Last_Num_Init < Str'Last - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) + else Last_Num_Init); + Is_Based : constant Boolean := + Starts_As_Based + and then Last_Num_Based < Str'Last + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + First_Exp : constant Integer := + (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); + begin + (if Starts_As_Based then + Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) + and then Last_Num_Based < Str'Last) + and then Is_Opt_Exponent_Format_Ghost + (Str (First_Exp .. Str'Last)))) + with + Ghost, + Pre => Str'Last /= Positive'Last, + Post => True; + -- Ghost function that determines if Str has the correct format for an + -- unsigned number without a sign character. + -- It is a natural number in base 10, optionally followed by a based + -- number surrounded by delimiters # or :, optionally followed by an + -- exponent part. + + function Raw_Unsigned_Overflows_Ghost + (Str : String; + From, To : Integer) + return Boolean + is + (declare + Last_Num_Init : constant Integer := + Last_Number_Ghost (Str (From .. To)); + Init_Val : constant Uns_Option := + Scan_Based_Number_Ghost (Str, From, Last_Num_Init); + Starts_As_Based : constant Boolean := + Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) + else Last_Num_Init); + Is_Based : constant Boolean := + Starts_As_Based + and then Last_Num_Based < To + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Based_Val : constant Uns_Option := + (if Starts_As_Based and then not Init_Val.Overflow + then Scan_Based_Number_Ghost + (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) + else Init_Val); + First_Exp : constant Integer := + (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); + Expon : constant Natural := + (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) + then Scan_Exponent_Ghost (Str (First_Exp .. To)) + else 0); + begin + Init_Val.Overflow + or else + (Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Init_Val.Value not in 2 .. 16) + or else + (Starts_As_Based + and then Based_Val.Overflow) + or else + (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) + and then + (declare + Base : constant Uns := + (if Is_Based then Init_Val.Value else 10); + Value : constant Uns := + (if Is_Based then Based_Val.Value else Init_Val.Value); + begin + Exponent_Unsigned_Ghost + (Value, Expon, Base).Overflow))) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then From in Str'Range + and then To in From .. Str'Last + and then Str (From) in '0' .. '9', + Post => True; + -- Ghost function that determines if the computation of the unsigned number + -- represented by Str will overflow. The computation overflows if either: + -- * The computation of the decimal part overflows, + -- * The decimal part is followed by a valid delimiter for a based + -- part, and the number corresponding to the base is not a valid base, + -- * The computation of the based part overflows, or + -- * There is an exponent and the computation of the exponentiation + -- overflows. + + function Scan_Raw_Unsigned_Ghost + (Str : String; + From, To : Integer) + return Uns + is + (declare + Last_Num_Init : constant Integer := + Last_Number_Ghost (Str (From .. To)); + Init_Val : constant Uns_Option := + Scan_Based_Number_Ghost (Str, From, Last_Num_Init); + Starts_As_Based : constant Boolean := + Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) + else Last_Num_Init); + Is_Based : constant Boolean := + Starts_As_Based + and then Last_Num_Based < To + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + Based_Val : constant Uns_Option := + (if Starts_As_Based and then not Init_Val.Overflow + then Scan_Based_Number_Ghost + (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) + else Init_Val); + First_Exp : constant Integer := + (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); + Expon : constant Natural := + (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) + then Scan_Exponent_Ghost (Str (First_Exp .. To)) + else 0); + Base : constant Uns := + (if Is_Based then Init_Val.Value else 10); + Value : constant Uns := + (if Is_Based then Based_Val.Value else Init_Val.Value); + begin + Exponent_Unsigned_Ghost (Value, Expon, Base).Value) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then From in Str'Range + and then To in From .. Str'Last + and then Str (From) in '0' .. '9' + and then not Raw_Unsigned_Overflows_Ghost (Str, From, To), + Post => True; + -- Ghost function that scans an unsigned number without a sign character + + function Raw_Unsigned_Last_Ghost + (Str : String; + From, To : Integer) + return Positive + is + (declare + Last_Num_Init : constant Integer := + Last_Number_Ghost (Str (From .. To)); + Starts_As_Based : constant Boolean := + Last_Num_Init < To - 1 + and then Str (Last_Num_Init + 1) in '#' | ':' + and then Str (Last_Num_Init + 2) in + '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; + Last_Num_Based : constant Integer := + (if Starts_As_Based + then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To)) + else Last_Num_Init); + Is_Based : constant Boolean := + Starts_As_Based + and then Last_Num_Based < To + and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1); + First_Exp : constant Integer := + (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1); + begin + (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To)) + then First_Exp + elsif Str (First_Exp + 1) in '-' | '+' then + Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1 + else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1)) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then From in Str'Range + and then To in From .. Str'Last + and then Str (From) in '0' .. '9', + Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1; + -- Ghost function that returns the position of the cursor once an unsigned + -- number has been seen. + + procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Uns; + Max : Integer; + Res : out Uns) + with Pre => Str'Last /= Positive'Last + and then Ptr.all in Str'Range + and then Max in Ptr.all .. Str'Last + and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)), + Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max) + and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max) + and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max); + -- This function scans the string starting at Str (Ptr.all) for a valid -- integer according to the syntax described in (RM 3.5(43)). The substring -- scanned extends no further than Str (Max). Note: this does not scan @@ -106,26 +426,158 @@ package System.Value_U is -- Note: if Str is empty, i.e. if Max is less than Ptr, then this is a -- special case of an all-blank string, and Ptr is unchanged, and hence -- is greater than Max as required in this case. + -- ??? This is not the case. We will read Str (Ptr.all) without checking + -- and increase Ptr.all by one. -- -- Note: this routine should not be called with Str'Last = Positive'Last. -- If this occurs Program_Error is raised with a message noting that this -- case is not supported. Most such cases are eliminated by the caller. - function Scan_Unsigned + procedure Scan_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Uns; + Max : Integer; + Res : out Uns) + with Pre => Str'Last /= Positive'Last + and then Ptr.all in Str'Range + and then Max in Ptr.all .. Str'Last + and then not Only_Space_Ghost (Str, Ptr.all, Max) + and then + (declare + Non_Blank : constant Positive := + First_Non_Space_Ghost (Str, Ptr.all, Max); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + begin + Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))), + Post => + (declare + Non_Blank : constant Positive := + First_Non_Space_Ghost (Str, Ptr.all'Old, Max); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + begin + not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max) + and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max) + and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max)); + -- Same as Scan_Raw_Unsigned, except scans optional leading -- blanks, and an optional leading plus sign. -- -- Note: if a minus sign is present, Constraint_Error will be raised. -- Note: trailing blanks are not scanned. + function Slide_To_1 (Str : String) return String + with Ghost, + Post => + Only_Space_Ghost (Str, Str'First, Str'Last) = + (for all J in Str'First .. Str'Last => + Slide_To_1'Result (J - Str'First + 1) = ' '); + -- Slides Str so that it starts at 1 + + function Slide_If_Necessary (Str : String) return String is + (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str) + with Ghost, + Post => + Only_Space_Ghost (Str, Str'First, Str'Last) = + Only_Space_Ghost (Slide_If_Necessary'Result, + Slide_If_Necessary'Result'First, + Slide_If_Necessary'Result'Last); + -- If Str'Last = Positive'Last then slides Str so that it starts at 1 + + function Is_Unsigned_Ghost (Str : String) return Boolean is + (declare + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + begin + Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) + and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last) + and then Only_Space_Ghost + (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) + with Ghost, + Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Last /= Positive'Last, + Post => True; + -- Ghost function that determines if Str has the correct format for an + -- unsigned number, consisting in some blank characters, an optional + -- + sign, a raw unsigned number which does not overflow and then some + -- more blank characters. + + function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is + (declare + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + begin + Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)) + with Ghost, + Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Last /= Positive'Last + and then Is_Unsigned_Ghost (Str), + Post => True; + -- Ghost function that returns True if Val is the value corresponding to + -- the unsigned number represented by Str. + function Value_Unsigned - (Str : String) return Uns; + (Str : String) return Uns + with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Length /= Positive'Last + and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)), + Post => + Is_Value_Unsigned_Ghost + (Slide_If_Necessary (Str), Value_Unsigned'Result), + Subprogram_Variant => (Decreases => Str'First); -- Used in computing X'Value (Str) where X is a modular integer type whose -- modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str -- is the string argument of the attribute. Constraint_Error is raised if -- the string is malformed, or if the value is out of range. +private + + ----------------------------- + -- Exponent_Unsigned_Ghost -- + ----------------------------- + + function Exponent_Unsigned_Ghost + (Value : Uns; + Exp : Natural; + Base : Uns := 10) return Uns_Option + is + (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value) + elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True) + else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); + + ----------------------------- + -- Scan_Based_Number_Ghost -- + ----------------------------- + + function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) return Uns_Option + is + (if From > To then (Overflow => False, Value => Acc) + elsif Str (From) = '_' + then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc) + elsif Scan_Overflows_Ghost + (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) + then (Overflow => True) + else Scan_Based_Number_Ghost + (Str, From + 1, To, Base, + Base * Acc + Hexa_To_Unsigned_Ghost (Str (From)))); + + ---------------- + -- Slide_To_1 -- + ---------------- + + function Slide_To_1 (Str : String) return String is + (declare + Res : constant String (1 .. Str'Length) := Str; + begin + Res); + end System.Value_U; diff --git a/gcc/ada/libgnat/s-valuns.ads b/gcc/ada/libgnat/s-valuns.ads index 2a65753..23f73ed 100644 --- a/gcc/ada/libgnat/s-valuns.ads +++ b/gcc/ada/libgnat/s-valuns.ads @@ -32,26 +32,40 @@ -- This package contains routines for scanning modular Unsigned -- values for use in Text_IO.Modular_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Value_U; -package System.Val_Uns is +package System.Val_Uns with SPARK_Mode is pragma Preelaborate; subtype Unsigned is Unsigned_Types.Unsigned; package Impl is new Value_U (Unsigned); - function Scan_Raw_Unsigned + procedure Scan_Raw_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Unsigned + Max : Integer; + Res : out Unsigned) renames Impl.Scan_Raw_Unsigned; - function Scan_Unsigned + procedure Scan_Unsigned (Str : String; Ptr : not null access Integer; - Max : Integer) return Unsigned + Max : Integer; + Res : out Unsigned) renames Impl.Scan_Unsigned; function Value_Unsigned diff --git a/gcc/ada/libgnat/s-valuti.adb b/gcc/ada/libgnat/s-valuti.adb index 1a27dbe..4da585a 100644 --- a/gcc/ada/libgnat/s-valuti.adb +++ b/gcc/ada/libgnat/s-valuti.adb @@ -66,14 +66,17 @@ is -- First_Non_Space_Ghost -- --------------------------- - function First_Non_Space_Ghost (S : String) return Positive is + function First_Non_Space_Ghost + (S : String; + From, To : Integer) return Positive + is begin - for J in S'Range loop + for J in From .. To loop if S (J) /= ' ' then return J; end if; - pragma Loop_Invariant (for all K in S'First .. J => S (K) = ' '); + pragma Loop_Invariant (for all K in From .. J => S (K) = ' '); end loop; raise Program_Error; @@ -172,6 +175,9 @@ is Exp := 0; return; end if; + pragma Annotate + (CodePeer, False_Positive, "test always false", + "the slice might be empty or not start with an 'e'"); -- We have an E/e, see if sign follows @@ -222,7 +228,6 @@ is pragma Assert (Is_Natural_Format_Ghost (Rest)); loop - pragma Assert (Str (P) = Rest (P)); pragma Assert (Str (P) in '0' .. '9'); if X < (Integer'Last / 10) then @@ -230,17 +235,11 @@ is end if; pragma Loop_Invariant (X >= 0); - pragma Loop_Invariant (P in P'Loop_Entry .. Last); + pragma Loop_Invariant (P in Rest'First .. 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))); + (Scan_Natural_Ghost (Rest, Rest'First, 0) + = Scan_Natural_Ghost (Rest, P + 1, X)); P := P + 1; @@ -252,6 +251,8 @@ is exit when Str (P) not in '0' .. '9'; end if; end loop; + + pragma Assert (P = Last + 1); end; if M then @@ -298,7 +299,7 @@ is Start := P; - pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max))); + pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max)); -- Skip past an initial plus sign @@ -354,7 +355,7 @@ is Start := P; - pragma Assert (Start = First_Non_Space_Ghost (Str (Ptr.all .. Max))); + pragma Assert (Start = First_Non_Space_Ghost (Str, Ptr.all, Max)); -- Remember an initial minus sign diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index e974251..5c0f2a5 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -41,6 +41,8 @@ pragma Assertion_Policy (Pre => Ignore, Post => Ignore, Contract_Cases => Ignore, Ghost => Ignore); +pragma Warnings (Off, "postcondition does not mention function result"); +-- True postconditions are used to avoid inlining for GNATprove with System.Case_Util; @@ -59,18 +61,23 @@ is (for all J in From .. To => S (J) = ' ') with Ghost, - Pre => From > To or else (From >= S'First and then To <= S'Last); + Pre => From > To or else (From >= S'First and then To <= S'Last), + Post => True; -- 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 + function First_Non_Space_Ghost + (S : String; + From, To : Integer) return Positive with Ghost, - Pre => not Only_Space_Ghost (S, S'First, S'Last), - Post => First_Non_Space_Ghost'Result in S'Range + Pre => From in S'Range + and then To in S'Range + and then not Only_Space_Ghost (S, From, To), + Post => First_Non_Space_Ghost'Result in From .. To and then S (First_Non_Space_Ghost'Result) /= ' ' and then Only_Space_Ghost - (S, S'First, First_Non_Space_Ghost'Result - 1); + (S, From, 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. @@ -117,14 +124,14 @@ is and then (declare F : constant Positive := - First_Non_Space_Ghost (Str (Ptr.all .. Max)); + 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)); + 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) @@ -162,14 +169,14 @@ is and then (declare F : constant Positive := - First_Non_Space_Ghost (Str (Ptr.all .. Max)); + 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)); + First_Non_Space_Ghost (Str, Ptr.all'Old, Max); begin Ptr.all = (if Str (F) = '+' then F + 1 else F) and then Start = F); @@ -195,7 +202,7 @@ is 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. + -- precondition on Str. function Is_Natural_Format_Ghost (Str : String) return Boolean is (Str /= "" @@ -215,7 +222,7 @@ is function Starts_As_Exponent_Format_Ghost (Str : String; - Real : Boolean) return Boolean + Real : Boolean := False) return Boolean is (Str'Length > 1 and then Str (Str'First) in 'E' | 'e' @@ -242,7 +249,7 @@ is function Is_Opt_Exponent_Format_Ghost (Str : String; - Real : Boolean) return Boolean + Real : Boolean := False) return Boolean is (not Starts_As_Exponent_Format_Ghost (Str, Real) or else @@ -265,13 +272,35 @@ is 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; + Pre => Str /= "" and then Str (Str'First) in '0' .. '9' + and then Str'Last < Natural'Last + and then P in Str'First .. Last_Number_Ghost (Str) + 1; -- 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. + function Scan_Exponent_Ghost + (Str : String; + Real : Boolean := False) + return Integer + is + (declare + Plus_Sign : constant Boolean := Str (Str'First + 1) = '+'; + Minus_Sign : constant Boolean := Str (Str'First + 1) = '-'; + Sign : constant Boolean := Plus_Sign or Minus_Sign; + Start : constant Natural := + (if Sign then Str'First + 2 else Str'First + 1); + Value : constant Natural := + Scan_Natural_Ghost (Str (Start .. Str'Last), Start, 0); + begin + (if Minus_Sign then -Value else Value)) + with + Ghost, + Pre => Str'Last < Natural'Last + and then Starts_As_Exponent_Format_Ghost (Str, Real), + Post => (if not Real then Scan_Exponent_Ghost'Result >= 0); + -- Ghost function that scans an exponent + procedure Scan_Exponent (Str : String; Ptr : not null access Integer; @@ -286,17 +315,11 @@ is and then Is_Opt_Exponent_Format_Ghost (Str (Ptr.all .. Max), Real), Post => (if Starts_As_Exponent_Format_Ghost (Str (Ptr.all'Old .. Max), Real) - 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; - 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)) + then Exp = Scan_Exponent_Ghost (Str (Ptr.all'Old .. Max), Real) + and then + (if Str (Ptr.all'Old + 1) in '-' | '+' then + Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 2 .. Max)) + 1 + else Ptr.all = Last_Number_Ghost (Str (Ptr.all'Old + 1 .. Max)) + 1) 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 @@ -340,7 +363,7 @@ is Str (P + 1) in '0' .. '9'), Post => P = P'Old + 1 - and then Ptr.all = Ptr.all; + and then Ptr.all'Old = Ptr.all; -- Called if an underscore is encountered while scanning digits. Str (P) -- contains the underscore. Ptr is the pointer to be returned to the -- ultimate caller of the scan routine, Max is the maximum subscript in @@ -365,19 +388,20 @@ private Acc : Natural) return Natural is - (if Str (P) = '_' then + (if P > Str'Last + or else Str (P) not in '0' .. '9' | '_' + or else Acc >= Integer'Last / 10 + then + Acc + elsif 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')); + Acc * 10 + + (Integer'(Character'Pos (Str (P))) - + Integer'(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)))); + Scan_Natural_Ghost (Str, P + 1, Shift_Acc))); end System.Val_Util; -- 2.7.4