diff options
Diffstat (limited to 'gcc')
| -rw-r--r-- | gcc/ada/libgnat/s-arit32.adb | 449 | ||||
| -rw-r--r-- | gcc/ada/libgnat/s-arit32.ads | 68 |
2 files changed, 499 insertions, 18 deletions
diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb index f9cd7fe..ac6582f 100644 --- a/gcc/ada/libgnat/s-arit32.adb +++ b/gcc/ada/libgnat/s-arit32.adb @@ -29,9 +29,24 @@ -- -- ------------------------------------------------------------------------------ +-- Preconditions, postconditions, 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 (Pre => Ignore, + Post => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore, + Assert => Ignore); + +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; +use Ada.Numerics.Big_Numbers.Big_Integers_Ghost; with Ada.Unchecked_Conversion; -package body System.Arith_32 is +package body System.Arith_32 + with SPARK_Mode +is pragma Suppress (Overflow_Check); pragma Suppress (Range_Check); @@ -43,27 +58,65 @@ package body System.Arith_32 is function To_Int is new Ada.Unchecked_Conversion (Uns32, Int32); + package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns32); + + function Big (Arg : Uns32) return Big_Integer is + (Unsigned_Conversion.To_Big_Integer (Arg)) + with Ghost; + + package Unsigned_Conversion_64 is new Unsigned_Conversions (Int => Uns64); + + function Big (Arg : Uns64) return Big_Integer is + (Unsigned_Conversion_64.To_Big_Integer (Arg)) + with Ghost; + + pragma Warnings + (Off, "non-preelaborable call not allowed in preelaborated unit", + Reason => "Ghost code is not compiled"); + Big_0 : constant Big_Integer := + Big (Uns32'(0)) + with Ghost; + Big_2xx32 : constant Big_Integer := + Big (Uns32'(2 ** 32 - 1)) + 1 + with Ghost; + Big_2xx64 : constant Big_Integer := + Big (Uns64'(2 ** 64 - 1)) + 1 + with Ghost; + pragma Warnings + (On, "non-preelaborable call not allowed in preelaborated unit"); + ----------------------- -- Local Subprograms -- ----------------------- function "abs" (X : Int32) return Uns32 is (if X = Int32'First - then 2**31 + then Uns32'(2**31) else Uns32 (Int32'(abs X))); -- Convert absolute value of X to unsigned. Note that we can't just use -- the expression of the Else since it overflows for X = Int32'First. + function Lo (A : Uns64) return Uns32 is (Uns32 (A and (2 ** 32 - 1))); + -- Low order half of 64-bit value + function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32))); -- High order half of 64-bit value - function To_Neg_Int (A : Uns32) return Int32; + function To_Neg_Int (A : Uns32) return Int32 + with + Annotate => (GNATprove, Terminating), + Pre => In_Int32_Range (-Big (A)), + Post => Big (To_Neg_Int'Result) = -Big (A); -- Convert to negative integer equivalent. If the input is in the range -- 0 .. 2**31, then the corresponding nonpositive signed integer (obtained -- by negating the given value) is returned, otherwise constraint error is -- raised. - function To_Pos_Int (A : Uns32) return Int32; + function To_Pos_Int (A : Uns32) return Int32 + with + Annotate => (GNATprove, Terminating), + Pre => In_Int32_Range (Big (A)), + Post => Big (To_Pos_Int'Result) = Big (A); -- Convert to positive integer equivalent. If the input is in the range -- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is -- returned, otherwise constraint error is raised. @@ -72,6 +125,168 @@ package body System.Arith_32 is pragma No_Return (Raise_Error); -- Raise constraint error with appropriate message + ------------------ + -- Local Lemmas -- + ------------------ + + procedure Lemma_Abs_Commutation (X : Int32) + with + Ghost, + Post => abs (Big (X)) = Big (Uns32'(abs X)); + + procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) + with + Ghost, + Pre => Y /= 0, + Post => abs (X / Y) = abs X / abs Y; + + procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) + with + Ghost, + Post => abs (X * Y) = abs X * abs Y; + + procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) + with + Ghost, + Pre => Y /= 0, + Post => abs (X rem Y) = (abs X) rem (abs Y); + + procedure Lemma_Div_Commutation (X, Y : Uns64) + with + Ghost, + Pre => Y /= 0, + Post => Big (X) / Big (Y) = Big (X / Y); + + procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) + with + Ghost, + Pre => Z > 0 and then X >= Y * Z, + Post => X / Z >= Y; + + procedure Lemma_Ge_Commutation (A, B : Uns32) + with + Ghost, + Pre => A >= B, + Post => Big (A) >= Big (B); + + procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32) + with + Ghost, + Pre => Xhi = Hi (Xu) and Xlo = Lo (Xu), + Post => Big (Xu) = Big_2xx32 * Big (Xhi) + Big (Xlo); + + procedure Lemma_Mult_Commutation (X, Y, Z : Uns64) + with + Ghost, + Pre => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y, + Post => Big (X) * Big (Y) = Big (Z); + + procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) + with + Ghost, + Pre => (X >= Big_0 and then Y >= Big_0) + or else (X <= Big_0 and then Y <= Big_0), + Post => X * Y >= Big_0; + + procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) + with + Ghost, + Pre => (X <= Big_0 and then Y >= Big_0) + or else (X >= Big_0 and then Y <= Big_0), + Post => X * Y <= Big_0; + + procedure Lemma_Neg_Div (X, Y : Big_Integer) + with + Ghost, + Pre => Y /= 0, + Post => X / Y = (-X) / (-Y); + + procedure Lemma_Neg_Rem (X, Y : Big_Integer) + with + Ghost, + Pre => Y /= 0, + Post => X rem Y = X rem (-Y); + + procedure Lemma_Not_In_Range_Big2xx32 + with + Post => not In_Int32_Range (Big_2xx32) + and then not In_Int32_Range (-Big_2xx32); + + procedure Lemma_Rem_Commutation (X, Y : Uns64) + with + Ghost, + Pre => Y /= 0, + Post => Big (X) rem Big (Y) = Big (X rem Y); + + ----------------------------- + -- Local lemma null bodies -- + ----------------------------- + + procedure Lemma_Abs_Commutation (X : Int32) is null; + procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null; + procedure Lemma_Div_Commutation (X, Y : Uns64) is null; + procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null; + procedure Lemma_Ge_Commutation (A, B : Uns32) is null; + procedure Lemma_Mult_Commutation (X, Y, Z : Uns64) is null; + procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null; + procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null; + procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null; + procedure Lemma_Not_In_Range_Big2xx32 is null; + procedure Lemma_Rem_Commutation (X, Y : Uns64) is null; + + ------------------------------- + -- Lemma_Abs_Div_Commutation -- + ------------------------------- + + procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is + begin + if Y < 0 then + if X < 0 then + pragma Assert (abs (X / Y) = abs (X / (-Y))); + else + Lemma_Neg_Div (X, Y); + pragma Assert (abs (X / Y) = abs ((-X) / (-Y))); + end if; + end if; + end Lemma_Abs_Div_Commutation; + + ------------------------------- + -- Lemma_Abs_Rem_Commutation -- + ------------------------------- + + procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) is + begin + if Y < 0 then + Lemma_Neg_Rem (X, Y); + if X < 0 then + pragma Assert (X rem Y = -((-X) rem (-Y))); + pragma Assert (abs (X rem Y) = (abs X) rem (abs Y)); + else + pragma Assert (abs (X rem Y) = (abs X) rem (abs Y)); + end if; + end if; + end Lemma_Abs_Rem_Commutation; + + ----------------- + -- Lemma_Hi_Lo -- + ----------------- + + procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32) is + begin + pragma Assert (Uns64 (Xhi) = Xu / Uns64'(2 ** 32)); + pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32); + end Lemma_Hi_Lo; + + ------------------- + -- Lemma_Neg_Div -- + ------------------- + + procedure Lemma_Neg_Div (X, Y : Big_Integer) is + begin + pragma Assert ((-X) / (-Y) = -(X / (-Y))); + pragma Assert (X / (-Y) = -(X / Y)); + end Lemma_Neg_Div; + ----------------- -- Raise_Error -- ----------------- @@ -79,6 +294,9 @@ package body System.Arith_32 is procedure Raise_Error is begin raise Constraint_Error with "32-bit arithmetic overflow"; + pragma Annotate + (GNATprove, Intentional, "exception might be raised", + "Procedure Raise_Error is called to signal input errors"); end Raise_Error; ------------------- @@ -101,51 +319,252 @@ package body System.Arith_32 is Ru : Uns32; -- Unsigned quotient and remainder + -- Local ghost variables + + Mult : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost; + Quot : Big_Integer with Ghost; + Big_R : Big_Integer with Ghost; + Big_Q : Big_Integer with Ghost; + + -- Local lemmas + + procedure Prove_Negative_Dividend + with + Ghost, + Pre => Z /= 0 + and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0)) + and then Big_Q = + (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), + Big (X) * Big (Y) rem Big (Z)) + else Big (X) * Big (Y) / Big (Z)), + Post => + (if Z > 0 then Big_Q <= Big_0 else Big_Q >= Big_0); + -- Proves the sign of rounded quotient when dividend is non-positive + + procedure Prove_Overflow + with + Ghost, + Pre => Z /= 0 and then Mult >= Big_2xx32 * Big (Uns32'(abs Z)), + Post => not In_Int32_Range (Big (X) * Big (Y) / Big (Z)) + and then not In_Int32_Range + (Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), + Big (X) * Big (Y) rem Big (Z))); + -- Proves overflow case + + procedure Prove_Positive_Dividend + with + Ghost, + Pre => Z /= 0 + and then ((X >= 0 and Y >= 0) or (X < 0 and Y < 0)) + and then Big_Q = + (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), + Big (X) * Big (Y) rem Big (Z)) + else Big (X) * Big (Y) / Big (Z)), + Post => + (if Z > 0 then Big_Q >= Big_0 else Big_Q <= Big_0); + -- Proves the sign of rounded quotient when dividend is non-negative + + procedure Prove_Rounding_Case + with + Ghost, + Pre => Z /= 0 + and then Quot = Big (X) * Big (Y) / Big (Z) + and then Big_R = Big (X) * Big (Y) rem Big (Z) + and then Big_Q = + Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R) + and then Big (Ru) = abs Big_R + and then Big (Zu) = Big (Uns32'(abs Z)), + Post => abs Big_Q = + (if Ru > (Zu - Uns32'(1)) / Uns32'(2) + then abs Quot + 1 + else abs Quot); + -- Proves correctness of the rounding of the unsigned quotient + + procedure Prove_Sign_R + with + Ghost, + Pre => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z), + Post => In_Int32_Range (Big_R); + + procedure Prove_Signs + with + Ghost, + Pre => Z /= 0 + and then Quot = Big (X) * Big (Y) / Big (Z) + and then Big_R = Big (X) * Big (Y) rem Big (Z) + and then Big_Q = + (if Round then + Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R) + else Quot) + and then Big (Ru) = abs Big_R + and then Big (Qu) = abs Big_Q + and then In_Int32_Range (Big_Q) + and then In_Int32_Range (Big_R) + and then R = + (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru)) + and then Q = + (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu) + else To_Neg_Int (Qu)), -- need to ensure To_Pos_Int precondition + Post => Big (R) = Big_R and then Big (Q) = Big_Q; + -- Proves final signs match the intended result after the unsigned + -- division is done. + + ----------------------------- + -- Prove_Negative_Dividend -- + ----------------------------- + + procedure Prove_Negative_Dividend is + begin + Lemma_Mult_Non_Positive (Big (X), Big (Y)); + end Prove_Negative_Dividend; + + -------------------- + -- Prove_Overflow -- + -------------------- + + procedure Prove_Overflow is + begin + Lemma_Div_Ge (Mult, Big_2xx32, Big (Uns32'(abs Z))); + Lemma_Abs_Commutation (Z); + Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z)); + end Prove_Overflow; + + ----------------------------- + -- Prove_Positive_Dividend -- + ----------------------------- + + procedure Prove_Positive_Dividend is + begin + Lemma_Mult_Non_Negative (Big (X), Big (Y)); + end Prove_Positive_Dividend; + + ------------------------- + -- Prove_Rounding_Case -- + ------------------------- + + procedure Prove_Rounding_Case is + begin + if Same_Sign (Big (X) * Big (Y), Big (Z)) then + null; + end if; + end Prove_Rounding_Case; + + ------------------ + -- Prove_Sign_R -- + ------------------ + + procedure Prove_Sign_R is + begin + pragma Assert (In_Int32_Range (Big (Z))); + end Prove_Sign_R; + + ----------------- + -- Prove_Signs -- + ----------------- + + procedure Prove_Signs is null; + + -- Start of processing for Scaled_Divide32 + begin -- First do the 64-bit multiplication D := Uns64 (Xu) * Uns64 (Yu); + pragma Assert (Mult = Big (D)); + Lemma_Hi_Lo (D, Hi (D), Lo (D)); + pragma Assert (Mult = Big_2xx32 * Big (Hi (D)) + Big (Lo (D))); + + -- If divisor is zero, raise error + + if Z = 0 then + Raise_Error; + end if; + + Quot := Big (X) * Big (Y) / Big (Z); + Big_R := Big (X) * Big (Y) rem Big (Z); + if Round then + Big_Q := Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R); + else + Big_Q := Quot; + end if; + -- If dividend is too large, raise error if Hi (D) >= Zu then + Lemma_Ge_Commutation (Hi (D), Zu); + pragma Assert (Mult >= Big_2xx32 * Big (Zu)); + Prove_Overflow; Raise_Error; + end if; -- Then do the 64-bit division - else - Qu := Uns32 (D / Uns64 (Zu)); - Ru := Uns32 (D rem Uns64 (Zu)); - end if; + Qu := Uns32 (D / Uns64 (Zu)); + Ru := Uns32 (D rem Uns64 (Zu)); + + Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z)); + Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z)); + Lemma_Abs_Mult_Commutation (Big (X), Big (Y)); + Lemma_Abs_Commutation (X); + Lemma_Abs_Commutation (Y); + Lemma_Abs_Commutation (Z); + Lemma_Mult_Commutation (Uns64 (Xu), Uns64 (Yu), D); + Lemma_Div_Commutation (D, Uns64 (Zu)); + Lemma_Rem_Commutation (D, Uns64 (Zu)); + + pragma Assert (Big (Ru) = abs Big_R); + pragma Assert (Big (Qu) = abs Quot); + pragma Assert (Big (Zu) = Big (Uns32'(abs Z))); -- Deal with rounding case - if Round and then Ru > (Zu - Uns32'(1)) / Uns32'(2) then + if Round then + Prove_Rounding_Case; - -- Protect against wrapping around when rounding, by signaling - -- an overflow when the quotient is too large. + if Ru > (Zu - Uns32'(1)) / Uns32'(2) then + pragma Assert (abs Big_Q = Big (Qu) + 1); - if Qu = Uns32'Last then - Raise_Error; - end if; + -- Protect against wrapping around when rounding, by signaling + -- an overflow when the quotient is too large. - Qu := Qu + Uns32'(1); + if Qu = Uns32'Last then + pragma Assert (abs Big_Q = Big_2xx32); + Lemma_Not_In_Range_Big2xx32; + Raise_Error; + end if; + + Qu := Qu + Uns32'(1); + end if; end if; + pragma Assert (Big (Qu) = abs Big_Q); + pragma Assert (Big (Ru) = abs Big_R); + -- Set final signs (RM 4.5.5(27-30)) -- Case of dividend (X * Y) sign positive if (X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0) then + Prove_Positive_Dividend; + R := To_Pos_Int (Ru); Q := (if Z > 0 then To_Pos_Int (Qu) else To_Neg_Int (Qu)); -- Case of dividend (X * Y) sign negative else + Prove_Negative_Dividend; + R := To_Neg_Int (Ru); Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu)); end if; + + Prove_Sign_R; + Prove_Signs; end Scaled_Divide32; ---------------- diff --git a/gcc/ada/libgnat/s-arit32.ads b/gcc/ada/libgnat/s-arit32.ads index 5dc197d..5163351 100644 --- a/gcc/ada/libgnat/s-arit32.ads +++ b/gcc/ada/libgnat/s-arit32.ads @@ -33,17 +33,79 @@ -- signed integer values in cases where either overflow checking is -- required, or intermediate results are longer than 32 bits. +-- 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 Interfaces; +with Ada.Numerics.Big_Numbers.Big_Integers_Ghost; -package System.Arith_32 is - pragma Pure; +package System.Arith_32 + with Pure, SPARK_Mode +is + use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer; + use type Interfaces.Integer_32; subtype Int32 is Interfaces.Integer_32; + subtype Big_Integer is + Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer + with Ghost; + + package Signed_Conversion is new + Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions + (Int => Int32); + + function Big (Arg : Int32) return Big_Integer is + (Signed_Conversion.To_Big_Integer (Arg)) + with Ghost; + + function In_Int32_Range (Arg : Big_Integer) return Boolean is + (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range + (Arg, Big (Int32'First), Big (Int32'Last))) + with Ghost; + + function Same_Sign (X, Y : Big_Integer) return Boolean is + (X = Big (Int32'(0)) + or else Y = Big (Int32'(0)) + or else (X < Big (Int32'(0))) = (Y < Big (Int32'(0)))) + with Ghost; + + function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is + (if abs R > (abs Y - Big (Int32'(1))) / Big (Int32'(2)) then + (if Same_Sign (X, Y) then Q + Big (Int32'(1)) + else Q - Big (Int32'(1))) + else + Q) + with + Ghost, + Pre => Y /= 0 and then Q = X / Y and then R = X rem Y; + procedure Scaled_Divide32 (X, Y, Z : Int32; Q, R : out Int32; - Round : Boolean); + Round : Boolean) + with + Pre => Z /= 0 + and then In_Int32_Range + (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), + Big (X) * Big (Y) rem Big (Z)) + else Big (X) * Big (Y) / Big (Z)), + Post => Big (R) = Big (X) * Big (Y) rem Big (Z) + and then + (if Round then + Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z), + Big (X) * Big (Y) / Big (Z), Big (R)) + else + Big (Q) = Big (X) * Big (Y) / Big (Z)); -- Performs the division of (X * Y) / Z, storing the quotient in Q -- and the remainder in R. Constraint_Error is raised if Z is zero, -- or if the quotient does not fit in 32 bits. Round indicates if |