| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- S Y S T E M . A R I T H _ 3 2 -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 2020-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| -- 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 |
| with SPARK_Mode |
| is |
| |
| pragma Suppress (Overflow_Check); |
| pragma Suppress (Range_Check); |
| |
| subtype Uns32 is Interfaces.Unsigned_32; |
| subtype Uns64 is Interfaces.Unsigned_64; |
| |
| use Interfaces; |
| |
| 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 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 |
| 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 |
| 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. |
| |
| procedure Raise_Error; |
| 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 -- |
| ----------------- |
| |
| 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; |
| |
| ------------------- |
| -- Scaled_Divide -- |
| ------------------- |
| |
| procedure Scaled_Divide32 |
| (X, Y, Z : Int32; |
| Q, R : out Int32; |
| Round : Boolean) |
| is |
| Xu : constant Uns32 := abs X; |
| Yu : constant Uns32 := abs Y; |
| Zu : constant Uns32 := abs Z; |
| |
| D : Uns64; |
| -- The dividend |
| |
| Qu : Uns32; |
| 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 |
| |
| 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 then |
| Prove_Rounding_Case; |
| |
| if Ru > (Zu - Uns32'(1)) / Uns32'(2) then |
| pragma Assert (abs Big_Q = Big (Qu) + 1); |
| |
| -- 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; |
| 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; |
| |
| ---------------- |
| -- To_Neg_Int -- |
| ---------------- |
| |
| function To_Neg_Int (A : Uns32) return Int32 is |
| R : constant Int32 := |
| (if A = 2**31 then Int32'First else -To_Int (A)); |
| -- Note that we can't just use the expression of the Else, because it |
| -- overflows for A = 2**31. |
| begin |
| if R <= 0 then |
| return R; |
| else |
| Raise_Error; |
| end if; |
| end To_Neg_Int; |
| |
| ---------------- |
| -- To_Pos_Int -- |
| ---------------- |
| |
| function To_Pos_Int (A : Uns32) return Int32 is |
| R : constant Int32 := To_Int (A); |
| begin |
| if R >= 0 then |
| return R; |
| else |
| Raise_Error; |
| end if; |
| end To_Pos_Int; |
| |
| end System.Arith_32; |
