From bd2560b726fa93b61060a9f469ad288c512961f3 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Mon, 30 Aug 2021 16:33:00 +0200 Subject: [PATCH] [Ada] Proof of the runtime support for attribute 'Width gcc/ada/ * libgnat/s-widlllu.ads: Mark in SPARK. * libgnat/s-widllu.ads: Likewise. * libgnat/s-widuns.ads: Likewise. * libgnat/s-widthu.adb: Add ghost code and a pseudo-postcondition. --- gcc/ada/libgnat/s-widlllu.ads | 5 +- gcc/ada/libgnat/s-widllu.ads | 5 +- gcc/ada/libgnat/s-widthu.adb | 107 ++++++++++++++++++++++++++++++++++ gcc/ada/libgnat/s-widuns.ads | 5 +- 4 files changed, 116 insertions(+), 6 deletions(-) diff --git a/gcc/ada/libgnat/s-widlllu.ads b/gcc/ada/libgnat/s-widlllu.ads index 018e740efb9..10a0c9c7f9b 100644 --- a/gcc/ada/libgnat/s-widlllu.ads +++ b/gcc/ada/libgnat/s-widlllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLLU is - +package System.Wid_LLLU + with SPARK_Mode +is subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned; function Width_Long_Long_Long_Unsigned is diff --git a/gcc/ada/libgnat/s-widllu.ads b/gcc/ada/libgnat/s-widllu.ads index ab7ec581e3b..7eaf966cbb7 100644 --- a/gcc/ada/libgnat/s-widllu.ads +++ b/gcc/ada/libgnat/s-widllu.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_LLU is - +package System.Wid_LLU + with SPARK_Mode +is subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned; function Width_Long_Long_Unsigned is new Width_U (Long_Long_Unsigned); diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index a91baec1601..e0e4d17b4d1 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,10 +29,87 @@ -- -- ------------------------------------------------------------------------------ +with Ada.Numerics.Big_Numbers.Big_Integers; +use Ada.Numerics.Big_Numbers.Big_Integers; + function System.Width_U (Lo, Hi : Uns) 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); + W : Natural; T : Uns; + 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; + + -- Maximum value of exponent for 10 that fits in Uns'Base + function Max_Log10 return Natural is + (case Uns'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; + + Max_W : constant Natural := Max_Log10 with Ghost; + Big_10 : constant Big_Integer := Big (10) with Ghost; + + 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 : Uns) + with + Ghost, + Pre => 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); + + procedure Lemma_Lower_Mult (A, B, C : Big_Natural) is + begin + null; + end Lemma_Lower_Mult; + + procedure Lemma_Div_Commutation (X, Y : Uns) is + begin + null; + end Lemma_Div_Commutation; + + 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; + + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; + begin if Lo > Hi then return 0; @@ -50,10 +127,40 @@ 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_Variant (Decreases => T); + 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); 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_U, + -- which cannot be expressed readily as a postcondition as this would + -- require making the instantiation Unsigned_Conversion and function + -- Big available from the spec. + + pragma Assert (Big (Lo) < Big_10 ** (W - 1)); + pragma Assert (Big (Hi) < Big_10 ** (W - 1)); + return W; end if; diff --git a/gcc/ada/libgnat/s-widuns.ads b/gcc/ada/libgnat/s-widuns.ads index 0528456406a..713532ed6d7 100644 --- a/gcc/ada/libgnat/s-widuns.ads +++ b/gcc/ada/libgnat/s-widuns.ads @@ -34,8 +34,9 @@ with System.Width_U; with System.Unsigned_Types; -package System.Wid_Uns is - +package System.Wid_Uns + with SPARK_Mode +is subtype Unsigned is Unsigned_Types.Unsigned; function Width_Unsigned is new Width_U (Unsigned);