OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Prove double precision integer arithmetic unit

Browse Source 
gcc/ada/

	* libgnat/a-nbnbig.ads: Mark the unit as Pure.
	* libgnat/s-aridou.adb: Add contracts and ghost code for proof.
	(Scaled_Divide): Reorder operations and use of temporaries in
	two places to facilitate proof.
	* libgnat/s-aridou.ads: Add full functional contracts.
	* libgnat/s-arit64.adb: Mark in SPARK.
	* libgnat/s-arit64.ads: Add contracts similar to those from
	s-aridou.ads.
	* rtsfind.ads: Document the limitation that runtime units
	loading does not work for private with-clauses.
This commit is contained in:
Pierre-Alexandre Bazin 2021-11-04 10:48:46 +01:00 committed by Pierre-Marie de Rodat
parent 99f8a65368
commit bbe3c88351
6 changed files with 2507 additions and 105 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
gcc/ada/libgnat/a-nbnbig.ads
View File

@ -30,7 +30,7 @@ pragma Assertion_Policy (Ghost => Ignore);
package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with
SPARK_Mode,
Ghost,
Preelaborate
Pure
is
type Big_Integer is private
with Integer_Literal => From_Universal_Image;

2401
gcc/ada/libgnat/s-aridou.adb
View File

File diff suppressed because it is too large Load Diff

98
gcc/ada/libgnat/s-aridou.ads
View File

