diff options
author | Claire Dross <dross@adacore.com> | 2022-01-20 09:15:28 +0100 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2022-05-10 08:19:23 +0000 |
commit | 336ea8f2d6ef528db37212ac7517330274a4793a (patch) | |
tree | 656606babf94e468a1c8070ced70ea2ccb1c1960 /gcc | |
parent | 7f8053225de072fed9c4822e589c853a6f5e47c4 (diff) | |
download | gcc-336ea8f2d6ef528db37212ac7517330274a4793a.zip gcc-336ea8f2d6ef528db37212ac7517330274a4793a.tar.gz gcc-336ea8f2d6ef528db37212ac7517330274a4793a.tar.bz2 |
[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.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/s-valint.ads | 27 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-vallli.ads | 31 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-valllli.ads | 31 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-valuei.adb | 55 | ||||
-rw-r--r-- | 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 4fef265..c0d47aa 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 ce1d9ee..dfb1729 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 176000a..84bca58 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 83828d3..faf5791 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 e0a34d9..d6a78fd 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; |