public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-5745] [Ada] Proof of System.Arith_32 for double arithmetic on 32bits
@ 2021-12-02 16:30 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-12-02 16:30 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:b5e57389c511b645ce66581ab5aba5dff7ea831b
commit r12-5745-gb5e57389c511b645ce66581ab5aba5dff7ea831b
Author: Yannick Moy <moy@adacore.com>
Date: Thu Nov 25 15:35:39 2021 +0100
[Ada] Proof of System.Arith_32 for double arithmetic on 32bits
gcc/ada/
* libgnat/s-arit32.adb: Add ghost instances and lemmas.
(Scaled_Divide32): Add ghost code to prove. Minor code
modification to return early in error when divisor is zero.
* libgnat/s-arit32.ads: Add ghost instances and utilities.
(Scaled_Divide32): Add contract.
Diff:
---
gcc/ada/libgnat/s-arit32.adb | 449 +++++++++++++++++++++++++++++++++++++++++--
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 f9cd7fe74e6..ac6582fb61a 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 5dc197dd8ed..5163351075b 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
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-12-02 16:30 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-12-02 16:30 [gcc r12-5745] [Ada] Proof of System.Arith_32 for double arithmetic on 32bits Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).