diff options
author | Yannick Moy <moy@adacore.com> | 2021-11-24 17:20:59 +0100 |
---|---|---|
committer | Pierre-Marie de Rodat <derodat@adacore.com> | 2021-12-02 16:26:28 +0000 |
commit | 3a54dfa801a1cfb387c8c43e7610b11905db505c (patch) | |
tree | 40a736016981b85ec70ac272c3f4d98f71dc58f0 /gcc | |
parent | 167be0845e555cf98a59d768002c7f48bf85fe11 (diff) | |
download | gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.zip gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.tar.gz gcc-3a54dfa801a1cfb387c8c43e7610b11905db505c.tar.bz2 |
[Ada] Proof of support units for 'Width on signed integers
gcc/ada/
* libgnat/s-widint.ads: Mark in SPARK.
* libgnat/s-widlli.ads: Likewise.
* libgnat/s-widllli.ads: Likewise.
* libgnat/s-widlllu.ads: Likewise.
* libgnat/s-widllu.ads: Disable ghost/contract.
* libgnat/s-widthi.adb: Replicate and adapt the proof from
s-widthu.adb.
* libgnat/s-widthi.ads: Add minimal postcondition.
* libgnat/s-widthu.adb: Fix comments in the modular case.
* libgnat/s-widthu.ads: Add minimal postcondition.
* libgnat/s-widuns.ads: Disable ghost/contract.
Diffstat (limited to 'gcc')
-rw-r--r-- | gcc/ada/libgnat/s-widint.ads | 15 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widlli.ads | 15 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widllli.ads | 15 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widlllu.ads | 11 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widllu.ads | 11 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widthi.adb | 130 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widthi.ads | 7 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widthu.adb | 54 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widthu.ads | 7 | ||||
-rw-r--r-- | gcc/ada/libgnat/s-widuns.ads | 11 |
10 files changed, 253 insertions, 23 deletions
diff --git a/gcc/ada/libgnat/s-widint.ads b/gcc/ada/libgnat/s-widint.ads index f9b5eda..fb71618 100644 --- a/gcc/ada/libgnat/s-widint.ads +++ b/gcc/ada/libgnat/s-widint.ads @@ -31,9 +31,22 @@ -- Width attribute for signed integers up to Integer +-- 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); + with System.Width_I; -package System.Wid_Int is +package System.Wid_Int + with SPARK_Mode +is function Width_Integer is new Width_I (Integer); pragma Pure_Function (Width_Integer); diff --git a/gcc/ada/libgnat/s-widlli.ads b/gcc/ada/libgnat/s-widlli.ads index 708dbdc..07ff8bf 100644 --- a/gcc/ada/libgnat/s-widlli.ads +++ b/gcc/ada/libgnat/s-widlli.ads @@ -31,9 +31,22 @@ -- Width attribute for signed integers larger than Integer +-- 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); + with System.Width_I; -package System.Wid_LLI is +package System.Wid_LLI + with SPARK_Mode +is function Width_Long_Long_Integer is new Width_I (Long_Long_Integer); pragma Pure_Function (Width_Long_Long_Integer); diff --git a/gcc/ada/libgnat/s-widllli.ads b/gcc/ada/libgnat/s-widllli.ads index 82a7e3d..af35616 100644 --- a/gcc/ada/libgnat/s-widllli.ads +++ b/gcc/ada/libgnat/s-widllli.ads @@ -31,9 +31,22 @@ -- Width attribute for signed integers larger than Long_Long_Integer +-- 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); + with System.Width_I; -package System.Wid_LLLI is +package System.Wid_LLLI + with SPARK_Mode +is function Width_Long_Long_Long_Integer is new Width_I (Long_Long_Long_Integer); diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads index 10a0c9c..fd6534f 100644 --- a/gcc/ada/libgnat/s-widlllu.ads +++ b/gcc/ada/libgnat/s-widlllu.ads @@ -31,6 +31,17 @@ -- Width attribute for modular integers larger than Long_Long_Integer +-- 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); + with System.Width_U; with System.Unsigned_Types; diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads index 7eaf966..ce01285 100644 --- a/gcc/ada/libgnat/s-widllu.ads +++ b/gcc/ada/libgnat/s-widllu.ads @@ -31,6 +31,17 @@ -- Width attribute for modular integers larger than Integer +-- 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); + with System.Width_U; with System.Unsigned_Types; diff --git a/gcc/ada/libgnat/s-widthi.adb b/gcc/ada/libgnat/s-widthi.adb index 2f2d5e0..55a94ec 100644 --- a/gcc/ada/libgnat/s-widthi.adb +++ b/gcc/ada/libgnat/s-widthi.adb @@ -29,10 +29,109 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; + function System.Width_I (Lo, Hi : Int) return Natural 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); + + ----------------------- + -- Local Subprograms -- + ----------------------- + + package Signed_Conversion is new Signed_Conversions (Int => Int); + + function Big (Arg : Int) return Big_Integer renames + Signed_Conversion.To_Big_Integer; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Int'Base'Size is + when 8 => 2, + when 16 => 4, + when 32 => 9, + when 64 => 19, + when 128 => 38, + when others => raise Program_Error) + with Ghost; + + ------------------ + -- Local Lemmas -- + ------------------ + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) + with + Ghost, + Pre => A <= B, + Post => A * C <= B * C; + + procedure Lemma_Div_Commutation (X, Y : Int) + with + Ghost, + Pre => X >= 0 and Y > 0, + Post => Big (X) / Big (Y) = Big (X / Y); + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) + with + Ghost, + Post => X / Y / Z = X / (Y * Z); + + ---------------------- + -- Lemma_Lower_Mult -- + ---------------------- + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; + + --------------------------- + -- Lemma_Div_Commutation -- + --------------------------- + + procedure Lemma_Div_Commutation (X, Y : Int) is null; + + --------------------- + -- Lemma_Div_Twice -- + --------------------- + + procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is + XY : constant Big_Natural := X / Y; + YZ : constant Big_Natural := Y * Z; + XYZ : constant Big_Natural := X / Y / Z; + R : constant Big_Natural := (XY rem Z) * Y + (X rem Y); + begin + pragma Assert (X = XY * Y + (X rem Y)); + pragma Assert (XY = XY / Z * Z + (XY rem Z)); + pragma Assert (X = XYZ * YZ + R); + pragma Assert ((XY rem Z) * Y <= (Z - 1) * Y); + pragma Assert (R <= YZ - 1); + pragma Assert (X / YZ = (XYZ * YZ + R) / YZ); + pragma Assert (X / YZ = XYZ + R / YZ); + end Lemma_Div_Twice; + + -- Local variables + W : Natural; T : Int; + -- Local ghost variables + + Max_W : constant Natural := Max_Log10 with Ghost; + Big_10 : constant Big_Integer := Big (10) with Ghost; + + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Int := + Int'Max (abs (Int'Max (Lo, Int'First + 1)), + abs (Int'Max (Hi, Int'First + 1))) + with Ghost; + +-- Start of processing for System.Width_I + begin if Lo > Hi then return 0; @@ -52,10 +151,41 @@ begin -- Increase value if more digits required while T >= 10 loop + Lemma_Div_Commutation (T, 10); + Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + T := T / 10; W := W + 1; + Pow := Pow * 10; + + pragma Loop_Invariant (T >= 0); + pragma Loop_Invariant (W in 3 .. Max_W + 3); + pragma Loop_Invariant (Pow = Big_10 ** (W - 2)); + pragma Loop_Invariant (Big (T) = Big (T_Init) / Pow); + pragma Loop_Variant (Decreases => T); end loop; + declare + F : constant Big_Integer := Big_10 ** (W - 2) with Ghost; + Q : constant Big_Integer := Big (T_Init) / F with Ghost; + R : constant Big_Integer := Big (T_Init) rem F with Ghost; + begin + pragma Assert (Q < Big_10); + pragma Assert (Big (T_Init) = Q * F + R); + Lemma_Lower_Mult (Q, Big (9), F); + pragma Assert (Big (T_Init) <= Big (9) * F + F - 1); + pragma Assert (Big (T_Init) < Big_10 * F); + pragma Assert (Big_10 * F = Big_10 ** (W - 1)); + end; + + -- This is an expression of the functional postcondition for Width_I, + -- which cannot be expressed readily as a postcondition as this would + -- require making the instantiation Signed_Conversion and function Big + -- available from the spec. + + pragma Assert (Big (Int'Max (Lo, Int'First + 1)) < Big_10 ** (W - 1)); + pragma Assert (Big (Int'Max (Hi, Int'First + 1)) < Big_10 ** (W - 1)); + return W; end if; diff --git a/gcc/ada/libgnat/s-widthi.ads b/gcc/ada/libgnat/s-widthi.ads index 37865b89..44e448d 100644 --- a/gcc/ada/libgnat/s-widthi.ads +++ b/gcc/ada/libgnat/s-widthi.ads @@ -36,4 +36,9 @@ generic type Int is range <>; -function System.Width_I (Lo, Hi : Int) return Natural; +function System.Width_I (Lo, Hi : Int) return Natural +with + Post => (if Lo > Hi then + System.Width_I'Result = 0 + else + System.Width_I'Result > 0); diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index 79a0074..0be44ff 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -42,14 +42,14 @@ function System.Width_U (Lo, Hi : Uns) return Natural is Loop_Invariant => Ignore, Assert => Ignore); - W : Natural; - T : Uns; + ----------------------- + -- Local Subprograms -- + ----------------------- package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); - function Big (Arg : Uns) return Big_Integer is - (Unsigned_Conversion.To_Big_Integer (Arg)) - with Ghost; + function Big (Arg : Uns) return Big_Integer renames + Unsigned_Conversion.To_Big_Integer; -- Maximum value of exponent for 10 that fits in Uns'Base function Max_Log10 return Natural is @@ -62,8 +62,9 @@ function System.Width_U (Lo, Hi : Uns) return Natural is when others => raise Program_Error) with Ghost; - Max_W : constant Natural := Max_Log10 with Ghost; - Big_10 : constant Big_Integer := Big (10) with Ghost; + ------------------ + -- Local Lemmas -- + ------------------ procedure Lemma_Lower_Mult (A, B, C : Big_Natural) with @@ -82,15 +83,21 @@ function System.Width_U (Lo, Hi : Uns) return Natural is Ghost, Post => X / Y / Z = X / (Y * Z); - procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is - begin - null; - end Lemma_Lower_Mult; + ---------------------- + -- Lemma_Lower_Mult -- + ---------------------- - procedure Lemma_Div_Commutation (X, Y : Uns) is - begin - null; - end Lemma_Div_Commutation; + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is null; + + --------------------------- + -- Lemma_Div_Commutation -- + --------------------------- + + procedure Lemma_Div_Commutation (X, Y : Uns) is null; + + --------------------- + -- Lemma_Div_Twice -- + --------------------- procedure Lemma_Div_Twice (X : Big_Natural; Y, Z : Big_Positive) is XY : constant Big_Natural := X / Y; @@ -107,20 +114,31 @@ function System.Width_U (Lo, Hi : Uns) return Natural is pragma Assert (X / YZ = XYZ + R / YZ); end Lemma_Div_Twice; + -- Local variables + + W : Natural; + T : Uns; + + -- Local ghost variables + + Max_W : constant Natural := Max_Log10 with Ghost; + Big_10 : constant Big_Integer := Big (10) with Ghost; + Pow : Big_Integer := 1 with Ghost; T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; +-- Start of processing for System.Width_U + begin if Lo > Hi then return 0; else - -- Minimum value is 2, one for sign, one for digit + -- Minimum value is 2, one for space, one for digit W := 2; - -- Get max of absolute values, but avoid bomb if we have the maximum - -- negative number (note that First + 1 has same digits as First) + -- Get max of absolute values T := Uns'Max (Lo, Hi); diff --git a/gcc/ada/libgnat/s-widthu.ads b/gcc/ada/libgnat/s-widthu.ads index 7b71119..c70d7ae 100644 --- a/gcc/ada/libgnat/s-widthu.ads +++ b/gcc/ada/libgnat/s-widthu.ads @@ -36,4 +36,9 @@ generic type Uns is mod <>; -function System.Width_U (Lo, Hi : Uns) return Natural; +function System.Width_U (Lo, Hi : Uns) return Natural +with + Post => (if Lo > Hi then + System.Width_U'Result = 0 + else + System.Width_U'Result > 0); diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads index 713532e..f694470 100644 --- a/gcc/ada/libgnat/s-widuns.ads +++ b/gcc/ada/libgnat/s-widuns.ads @@ -31,6 +31,17 @@ -- Width attribute for modular integers up to Integer +-- 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); + with System.Width_U; with System.Unsigned_Types; |