FreeChainXenon/gcc
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

[Ada] Proof of System.Arith_32 for double arithmetic on 32bits

Browse source 
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.
This commit is contained in:
Yannick Moy 2021-11-25 15:35:39 +01:00 • committed by Pierre-Marie de Rodat
parent 544b30f81e
commit b5e57389c5
2 changed files with 500 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

449
gcc/ada/libgnat/s-arit32.adb
View file

@ -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;
-- Protect against wrapping around when rounding, by signaling
-- an overflow when the quotient is too large.
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;
Qu := Qu + Uns32'(1);
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;
----------------

70
gcc/ada/libgnat/s-arit32.ads
View file

@ -33,17 +33,79 @@
-- signed integer values in cases where either overflow checking is
-- required, or intermediate results are longer than 32 bits.
with Interfaces;
-- 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.
package System.Arith_32 is
pragma Pure;
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
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