diff options
Diffstat (limited to 'gcc/ada/libgnat/s-widthu.adb')
| -rw-r--r-- | gcc/ada/libgnat/s-widthu.adb | 263 |
1 files changed, 122 insertions, 141 deletions
diff --git a/gcc/ada/libgnat/s-widthu.adb b/gcc/ada/libgnat/s-widthu.adb index e23ecef..390942c 100644 --- a/gcc/ada/libgnat/s-widthu.adb +++ b/gcc/ada/libgnat/s-widthu.adb @@ -29,157 +29,138 @@ -- -- ------------------------------------------------------------------------------ -with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; -use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; - -function System.Width_U (Lo, Hi : Uns) return Natural is +package body System.Width_U 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 Unsigned_Conversion is new Unsigned_Conversions (Int => Uns); - - 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 - (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; - - ------------------ - -- 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 : 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); - - ---------------------- - -- Lemma_Lower_Mult -- - ---------------------- - - 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; - 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 : 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 space, one for digit - - W := 2; - - -- Get max of absolute values + pragma Assertion_Policy (Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore, + Assert_And_Cut => Ignore, + Subprogram_Variant => Ignore); + + function Width (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); + + ------------------ + -- 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 : 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); + + ---------------------- + -- Lemma_Lower_Mult -- + ---------------------- + + 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; + 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; - T := Uns'Max (Lo, Hi); + -- Local variables - -- Increase value if more digits required + W : Natural; + T : Uns; - while T >= 10 loop - Lemma_Div_Commutation (T, 10); - Lemma_Div_Twice (Big (T_Init), Big_10 ** (W - 2), Big_10); + -- Local ghost variables - T := T / 10; - W := W + 1; - Pow := Pow * 10; + Max_W : constant Natural := Max_Log10 with Ghost; + Pow : Big_Integer := 1 with Ghost; + T_Init : constant Uns := Uns'Max (Lo, Hi) with Ghost; - 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; + -- Start of processing for System.Width_U - 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; + begin + if Lo > Hi then + return 0; + + else + -- Minimum value is 2, one for space, one for digit + + W := 2; + + -- Get max of absolute values + + T := Uns'Max (Lo, Hi); + + -- 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 (W in 3 .. Max_W + 2); + 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; + + return W; + end if; + end Width; end System.Width_U; |