1 ------------------------------------------------------------------------------
3 -- GNAT RUN-TIME COMPONENTS --
5 -- S Y S T E M . A R I T H _ 3 2 --
9 -- Copyright (C) 2020-2024, Free Software Foundation, Inc. --
11 -- GNAT is free software; you can redistribute it and/or modify it under --
12 -- terms of the GNU General Public License as published by the Free Soft- --
13 -- ware Foundation; either version 3, or (at your option) any later ver- --
14 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
15 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
16 -- or FITNESS FOR A PARTICULAR PURPOSE. --
18 -- As a special exception under Section 7 of GPL version 3, you are granted --
19 -- additional permissions described in the GCC Runtime Library Exception, --
20 -- version 3.1, as published by the Free Software Foundation. --
22 -- You should have received a copy of the GNU General Public License and --
23 -- a copy of the GCC Runtime Library Exception along with this program; --
24 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
25 -- <http://www.gnu.org/licenses/>. --
27 -- GNAT was originally developed by the GNAT team at New York University. --
28 -- Extensive contributions were provided by Ada Core Technologies Inc. --
30 ------------------------------------------------------------------------------
32 -- Preconditions, postconditions, ghost code, loop invariants and assertions
33 -- in this unit are meant for analysis only, not for run-time checking, as it
34 -- would be too costly otherwise. This is enforced by setting the assertion
37 pragma Assertion_Policy
(Pre
=> Ignore
,
40 Loop_Invariant
=> Ignore
,
43 with Ada
.Numerics
.Big_Numbers
.Big_Integers_Ghost
;
44 use Ada
.Numerics
.Big_Numbers
.Big_Integers_Ghost
;
45 with Ada
.Unchecked_Conversion
;
47 package body System
.Arith_32
51 pragma Suppress
(Overflow_Check
);
52 pragma Suppress
(Range_Check
);
54 subtype Uns32
is Interfaces
.Unsigned_32
;
55 subtype Uns64
is Interfaces
.Unsigned_64
;
59 function To_Int
is new Ada
.Unchecked_Conversion
(Uns32
, Int32
);
61 package Unsigned_Conversion
is new Unsigned_Conversions
(Int
=> Uns32
);
63 function Big
(Arg
: Uns32
) return Big_Integer
is
64 (Unsigned_Conversion
.To_Big_Integer
(Arg
))
67 package Unsigned_Conversion_64
is new Unsigned_Conversions
(Int
=> Uns64
);
69 function Big
(Arg
: Uns64
) return Big_Integer
is
70 (Unsigned_Conversion_64
.To_Big_Integer
(Arg
))
74 (Off
, "non-preelaborable call not allowed in preelaborated unit",
75 Reason
=> "Ghost code is not compiled");
76 Big_0
: constant Big_Integer
:=
79 Big_2xx32 : constant Big_Integer :=
80 Big (Uns32'(2 ** 32 - 1)) + 1
82 Big_2xx64
: constant Big_Integer
:=
83 Big
(Uns64
'(2 ** 64 - 1)) + 1
86 (On, "non-preelaborable call not allowed in preelaborated unit");
88 -----------------------
89 -- Local Subprograms --
90 -----------------------
92 function "abs" (X : Int32) return Uns32 is
95 else Uns32
(Int32
'(abs X)));
96 -- Convert absolute value of X to unsigned. Note that we can't just use
97 -- the expression of the Else since it overflows for X = Int32'First.
99 function Lo (A : Uns64) return Uns32 is (Uns32 (A and (2 ** 32 - 1)));
100 -- Low order half of 64-bit value
102 function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32)));
103 -- High order half of 64-bit value
105 function To_Neg_Int (A : Uns32) return Int32
107 Pre => In_Int32_Range (-Big (A)),
108 Post => Big (To_Neg_Int'Result) = -Big (A);
109 -- Convert to negative integer equivalent. If the input is in the range
110 -- 0 .. 2**31, then the corresponding nonpositive signed integer (obtained
111 -- by negating the given value) is returned, otherwise constraint error is
114 function To_Pos_Int (A : Uns32) return Int32
116 Pre => In_Int32_Range (Big (A)),
117 Post => Big (To_Pos_Int'Result) = Big (A);
118 -- Convert to positive integer equivalent. If the input is in the range
119 -- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
120 -- returned, otherwise constraint error is raised.
122 procedure Raise_Error;
123 pragma No_Return (Raise_Error);
124 -- Raise constraint error with appropriate message
130 procedure Lemma_Abs_Commutation (X : Int32)
133 Post => abs (Big (X)) = Big (Uns32'(abs X
));
135 procedure Lemma_Abs_Div_Commutation
(X
, Y
: Big_Integer
)
139 Post
=> abs (X
/ Y
) = abs X
/ abs Y
;
141 procedure Lemma_Abs_Mult_Commutation
(X
, Y
: Big_Integer
)
144 Post
=> abs (X
* Y
) = abs X
* abs Y
;
146 procedure Lemma_Abs_Rem_Commutation
(X
, Y
: Big_Integer
)
150 Post
=> abs (X
rem Y
) = (abs X
) rem (abs Y
);
152 procedure Lemma_Div_Commutation
(X
, Y
: Uns64
)
156 Post
=> Big
(X
) / Big
(Y
) = Big
(X
/ Y
);
158 procedure Lemma_Div_Ge
(X
, Y
, Z
: Big_Integer
)
161 Pre
=> Z
> 0 and then X
>= Y
* Z
,
164 procedure Lemma_Ge_Commutation
(A
, B
: Uns32
)
168 Post
=> Big
(A
) >= Big
(B
);
170 procedure Lemma_Hi_Lo
(Xu
: Uns64
; Xhi
, Xlo
: Uns32
)
173 Pre
=> Xhi
= Hi
(Xu
) and Xlo
= Lo
(Xu
),
174 Post
=> Big
(Xu
) = Big_2xx32
* Big
(Xhi
) + Big
(Xlo
);
176 procedure Lemma_Mult_Commutation
(X
, Y
, Z
: Uns64
)
179 Pre
=> Big
(X
) * Big
(Y
) < Big_2xx64
and then Z
= X
* Y
,
180 Post
=> Big
(X
) * Big
(Y
) = Big
(Z
);
182 procedure Lemma_Mult_Non_Negative
(X
, Y
: Big_Integer
)
185 Pre
=> (X
>= Big_0
and then Y
>= Big_0
)
186 or else (X
<= Big_0
and then Y
<= Big_0
),
187 Post
=> X
* Y
>= Big_0
;
189 procedure Lemma_Mult_Non_Positive
(X
, Y
: Big_Integer
)
192 Pre
=> (X
<= Big_0
and then Y
>= Big_0
)
193 or else (X
>= Big_0
and then Y
<= Big_0
),
194 Post
=> X
* Y
<= Big_0
;
196 procedure Lemma_Neg_Rem
(X
, Y
: Big_Integer
)
200 Post
=> X
rem Y
= X
rem (-Y
);
202 procedure Lemma_Not_In_Range_Big2xx32
204 Post
=> not In_Int32_Range
(Big_2xx32
)
205 and then not In_Int32_Range
(-Big_2xx32
);
207 procedure Lemma_Rem_Commutation
(X
, Y
: Uns64
)
211 Post
=> Big
(X
) rem Big
(Y
) = Big
(X
rem Y
);
213 -----------------------------
214 -- Local lemma null bodies --
215 -----------------------------
217 procedure Lemma_Abs_Commutation
(X
: Int32
) is null;
218 procedure Lemma_Abs_Div_Commutation
(X
, Y
: Big_Integer
) is null;
219 procedure Lemma_Abs_Mult_Commutation
(X
, Y
: Big_Integer
) is null;
220 procedure Lemma_Div_Commutation
(X
, Y
: Uns64
) is null;
221 procedure Lemma_Div_Ge
(X
, Y
, Z
: Big_Integer
) is null;
222 procedure Lemma_Ge_Commutation
(A
, B
: Uns32
) is null;
223 procedure Lemma_Mult_Commutation
(X
, Y
, Z
: Uns64
) is null;
224 procedure Lemma_Mult_Non_Negative
(X
, Y
: Big_Integer
) is null;
225 procedure Lemma_Mult_Non_Positive
(X
, Y
: Big_Integer
) is null;
226 procedure Lemma_Neg_Rem
(X
, Y
: Big_Integer
) is null;
227 procedure Lemma_Not_In_Range_Big2xx32
is null;
228 procedure Lemma_Rem_Commutation
(X
, Y
: Uns64
) is null;
230 -------------------------------
231 -- Lemma_Abs_Rem_Commutation --
232 -------------------------------
234 procedure Lemma_Abs_Rem_Commutation
(X
, Y
: Big_Integer
) is
237 Lemma_Neg_Rem
(X
, Y
);
239 pragma Assert
(X
rem Y
= -((-X
) rem (-Y
)));
240 pragma Assert
(abs (X
rem Y
) = (abs X
) rem (abs Y
));
242 pragma Assert
(abs (X
rem Y
) = (abs X
) rem (abs Y
));
245 end Lemma_Abs_Rem_Commutation
;
251 procedure Lemma_Hi_Lo
(Xu
: Uns64
; Xhi
, Xlo
: Uns32
) is
253 pragma Assert
(Uns64
(Xhi
) = Xu
/ Uns64
'(2 ** 32));
254 pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32);
261 procedure Raise_Error is
263 raise Constraint_Error with "32-bit arithmetic overflow";
265 (GNATprove, Intentional, "exception might be raised",
266 "Procedure Raise_Error is called to signal input errors");
273 procedure Scaled_Divide32
278 Xu : constant Uns32 := abs X;
279 Yu : constant Uns32 := abs Y;
280 Zu : constant Uns32 := abs Z;
287 -- Unsigned quotient and remainder
289 -- Local ghost variables
291 Mult : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
292 Quot : Big_Integer with Ghost;
293 Big_R : Big_Integer with Ghost;
294 Big_Q : Big_Integer with Ghost;
298 procedure Prove_Negative_Dividend
302 and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0))
304 (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
305 Big (X) * Big (Y) / Big (Z),
306 Big (X) * Big (Y) rem Big (Z))
307 else Big (X) * Big (Y) / Big (Z)),
309 (if Z > 0 then Big_Q <= Big_0 else Big_Q >= Big_0);
310 -- Proves the sign of rounded quotient when dividend is non-positive
312 procedure Prove_Overflow
315 Pre => Z /= 0 and then Mult >= Big_2xx32 * Big (Uns32'(abs Z
)),
316 Post
=> not In_Int32_Range
(Big
(X
) * Big
(Y
) / Big
(Z
))
317 and then not In_Int32_Range
318 (Round_Quotient
(Big
(X
) * Big
(Y
), Big
(Z
),
319 Big
(X
) * Big
(Y
) / Big
(Z
),
320 Big
(X
) * Big
(Y
) rem Big
(Z
)));
321 -- Proves overflow case
323 procedure Prove_Positive_Dividend
327 and then ((X
>= 0 and Y
>= 0) or (X
< 0 and Y
< 0))
329 (if Round
then Round_Quotient
(Big
(X
) * Big
(Y
), Big
(Z
),
330 Big
(X
) * Big
(Y
) / Big
(Z
),
331 Big
(X
) * Big
(Y
) rem Big
(Z
))
332 else Big
(X
) * Big
(Y
) / Big
(Z
)),
334 (if Z
> 0 then Big_Q
>= Big_0
else Big_Q
<= Big_0
);
335 -- Proves the sign of rounded quotient when dividend is non-negative
337 procedure Prove_Rounding_Case
341 and then Quot
= Big
(X
) * Big
(Y
) / Big
(Z
)
342 and then Big_R
= Big
(X
) * Big
(Y
) rem Big
(Z
)
344 Round_Quotient
(Big
(X
) * Big
(Y
), Big
(Z
), Quot
, Big_R
)
345 and then Big
(Ru
) = abs Big_R
346 and then Big
(Zu
) = Big
(Uns32
'(abs Z)),
348 (if Ru > (Zu - Uns32'(1)) / Uns32
'(2)
351 -- Proves correctness of the rounding of the unsigned quotient
353 procedure Prove_Sign_R
356 Pre => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z),
357 Post => In_Int32_Range (Big_R);
359 procedure Prove_Signs
363 and then Quot = Big (X) * Big (Y) / Big (Z)
364 and then Big_R = Big (X) * Big (Y) rem Big (Z)
367 Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
369 and then Big (Ru) = abs Big_R
370 and then Big (Qu) = abs Big_Q
371 and then In_Int32_Range (Big_Q)
372 and then In_Int32_Range (Big_R)
374 (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru))
376 (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu)
377 else To_Neg_Int (Qu)), -- need to ensure To_Pos_Int precondition
378 Post => Big (R) = Big_R and then Big (Q) = Big_Q;
379 -- Proves final signs match the intended result after the unsigned
382 -----------------------------
383 -- Prove_Negative_Dividend --
384 -----------------------------
386 procedure Prove_Negative_Dividend is
388 Lemma_Mult_Non_Positive (Big (X), Big (Y));
389 end Prove_Negative_Dividend;
395 procedure Prove_Overflow is
397 Lemma_Div_Ge (Mult, Big_2xx32, Big (Uns32'(abs Z
)));
398 Lemma_Abs_Commutation
(Z
);
399 Lemma_Abs_Div_Commutation
(Big
(X
) * Big
(Y
), Big
(Z
));
402 -----------------------------
403 -- Prove_Positive_Dividend --
404 -----------------------------
406 procedure Prove_Positive_Dividend
is
408 Lemma_Mult_Non_Negative
(Big
(X
), Big
(Y
));
409 end Prove_Positive_Dividend
;
411 -------------------------
412 -- Prove_Rounding_Case --
413 -------------------------
415 procedure Prove_Rounding_Case
is
417 if Same_Sign
(Big
(X
) * Big
(Y
), Big
(Z
)) then
420 (if Ru
> (Zu
- Uns32
'(1)) / Uns32'(2)
424 end Prove_Rounding_Case
;
430 procedure Prove_Sign_R
is
432 pragma Assert
(In_Int32_Range
(Big
(Z
)));
439 procedure Prove_Signs
is
441 if (X
>= 0) = (Y
>= 0) then
442 pragma Assert
(Big
(R
) = Big_R
and then Big
(Q
) = Big_Q
);
444 pragma Assert
(Big
(R
) = Big_R
and then Big
(Q
) = Big_Q
);
448 -- Start of processing for Scaled_Divide32
451 -- First do the 64-bit multiplication
453 D
:= Uns64
(Xu
) * Uns64
(Yu
);
455 Lemma_Abs_Mult_Commutation
(Big
(X
), Big
(Y
));
456 pragma Assert
(Mult
= Big
(D
));
457 Lemma_Hi_Lo
(D
, Hi
(D
), Lo
(D
));
458 pragma Assert
(Mult
= Big_2xx32
* Big
(Hi
(D
)) + Big
(Lo
(D
)));
460 -- If divisor is zero, raise error
466 Quot
:= Big
(X
) * Big
(Y
) / Big
(Z
);
467 Big_R
:= Big
(X
) * Big
(Y
) rem Big
(Z
);
469 Big_Q
:= Round_Quotient
(Big
(X
) * Big
(Y
), Big
(Z
), Quot
, Big_R
);
474 -- If dividend is too large, raise error
477 Lemma_Ge_Commutation
(Hi
(D
), Zu
);
478 pragma Assert
(Mult
>= Big_2xx32
* Big
(Zu
));
483 -- Then do the 64-bit division
485 Qu
:= Uns32
(D
/ Uns64
(Zu
));
486 Ru
:= Uns32
(D
rem Uns64
(Zu
));
488 Lemma_Abs_Div_Commutation
(Big
(X
) * Big
(Y
), Big
(Z
));
489 Lemma_Abs_Rem_Commutation
(Big
(X
) * Big
(Y
), Big
(Z
));
490 Lemma_Abs_Commutation
(X
);
491 Lemma_Abs_Commutation
(Y
);
492 Lemma_Abs_Commutation
(Z
);
493 Lemma_Mult_Commutation
(Uns64
(Xu
), Uns64
(Yu
), D
);
494 Lemma_Div_Commutation
(D
, Uns64
(Zu
));
495 Lemma_Rem_Commutation
(D
, Uns64
(Zu
));
497 pragma Assert
(Uns64
(Qu
) = D
/ Uns64
(Zu
));
498 pragma Assert
(Uns64
(Ru
) = D
rem Uns64
(Zu
));
499 pragma Assert
(Big
(Ru
) = abs Big_R
);
500 pragma Assert
(Big
(Qu
) = abs Quot
);
501 pragma Assert
(Big
(Zu
) = Big
(Uns32
'(abs Z)));
503 -- Deal with rounding case
508 if Ru > (Zu - Uns32'(1)) / Uns32
'(2) then
509 pragma Assert (abs Big_Q = Big (Qu) + 1);
511 -- Protect against wrapping around when rounding, by signaling
512 -- an overflow when the quotient is too large.
514 if Qu = Uns32'Last then
515 pragma Assert (abs Big_Q = Big_2xx32);
516 Lemma_Not_In_Range_Big2xx32;
520 Qu := Qu + Uns32'(1);
524 pragma Assert
(In_Int32_Range
(Big_Q
));
525 pragma Assert
(Big
(Qu
) = abs Big_Q
);
526 pragma Assert
(Big
(Ru
) = abs Big_R
);
529 -- Set final signs (RM 4.5.5(27-30))
531 -- Case of dividend (X * Y) sign positive
533 if (X
>= 0 and then Y
>= 0) or else (X
< 0 and then Y
< 0) then
534 Prove_Positive_Dividend
;
536 R
:= To_Pos_Int
(Ru
);
537 Q
:= (if Z
> 0 then To_Pos_Int
(Qu
) else To_Neg_Int
(Qu
));
539 -- Case of dividend (X * Y) sign negative
542 Prove_Negative_Dividend
;
544 R
:= To_Neg_Int
(Ru
);
545 Q
:= (if Z
> 0 then To_Neg_Int
(Qu
) else To_Pos_Int
(Qu
));
555 function To_Neg_Int
(A
: Uns32
) return Int32
is
556 R
: constant Int32
:=
557 (if A
= 2**31 then Int32
'First else -To_Int
(A
));
558 -- Note that we can't just use the expression of the Else, because it
559 -- overflows for A = 2**31.
572 function To_Pos_Int
(A
: Uns32
) return Int32
is
573 R
: constant Int32
:= To_Int
(A
);