Similar to the contracts added for the 32bits and 64bits versions, add
corresponding contracts for the 128bits version. Proof is currently too
difficult for this instance of generic System.Arith_Double, as even with
a huge prover timeout of 15 minutes, 2 checks remain unproved.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-arit128.adb: Mark in SPARK.
* libgnat/s-arit128.ads: Add functional contracts.diff --git a/gcc/ada/libgnat/s-arit128.adb b/gcc/ada/libgnat/s-arit128.adb
--- a/gcc/ada/libgnat/s-arit128.adb
+++ b/gcc/ada/libgnat/s-arit128.adb
@@ -31,7 +31,9 @@
with System.Arith_Double;
-package body System.Arith_128 is
+package body System.Arith_128
+ with SPARK_Mode
+is
subtype Uns128 is Interfaces.Unsigned_128;
subtype Uns64 is Interfaces.Unsigned_64;
diff --git a/gcc/ada/libgnat/s-arit128.ads b/gcc/ada/libgnat/s-arit128.ads
--- a/gcc/ada/libgnat/s-arit128.ads
+++ b/gcc/ada/libgnat/s-arit128.ads
@@ -36,31 +36,102 @@
pragma Restrictions (No_Elaboration_Code);
-- Allow direct call from gigi generated code
+-- 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 Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
with Interfaces;
-package System.Arith_128 is
- pragma Pure;
+package System.Arith_128
+ with Pure, SPARK_Mode
+is
+ use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
+ use type Interfaces.Integer_128;
subtype Int128 is Interfaces.Integer_128;
- function Add_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+ 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 => Int128);
+
+ function Big (Arg : Int128) return Big_Integer is
+ (Signed_Conversion.To_Big_Integer (Arg))
+ with Ghost;
+
+ function In_Int128_Range (Arg : Big_Integer) return Boolean is
+ (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
+ (Arg, Big (Int128'First), Big (Int128'Last)))
+ with Ghost;
+
+ function Add_With_Ovflo_Check128 (X, Y : Int128) return Int128
+ with
+ Pre => In_Int128_Range (Big (X) + Big (Y)),
+ Post => Add_With_Ovflo_Check128'Result = X + Y;
-- Raises Constraint_Error if sum of operands overflows 128 bits,
-- otherwise returns the 128-bit signed integer sum.
- function Subtract_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+ function Subtract_With_Ovflo_Check128 (X, Y : Int128) return Int128
+ with
+ Pre => In_Int128_Range (Big (X) - Big (Y)),
+ Post => Subtract_With_Ovflo_Check128'Result = X - Y;
-- Raises Constraint_Error if difference of operands overflows 128
-- bits, otherwise returns the 128-bit signed integer difference.
- function Multiply_With_Ovflo_Check128 (X, Y : Int128) return Int128;
+ function Multiply_With_Ovflo_Check128 (X, Y : Int128) return Int128
+ with
+ Pre => In_Int128_Range (Big (X) * Big (Y)),
+ Post => Multiply_With_Ovflo_Check128'Result = X * Y;
pragma Export (C, Multiply_With_Ovflo_Check128, "__gnat_mulv128");
-- Raises Constraint_Error if product of operands overflows 128
-- bits, otherwise returns the 128-bit signed integer product.
-- Gigi may also call this routine directly.
+ function Same_Sign (X, Y : Big_Integer) return Boolean is
+ (X = Big (Int128'(0))
+ or else Y = Big (Int128'(0))
+ or else (X < Big (Int128'(0))) = (Y < Big (Int128'(0))))
+ with Ghost;
+
+ function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
+ (if abs R > (abs Y - Big (Int128'(1))) / Big (Int128'(2)) then
+ (if Same_Sign (X, Y) then Q + Big (Int128'(1))
+ else Q - Big (Int128'(1)))
+ else
+ Q)
+ with
+ Ghost,
+ Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+
procedure Scaled_Divide128
(X, Y, Z : Int128;
Q, R : out Int128;
- Round : Boolean);
+ Round : Boolean)
+ with
+ Pre => Z /= 0
+ and then In_Int128_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 128 bits. Round indicates if
@@ -72,7 +143,22 @@ package System.Arith_128 is
procedure Double_Divide128
(X, Y, Z : Int128;
Q, R : out Int128;
- Round : Boolean);
+ Round : Boolean)
+ with
+ Pre => Y /= 0
+ and then Z /= 0
+ and then In_Int128_Range
+ (if Round then Round_Quotient (Big (X), Big (Y) * Big (Z),
+ Big (X) / (Big (Y) * Big (Z)),
+ Big (X) rem (Big (Y) * Big (Z)))
+ else Big (X) / (Big (Y) * Big (Z))),
+ Post => Big (R) = Big (X) rem (Big (Y) * 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 X / (Y * Z), storing the quotient in Q and
-- the remainder in R. Constraint_Error is raised if Y or Z is zero,
-- or if the quotient does not fit in 128 bits. Round indicates if the
