From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 7871) id D018A3858D1E; Fri, 2 Sep 2022 07:52:12 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org D018A3858D1E DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1662105132; bh=b9nzMVMRazAAs3gMpJGzGG2/WqDaxcWUBAjyacemd0U=; h=From:To:Subject:Date:From; b=KtXN1V3gpjMY34vSGeJdyrskWyLJXnBipsDWqQDfJTeKOgYuvgnvIUNF3UmK+CM2x 2cjMVmaIFhgLVAuSnapFDStQGKqFBe/r/39w0RvCdBAuCJkLsTUcGSdyW3W20ploPN thpTTwOjWQrXM/sYU3cwnHkDm1Di2AKwUt43Et2U= MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: =?iso-8859-1?q?Marc_Poulhi=E8s?= To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-2363] [Ada] Fix proof of runtime unit System.Value* and System.Image* X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/master X-Git-Oldrev: 6713cc703c0914f993891d8ccb8167b29a8855cc X-Git-Newrev: b3ae28dca103a45bb97ec5b47acad9b9380d1113 Message-Id: <20220902075212.D018A3858D1E@sourceware.org> Date: Fri, 2 Sep 2022 07:52:12 +0000 (GMT) List-Id: https://gcc.gnu.org/g:b3ae28dca103a45bb97ec5b47acad9b9380d1113 commit r13-2363-gb3ae28dca103a45bb97ec5b47acad9b9380d1113 Author: Claire Dross Date: Thu Jul 7 16:04:24 2022 +0200 [Ada] Fix proof of runtime unit System.Value* and System.Image* Refactor specification of the Value* and Image* units and fix proofs. gcc/ada/ * libgnat/a-nbnbig.ads: Add Always_Return annotation. * libgnat/s-vaispe.ads: New ghost unit for the specification of System.Value_I. Restore proofs. * libgnat/s-vauspe.ads: New ghost unit for the specification of System.Value_U. Restore proofs. * libgnat/s-valuei.adb: The specification only subprograms are moved to System.Value_I_Spec. Restore proofs. * libgnat/s-valueu.adb: The specification only subprograms are moved to System.Value_U_Spec. Restore proofs. * libgnat/s-valuti.ads (Uns_Params): Generic unit used to bundle together the specification functions of System.Value_U_Spec. (Int_Params): Generic unit used to bundle together the specification functions of System.Value_I_Spec. * libgnat/s-imagef.adb: It is now possible to instantiate the appropriate specification units instead of creating imported ghost subprograms. * libgnat/s-imagei.adb: Update to refactoring of specifications and fix proofs. * libgnat/s-imageu.adb: Likewise. * libgnat/s-imgint.ads: Ghost parameters are grouped together in a package now. * libgnat/s-imglli.ads: Likewise. * libgnat/s-imgllu.ads: Likewise. * libgnat/s-imgllli.ads: Likewise. * libgnat/s-imglllu.ads: Likewise. * libgnat/s-imguns.ads: Likewise. * libgnat/s-vallli.ads: Likewise. * libgnat/s-valllli.ads: Likewise. * libgnat/s-imagei.ads: Likewise. * libgnat/s-imageu.ads: Likewise. * libgnat/s-vaispe.adb: Likewise. * libgnat/s-valint.ads: Likewise. * libgnat/s-valuei.ads: Likewise. * libgnat/s-valueu.ads: Likewise. * libgnat/s-vauspe.adb: Likewise. Diff: --- gcc/ada/libgnat/a-nbnbig.ads | 2 + gcc/ada/libgnat/s-imagef.adb | 73 +---- gcc/ada/libgnat/s-imagei.adb | 252 ++++++++--------- gcc/ada/libgnat/s-imagei.ads | 36 +-- gcc/ada/libgnat/s-imageu.adb | 194 ++++++------- gcc/ada/libgnat/s-imageu.ads | 44 +-- gcc/ada/libgnat/s-imgint.ads | 27 +- gcc/ada/libgnat/s-imglli.ads | 30 +- gcc/ada/libgnat/s-imgllli.ads | 27 +- gcc/ada/libgnat/s-imglllu.ads | 18 +- gcc/ada/libgnat/s-imgllu.ads | 18 +- gcc/ada/libgnat/s-imguns.ads | 18 +- gcc/ada/libgnat/s-vaispe.adb | 87 ++++++ gcc/ada/libgnat/s-vaispe.ads | 199 +++++++++++++ gcc/ada/libgnat/s-valint.ads | 21 +- gcc/ada/libgnat/s-vallli.ads | 22 +- gcc/ada/libgnat/s-valllli.ads | 22 +- gcc/ada/libgnat/s-valuei.adb | 95 +++---- gcc/ada/libgnat/s-valuei.ads | 188 ++----------- gcc/ada/libgnat/s-valueu.adb | 444 +++++++++-------------------- gcc/ada/libgnat/s-valueu.ads | 478 +------------------------------ gcc/ada/libgnat/s-valuti.ads | 268 ++++++++++++++++-- gcc/ada/libgnat/s-vauspe.adb | 198 +++++++++++++ gcc/ada/libgnat/s-vauspe.ads | 639 ++++++++++++++++++++++++++++++++++++++++++ 24 files changed, 1853 insertions(+), 1547 deletions(-) diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads index f574e78f8dc..3979f147d2a 100644 --- a/gcc/ada/libgnat/a-nbnbig.ads +++ b/gcc/ada/libgnat/a-nbnbig.ads @@ -32,6 +32,8 @@ package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with Ghost, Pure is + pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost); + type Big_Integer is private with Integer_Literal => From_Universal_Image; diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb index fd8e848438e..bfe85403888 100644 --- a/gcc/ada/libgnat/s-imagef.adb +++ b/gcc/ada/libgnat/s-imagef.adb @@ -31,7 +31,8 @@ with System.Image_I; with System.Img_Util; use System.Img_Util; -with System.Val_Util; +with System.Value_I_Spec; +with System.Value_U_Spec; package body System.Image_F is @@ -69,70 +70,16 @@ package body System.Image_F is -- if the small is larger than 1, and smaller than 2**(Int'Size - 1) / 10 -- if the small is smaller than 1. - -- Define ghost subprograms without implementation (marked as Import) to - -- create a suitable package Int_Params for type Int, as instantiations - -- of System.Image_F use for this type one of the derived integer types - -- defined in Interfaces, instead of the standard signed integer types - -- which are used to define System.Img_*.Int_Params. - - type Uns_Option (Overflow : Boolean := False) is record - case Overflow is - when True => - null; - when False => - Value : Uns := 0; - end case; - end record; - Unsigned_Width_Ghost : constant Natural := Int'Width; - function Wrap_Option (Value : Uns) return Uns_Option - with Ghost, Import; - function Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost, Import; - function Hexa_To_Unsigned_Ghost (X : Character) return Uns - with Ghost, Import; - function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - return Uns_Option - with Ghost, Import; - function Is_Integer_Ghost (Str : String) return Boolean - with Ghost, Import; - procedure Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost, Import; - procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) - with Ghost, Import; - function Abs_Uns_Of_Int (Val : Int) return Uns - with Ghost, Import; - function Value_Integer (Str : String) return Int - with Ghost, Import; - - package Int_Params is new Val_Util.Int_Params - (Int => Int, - Uns => Uns, - Uns_Option => Uns_Option, - Unsigned_Width_Ghost => Unsigned_Width_Ghost, - Wrap_Option => Wrap_Option, - Only_Decimal_Ghost => Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost, - Scan_Based_Number_Ghost => Scan_Based_Number_Ghost, - Is_Integer_Ghost => Is_Integer_Ghost, - Prove_Iter_Scan_Based_Number_Ghost => Prove_Iter_Scan_Based_Number_Ghost, - Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost, - Abs_Uns_Of_Int => Abs_Uns_Of_Int, - Value_Integer => Value_Integer); - - package Image_I is new System.Image_I (Int_Params); + package Uns_Spec is new System.Value_U_Spec (Uns); + package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec.Uns_Params); + + package Image_I is new System.Image_I + (Int => Int, + Uns => Uns, + Unsigned_Width_Ghost => Unsigned_Width_Ghost, + Int_Params => Int_Spec.Int_Params); procedure Set_Image_Integer (V : Int; diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb index ff853d3ac6b..8997e3c5a75 100644 --- a/gcc/ada/libgnat/s-imagei.adb +++ b/gcc/ada/libgnat/s-imagei.adb @@ -46,42 +46,6 @@ package body System.Image_I is Post => Ignore, Subprogram_Variant => Ignore); - -- As a use_clause for Int_Params cannot be used for instances of this - -- generic in System specs, rename all constants and subprograms. - - Unsigned_Width_Ghost : constant Natural := Int_Params.Unsigned_Width_Ghost; - - function Wrap_Option (Value : Uns) return Uns_Option - renames Int_Params.Wrap_Option; - function Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - renames Int_Params.Only_Decimal_Ghost; - function Hexa_To_Unsigned_Ghost (X : Character) return Uns - renames Int_Params.Hexa_To_Unsigned_Ghost; - function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - return Uns_Option - renames Int_Params.Scan_Based_Number_Ghost; - function Is_Integer_Ghost (Str : String) return Boolean - renames Int_Params.Is_Integer_Ghost; - procedure Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - renames Int_Params.Prove_Iter_Scan_Based_Number_Ghost; - procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) - renames Int_Params.Prove_Scan_Only_Decimal_Ghost; - function Abs_Uns_Of_Int (Val : Int) return Uns - renames Int_Params.Abs_Uns_Of_Int; - function Value_Integer (Str : String) return Int - renames Int_Params.Value_Integer; - subtype Non_Positive is Int range Int'First .. 0; function Uns_Of_Non_Positive (T : Non_Positive) return Uns is @@ -99,9 +63,9 @@ package body System.Image_I is and then P <= S'Last - Unsigned_Width_Ghost + 1, Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old) and then P in P'Old + 1 .. S'Last - and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P) - and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P) - = Wrap_Option (Uns_Of_Non_Positive (T)); + and then UP.Only_Decimal_Ghost (S, From => P'Old + 1, To => P) + and then UP.Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P) + = UP.Wrap_Option (Uns_Of_Non_Positive (T)); -- Set digits of absolute value of T, which is zero or negative. We work -- with the negative of the value so that the largest negative number is -- not a special case. @@ -182,11 +146,12 @@ package body System.Image_I is and then P in 2 .. S'Last and then S (1) in ' ' | '-' and then (S (1) = '-') = (V < 0) - and then Only_Decimal_Ghost (S, From => 2, To => P) - and then Scan_Based_Number_Ghost (S, From => 2, To => P) - = Wrap_Option (Abs_Uns_Of_Int (V)), - Post => Is_Integer_Ghost (S (1 .. P)) - and then Value_Integer (S (1 .. P)) = V; + and then UP.Only_Decimal_Ghost (S, From => 2, To => P) + and then UP.Scan_Based_Number_Ghost (S, From => 2, To => P) + = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)), + Post => not System.Val_Util.Only_Space_Ghost (S, 1, P) + and then IP.Is_Integer_Ghost (S (1 .. P)) + and then IP.Is_Value_Integer_Ghost (S (1 .. P), V); -- Ghost lemma to prove the value of Value_Integer from the value of -- Scan_Based_Number_Ghost and the sign on a decimal string. @@ -198,11 +163,14 @@ package body System.Image_I is Str : constant String := S (1 .. P); begin pragma Assert (Str'First = 1); - pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P)); - Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P); - pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P) - = Wrap_Option (Abs_Uns_Of_Int (V))); - Prove_Scan_Only_Decimal_Ghost (Str, V); + pragma Assert (Str (2) /= ' '); + pragma Assert + (UP.Only_Decimal_Ghost (Str, From => 2, To => P)); + UP.Prove_Scan_Based_Number_Ghost_Eq (S, Str, From => 2, To => P); + pragma Assert + (UP.Scan_Based_Number_Ghost (Str, From => 2, To => P) + = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V))); + IP.Prove_Scan_Only_Decimal_Ghost (Str, V); end Prove_Value_Integer; -- Start of processing for Image_Integer @@ -226,6 +194,8 @@ package body System.Image_I is pragma Assert (P_Prev + Offset = 2); end; + pragma Assert (if V >= 0 then S (1) = ' '); + pragma Assert (S (1) in ' ' | '-'); Prove_Value_Integer; end Image_Integer; @@ -248,42 +218,78 @@ package body System.Image_I is S_Init : constant String := S with Ghost; Uns_T : constant Uns := Uns_Of_Non_Positive (T) with Ghost; Uns_Value : Uns := Uns_Of_Non_Positive (Value) with Ghost; - Prev, Cur : Uns_Option with Ghost; Prev_Value : Uns with Ghost; Prev_S : String := S with Ghost; -- Local ghost lemmas - procedure Prove_Character_Val (RU : Uns; RI : Int) + procedure Prove_Character_Val (RU : Uns; RI : Non_Positive) with Ghost, - Pre => RU in 0 .. 9 - and then RI in 0 .. 9, - Post => Character'Val (48 + RU) in '0' .. '9' - and then Character'Val (48 + RI) in '0' .. '9'; + Post => RU rem 10 in 0 .. 9 + and then -(RI rem 10) in 0 .. 9 + and then Character'Val (48 + RU rem 10) in '0' .. '9' + and then Character'Val (48 - RI rem 10) in '0' .. '9'; -- Ghost lemma to prove the value of a character corresponding to the -- next figure. + procedure Prove_Euclidian (Val, Quot, Rest : Uns) + with + Ghost, + Pre => Quot = Val / 10 + and then Rest = Val rem 10, + Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest; + -- Ghost lemma to prove the relation between the quotient/remainder of + -- division by 10 and the initial value. + procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) with Ghost, Pre => RU in 0 .. 9 and then RI in 0 .. 9, - Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + RU)) = RU - and then Hexa_To_Unsigned_Ghost (Character'Val (48 + RI)) = Uns (RI); + Post => UP.Hexa_To_Unsigned_Ghost + (Character'Val (48 + RU)) = RU + and then UP.Hexa_To_Unsigned_Ghost + (Character'Val (48 + RI)) = Uns (RI); -- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source -- figure when applied to the corresponding character. - procedure Prove_Unchanged - with - Ghost, - Pre => P <= S'Last - and then S_Init'First = S'First - and then S_Init'Last = S'Last - and then (for all K in S'First .. P => S (K) = S_Init (K)), - Post => S (S'First .. P) = S_Init (S'First .. P); - -- Ghost lemma to prove that the part of string S before P has not been - -- modified. + procedure Prove_Scan_Iter + (S, Prev_S : String; + V, Prev_V, Res : Uns; + P, Max : Natural) + with + Ghost, + Pre => + S'First = Prev_S'First and then S'Last = Prev_S'Last + and then S'Last < Natural'Last and then + Max in S'Range and then P in S'First .. Max and then + (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9') + and then (for all I in P + 1 .. Max => Prev_S (I) = S (I)) + and then S (P) in '0' .. '9' + and then V <= Uns'Last / 10 + and then Uns'Last - UP.Hexa_To_Unsigned_Ghost (S (P)) + >= 10 * V + and then Prev_V = + V * 10 + UP.Hexa_To_Unsigned_Ghost (S (P)) + and then + (if P = Max then Prev_V = Res + else UP.Scan_Based_Number_Ghost + (Str => Prev_S, + From => P + 1, + To => Max, + Base => 10, + Acc => Prev_V) = UP.Wrap_Option (Res)), + Post => + (for all I in P .. Max => S (I) in '0' .. '9') + and then UP.Scan_Based_Number_Ghost + (Str => S, + From => P, + To => Max, + Base => 10, + Acc => V) = UP.Wrap_Option (Res); + -- Ghost lemma to prove that Scan_Based_Number_Ghost is preserved + -- through an iteration of the loop. procedure Prove_Uns_Of_Non_Positive_Value with @@ -294,50 +300,44 @@ package body System.Image_I is -- Ghost lemma to prove that the relation between Value and its unsigned -- version is preserved. - procedure Prove_Iter_Scan - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Ghost, - Pre => Str1'Last /= Positive'Last - and then - (From > To or else (From >= Str1'First and then To <= Str1'Last)) - and then Only_Decimal_Ghost (Str1, From, To) - and then Str1'First = Str2'First - and then Str1'Last = Str2'Last - and then (for all J in From .. To => Str1 (J) = Str2 (J)), - Post => - Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) - = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); - -- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only - -- depends on the value of the argument string in the (From .. To) range - -- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost - -- so that we can call it here on ghost arguments. - ----------------------------- -- Local lemma null bodies -- ----------------------------- - procedure Prove_Character_Val (RU : Uns; RI : Int) is null; + procedure Prove_Character_Val (RU : Uns; RI : Non_Positive) is null; + procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null; procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null; - procedure Prove_Unchanged is null; procedure Prove_Uns_Of_Non_Positive_Value is null; --------------------- - -- Prove_Iter_Scan -- + -- Prove_Scan_Iter -- --------------------- - procedure Prove_Iter_Scan - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) + procedure Prove_Scan_Iter + (S, Prev_S : String; + V, Prev_V, Res : Uns; + P, Max : Natural) is + pragma Unreferenced (Res); begin - Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc); - end Prove_Iter_Scan; + UP.Lemma_Scan_Based_Number_Ghost_Step + (Str => S, + From => P, + To => Max, + Base => 10, + Acc => V); + if P < Max then + UP.Prove_Scan_Based_Number_Ghost_Eq + (Prev_S, S, P + 1, Max, 10, Prev_V); + else + UP.Lemma_Scan_Based_Number_Ghost_Base + (Str => S, + From => P + 1, + To => Max, + Base => 10, + Acc => Prev_V); + end if; + end Prove_Scan_Iter; -- Start of processing for Set_Digits @@ -383,13 +383,9 @@ package body System.Image_I is for J in reverse 1 .. Nb_Digits loop Lemma_Div_Commutation (Uns_Value, 10); Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10); - Prove_Character_Val (Uns_Value rem 10, -(Value rem 10)); + Prove_Character_Val (Uns_Value, Value); Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10)); Prove_Uns_Of_Non_Positive_Value; - pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10)); - pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10))); - pragma Assert - (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J))); Prev_Value := Uns_Value; Prev_S := S; @@ -399,68 +395,44 @@ package body System.Image_I is S (P + J) := Character'Val (48 - (Value rem 10)); Value := Value / 10; - pragma Assert (S (P + J) in '0' .. '9'); - pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) = - From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)) rem 10); - pragma Assert - (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9'); + Prove_Euclidian + (Val => Prev_Value, + Quot => Uns_Value, + Rest => UP.Hexa_To_Unsigned_Ghost (S (P + J))); - Prev := Scan_Based_Number_Ghost - (Str => S, - From => P + J + 1, - To => P + Nb_Digits, - Base => 10, - Acc => Prev_Value); - Cur := Scan_Based_Number_Ghost - (Str => S, - From => P + J, - To => P + Nb_Digits, - Base => 10, - Acc => Uns_Value); - pragma Assert (Prev_Value = 10 * Uns_Value + (Prev_Value rem 10)); - pragma Assert - (Prev_Value rem 10 = Hexa_To_Unsigned_Ghost (S (P + J))); - pragma Assert - (Prev_Value = 10 * Uns_Value + Hexa_To_Unsigned_Ghost (S (P + J))); - - if J /= Nb_Digits then - Prove_Iter_Scan - (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value); - end if; - - pragma Assert (Prev = Cur); - pragma Assert (Prev = Wrap_Option (Uns_T)); + Prove_Scan_Iter + (S, Prev_S, Uns_Value, Prev_Value, Uns_T, P + J, P + Nb_Digits); pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value)); pragma Loop_Invariant (Uns_Value <= Uns'Last / 10); pragma Loop_Invariant (for all K in S'First .. P => S (K) = S_Init (K)); - pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits)); + pragma Loop_Invariant + (UP.Only_Decimal_Ghost (S, P + J, P + Nb_Digits)); pragma Loop_Invariant (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9'); pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1)); pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow); pragma Loop_Invariant - (Scan_Based_Number_Ghost + (UP.Scan_Based_Number_Ghost (Str => S, From => P + J, To => P + Nb_Digits, Base => 10, Acc => Uns_Value) - = Wrap_Option (Uns_T)); + = UP.Wrap_Option (Uns_T)); end loop; pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits)); pragma Assert (Uns_Value = 0); - Prove_Unchanged; pragma Assert - (Scan_Based_Number_Ghost + (UP.Scan_Based_Number_Ghost (Str => S, From => P + 1, To => P + Nb_Digits, Base => 10, Acc => Uns_Value) - = Wrap_Option (Uns_T)); + = UP.Wrap_Option (Uns_T)); P := P + Nb_Digits; end Set_Digits; diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads index 10116d123ed..575c60abb2c 100644 --- a/gcc/ada/libgnat/s-imagei.ads +++ b/gcc/ada/libgnat/s-imagei.ads @@ -48,19 +48,19 @@ pragma Assertion_Policy (Pre => Ignore, with System.Val_Util; generic + type Int is range <>; + type Uns is mod <>; - with package Int_Params is new System.Val_Util.Int_Params (<>); + Unsigned_Width_Ghost : Natural; -package System.Image_I is - - subtype Int is Int_Params.Int; - use type Int_Params.Int; + with package Int_Params is new System.Val_Util.Int_Params + (Int => Int, Uns => Uns, others => <>) + with Ghost; - subtype Uns is Int_Params.Uns; - use type Int_Params.Uns; - - subtype Uns_Option is Int_Params.Uns_Option; - use type Int_Params.Uns_Option; +package System.Image_I is + package IP renames Int_Params; + package UP renames IP.Uns_Params; + use type UP.Uns_Option; procedure Image_Integer (V : Int; @@ -69,9 +69,9 @@ package System.Image_I is with Pre => S'First = 1 and then S'Last < Integer'Last - and then S'Last >= Int_Params.Unsigned_Width_Ghost, + and then S'Last >= Unsigned_Width_Ghost, Post => P in S'Range - and then Int_Params.Value_Integer (S (1 .. P)) = V; + and then IP.Is_Value_Integer_Ghost (S (1 .. P), V); -- Computes Int'Image (V) and stores the result in S (1 .. P) -- setting the resulting value of P. The caller guarantees that S -- is long enough to hold the result, and that S'First is 1. @@ -87,23 +87,23 @@ package System.Image_I is and then S'First <= S'Last and then (if V >= 0 then - P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1 + P <= S'Last - Unsigned_Width_Ghost + 1 else - P <= S'Last - Int_Params.Unsigned_Width_Ghost), + P <= S'Last - Unsigned_Width_Ghost), Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old) and then (declare Minus : constant Boolean := S (P'Old + 1) = '-'; Offset : constant Positive := (if V >= 0 then 1 else 2); - Abs_V : constant Uns := Int_Params.Abs_Uns_Of_Int (V); + Abs_V : constant Uns := IP.Abs_Uns_Of_Int (V); begin Minus = (V < 0) and then P in P'Old + Offset .. S'Last - and then Int_Params.Only_Decimal_Ghost + and then UP.Only_Decimal_Ghost (S, From => P'Old + Offset, To => P) - and then Int_Params.Scan_Based_Number_Ghost + and then UP.Scan_Based_Number_Ghost (S, From => P'Old + Offset, To => P) - = Int_Params.Wrap_Option (Abs_V)); + = UP.Wrap_Option (Abs_V)); -- Stores the image of V in S starting at S (P + 1), P is updated to point -- to the last character stored. The value stored is identical to the value -- of Int'Image (V) except that no leading space is stored when V is diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb index 69324878010..0e1c2bb593f 100644 --- a/gcc/ada/libgnat/s-imageu.adb +++ b/gcc/ada/libgnat/s-imageu.adb @@ -147,11 +147,12 @@ package body System.Image_U is and then S'Last < Integer'Last and then P in 2 .. S'Last and then S (1) = ' ' - and then Only_Decimal_Ghost (S, From => 2, To => P) - and then Scan_Based_Number_Ghost (S, From => 2, To => P) - = Wrap_Option (V), - Post => Is_Unsigned_Ghost (S (1 .. P)) - and then Value_Unsigned (S (1 .. P)) = V; + and then Uns_Params.Only_Decimal_Ghost (S, From => 2, To => P) + and then Uns_Params.Scan_Based_Number_Ghost (S, From => 2, To => P) + = Uns_Params.Wrap_Option (V), + Post => not System.Val_Util.Only_Space_Ghost (S, 1, P) + and then Uns_Params.Is_Unsigned_Ghost (S (1 .. P)) + and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V); -- Ghost lemma to prove the value of Value_Unsigned from the value of -- Scan_Based_Number_Ghost on a decimal string. @@ -163,11 +164,15 @@ package body System.Image_U is Str : constant String := S (1 .. P); begin pragma Assert (Str'First = 1); - pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P)); - Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P); - pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P) - = Wrap_Option (V)); - Prove_Scan_Only_Decimal_Ghost (Str, V); + pragma Assert (S (2) /= ' '); + pragma Assert + (Uns_Params.Only_Decimal_Ghost (Str, From => 2, To => P)); + Uns_Params.Prove_Scan_Based_Number_Ghost_Eq + (S, Str, From => 2, To => P); + pragma Assert + (Uns_Params.Scan_Based_Number_Ghost (Str, From => 2, To => P) + = Uns_Params.Wrap_Option (V)); + Uns_Params.Prove_Scan_Only_Decimal_Ghost (Str, V); end Prove_Value_Unsigned; -- Start of processing for Image_Unsigned @@ -196,7 +201,6 @@ package body System.Image_U is Pow : Big_Positive := 1 with Ghost; S_Init : constant String := S with Ghost; - Prev, Cur : Uns_Option with Ghost; Prev_Value : Uns with Ghost; Prev_S : String := S with Ghost; @@ -205,8 +209,8 @@ package body System.Image_U is procedure Prove_Character_Val (R : Uns) with Ghost, - Pre => R in 0 .. 9, - Post => Character'Val (48 + R) in '0' .. '9'; + Post => R rem 10 in 0 .. 9 + and then Character'Val (48 + R rem 10) in '0' .. '9'; -- Ghost lemma to prove the value of a character corresponding to the -- next figure. @@ -215,7 +219,7 @@ package body System.Image_U is Ghost, Pre => Quot = Val / 10 and then Rest = Val rem 10, - Post => Val = 10 * Quot + Rest; + Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest; -- Ghost lemma to prove the relation between the quotient/remainder of -- division by 10 and the initial value. @@ -223,42 +227,46 @@ package body System.Image_U is with Ghost, Pre => R in 0 .. 9, - Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R; + Post => Uns_Params.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R; -- Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source -- figure when applied to the corresponding character. - procedure Prove_Unchanged - with - Ghost, - Pre => P <= S'Last - and then S_Init'First = S'First - and then S_Init'Last = S'Last - and then (for all K in S'First .. P => S (K) = S_Init (K)), - Post => S (S'First .. P) = S_Init (S'First .. P); - -- Ghost lemma to prove that the part of string S before P has not been - -- modified. - - procedure Prove_Iter_Scan - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Ghost, - Pre => Str1'Last /= Positive'Last - and then - (From > To or else (From >= Str1'First and then To <= Str1'Last)) - and then Only_Decimal_Ghost (Str1, From, To) - and then Str1'First = Str2'First - and then Str1'Last = Str2'Last - and then (for all J in From .. To => Str1 (J) = Str2 (J)), - Post => - Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) - = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); - -- Ghost lemma to prove that the result of Scan_Based_Number_Ghost only - -- depends on the value of the argument string in the (From .. To) range - -- of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost - -- so that we can call it here on ghost arguments. + procedure Prove_Scan_Iter + (S, Prev_S : String; + V, Prev_V, Res : Uns; + P, Max : Natural) + with + Ghost, + Pre => + S'First = Prev_S'First and then S'Last = Prev_S'Last + and then S'Last < Natural'Last and then + Max in S'Range and then P in S'First .. Max and then + (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9') + and then (for all I in P + 1 .. Max => Prev_S (I) = S (I)) + and then S (P) in '0' .. '9' + and then V <= Uns'Last / 10 + and then Uns'Last - Uns_Params.Hexa_To_Unsigned_Ghost (S (P)) + >= 10 * V + and then Prev_V = + V * 10 + Uns_Params.Hexa_To_Unsigned_Ghost (S (P)) + and then + (if P = Max then Prev_V = Res + else Uns_Params.Scan_Based_Number_Ghost + (Str => Prev_S, + From => P + 1, + To => Max, + Base => 10, + Acc => Prev_V) = Uns_Params.Wrap_Option (Res)), + Post => + (for all I in P .. Max => S (I) in '0' .. '9') + and then Uns_Params.Scan_Based_Number_Ghost + (Str => S, + From => P, + To => Max, + Base => 10, + Acc => V) = Uns_Params.Wrap_Option (Res); + -- Ghost lemma to prove that Scan_Based_Number_Ghost is preserved + -- through an iteration of the loop. ----------------------------- -- Local lemma null bodies -- @@ -267,21 +275,36 @@ package body System.Image_U is procedure Prove_Character_Val (R : Uns) is null; procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null; procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null; - procedure Prove_Unchanged is null; --------------------- - -- Prove_Iter_Scan -- + -- Prove_Scan_Iter -- --------------------- - procedure Prove_Iter_Scan - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) + procedure Prove_Scan_Iter + (S, Prev_S : String; + V, Prev_V, Res : Uns; + P, Max : Natural) is + pragma Unreferenced (Res); begin - Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc); - end Prove_Iter_Scan; + Uns_Params.Lemma_Scan_Based_Number_Ghost_Step + (Str => S, + From => P, + To => Max, + Base => 10, + Acc => V); + if P < Max then + Uns_Params.Prove_Scan_Based_Number_Ghost_Eq + (Prev_S, S, P + 1, Max, 10, Prev_V); + else + Uns_Params.Lemma_Scan_Based_Number_Ghost_Base + (Str => S, + From => P + 1, + To => Max, + Base => 10, + Acc => Prev_V); + end if; + end Prove_Scan_Iter; -- Start of processing for Set_Image_Unsigned @@ -313,6 +336,7 @@ package body System.Image_U is Lemma_Non_Zero (Value); pragma Assert (Pow <= Big (Uns'Last)); end loop; + pragma Assert (Big (V) / (Big_10 ** Nb_Digits) = 0); Value := V; Pow := 1; @@ -323,77 +347,43 @@ package body System.Image_U is for J in reverse 1 .. Nb_Digits loop Lemma_Div_Commutation (Value, 10); Lemma_Div_Twice (Big (V), Big_10 ** (Nb_Digits - J), Big_10); - Prove_Character_Val (Value rem 10); + Prove_Character_Val (Value); Prove_Hexa_To_Unsigned_Ghost (Value rem 10); Prev_Value := Value; Prev_S := S; Pow := Pow * 10; - S (P + J) := Character'Val (48 + (Value rem 10)); Value := Value / 10; - pragma Assert (S (P + J) in '0' .. '9'); - pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) = - From_Big (Big (V) / Big_10 ** (Nb_Digits - J)) rem 10); - pragma Assert - (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9'); - pragma Assert - (for all K in P + J + 1 .. P + Nb_Digits => - Hexa_To_Unsigned_Ghost (S (K)) = - From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10); - - Prev := Scan_Based_Number_Ghost - (Str => S, - From => P + J + 1, - To => P + Nb_Digits, - Base => 10, - Acc => Prev_Value); - Cur := Scan_Based_Number_Ghost - (Str => S, - From => P + J, - To => P + Nb_Digits, - Base => 10, - Acc => Value); - - if J /= Nb_Digits then - Prove_Euclidian (Val => Prev_Value, - Quot => Value, - Rest => Hexa_To_Unsigned_Ghost (S (P + J))); - pragma Assert - (Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J))); - Prove_Iter_Scan - (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value); - end if; + Prove_Euclidian + (Val => Prev_Value, + Quot => Value, + Rest => Uns_Params.Hexa_To_Unsigned_Ghost (S (P + J))); - pragma Assert (Prev = Cur); - pragma Assert (Prev = Wrap_Option (V)); + Prove_Scan_Iter + (S, Prev_S, Value, Prev_Value, V, P + J, P + Nb_Digits); pragma Loop_Invariant (Value <= Uns'Last / 10); pragma Loop_Invariant (for all K in S'First .. P => S (K) = S_Init (K)); - pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits)); - pragma Loop_Invariant - (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9'); pragma Loop_Invariant - (for all K in P + J .. P + Nb_Digits => - Hexa_To_Unsigned_Ghost (S (K)) = - From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10); + (Uns_Params.Only_Decimal_Ghost + (S, From => P + J, To => P + Nb_Digits)); pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1)); pragma Loop_Invariant (Big (Value) = Big (V) / Pow); pragma Loop_Invariant - (Scan_Based_Number_Ghost + (Uns_Params.Scan_Based_Number_Ghost (Str => S, From => P + J, To => P + Nb_Digits, Base => 10, Acc => Value) - = Wrap_Option (V)); + = Uns_Params.Wrap_Option (V)); end loop; + pragma Assert (Big (Value) = Big (V) / (Big_10 ** Nb_Digits)); pragma Assert (Value = 0); - Prove_Unchanged; - P := P + Nb_Digits; end Set_Image_Unsigned; diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads index 789cf65a9d2..3d80ea9af5a 100644 --- a/gcc/ada/libgnat/s-imageu.ads +++ b/gcc/ada/libgnat/s-imageu.ads @@ -45,45 +45,22 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); +with System.Val_Util; + generic type Uns is mod <>; - type Uns_Option is private; -- Additional parameters for ghost subprograms used inside contracts Unsigned_Width_Ghost : Natural; - with function Wrap_Option (Value : Uns) return Uns_Option - with Ghost; - with function Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns - with Ghost; - with function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) return Uns_Option - with Ghost; - with function Is_Unsigned_Ghost (Str : String) return Boolean - with Ghost; - with function Value_Unsigned (Str : String) return Uns; - with procedure Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with Ghost; - with procedure Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - with Ghost; + with package Uns_Params is new System.Val_Util.Uns_Params + (Uns => Uns, others => <>) + with Ghost; package System.Image_U is + use all type Uns_Params.Uns_Option; procedure Image_Unsigned (V : Uns; @@ -94,7 +71,7 @@ package System.Image_U is and then S'Last < Integer'Last and then S'Last >= Unsigned_Width_Ghost, Post => P in S'Range - and then Value_Unsigned (S (1 .. P)) = V; + and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V); pragma Inline (Image_Unsigned); -- Computes Uns'Image (V) and stores the result in S (1 .. P) setting -- the resulting value of P. The caller guarantees that S is long enough to @@ -112,9 +89,10 @@ package System.Image_U is and then P <= S'Last - Unsigned_Width_Ghost + 1, Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old) and then P in P'Old + 1 .. S'Last - and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P) - and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P) - = Wrap_Option (V); + and then Uns_Params.Only_Decimal_Ghost (S, From => P'Old + 1, To => P) + and then Uns_Params.Scan_Based_Number_Ghost + (S, From => P'Old + 1, To => P) + = Uns_Params.Wrap_Option (V); -- Stores the image of V in S starting at S (P + 1), P is updated to point -- to the last character stored. The value stored is identical to the value -- of Uns'Image (V) except that no leading space is stored. The caller diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads index fd5bea31c2a..8672e58b083 100644 --- a/gcc/ada/libgnat/s-imgint.ads +++ b/gcc/ada/libgnat/s-imgint.ads @@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; with System.Val_Int; -with System.Val_Uns; -with System.Val_Util; with System.Wid_Uns; package System.Img_Int @@ -57,27 +55,12 @@ package System.Img_Int is subtype Unsigned is Unsigned_Types.Unsigned; - package Int_Params is new Val_Util.Int_Params - (Int => Integer, - Uns => Unsigned, - Uns_Option => Val_Uns.Impl.Uns_Option, - Unsigned_Width_Ghost => + package Impl is new Image_I + (Int => Integer, + Uns => Unsigned, + Unsigned_Width_Ghost => Wid_Uns.Width_Unsigned (0, Unsigned'Last), - Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_Uns.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_Uns.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_Uns.Impl.Scan_Based_Number_Ghost, - Prove_Iter_Scan_Based_Number_Ghost => - Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Is_Integer_Ghost => Val_Int.Impl.Is_Integer_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_Int.Impl.Prove_Scan_Only_Decimal_Ghost, - Abs_Uns_Of_Int => Val_Int.Impl.Abs_Uns_Of_Int, - Value_Integer => Val_Int.Impl.Value_Integer); - - package Impl is new Image_I (Int_Params); + Int_Params => System.Val_Int.Impl.Spec.Int_Params); procedure Image_Integer (V : Integer; diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads index 20f108c8e45..99c1951348d 100644 --- a/gcc/ada/libgnat/s-imglli.ads +++ b/gcc/ada/libgnat/s-imglli.ads @@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; with System.Val_LLI; -with System.Val_LLU; -with System.Val_Util; with System.Wid_LLU; package System.Img_LLI @@ -57,27 +55,13 @@ package System.Img_LLI is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; - package Int_Params is new Val_Util.Int_Params - (Int => Long_Long_Integer, - Uns => Long_Long_Unsigned, - Uns_Option => Val_LLU.Impl.Uns_Option, - Unsigned_Width_Ghost => - Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last), - Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_LLU.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_LLU.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_LLU.Impl.Scan_Based_Number_Ghost, - Prove_Iter_Scan_Based_Number_Ghost => - Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Is_Integer_Ghost => Val_LLI.Impl.Is_Integer_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_LLI.Impl.Prove_Scan_Only_Decimal_Ghost, - Abs_Uns_Of_Int => Val_LLI.Impl.Abs_Uns_Of_Int, - Value_Integer => Val_LLI.Impl.Value_Integer); - - package Impl is new Image_I (Int_Params); + package Impl is new Image_I + (Int => Long_Long_Integer, + Uns => Long_Long_Unsigned, + Unsigned_Width_Ghost => + Wid_LLU.Width_Long_Long_Unsigned + (0, Long_Long_Unsigned'Last), + Int_Params => System.Val_LLI.Impl.Spec.Int_Params); procedure Image_Long_Long_Integer (V : Long_Long_Integer; diff --git a/gcc/ada/libgnat/s-imgllli.ads b/gcc/ada/libgnat/s-imgllli.ads index 989c296d759..931c288d20e 100644 --- a/gcc/ada/libgnat/s-imgllli.ads +++ b/gcc/ada/libgnat/s-imgllli.ads @@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre => Ignore, with System.Image_I; with System.Unsigned_Types; with System.Val_LLLI; -with System.Val_LLLU; -with System.Val_Util; with System.Wid_LLLU; package System.Img_LLLI @@ -57,28 +55,13 @@ package System.Img_LLLI is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - package Int_Params is new Val_Util.Int_Params - (Int => Long_Long_Long_Integer, - Uns => Long_Long_Long_Unsigned, - Uns_Option => Val_LLLU.Impl.Uns_Option, - Unsigned_Width_Ghost => + package Impl is new Image_I + (Int => Long_Long_Long_Integer, + Uns => Long_Long_Long_Unsigned, + Unsigned_Width_Ghost => Wid_LLLU.Width_Long_Long_Long_Unsigned (0, Long_Long_Long_Unsigned'Last), - Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_LLLU.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_LLLU.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_LLLU.Impl.Scan_Based_Number_Ghost, - Prove_Iter_Scan_Based_Number_Ghost => - Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Is_Integer_Ghost => Val_LLLI.Impl.Is_Integer_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_LLLI.Impl.Prove_Scan_Only_Decimal_Ghost, - Abs_Uns_Of_Int => Val_LLLI.Impl.Abs_Uns_Of_Int, - Value_Integer => Val_LLLI.Impl.Value_Integer); - - package Impl is new Image_I (Int_Params); + Int_Params => System.Val_LLLI.Impl.Spec.Int_Params); procedure Image_Long_Long_Long_Integer (V : Long_Long_Long_Integer; diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads index 0116aa83bc7..53b39a8fdd2 100644 --- a/gcc/ada/libgnat/s-imglllu.ads +++ b/gcc/ada/libgnat/s-imglllu.ads @@ -56,23 +56,11 @@ is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; package Impl is new Image_U - (Uns => Long_Long_Long_Unsigned, - Uns_Option => Val_LLLU.Impl.Uns_Option, - Unsigned_Width_Ghost => + (Uns => Long_Long_Long_Unsigned, + Unsigned_Width_Ghost => Wid_LLLU.Width_Long_Long_Long_Unsigned (0, Long_Long_Long_Unsigned'Last), - Only_Decimal_Ghost => Val_LLLU.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_LLLU.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_LLLU.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_LLLU.Impl.Scan_Based_Number_Ghost, - Is_Unsigned_Ghost => Val_LLLU.Impl.Is_Unsigned_Ghost, - Value_Unsigned => Val_LLLU.Impl.Value_Unsigned, - Prove_Iter_Scan_Based_Number_Ghost => - Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_LLLU.Impl.Prove_Scan_Only_Decimal_Ghost); + Uns_Params => System.Val_LLLU.Impl.Spec.Uns_Params); procedure Image_Long_Long_Long_Unsigned (V : Long_Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-imgllu.ads b/gcc/ada/libgnat/s-imgllu.ads index 67372d77227..28339cd7afe 100644 --- a/gcc/ada/libgnat/s-imgllu.ads +++ b/gcc/ada/libgnat/s-imgllu.ads @@ -56,22 +56,10 @@ is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; package Impl is new Image_U - (Uns => Long_Long_Unsigned, - Uns_Option => Val_LLU.Impl.Uns_Option, - Unsigned_Width_Ghost => + (Uns => Long_Long_Unsigned, + Unsigned_Width_Ghost => Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last), - Only_Decimal_Ghost => Val_LLU.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_LLU.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_LLU.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_LLU.Impl.Scan_Based_Number_Ghost, - Is_Unsigned_Ghost => Val_LLU.Impl.Is_Unsigned_Ghost, - Value_Unsigned => Val_LLU.Impl.Value_Unsigned, - Prove_Iter_Scan_Based_Number_Ghost => - Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_LLU.Impl.Prove_Scan_Only_Decimal_Ghost); + Uns_Params => System.Val_LLU.Impl.Spec.Uns_Params); procedure Image_Long_Long_Unsigned (V : Long_Long_Unsigned; diff --git a/gcc/ada/libgnat/s-imguns.ads b/gcc/ada/libgnat/s-imguns.ads index fa903cece7a..120bd5db7df 100644 --- a/gcc/ada/libgnat/s-imguns.ads +++ b/gcc/ada/libgnat/s-imguns.ads @@ -56,22 +56,10 @@ is subtype Unsigned is Unsigned_Types.Unsigned; package Impl is new Image_U - (Uns => Unsigned, - Uns_Option => Val_Uns.Impl.Uns_Option, - Unsigned_Width_Ghost => + (Uns => Unsigned, + Unsigned_Width_Ghost => Wid_Uns.Width_Unsigned (0, Unsigned'Last), - Only_Decimal_Ghost => Val_Uns.Impl.Only_Decimal_Ghost, - Hexa_To_Unsigned_Ghost => - Val_Uns.Impl.Hexa_To_Unsigned_Ghost, - Wrap_Option => Val_Uns.Impl.Wrap_Option, - Scan_Based_Number_Ghost => - Val_Uns.Impl.Scan_Based_Number_Ghost, - Is_Unsigned_Ghost => Val_Uns.Impl.Is_Unsigned_Ghost, - Value_Unsigned => Val_Uns.Impl.Value_Unsigned, - Prove_Iter_Scan_Based_Number_Ghost => - Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost, - Prove_Scan_Only_Decimal_Ghost => - Val_Uns.Impl.Prove_Scan_Only_Decimal_Ghost); + Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params); procedure Image_Unsigned (V : Unsigned; diff --git a/gcc/ada/libgnat/s-vaispe.adb b/gcc/ada/libgnat/s-vaispe.adb new file mode 100644 index 00000000000..dca2fd782f5 --- /dev/null +++ b/gcc/ada/libgnat/s-vaispe.adb @@ -0,0 +1,87 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L U E _ I _ S P E C -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2022-2022, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + +package body System.Value_I_Spec is + + ----------------------------------- + -- Prove_Scan_Only_Decimal_Ghost -- + ----------------------------------- + + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + pragma Assert (Str (Str'First + 1) /= ' '); + pragma Assert + (if Val < 0 then Non_Blank = Str'First + else + Str (Str'First) = ' ' + and then Non_Blank = Str'First + 1); + Minus : constant Boolean := Str (Non_Blank) = '-'; + Fst_Num : constant Positive := + (if Minus then Non_Blank + 1 else Non_Blank); + pragma Assert (Fst_Num = Str'First + 1); + Uval : constant Uns := Abs_Uns_Of_Int (Val); + + procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns) + with + Pre => Minus = (Val < 0) + and then Uval = Abs_Uns_Of_Int (Val), + Post => Uns_Is_Valid_Int (Minus, Uval) + and then Is_Int_Of_Uns (Minus, Uval, Val); + -- Local proof of the unicity of the signed representation + + procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns) is null; + + -- Start of processing for Prove_Scan_Only_Decimal_Ghost + + begin + Prove_Conversion_Is_Identity (Val, Uval); + pragma Assert + (Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + pragma Assert + (Uns_Params.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); + Uns_Params.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10); + pragma Assert + (Uns_Params.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); + pragma Assert (Only_Space_Ghost + (Str, Uns_Params.Raw_Unsigned_Last_Ghost + (Str, Fst_Num, Str'Last), Str'Last)); + pragma Assert (Is_Integer_Ghost (Str)); + pragma Assert (Is_Value_Integer_Ghost (Str, Val)); + end Prove_Scan_Only_Decimal_Ghost; + +end System.Value_I_Spec; diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads new file mode 100644 index 00000000000..5a5e051620a --- /dev/null +++ b/gcc/ada/libgnat/s-vaispe.ads @@ -0,0 +1,199 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L U E _ I _ S P E C -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2022-2022, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains the specification entities using for the formal +-- verification of the routines for scanning signed integer values. + +-- 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.Val_Util; use System.Val_Util; + +generic + + type Int is range <>; + + type Uns is mod <>; + + -- Additional parameters for specification subprograms on modular Unsigned + -- integers. + + with package Uns_Params is new System.Val_Util.Uns_Params + (Uns => Uns, others => <>) + with Ghost; + +package System.Value_I_Spec with + Ghost, + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is + pragma Preelaborate; + use all type Uns_Params.Uns_Option; + + function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is + (if Minus then Uval <= Uns (Int'Last) + 1 + else Uval <= Uns (Int'Last)) + with Post => True; + -- Return True if Uval (or -Uval when Minus is True) is a valid number of + -- type Int. + + function Is_Int_Of_Uns + (Minus : Boolean; + Uval : Uns; + Val : Int) + return Boolean + is + (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First + elsif Minus then Val = -(Int (Uval)) + else Val = Int (Uval)) + with + Pre => Uns_Is_Valid_Int (Minus, Uval), + Post => True; + -- Return True if Uval (or -Uval when Minus is True) is equal to Val + + function Abs_Uns_Of_Int (Val : Int) return Uns is + (if Val = Int'First then Uns (Int'Last) + 1 + elsif Val < 0 then Uns (-Val) + else Uns (Val)); + -- Return the unsigned absolute value of Val + + function Slide_To_1 (Str : String) return String + with + 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); + -- If Str'Last = Positive'Last then slides Str so that it starts at 1 + + function Is_Integer_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) in '+' | '-' then Non_Blank + 1 else Non_Blank); + begin + Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)) + and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost + (Str, Fst_Num, Str'Last) + and then + Uns_Is_Valid_Int + (Minus => Str (Non_Blank) = '-', + Uval => Uns_Params.Scan_Raw_Unsigned_Ghost + (Str, Fst_Num, Str'Last)) + and then Only_Space_Ghost + (Str, Uns_Params.Raw_Unsigned_Last_Ghost + (Str, Fst_Num, Str'Last), Str'Last)) + with + 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 a + -- signed 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_Integer_Ghost (Str : String; Val : Int) 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) in '+' | '-' then Non_Blank + 1 else Non_Blank); + Uval : constant Uns := + Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); + begin + Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', + Uval => Uval, + Val => Val)) + with + Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Last /= Positive'Last + and then Is_Integer_Ghost (Str), + Post => True; + -- Ghost function that returns True if Val is the value corresponding to + -- the signed number represented by Str. + + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with + Ghost, + Pre => Str'Last /= Positive'Last + and then Str'Length >= 2 + and then Str (Str'First) in ' ' | '-' + and then (Str (Str'First) = '-') = (Val < 0) + and then Uns_Params.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) + and then Uns_Params.Scan_Based_Number_Ghost + (Str, Str'First + 1, Str'Last) + = Uns_Params.Wrap_Option (Abs_Uns_Of_Int (Val)), + Post => Is_Integer_Ghost (Slide_If_Necessary (Str)) + and then Is_Value_Integer_Ghost (Str, Val); + -- Ghost lemma used in the proof of 'Image implementation, to prove that + -- the result of Value_Integer on a decimal string is the same as the + -- signing the result of Scan_Based_Number_Ghost. + + -- Bundle Int type with other types, constants and subprograms used in + -- ghost code, so that this package can be instantiated once and used + -- multiple times as generic formal for a given Int type. + + package Int_Params is new System.Val_Util.Int_Params + (Uns => Uns, + Int => Int, + P_Uns_Params => Uns_Params, + P_Is_Integer_Ghost => Is_Integer_Ghost, + P_Is_Value_Integer_Ghost => Is_Value_Integer_Ghost, + P_Is_Int_Of_Uns => Is_Int_Of_Uns, + P_Abs_Uns_Of_Int => Abs_Uns_Of_Int, + P_Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost); + +private + + ---------------- + -- 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_I_Spec; diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads index 9e47f1bc9f0..3872d7cc7e1 100644 --- a/gcc/ada/libgnat/s-valint.ads +++ b/gcc/ada/libgnat/s-valint.ads @@ -54,23 +54,10 @@ package System.Val_Int with SPARK_Mode is subtype Unsigned is Unsigned_Types.Unsigned; package Impl is new Value_I - (Int => Integer, - Uns => Unsigned, - Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned, - Uns_Option => Val_Uns.Impl.Uns_Option, - Wrap_Option => Val_Uns.Impl.Wrap_Option, - Is_Raw_Unsigned_Format_Ghost => - Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost, - Raw_Unsigned_Overflows_Ghost => - Val_Uns.Impl.Raw_Unsigned_Overflows_Ghost, - Scan_Raw_Unsigned_Ghost => - Val_Uns.Impl.Scan_Raw_Unsigned_Ghost, - Raw_Unsigned_Last_Ghost => - Val_Uns.Impl.Raw_Unsigned_Last_Ghost, - Only_Decimal_Ghost => - Val_Uns.Impl.Only_Decimal_Ghost, - Scan_Based_Number_Ghost => - Val_Uns.Impl.Scan_Based_Number_Ghost); + (Int => Integer, + Uns => Unsigned, + Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned, + Uns_Params => System.Val_Uns.Impl.Spec.Uns_Params); procedure Scan_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index 5bccb1a726b..85bf28203b5 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -54,24 +54,10 @@ package System.Val_LLI with SPARK_Mode is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; package Impl is new Value_I - (Int => Long_Long_Integer, - Uns => Long_Long_Unsigned, - Scan_Raw_Unsigned => - Val_LLU.Scan_Raw_Long_Long_Unsigned, - Uns_Option => Val_LLU.Impl.Uns_Option, - Wrap_Option => Val_LLU.Impl.Wrap_Option, - Is_Raw_Unsigned_Format_Ghost => - Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost, - Raw_Unsigned_Overflows_Ghost => - Val_LLU.Impl.Raw_Unsigned_Overflows_Ghost, - Scan_Raw_Unsigned_Ghost => - Val_LLU.Impl.Scan_Raw_Unsigned_Ghost, - Raw_Unsigned_Last_Ghost => - Val_LLU.Impl.Raw_Unsigned_Last_Ghost, - Only_Decimal_Ghost => - Val_LLU.Impl.Only_Decimal_Ghost, - Scan_Based_Number_Ghost => - Val_LLU.Impl.Scan_Based_Number_Ghost); + (Int => Long_Long_Integer, + Uns => Long_Long_Unsigned, + Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned, + Uns_Params => System.Val_LLU.Impl.Spec.Uns_Params); procedure Scan_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads index 586c7379d21..e53fb0b0357 100644 --- a/gcc/ada/libgnat/s-valllli.ads +++ b/gcc/ada/libgnat/s-valllli.ads @@ -54,24 +54,10 @@ package System.Val_LLLI with SPARK_Mode is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; package Impl is new Value_I - (Int => Long_Long_Long_Integer, - Uns => Long_Long_Long_Unsigned, - Scan_Raw_Unsigned => - Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned, - Uns_Option => Val_LLLU.Impl.Uns_Option, - Wrap_Option => Val_LLLU.Impl.Wrap_Option, - Is_Raw_Unsigned_Format_Ghost => - Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost, - Raw_Unsigned_Overflows_Ghost => - Val_LLLU.Impl.Raw_Unsigned_Overflows_Ghost, - Scan_Raw_Unsigned_Ghost => - Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost, - Raw_Unsigned_Last_Ghost => - Val_LLLU.Impl.Raw_Unsigned_Last_Ghost, - Only_Decimal_Ghost => - Val_LLLU.Impl.Only_Decimal_Ghost, - Scan_Based_Number_Ghost => - Val_LLLU.Impl.Scan_Based_Number_Ghost); + (Int => Long_Long_Long_Integer, + Uns => Long_Long_Long_Unsigned, + Scan_Raw_Unsigned => Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned, + Uns_Params => System.Val_LLLU.Impl.Spec.Uns_Params); procedure Scan_Long_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb index b453ffc38da..51764b20c9d 100644 --- a/gcc/ada/libgnat/s-valuei.adb +++ b/gcc/ada/libgnat/s-valuei.adb @@ -41,59 +41,6 @@ package body System.Value_I is Assert_And_Cut => Ignore, Subprogram_Variant => Ignore); - ----------------------------------- - -- Prove_Scan_Only_Decimal_Ghost -- - ----------------------------------- - - procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is - Non_Blank : constant Positive := First_Non_Space_Ghost - (Str, Str'First, Str'Last); - pragma Assert - (if Val < 0 then Non_Blank = Str'First - else - Only_Space_Ghost (Str, Str'First, Str'First) - and then Non_Blank = Str'First + 1); - Minus : constant Boolean := Str (Non_Blank) = '-'; - Fst_Num : constant Positive := - (if Minus then Non_Blank + 1 else Non_Blank); - pragma Assert (Fst_Num = Str'First + 1); - Uval : constant Uns := - Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); - - procedure Unique_Int_Of_Uns (Val1, Val2 : Int) - with - Pre => Uns_Is_Valid_Int (Minus, Uval) - and then Is_Int_Of_Uns (Minus, Uval, Val1) - and then Is_Int_Of_Uns (Minus, Uval, Val2), - Post => Val1 = Val2; - -- Local proof of the unicity of the signed representation - - procedure Unique_Int_Of_Uns (Val1, Val2 : Int) is null; - - -- Start of processing for Prove_Scan_Only_Decimal_Ghost - - begin - pragma Assert (Minus = (Val < 0)); - pragma Assert (Uval = Abs_Uns_Of_Int (Val)); - pragma Assert (if Minus then Uval <= Uns (Int'Last) + 1 - else Uval <= Uns (Int'Last)); - pragma Assert (Uns_Is_Valid_Int (Minus, Uval)); - pragma Assert - (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First - elsif Minus then Val = -(Int (Uval)) - else Val = Int (Uval)); - pragma Assert (Is_Int_Of_Uns (Minus, Uval, Val)); - pragma Assert - (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); - pragma Assert - (not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)); - pragma Assert (Only_Space_Ghost - (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)); - pragma Assert (Is_Integer_Ghost (Str)); - pragma Assert (Is_Value_Integer_Ghost (Str, Val)); - Unique_Int_Of_Uns (Val, Value_Integer (Str)); - end Prove_Scan_Only_Decimal_Ghost; - ------------------ -- Scan_Integer -- ------------------ @@ -104,6 +51,25 @@ package body System.Value_I is Max : Integer; Res : out Int) is + procedure Prove_Is_Int_Of_Uns + (Minus : Boolean; + Uval : Uns; + Val : Int) + with Ghost, + Pre => Spec.Uns_Is_Valid_Int (Minus, Uval) + and then + (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First + elsif Minus then Val = -(Int (Uval)) + else Val = Int (Uval)), + Post => Spec.Is_Int_Of_Uns (Minus, Uval, Val); + -- Unfold the definition of Is_Int_Of_Uns + + procedure Prove_Is_Int_Of_Uns + (Minus : Boolean; + Uval : Uns; + Val : Int) + is null; + Uval : Uns; -- Unsigned result @@ -131,7 +97,8 @@ package body System.Value_I is end if; Scan_Raw_Unsigned (Str, Ptr, Max, Uval); - pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)); + pragma Assert + (Uval = Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)); -- Deal with overflow cases, and also with largest negative number @@ -152,6 +119,11 @@ package body System.Value_I is else Res := Int (Uval); end if; + + Prove_Is_Int_Of_Uns + (Minus => Str (Non_Blank) = '-', + Uval => Uval, + Val => Res); end Scan_Integer; ------------------- @@ -167,7 +139,15 @@ package body System.Value_I is if Str'Last = Positive'Last then declare subtype NT is String (1 .. Str'Length); + procedure Prove_Is_Integer_Ghost with + Ghost, + Pre => Str'Length < Natural'Last + and then not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Spec.Is_Integer_Ghost (Spec.Slide_To_1 (Str)), + Post => Spec.Is_Integer_Ghost (NT (Str)); + procedure Prove_Is_Integer_Ghost is null; begin + Prove_Is_Integer_Ghost; return Value_Integer (NT (Str)); end; @@ -187,8 +167,6 @@ package body System.Value_I is else Non_Blank) with Ghost; begin - pragma Assert - (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); declare P_Acc : constant not null access Integer := P'Access; @@ -197,12 +175,13 @@ package body System.Value_I is end; pragma Assert - (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); + (P = Uns_Params.Raw_Unsigned_Last_Ghost + (Str, Fst_Num, Str'Last)); Scan_Trailing_Blanks (Str, P); pragma Assert - (Is_Value_Integer_Ghost (Slide_If_Necessary (Str), V)); + (Spec.Is_Value_Integer_Ghost (Spec.Slide_If_Necessary (Str), V)); return V; end; end if; diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index 5e42773b36a..3f78db6ee43 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -39,6 +39,7 @@ pragma Assertion_Policy (Pre => Ignore, Subprogram_Variant => Ignore); with System.Val_Util; use System.Val_Util; +with System.Value_I_Spec; generic @@ -54,71 +55,15 @@ generic -- Additional parameters for ghost subprograms used inside contracts - type Uns_Option is private; - with function Wrap_Option (Value : Uns) return Uns_Option - with Ghost; - with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean - with Ghost; - with function Raw_Unsigned_Overflows_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - with function Scan_Raw_Unsigned_Ghost - (Str : String; - From, To : Integer) - return Uns - with Ghost; - with function Raw_Unsigned_Last_Ghost - (Str : String; - From, To : Integer) - return Positive - with Ghost; - with function Only_Decimal_Ghost - (Str : String; - From, To : Integer) - return Boolean - with Ghost; - with function Scan_Based_Number_Ghost - (Str : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - return Uns_Option - with Ghost; + with package Uns_Params is new System.Val_Util.Uns_Params + (Uns => Uns, others => <>) + with Ghost; package System.Value_I is pragma Preelaborate; + use all type Uns_Params.Uns_Option; - function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is - (if Minus then Uval <= Uns (Int'Last) + 1 - else Uval <= Uns (Int'Last)) - with Ghost, - Post => True; - -- Return True if Uval (or -Uval when Minus is True) is a valid number of - -- type Int. - - function Is_Int_Of_Uns - (Minus : Boolean; - Uval : Uns; - Val : Int) - return Boolean - is - (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First - elsif Minus then Val = -(Int (Uval)) - else Val = Int (Uval)) - with - Ghost, - Pre => Uns_Is_Valid_Int (Minus, Uval), - Post => True; - -- Return True if Uval (or -Uval when Minus is True) is equal to Val - - function Abs_Uns_Of_Int (Val : Int) return Uns is - (if Val = Int'First then Uns (Int'Last) + 1 - elsif Val < 0 then Uns (-Val) - else Uns (Val)) - with Ghost; - -- Return the unsigned absolute value of Val + package Spec is new System.Value_I_Spec (Int, Uns, Uns_Params); procedure Scan_Integer (Str : String; @@ -139,11 +84,13 @@ package System.Value_I is (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); begin - Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max)) - and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max) - and then Uns_Is_Valid_Int + Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max)) + and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost + (Str, Fst_Num, Max) + and then Spec.Uns_Is_Valid_Int (Minus => Str (Non_Blank) = '-', - Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))), + Uval => Uns_Params.Scan_Raw_Unsigned_Ghost + (Str, Fst_Num, Max))), Post => (declare Non_Blank : constant Positive := First_Non_Space_Ghost @@ -152,12 +99,13 @@ package System.Value_I is (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank); Uval : constant Uns := - Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max); + Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max); begin - Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', - Uval => Uval, - Val => Res) - and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max)); + Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', + Uval => Uval, + Val => Res) + and then Ptr.all = Uns_Params.Raw_Unsigned_Last_Ghost + (Str, Fst_Num, Max)); -- 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 @@ -183,111 +131,17 @@ package System.Value_I is -- special case of an all-blank string, and Ptr is unchanged, and hence -- is greater than Max as required in this case. - 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_Integer_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) in '+' | '-' 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 - Uns_Is_Valid_Int - (Minus => Str (Non_Blank) = '-', - Uval => Scan_Raw_Unsigned_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 a - -- signed 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_Integer_Ghost (Str : String; Val : Int) 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) in '+' | '-' then Non_Blank + 1 else Non_Blank); - Uval : constant Uns := - Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last); - begin - Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-', - Uval => Uval, - Val => Val)) - with - Ghost, - Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) - and then Str'Last /= Positive'Last - and then Is_Integer_Ghost (Str), - Post => True; - -- Ghost function that returns True if Val is the value corresponding to - -- the signed number represented by Str. - function Value_Integer (Str : String) return Int with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) and then Str'Length /= Positive'Last - and then Is_Integer_Ghost (Slide_If_Necessary (Str)), - Post => Is_Value_Integer_Ghost - (Slide_If_Necessary (Str), Value_Integer'Result), + and then Spec.Is_Integer_Ghost (Spec.Slide_If_Necessary (Str)), + Post => Spec.Is_Value_Integer_Ghost + (Spec.Slide_If_Necessary (Str), Value_Integer'Result), Subprogram_Variant => (Decreases => Str'First); -- Used in computing X'Value (Str) where X is a signed integer type whose -- base range does not exceed the base range of Integer. 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. - procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) - with - Ghost, - Pre => Str'Last /= Positive'Last - and then Str'Length >= 2 - and then Str (Str'First) in ' ' | '-' - and then (Str (Str'First) = '-') = (Val < 0) - and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) - and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) - = Wrap_Option (Abs_Uns_Of_Int (Val)), - Post => Is_Integer_Ghost (Slide_If_Necessary (Str)) - and then Value_Integer (Str) = Val; - -- Ghost lemma used in the proof of 'Image implementation, to prove that - -- the result of Value_Integer on a decimal string is the same as the - -- signing the result of Scan_Based_Number_Ghost. - -private - - ---------------- - -- 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_I; diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb index f5a6881dbc5..8f19086508b 100644 --- a/gcc/ada/libgnat/s-valueu.adb +++ b/gcc/ada/libgnat/s-valueu.adb @@ -41,9 +41,12 @@ package body System.Value_U is Assert_And_Cut => Ignore, Subprogram_Variant => Ignore); + use type Spec.Uns_Option; + use type Spec.Split_Value_Ghost; + -- Local lemmas - procedure Lemma_Digit_Is_Before_Last + procedure Lemma_Digit_Not_Last (Str : String; P : Integer; From : Integer; @@ -54,257 +57,47 @@ package body System.Value_U is 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. + and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1 + and then Spec.Is_Based_Format_Ghost (Str (From .. To)), + Post => + (if Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + then P <= Spec.Last_Hexa_Ghost (Str (From .. To))); - procedure Lemma_End_Of_Scan + procedure Lemma_Underscore_Not_Last (Str : String; + P : Integer; 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) + To : Integer) 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 (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' + and then P in 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. + and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1 + and then Spec.Is_Based_Format_Ghost (Str (From .. To)), + Post => P + 1 <= Spec.Last_Hexa_Ghost (Str (From .. To)) + and then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'; ----------------------------- -- Local lemma null bodies -- ----------------------------- - procedure Lemma_Digit_Is_Before_Last + procedure Lemma_Digit_Not_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) + procedure Lemma_Underscore_Not_Last + (Str : String; + P : Integer; + From : Integer; + To : Integer) 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; - - ---------------------------------------- - -- Prove_Iter_Scan_Based_Number_Ghost -- - ---------------------------------------- - - procedure Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - is - begin - if From > To then - null; - elsif Str1 (From) = '_' then - Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2, From + 1, To, Base, Acc); - elsif Scan_Overflows_Ghost - (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc) - then - null; - else - Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2, From + 1, To, Base, - Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From))); - end if; - end Prove_Iter_Scan_Based_Number_Ghost; - - ----------------------------------- - -- Prove_Scan_Only_Decimal_Ghost -- - ----------------------------------- - - procedure Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - is - Non_Blank : constant Positive := First_Non_Space_Ghost - (Str, Str'First, Str'Last); - pragma Assert (Non_Blank = Str'First + 1); - Fst_Num : constant Positive := - (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); - pragma Assert (Fst_Num = Str'First + 1); - Last_Num_Init : constant Integer := - Last_Number_Ghost (Str (Str'First + 1 .. Str'Last)); - pragma Assert (Last_Num_Init = Str'Last); - 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'; - pragma Assert (Starts_As_Based = False); - Last_Num_Based : constant Integer := - (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last)) - else Last_Num_Init); - pragma Assert (Last_Num_Based = Str'Last); - begin - pragma Assert - (Is_Opt_Exponent_Format_Ghost (Str (Str'Last + 1 .. Str'Last))); - pragma Assert - (Is_Natural_Format_Ghost (Str (Str'First + 1 .. Str'Last))); - pragma Assert - (Is_Raw_Unsigned_Format_Ghost (Str (Str'First + 1 .. Str'Last))); - pragma Assert - (not Raw_Unsigned_Overflows_Ghost (Str, Str'First + 1, Str'Last)); - pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value); - pragma Assert - (Val = Scan_Raw_Unsigned_Ghost (Str, Str'First + 1, Str'Last)); - pragma Assert (Is_Unsigned_Ghost (Str)); - pragma Assert (Is_Value_Unsigned_Ghost (Str, Val)); - end Prove_Scan_Only_Decimal_Ghost; - ----------------------- -- Scan_Raw_Unsigned -- ----------------------- @@ -341,8 +134,8 @@ package body System.Value_U is 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) + Init_Val : constant Spec.Uns_Option := + Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init) with Ghost; Starts_As_Based : constant Boolean := Last_Num_Init < Max - 1 @@ -352,7 +145,7 @@ package body System.Value_U is with Ghost; Last_Num_Based : constant Integer := (if Starts_As_Based - then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max)) + then Spec.Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max)) else Last_Num_Init) with Ghost; Is_Based : constant Boolean := @@ -360,9 +153,9 @@ package body System.Value_U is 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 := + Based_Val : constant Spec.Uns_Option := (if Starts_As_Based and then not Init_Val.Overflow - then Scan_Based_Number_Ghost + then Spec.Scan_Based_Number_Ghost (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value) else Init_Val) with Ghost; @@ -379,6 +172,7 @@ package body System.Value_U is end if; P := Ptr.all; + Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init); Uval := Character'Pos (Str (P)) - Character'Pos ('0'); P := P + 1; @@ -392,9 +186,6 @@ 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 @@ -403,7 +194,7 @@ package body System.Value_U is (if Overflow then Init_Val.Overflow); pragma Loop_Invariant (if not Overflow - then Init_Val = Scan_Based_Number_Ghost + then Init_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Init, Acc => Uval)); exit when P > Max; @@ -414,9 +205,8 @@ 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); + Spec.Lemma_Scan_Based_Number_Ghost_Underscore + (Str, P, Last_Num_Init, Acc => Uval); Scan_Underscore (Str, P, Ptr, Max, False); else exit; @@ -425,11 +215,19 @@ package body System.Value_U is -- Accumulate result, checking for overflow else - Old_Uval := Uval; - Old_Overflow := Overflow; + Spec.Lemma_Scan_Based_Number_Ghost_Step + (Str, P, Last_Num_Init, Acc => Uval); + Spec.Lemma_Scan_Based_Number_Ghost_Overflow + (Str, P, Last_Num_Init, Acc => Uval); if Uval <= Umax then + pragma Assert + (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit); Uval := 10 * Uval + Digit; + pragma Assert + (if not Overflow + then Init_Val = Spec.Scan_Based_Number_Ghost + (Str, P + 1, Last_Num_Init, Acc => Uval)); elsif Uval > Umax10 then Overflow := True; @@ -440,17 +238,17 @@ package body System.Value_U is if Uval < Umax10 then Overflow := True; end if; + pragma Assert + (if not Overflow + then Init_Val = Spec.Scan_Based_Number_Ghost + (Str, P + 1, Last_Num_Init, Acc => Uval)); 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); + Spec.Lemma_Scan_Based_Number_Ghost_Base + (Str, P, Last_Num_Init, Acc => Uval); end; pragma Assert_And_Cut @@ -488,18 +286,14 @@ 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))); + then Spec.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 @@ -519,6 +313,8 @@ package body System.Value_U is -- already stored in Ptr.all. else + Spec.Lemma_Scan_Based_Number_Ghost_Base + (Str, P, Last_Num_Based, Base, Uval); Uval := Base; Base := 10; pragma Assert (Ptr.all = Last_Num_Init + 1); @@ -529,25 +325,25 @@ package body System.Value_U is 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))); + and then Digit = Spec.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); + (Overflow'Loop_Entry or else Based_Val.Overflow)); pragma Loop_Invariant (if not Overflow - then Based_Val = Scan_Based_Number_Ghost + then Based_Val = Spec.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; + Spec.Lemma_Scan_Based_Number_Ghost_Step + (Str, P, Last_Num_Based, Base, Uval); + Spec.Lemma_Scan_Based_Number_Ghost_Overflow + (Str, P, Last_Num_Based, Base, Uval); -- If digit is too large, just signal overflow and continue. -- The idea here is to keep scanning as long as the input is @@ -560,6 +356,10 @@ package body System.Value_U is elsif Uval <= Umax then Uval := Base * Uval + Digit; + pragma Assert + (if not Overflow + then Based_Val = Spec.Scan_Based_Number_Ghost + (Str, P + 1, Last_Num_Based, Base, Uval)); elsif Uval > UmaxB then Overflow := True; @@ -570,6 +370,10 @@ package body System.Value_U is if Uval < UmaxB then Overflow := True; end if; + pragma Assert + (if not Overflow + then Based_Val = Spec.Scan_Based_Number_Ghost + (Str, P + 1, Last_Num_Based, Base, Uval)); end if; -- If at end of string with no base char, not a based number @@ -579,10 +383,6 @@ package body System.Value_U is P := P + 1; - Lemma_Scan_Digit - (Str, P - 1, Last_Num_Based, Digit, Base, Old_Uval, Uval, - Based_Val, Old_Overflow, Overflow); - if P > Max then Ptr.all := P; Bad_Value (Str); @@ -592,48 +392,54 @@ package body System.Value_U is if Str (P) = Base_Char then Ptr.all := P + 1; + pragma Assert (P = Last_Num_Based + 1); pragma Assert (Ptr.all = Last_Num_Based + 2); + pragma Assert (Starts_As_Based); + pragma Assert (Last_Num_Based < Max); + pragma Assert (Str (Last_Num_Based + 1) = Base_Char); + pragma Assert (Base_Char = Str (Last_Num_Init + 1)); pragma Assert (Is_Based); - pragma Assert - (if not Overflow then - Based_Val = Scan_Based_Number_Ghost - (Str, P, Last_Num_Based, Base, Uval)); - Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval); - pragma Assert (if not Overflow then Uval = Based_Val.Value); + Spec.Lemma_Scan_Based_Number_Ghost_Base + (Str, P, Last_Num_Based, Base, Uval); 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); + Lemma_Underscore_Not_Last (Str, P, Last_Num_Init + 2, Max); + Spec.Lemma_Scan_Based_Number_Ghost_Underscore + (Str, P, Last_Num_Based, Base, Uval); Scan_Underscore (Str, P, Ptr, Max, True); pragma Assert (if not Overflow - then Based_Val = Scan_Based_Number_Ghost + then Based_Val = Spec.Scan_Based_Number_Ghost (Str, P, Last_Num_Based, Base, Uval)); + pragma Assert (Str (P) /= '_'); + pragma Assert (Str (P) /= Base_Char); end if; + + Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max); + pragma Assert (Str (P) /= '_'); + pragma Assert (Str (P) /= Base_Char); end loop; end; pragma Assert (if Starts_As_Based then P = Last_Num_Based + 1 else P = Last_Num_Init + 2); + pragma Assert + (Last_Num_Init < Max - 1 + and then Str (Last_Num_Init + 1) in '#' | ':'); 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))); + pragma Assert + (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)); 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)) + (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max) and then (if not Overflow then (if Is_Based then Uval = Based_Val.Value @@ -649,10 +455,12 @@ package body System.Value_U is Scan_Exponent (Str, Ptr, Max, Expon); - pragma Assert (Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max)); pragma Assert - (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max)) - then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max))); + (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max)); + pragma Assert + (if not Overflow + then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) = + (Uval, Base, Expon)); if Expon /= 0 and then Uval /= 0 then @@ -664,8 +472,8 @@ 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) + Res_Val : constant Spec.Uns_Option := + Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) with Ghost; begin for J in 1 .. Expon loop @@ -674,48 +482,45 @@ package body System.Value_U is pragma Loop_Invariant (if Overflow then Overflow'Loop_Entry or else Res_Val.Overflow); + pragma Loop_Invariant (Uval /= 0); pragma Loop_Invariant (if not Overflow - then Res_Val = Exponent_Unsigned_Ghost + then Res_Val = Spec.Exponent_Unsigned_Ghost (Uval, Expon - J + 1, Base)); pragma Assert - ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval)); + ((Uval > UmaxB) = Spec.Scan_Overflows_Ghost (0, Base, Uval)); if Uval > UmaxB then + Spec.Lemma_Exponent_Unsigned_Ghost_Overflow + (Uval, Expon - J + 1, Base); Overflow := True; exit; end if; + Spec.Lemma_Exponent_Unsigned_Ghost_Step + (Uval, Expon - J + 1, Base); + Uval := Uval * Base; end loop; + Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, Base); + 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)); + (Overflow /= + Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max)); + pragma Assert (if not Overflow then Res_Val = (False, Uval)); end; end if; + Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, Expon, Base); pragma Assert (if Expon = 0 or else Uval = 0 then - Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval)); + Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval)); pragma Assert - (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max)); + (Overflow /= + Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max)); pragma Assert (if not Overflow then - Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max)); + Uval = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max)); -- Return result, dealing with overflow @@ -774,7 +579,15 @@ package body System.Value_U is if Str'Last = Positive'Last then declare subtype NT is String (1 .. Str'Length); + procedure Prove_Is_Unsigned_Ghost with + Ghost, + Pre => Str'Length < Natural'Last + and then not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Spec.Is_Unsigned_Ghost (Spec.Slide_To_1 (Str)), + Post => Spec.Is_Unsigned_Ghost (NT (Str)); + procedure Prove_Is_Unsigned_Ghost is null; begin + Prove_Is_Unsigned_Ghost; return Value_Unsigned (NT (Str)); end; @@ -784,7 +597,6 @@ 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; @@ -792,9 +604,6 @@ package body System.Value_U is (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank) with Ghost; begin - pragma Assert - (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); - declare P_Acc : constant not null access Integer := P'Access; begin @@ -802,14 +611,15 @@ package body System.Value_U is end; pragma Assert - (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); + (P = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last)); pragma Assert - (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last)); + (V = Spec.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)); + (Spec.Is_Value_Unsigned_Ghost + (Spec.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 1508b6ecb1c..466b96a6fa6 100644 --- a/gcc/ada/libgnat/s-valueu.ads +++ b/gcc/ada/libgnat/s-valueu.ads @@ -44,6 +44,7 @@ pragma Assertion_Policy (Pre => Ignore, Ghost => Ignore, Subprogram_Variant => Ignore); +with System.Value_U_Spec; with System.Val_Util; use System.Val_Util; generic @@ -53,317 +54,7 @@ generic package System.Value_U is pragma Preelaborate; - type Uns_Option (Overflow : Boolean := False) is record - case Overflow is - when True => - null; - when False => - Value : Uns := 0; - end case; - end record; - - function Wrap_Option (Value : Uns) return Uns_Option is - (Overflow => False, Value => Value) - with - Ghost; - - function Only_Decimal_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 decimal characters - -- from index From to index To. - - 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. + package Spec is new System.Value_U_Spec (Uns); procedure Scan_Raw_Unsigned (Str : String; @@ -373,10 +64,10 @@ package System.Value_U is 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); + and then Spec.Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)), + Post => Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr.all'Old, Max) + and Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max) + and Ptr.all = Spec.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 @@ -464,7 +155,7 @@ package System.Value_U is 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))), + Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))), Post => (declare Non_Blank : constant Positive := @@ -472,9 +163,9 @@ package System.Value_U is 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)); + Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Max) + and then Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max) + and then Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max)); -- Same as Scan_Raw_Unsigned, except scans optional leading -- blanks, and an optional leading plus sign. @@ -482,157 +173,18 @@ package System.Value_U is -- 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 - 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)), + with Pre => Str'Length /= Positive'Last + and then not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Spec.Is_Unsigned_Ghost (Spec.Slide_If_Necessary (Str)), Post => - Is_Value_Unsigned_Ghost - (Slide_If_Necessary (Str), Value_Unsigned'Result), + Spec.Is_Value_Unsigned_Ghost + (Spec.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. - procedure Prove_Iter_Scan_Based_Number_Ghost - (Str1, Str2 : String; - From, To : Integer; - Base : Uns := 10; - Acc : Uns := 0) - with - Ghost, - Subprogram_Variant => (Increases => From), - Pre => Str1'Last /= Positive'Last - and then Str2'Last /= Positive'Last - and then - (From > To or else (From >= Str1'First and then To <= Str1'Last)) - and then - (From > To or else (From >= Str2'First and then To <= Str2'Last)) - and then Only_Hexa_Ghost (Str1, From, To) - and then (for all J in From .. To => Str1 (J) = Str2 (J)), - Post => - Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) - = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); - -- Ghost lemma used in the proof of 'Image implementation, to prove the - -- preservation of Scan_Based_Number_Ghost across an update in the string - -- in lower indexes. - - procedure Prove_Scan_Only_Decimal_Ghost - (Str : String; - Val : Uns) - with - Ghost, - Pre => Str'Last /= Positive'Last - and then Str'Length >= 2 - and then Str (Str'First) = ' ' - and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) - and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) - = Wrap_Option (Val), - Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str)) - and then Value_Unsigned (Str) = Val; - -- Ghost lemma used in the proof of 'Image implementation, to prove that - -- the result of Value_Unsigned on a decimal string is the same as the - -- result of Scan_Based_Number_Ghost. - -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-valuti.ads b/gcc/ada/libgnat/s-valuti.ads index 2b89b1246f2..7c2da17aa53 100644 --- a/gcc/ada/libgnat/s-valuti.ads +++ b/gcc/ada/libgnat/s-valuti.ads @@ -374,48 +374,274 @@ is -- no check for this case, the caller must ensure this condition is met. pragma Warnings (GNATprove, On, """Ptr"" is not modified"); - -- Bundle Int type with other types, constants and subprograms used in + -- Bundle Uns type with other types, constants and subprograms used in -- ghost code, so that this package can be instantiated once and used - -- multiple times as generic formal for a given Int type. + -- multiple times as generic formal for a given Uns type. generic - type Int is range <>; type Uns is mod <>; - type Uns_Option is private; + type P_Uns_Option is private with Ghost; + with function P_Wrap_Option (Value : Uns) return P_Uns_Option + with Ghost; + with function P_Hexa_To_Unsigned_Ghost (X : Character) return Uns + with Ghost; + with function P_Scan_Overflows_Ghost + (Digit : Uns; + Base : Uns; + Acc : Uns) return Boolean + with Ghost; + with function P_Is_Raw_Unsigned_Format_Ghost + (Str : String) return Boolean + with Ghost; + with function P_Scan_Split_No_Overflow_Ghost + (Str : String; + From, To : Integer) + return Boolean + with Ghost; + with function P_Raw_Unsigned_No_Overflow_Ghost + (Str : String; + From, To : Integer) + return Boolean + with Ghost; - Unsigned_Width_Ghost : Natural; + with function P_Exponent_Unsigned_Ghost + (Value : Uns; + Exp : Natural; + Base : Uns := 10) return P_Uns_Option + with Ghost; + with procedure P_Lemma_Exponent_Unsigned_Ghost_Base + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with Ghost; + with procedure P_Lemma_Exponent_Unsigned_Ghost_Overflow + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with Ghost; + with procedure P_Lemma_Exponent_Unsigned_Ghost_Step + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with Ghost; - with function Wrap_Option (Value : Uns) return Uns_Option - with Ghost; - with function Only_Decimal_Ghost + with function P_Scan_Raw_Unsigned_Ghost (Str : String; From, To : Integer) - return Boolean - with Ghost; - with function Hexa_To_Unsigned_Ghost (X : Character) return Uns - with Ghost; - with function Scan_Based_Number_Ghost + return Uns + with Ghost; + with procedure P_Lemma_Scan_Based_Number_Ghost_Base (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) - return Uns_Option - with Ghost; - with function Is_Integer_Ghost (Str : String) return Boolean - with Ghost; - with procedure Prove_Iter_Scan_Based_Number_Ghost + with Ghost; + with procedure P_Lemma_Scan_Based_Number_Ghost_Underscore + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with Ghost; + with procedure P_Lemma_Scan_Based_Number_Ghost_Overflow + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with Ghost; + with procedure P_Lemma_Scan_Based_Number_Ghost_Step + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with Ghost; + + with function P_Raw_Unsigned_Last_Ghost + (Str : String; + From, To : Integer) + return Positive + with Ghost; + with function P_Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean + with Ghost; + with function P_Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + return P_Uns_Option + with Ghost; + with function P_Is_Unsigned_Ghost (Str : String) return Boolean + with Ghost; + with function P_Is_Value_Unsigned_Ghost + (Str : String; + Val : Uns) return Boolean + with Ghost; + + with procedure P_Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + with Ghost; + with procedure P_Prove_Scan_Based_Number_Ghost_Eq (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with Ghost; + + package Uns_Params is + subtype Uns_Option is P_Uns_Option with Ghost; + function Wrap_Option (Value : Uns) return Uns_Option renames + P_Wrap_Option; + function Hexa_To_Unsigned_Ghost + (X : Character) return Uns + renames P_Hexa_To_Unsigned_Ghost; + function Scan_Overflows_Ghost + (Digit : Uns; + Base : Uns; + Acc : Uns) return Boolean + renames P_Scan_Overflows_Ghost; + function Is_Raw_Unsigned_Format_Ghost + (Str : String) return Boolean + renames P_Is_Raw_Unsigned_Format_Ghost; + function Scan_Split_No_Overflow_Ghost + (Str : String; + From, To : Integer) return Boolean + renames P_Scan_Split_No_Overflow_Ghost; + function Raw_Unsigned_No_Overflow_Ghost + (Str : String; + From, To : Integer) return Boolean + renames P_Raw_Unsigned_No_Overflow_Ghost; + + function Exponent_Unsigned_Ghost + (Value : Uns; + Exp : Natural; + Base : Uns := 10) return Uns_Option + renames P_Exponent_Unsigned_Ghost; + procedure Lemma_Exponent_Unsigned_Ghost_Base + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + renames P_Lemma_Exponent_Unsigned_Ghost_Base; + procedure Lemma_Exponent_Unsigned_Ghost_Overflow + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + renames P_Lemma_Exponent_Unsigned_Ghost_Overflow; + procedure Lemma_Exponent_Unsigned_Ghost_Step + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + renames P_Lemma_Exponent_Unsigned_Ghost_Step; + + function Scan_Raw_Unsigned_Ghost + (Str : String; + From, To : Integer) return Uns + renames P_Scan_Raw_Unsigned_Ghost; + procedure Lemma_Scan_Based_Number_Ghost_Base + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + renames P_Lemma_Scan_Based_Number_Ghost_Base; + procedure Lemma_Scan_Based_Number_Ghost_Underscore + (Str : String; From, To : Integer; Base : Uns := 10; Acc : Uns := 0) + renames P_Lemma_Scan_Based_Number_Ghost_Underscore; + procedure Lemma_Scan_Based_Number_Ghost_Overflow + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + renames P_Lemma_Scan_Based_Number_Ghost_Overflow; + procedure Lemma_Scan_Based_Number_Ghost_Step + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + renames P_Lemma_Scan_Based_Number_Ghost_Step; + + function Raw_Unsigned_Last_Ghost + (Str : String; + From, To : Integer) return Positive + renames P_Raw_Unsigned_Last_Ghost; + function Only_Decimal_Ghost + (Str : String; + From, To : Integer) return Boolean + renames P_Only_Decimal_Ghost; + function Scan_Based_Number_Ghost + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) return Uns_Option + renames P_Scan_Based_Number_Ghost; + function Is_Unsigned_Ghost (Str : String) return Boolean + renames P_Is_Unsigned_Ghost; + function Is_Value_Unsigned_Ghost + (Str : String; + Val : Uns) return Boolean + renames P_Is_Value_Unsigned_Ghost; + + procedure Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + renames P_Prove_Scan_Only_Decimal_Ghost; + procedure Prove_Scan_Based_Number_Ghost_Eq + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + renames P_Prove_Scan_Based_Number_Ghost_Eq; + end Uns_Params; + + -- Bundle Int type with other types, constants and subprograms used in + -- ghost code, so that this package can be instantiated once and used + -- multiple times as generic formal for a given Int type. + generic + type Int is range <>; + type Uns is mod <>; + + with package P_Uns_Params is new System.Val_Util.Uns_Params + (Uns => Uns, others => <>) + with Ghost; + + with function P_Abs_Uns_Of_Int (Val : Int) return Uns + with Ghost; + with function P_Is_Int_Of_Uns + (Minus : Boolean; + Uval : Uns; + Val : Int) + return Boolean with Ghost; - with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) + with function P_Is_Integer_Ghost (Str : String) return Boolean with Ghost; - with function Abs_Uns_Of_Int (Val : Int) return Uns + with function P_Is_Value_Integer_Ghost + (Str : String; + Val : Int) return Boolean with Ghost; - with function Value_Integer (Str : String) return Int + with procedure P_Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) with Ghost; package Int_Params is + package Uns_Params renames P_Uns_Params; + function Abs_Uns_Of_Int (Val : Int) return Uns renames + P_Abs_Uns_Of_Int; + function Is_Int_Of_Uns + (Minus : Boolean; + Uval : Uns; + Val : Int) + return Boolean + renames P_Is_Int_Of_Uns; + function Is_Integer_Ghost (Str : String) return Boolean renames + P_Is_Integer_Ghost; + function Is_Value_Integer_Ghost + (Str : String; + Val : Int) return Boolean + renames P_Is_Value_Integer_Ghost; + procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) renames + P_Prove_Scan_Only_Decimal_Ghost; end Int_Params; private diff --git a/gcc/ada/libgnat/s-vauspe.adb b/gcc/ada/libgnat/s-vauspe.adb new file mode 100644 index 00000000000..1a870b9b997 --- /dev/null +++ b/gcc/ada/libgnat/s-vauspe.adb @@ -0,0 +1,198 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L U E _ U _ S P E C -- +-- -- +-- B o d y -- +-- -- +-- Copyright (C) 2022-2022, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + +package body System.Value_U_Spec with SPARK_Mode is + + ----------------------------- + -- 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)); + + --------------------- + -- 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; + + ----------------------------- + -- Lemmas with null bodies -- + ----------------------------- + + procedure Lemma_Scan_Based_Number_Ghost_Base + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is null; + + procedure Lemma_Scan_Based_Number_Ghost_Underscore + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is null; + + procedure Lemma_Scan_Based_Number_Ghost_Overflow + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is null; + + procedure Lemma_Scan_Based_Number_Ghost_Step + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is null; + + procedure Lemma_Exponent_Unsigned_Ghost_Base + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + is null; + + procedure Lemma_Exponent_Unsigned_Ghost_Overflow + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + is null; + + procedure Lemma_Exponent_Unsigned_Ghost_Step + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + is null; + + -------------------------------------- + -- Prove_Scan_Based_Number_Ghost_Eq -- + -------------------------------------- + + procedure Prove_Scan_Based_Number_Ghost_Eq + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + is + begin + if From > To then + null; + elsif Str1 (From) = '_' then + Prove_Scan_Based_Number_Ghost_Eq + (Str1, Str2, From + 1, To, Base, Acc); + elsif Scan_Overflows_Ghost + (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc) + then + null; + else + Prove_Scan_Based_Number_Ghost_Eq + (Str1, Str2, From + 1, To, Base, + Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From))); + end if; + end Prove_Scan_Based_Number_Ghost_Eq; + + ----------------------------------- + -- Prove_Scan_Only_Decimal_Ghost -- + ----------------------------------- + + procedure Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + is + pragma Assert (Str (Str'First + 1) /= ' '); + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last); + pragma Assert (Non_Blank = Str'First + 1); + Fst_Num : constant Positive := + (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank); + pragma Assert (Fst_Num = Str'First + 1); + begin + pragma Assert + (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + pragma Assert + (Scan_Split_No_Overflow_Ghost (Str, Str'First + 1, Str'Last)); + pragma Assert + ((Val, 10, 0) = Scan_Split_Value_Ghost (Str, Str'First + 1, Str'Last)); + pragma Assert + (Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)); + pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value); + pragma Assert (Is_Unsigned_Ghost (Str)); + pragma Assert (Is_Value_Unsigned_Ghost (Str, Val)); + end Prove_Scan_Only_Decimal_Ghost; + + ----------------------------- + -- 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)))); + +end System.Value_U_Spec; diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads new file mode 100644 index 00000000000..0d5c19e8c53 --- /dev/null +++ b/gcc/ada/libgnat/s-vauspe.ads @@ -0,0 +1,639 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT COMPILER COMPONENTS -- +-- -- +-- S Y S T E M . V A L U E _ U _ S P E C -- +-- -- +-- S p e c -- +-- -- +-- Copyright (C) 2022-2022, Free Software Foundation, Inc. -- +-- -- +-- GNAT is free software; you can redistribute it and/or modify it under -- +-- terms of the GNU General Public License as published by the Free Soft- -- +-- ware Foundation; either version 3, or (at your option) any later ver- -- +-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- +-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- +-- or FITNESS FOR A PARTICULAR PURPOSE. -- +-- -- +-- As a special exception under Section 7 of GPL version 3, you are granted -- +-- additional permissions described in the GCC Runtime Library Exception, -- +-- version 3.1, as published by the Free Software Foundation. -- +-- -- +-- You should have received a copy of the GNU General Public License and -- +-- a copy of the GCC Runtime Library Exception along with this program; -- +-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- +-- . -- +-- -- +-- GNAT was originally developed by the GNAT team at New York University. -- +-- Extensive contributions were provided by Ada Core Technologies Inc. -- +-- -- +------------------------------------------------------------------------------ + +-- This package contains the specification entities using for the formal +-- verification of the routines for scanning modular Unsigned values. + +-- 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.Val_Util; use System.Val_Util; + +generic + + type Uns is mod <>; + +package System.Value_U_Spec with + Ghost, + SPARK_Mode, + Annotate => (GNATprove, Always_Return) +is + pragma Preelaborate; + + type Uns_Option (Overflow : Boolean := False) is record + case Overflow is + when True => + null; + when False => + Value : Uns := 0; + end case; + end record; + + function Wrap_Option (Value : Uns) return Uns_Option is + (Overflow => False, Value => Value); + + function Only_Decimal_Ghost + (Str : String; + From, To : Integer) + return Boolean + is + (for all J in From .. To => Str (J) in '0' .. '9') + with + Pre => From > To or else (From >= Str'First and then To <= Str'Last); + -- Ghost function that returns True if S has only decimal characters + -- from index From to index To. + + 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 + 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 + 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) /= '_')))); + -- 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 + 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); + -- 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 + 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. + + -- Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost + + procedure Lemma_Scan_Based_Number_Ghost_Base + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Global => null, + 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), + Post => + (if From > To + then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = + (Overflow => False, Value => Acc)); + -- Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To + + procedure Lemma_Scan_Based_Number_Ghost_Underscore + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Global => null, + 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), + Post => + (if From <= To and then Str (From) = '_' + then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = + Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)); + -- Underscore case: underscores are ignored while scanning + + procedure Lemma_Scan_Based_Number_Ghost_Overflow + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Global => null, + 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), + Post => + (if From <= To + and then Str (From) /= '_' + and then Scan_Overflows_Ghost + (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) + then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = + (Overflow => True)); + -- Overflow case: scanning a digit which causes an overflow + + procedure Lemma_Scan_Based_Number_Ghost_Step + (Str : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Global => null, + 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), + Post => + (if From <= To + and then Str (From) /= '_' + and then not Scan_Overflows_Ghost + (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc) + then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) = + Scan_Based_Number_Ghost + (Str, From + 1, To, Base, + Base * Acc + Hexa_To_Unsigned_Ghost (Str (From)))); + -- Normal case: scanning a digit without overflows + + function Exponent_Unsigned_Ghost + (Value : Uns; + Exp : Natural; + Base : Uns := 10) return Uns_Option + with + Subprogram_Variant => (Decreases => Exp); + -- Ghost function that recursively computes Value * Base ** Exp + + -- Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost + + procedure Lemma_Exponent_Unsigned_Ghost_Base + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with + Post => + (if Exp = 0 or Value = 0 + then Exponent_Unsigned_Ghost (Value, Exp, Base) = + (Overflow => False, Value => Value)); + -- Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0 + + procedure Lemma_Exponent_Unsigned_Ghost_Overflow + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with + Post => + (if Exp /= 0 + and then Value /= 0 + and then Scan_Overflows_Ghost (0, Base, Value) + then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True)); + -- Overflow case: the next multiplication overflows + + procedure Lemma_Exponent_Unsigned_Ghost_Step + (Value : Uns; + Exp : Natural; + Base : Uns := 10) + with + Post => + (if Exp /= 0 + and then Value /= 0 + and then not Scan_Overflows_Ghost (0, Base, Value) + then Exponent_Unsigned_Ghost (Value, Exp, Base) = + Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base)); + -- Normal case: exponentiation without overflows + + 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 + Pre => Str'Last /= Positive'Last; + -- 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. + + type Split_Value_Ghost is record + Value : Uns; + Base : Uns; + Expon : Natural; + end record; + + function Scan_Split_No_Overflow_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); + 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); + begin + not Init_Val.Overflow + and then + (Last_Num_Init >= To - 1 + or else Str (Last_Num_Init + 1) not in '#' | ':' + or else Init_Val.Value in 2 .. 16) + and then + (not Starts_As_Based + or else not Based_Val.Overflow)) + with + 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'; + -- Ghost function that determines if an overflow might occur while scanning + -- the representation of an unsigned number. 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, + -- or + -- * The computation of the based part overflows. + + pragma Warnings (Off, "constant * is not referenced"); + function Scan_Split_Value_Ghost + (Str : String; + From, To : Integer) + return Split_Value_Ghost + 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 + (Value => Value, Base => Base, Expon => Expon)) + with + 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 Scan_Split_No_Overflow_Ghost (Str, From, To); + -- Ghost function that scans an unsigned number without a sign character + -- and return a record containing the values scanned for its value, its + -- base, and its exponent. + pragma Warnings (On, "constant * is not referenced"); + + function Raw_Unsigned_No_Overflow_Ghost + (Str : String; + From, To : Integer) + return Boolean + is + (Scan_Split_No_Overflow_Ghost (Str, From, To) + and then + (declare + Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost + (Str, From, To); + begin + not Exponent_Unsigned_Ghost + (Val.Value, Val.Expon, Val.Base).Overflow)) + with + 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'; + -- Ghost function that determines if the computation of the unsigned number + -- represented by Str will overflow. The computation overflows if either: + -- * The scan of the string overflows, or + -- * The computation of the exponentiation overflows. + + function Scan_Raw_Unsigned_Ghost + (Str : String; + From, To : Integer) + return Uns + is + (declare + Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost + (Str, From, To); + begin + Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value) + with + 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 Raw_Unsigned_No_Overflow_Ghost (Str, From, To); + -- 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 + 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'; + -- Ghost function that returns the position of the cursor once an unsigned + -- number has been seen. + + function Slide_To_1 (Str : String) return String + with + 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); + -- 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 Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last) + and then Only_Space_Ghost + (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last)) + with + Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Last /= Positive'Last; + -- 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 + Pre => not Only_Space_Ghost (Str, Str'First, Str'Last) + and then Str'Last /= Positive'Last + and then Is_Unsigned_Ghost (Str); + -- Ghost function that returns True if Val is the value corresponding to + -- the unsigned number represented by Str. + + procedure Prove_Scan_Based_Number_Ghost_Eq + (Str1, Str2 : String; + From, To : Integer; + Base : Uns := 10; + Acc : Uns := 0) + with + Subprogram_Variant => (Increases => From), + Pre => Str1'Last /= Positive'Last + and then Str2'Last /= Positive'Last + and then + (From > To or else (From >= Str1'First and then To <= Str1'Last)) + and then + (From > To or else (From >= Str2'First and then To <= Str2'Last)) + and then Only_Hexa_Ghost (Str1, From, To) + and then (for all J in From .. To => Str1 (J) = Str2 (J)), + Post => + Scan_Based_Number_Ghost (Str1, From, To, Base, Acc) + = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc); + -- Scan_Based_Number_Ghost returns the same value on two slices which are + -- equal. + + procedure Prove_Scan_Only_Decimal_Ghost + (Str : String; + Val : Uns) + with + Pre => Str'Last /= Positive'Last + and then Str'Length >= 2 + and then Str (Str'First) = ' ' + and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last) + and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last) + = Wrap_Option (Val), + Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str)) + and then + Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val); + -- Ghost lemma used in the proof of 'Image implementation, to prove that + -- the result of Value_Unsigned on a decimal string is the same as the + -- result of Scan_Based_Number_Ghost. + + -- Bundle Uns type with other types, constants and subprograms used in + -- ghost code, so that this package can be instantiated once and used + -- multiple times as generic formal for a given Int type. + + package Uns_Params is new System.Val_Util.Uns_Params + (Uns => Uns, + P_Uns_Option => Uns_Option, + P_Wrap_Option => Wrap_Option, + P_Hexa_To_Unsigned_Ghost => Hexa_To_Unsigned_Ghost, + P_Scan_Overflows_Ghost => Scan_Overflows_Ghost, + P_Is_Raw_Unsigned_Format_Ghost => + Is_Raw_Unsigned_Format_Ghost, + P_Scan_Split_No_Overflow_Ghost => + Scan_Split_No_Overflow_Ghost, + P_Raw_Unsigned_No_Overflow_Ghost => + Raw_Unsigned_No_Overflow_Ghost, + P_Exponent_Unsigned_Ghost => Exponent_Unsigned_Ghost, + P_Lemma_Exponent_Unsigned_Ghost_Base => + Lemma_Exponent_Unsigned_Ghost_Base, + P_Lemma_Exponent_Unsigned_Ghost_Overflow => + Lemma_Exponent_Unsigned_Ghost_Overflow, + P_Lemma_Exponent_Unsigned_Ghost_Step => + Lemma_Exponent_Unsigned_Ghost_Step, + P_Scan_Raw_Unsigned_Ghost => Scan_Raw_Unsigned_Ghost, + P_Lemma_Scan_Based_Number_Ghost_Base => + Lemma_Scan_Based_Number_Ghost_Base, + P_Lemma_Scan_Based_Number_Ghost_Underscore => + Lemma_Scan_Based_Number_Ghost_Underscore, + P_Lemma_Scan_Based_Number_Ghost_Overflow => + Lemma_Scan_Based_Number_Ghost_Overflow, + P_Lemma_Scan_Based_Number_Ghost_Step => + Lemma_Scan_Based_Number_Ghost_Step, + P_Raw_Unsigned_Last_Ghost => Raw_Unsigned_Last_Ghost, + P_Only_Decimal_Ghost => Only_Decimal_Ghost, + P_Scan_Based_Number_Ghost => Scan_Based_Number_Ghost, + P_Is_Unsigned_Ghost => + Is_Unsigned_Ghost, + P_Is_Value_Unsigned_Ghost => + Is_Value_Unsigned_Ghost, + P_Prove_Scan_Only_Decimal_Ghost => + Prove_Scan_Only_Decimal_Ghost, + P_Prove_Scan_Based_Number_Ghost_Eq => + Prove_Scan_Based_Number_Ghost_Eq); + +private + + ---------------- + -- 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_Spec;