From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id EEA1638346A4; Tue, 10 May 2022 08:21:31 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org EEA1638346A4 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r13-233] [Ada] Proof of System.Val_Int at gold level X-Act-Checkin: gcc X-Git-Author: Claire Dross X-Git-Refname: refs/heads/master X-Git-Oldrev: 7f8053225de072fed9c4822e589c853a6f5e47c4 X-Git-Newrev: 336ea8f2d6ef528db37212ac7517330274a4793a Message-Id: <20220510082131.EEA1638346A4@sourceware.org> Date: Tue, 10 May 2022 08:21:31 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Tue, 10 May 2022 08:21:32 -0000 https://gcc.gnu.org/g:336ea8f2d6ef528db37212ac7517330274a4793a commit r13-233-g336ea8f2d6ef528db37212ac7517330274a4793a Author: Claire Dross Date: Thu Jan 20 09:15:28 2022 +0100 [Ada] Proof of System.Val_Int at gold level gcc/ada/ * libgnat/s-valint.ads: Add SPARK_Mode and pragma to ignore assertions in instance and add additional ghost parameters to the instance of Value_I. * libgnat/s-vallli.ads: Idem. * libgnat/s-valllli.ads: Idem. * libgnat/s-valuei.ads, libgnat/s-valuei.adb: New generic parameters for ghost functions from System.Valueu. Add functional contracts. Diff: --- gcc/ada/libgnat/s-valint.ads | 27 ++++++- gcc/ada/libgnat/s-vallli.ads | 31 ++++++-- gcc/ada/libgnat/s-valllli.ads | 31 ++++++-- gcc/ada/libgnat/s-valuei.adb | 55 ++++++++++++-- gcc/ada/libgnat/s-valuei.ads | 167 +++++++++++++++++++++++++++++++++++++++++- 5 files changed, 289 insertions(+), 22 deletions(-) diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads index 4fef265e9cf..c0d47aa1ce7 100644 --- a/gcc/ada/libgnat/s-valint.ads +++ b/gcc/ada/libgnat/s-valint.ads @@ -32,16 +32,39 @@ -- This package contains routines for scanning signed Integer values for use -- in Text_IO.Integer_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Val_Uns; with System.Value_I; -package System.Val_Int is +package System.Val_Int with SPARK_Mode is pragma Preelaborate; subtype Unsigned is Unsigned_Types.Unsigned; - package Impl is new Value_I (Integer, Unsigned, Val_Uns.Scan_Raw_Unsigned); + package Impl is new Value_I + (Int => Integer, + Uns => Unsigned, + Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned, + 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); procedure Scan_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads index ce1d9ee1340..dfb1729e41c 100644 --- a/gcc/ada/libgnat/s-vallli.ads +++ b/gcc/ada/libgnat/s-vallli.ads @@ -32,19 +32,40 @@ -- This package contains routines for scanning signed Long_Long_Integer -- values for use in Text_IO.Integer_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Val_LLU; with System.Value_I; -package System.Val_LLI is +package System.Val_LLI with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; - package Impl is new - Value_I (Long_Long_Integer, - Long_Long_Unsigned, - Val_LLU.Scan_Raw_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, + 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); procedure Scan_Long_Long_Integer (Str : String; diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads index 176000a4060..84bca5878ed 100644 --- a/gcc/ada/libgnat/s-valllli.ads +++ b/gcc/ada/libgnat/s-valllli.ads @@ -32,19 +32,40 @@ -- This package contains routines for scanning signed Long_Long_Long_Integer -- values for use in Text_IO.Integer_IO, and the Value attribute. +-- Preconditions in this unit are meant for analysis only, not for run-time +-- checking, so that the expected exceptions are raised. This is enforced by +-- setting the corresponding assertion policy to Ignore. Postconditions and +-- contract cases should not be executed at runtime as well, in order not to +-- slow down the execution of these functions. + +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); + with System.Unsigned_Types; with System.Val_LLLU; with System.Value_I; -package System.Val_LLLI is +package System.Val_LLLI with SPARK_Mode is pragma Preelaborate; subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; - package Impl is new - Value_I (Long_Long_Long_Integer, - Long_Long_Long_Unsigned, - Val_LLLU.Scan_Raw_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, + 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); 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 83828d34dd7..faf57915c78 100644 --- a/gcc/ada/libgnat/s-valuei.adb +++ b/gcc/ada/libgnat/s-valuei.adb @@ -29,10 +29,18 @@ -- -- ------------------------------------------------------------------------------ -with System.Val_Util; use System.Val_Util; - package body System.Value_I is + -- Ghost code, loop invariants and assertions in this unit are meant for + -- analysis only, not for run-time checking, as it would be too costly + -- otherwise. This is enforced by setting the assertion policy to Ignore. + + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore, + Assert_And_Cut => Ignore, + Subprogram_Variant => Ignore); + ------------------ -- Scan_Integer -- ------------------ @@ -46,26 +54,35 @@ package body System.Value_I is Uval : Uns; -- Unsigned result - Minus : Boolean := False; + Minus : Boolean; -- Set to True if minus sign is present, otherwise to False - Start : Positive; + Unused_Start : Positive; -- Saves location of first non-blank (not used in this case) + Non_Blank : constant Positive := + First_Non_Space_Ghost (Str, Ptr.all, Max) + with Ghost; + Fst_Num : constant Positive := + (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 + else Non_Blank) + with Ghost; + begin - Scan_Sign (Str, Ptr, Max, Minus, Start); + Scan_Sign (Str, Ptr, Max, Minus, Unused_Start); if Str (Ptr.all) not in '0' .. '9' then - Ptr.all := Start; + Ptr.all := Unused_Start; Bad_Value (Str); end if; Scan_Raw_Unsigned (Str, Ptr, Max, Uval); + pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)); -- Deal with overflow cases, and also with largest negative number if Uval > Uns (Int'Last) then - if Minus and then Uval = Uns (-(Int'First)) then + if Minus and then Uval = Uns (Int'Last) + 1 then Res := Int'First; else Bad_Value (Str); @@ -106,9 +123,31 @@ package body System.Value_I is declare V : Int; P : aliased Integer := Str'First; + + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Str'First, Str'Last) + with Ghost; + Fst_Num : constant Positive := + (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 + else Non_Blank) + with Ghost; begin - Scan_Integer (Str, P'Access, Str'Last, V); + pragma Assert + (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))); + + declare + P_Acc : constant not null access Integer := P'Access; + begin + Scan_Integer (Str, P_Acc, Str'Last, V); + end; + + pragma Assert + (P = 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)); return V; end; end if; diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads index e0a34d9465c..d6a78fda540 100644 --- a/gcc/ada/libgnat/s-valuei.ads +++ b/gcc/ada/libgnat/s-valuei.ads @@ -32,6 +32,16 @@ -- This package contains routines for scanning signed integer values for use -- in Text_IO.Integer_IO, and the Value attribute. +pragma Assertion_Policy (Pre => Ignore, + Post => Ignore, + Contract_Cases => Ignore, + Ghost => Ignore, + Subprogram_Variant => Ignore); +pragma Warnings (Off, "postcondition does not mention function result"); +-- True postconditions are used to avoid inlining for GNATprove + +with System.Val_Util; use System.Val_Util; + generic type Int is range <>; @@ -44,14 +54,86 @@ generic Max : Integer; Res : out Uns); + -- Additional parameters for ghost subprograms used inside contracts + + with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean; + with function Raw_Unsigned_Overflows_Ghost + (Str : String; + From, To : Integer) + return Boolean; + with function Scan_Raw_Unsigned_Ghost + (Str : String; + From, To : Integer) + return Uns; + with function Raw_Unsigned_Last_Ghost + (Str : String; + From, To : Integer) + return Positive; + package System.Value_I is pragma Preelaborate; + 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 + procedure Scan_Integer (Str : String; Ptr : not null access Integer; Max : Integer; - Res : out Int); + Res : out Int) + with + Pre => + Str'Last /= Positive'Last + -- Ptr.all .. Max is either an empty range, or a valid range in Str + and then (Ptr.all > Max + or else (Ptr.all >= Str'First and then Max <= Str'Last)) + and then not Only_Space_Ghost (Str, Ptr.all, Max) + and then + (declare + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Ptr.all, Max); + 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 .. Max)) + and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max) + and then Uns_Is_Valid_Int + (Minus => Str (Non_Blank) = '-', + Uval => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))), + Post => + (declare + Non_Blank : constant Positive := First_Non_Space_Ghost + (Str, Ptr.all'Old, Max); + Fst_Num : constant Positive := + (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 + else Non_Blank); + Uval : constant Uns := + 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)); -- 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 @@ -77,10 +159,91 @@ 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 Value_Integer (Str : String) return Int; + 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), + 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. +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;