@ -33,6 +33,9 @@
-- signed integer values in cases where either overflow checking is required,
-- or intermediate results are longer than the result type.
with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
generic
type Double_Int is range <>;
@ -50,27 +53,93 @@ generic
with function Shift_Left (A : Single_Uns; B : Natural) return Single_Uns
is <>;
package System.Arith_Double is
pragma Pure;
package System.Arith_Double
with Pure, SPARK_Mode
is
-- 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.
function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int;
pragma Assertion_Policy (Pre => Ignore,
Post => Ignore,
Contract_Cases => Ignore,
Ghost => Ignore);
package Signed_Conversion is new Signed_Conversions (Int => Double_Int);
function Big (Arg : Double_Int) return Big_Integer is
(Signed_Conversion.To_Big_Integer (Arg))
with Ghost;
package Unsigned_Conversion is new Unsigned_Conversions (Int => Double_Uns);
function Big (Arg : Double_Uns) return Big_Integer is
(Unsigned_Conversion.To_Big_Integer (Arg))
with Ghost;
function In_Double_Int_Range (Arg : Big_Integer) return Boolean is
(In_Range (Arg, Big (Double_Int'First), Big (Double_Int'Last)))
with Ghost;
function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int
with
Pre => In_Double_Int_Range (Big (X) + Big (Y)),
Post => Add_With_Ovflo_Check'Result = X + Y;
-- Raises Constraint_Error if sum of operands overflows Double_Int,
-- otherwise returns the signed integer sum.
function Subtract_With_Ovflo_Check (X, Y : Double_Int) return Double_Int;
function Subtract_With_Ovflo_Check (X, Y : Double_Int) return Double_Int
with
Pre => In_Double_Int_Range (Big (X) - Big (Y)),
Post => Subtract_With_Ovflo_Check'Result = X - Y;
-- Raises Constraint_Error if difference of operands overflows Double_Int,
-- otherwise returns the signed integer difference.
function Multiply_With_Ovflo_Check (X, Y : Double_Int) return Double_Int;
function Multiply_With_Ovflo_Check (X, Y : Double_Int) return Double_Int
with
Pre => In_Double_Int_Range (Big (X) * Big (Y)),
Post => Multiply_With_Ovflo_Check'Result = X * Y;
pragma Convention (C, Multiply_With_Ovflo_Check);
-- Raises Constraint_Error if product of operands overflows Double_Int,
-- otherwise returns the signed integer product. Gigi may also call this
-- routine directly.
function Same_Sign (X, Y : Big_Integer) return Boolean is
(X = Big (Double_Int'(0))
or else Y = Big (Double_Int'(0))
or else (X < Big (Double_Int'(0))) = (Y < Big (Double_Int'(0))))
with Ghost;
function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
(if abs R > (abs Y - Big (Double_Int'(1))) / Big (Double_Int'(2)) then
(if Same_Sign (X, Y) then Q + Big (Double_Int'(1))
else Q - Big (Double_Int'(1)))
else
Q)
with
Ghost,
Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
procedure Scaled_Divide
(X, Y, Z : Double_Int;
Q, R : out Double_Int;
Round : Boolean);
Round : Boolean)
with
Pre => Z /= 0
and then In_Double_Int_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 Double_Int. Round indicates if
@ -82,7 +151,22 @@ package System.Arith_Double is
procedure Double_Divide
(X, Y, Z : Double_Int;
Q, R : out Double_Int;
Round : Boolean);
Round : Boolean)
with
Pre => Y /= 0
and then Z /= 0
and then In_Double_Int_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 Double_Int. Round indicates if the

4
gcc/ada/libgnat/s-arit64.adb
View File

@ -31,7 +31,9 @@
with System.Arith_Double;
package body System.Arith_64 is
package body System.Arith_64
with SPARK_Mode
is
subtype Uns64 is Interfaces.Unsigned_64;
subtype Uns32 is Interfaces.Unsigned_32;

101
gcc/ada/libgnat/s-arit64.ads
View File

@ -36,31 +36,103 @@
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_64 is
pragma Pure;
package System.Arith_64
with Pure, SPARK_Mode
is
use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
use type Interfaces.Integer_64;
subtype Int64 is Interfaces.Integer_64;
function Add_With_Ovflo_Check64 (X, Y : Int64) return Int64;
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 => Int64);
function Big (Arg : Int64) return Big_Integer is
(Signed_Conversion.To_Big_Integer (Arg))
with Ghost;
function In_Int64_Range (Arg : Big_Integer) return Boolean is
(Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
(Arg, Big (Int64'First), Big (Int64'Last)))
with Ghost;
function Add_With_Ovflo_Check64 (X, Y : Int64) return Int64
with
Pre => In_Int64_Range (Big (X) + Big (Y)),
Post => Add_With_Ovflo_Check64'Result = X + Y;
-- Raises Constraint_Error if sum of operands overflows 64 bits,
-- otherwise returns the 64-bit signed integer sum.
function Subtract_With_Ovflo_Check64 (X, Y : Int64) return Int64;
function Subtract_With_Ovflo_Check64 (X, Y : Int64) return Int64
with
Pre => In_Int64_Range (Big (X) - Big (Y)),
Post => Subtract_With_Ovflo_Check64'Result = X - Y;
-- Raises Constraint_Error if difference of operands overflows 64
-- bits, otherwise returns the 64-bit signed integer difference.
function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64;
function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64
with
Pure_Function,
Pre => In_Int64_Range (Big (X) * Big (Y)),
Post => Multiply_With_Ovflo_Check64'Result = X * Y;
pragma Export (C, Multiply_With_Ovflo_Check64, "__gnat_mulv64");
-- Raises Constraint_Error if product of operands overflows 64
-- bits, otherwise returns the 64-bit signed integer product.
-- Gigi may also call this routine directly.
function Same_Sign (X, Y : Big_Integer) return Boolean is
(X = Big (Int64'(0))
or else Y = Big (Int64'(0))
or else (X < Big (Int64'(0))) = (Y < Big (Int64'(0))))
with Ghost;
function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
(if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
(if Same_Sign (X, Y) then Q + Big (Int64'(1))
else Q - Big (Int64'(1)))
else
Q)
with
Ghost,
Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
procedure Scaled_Divide64
(X, Y, Z : Int64;
Q, R : out Int64;
Round : Boolean);
Round : Boolean)
with
Pre => Z /= 0
and then In_Int64_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 64 bits. Round indicates if
@ -78,7 +150,22 @@ package System.Arith_64 is
procedure Double_Divide64
(X, Y, Z : Int64;
Q, R : out Int64;
Round : Boolean);
Round : Boolean)
with
Pre => Y /= 0
and then Z /= 0
and then In_Int64_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 64 bits. Round indicates if the

6
gcc/ada/rtsfind.ads
View File

@ -60,6 +60,12 @@ package Rtsfind is
-- the compilation except in the presence of use clauses, which might
-- result in unexpected ambiguities.
-- IMPORTANT NOTE: the specs of packages and procedures with'ed using
-- this mechanism must not contain private with clauses. This is because
-- the special context installation/removal for private with clauses
-- only works in a clean environment for compilation, and could lead
-- here to removing visibility over lib units in the calling context.
-- NOTE: If RTU_Id is modified, the subtypes of RTU_Id in the package body
-- might need to be modified. See Get_Unit_Name.