1 with Interfaces
; use Interfaces
;
3 with Ada
.Unchecked_Conversion
;
5 package body Opt61_Pkg
is
7 pragma Suppress
(Overflow_Check
);
8 pragma Suppress
(Range_Check
);
10 subtype Uns64
is Unsigned_64
;
12 function To_Int
is new Ada
.Unchecked_Conversion
(Uns64
, Int64
);
14 subtype Uns32
is Unsigned_32
;
16 -----------------------
17 -- Local Subprograms --
18 -----------------------
20 function "+" (A
: Uns64
; B
: Uns32
) return Uns64
is (A
+ Uns64
(B
));
21 -- Length doubling additions
23 function "*" (A
, B
: Uns32
) return Uns64
is (Uns64
(A
) * Uns64
(B
));
24 -- Length doubling multiplication
26 function "&" (Hi
, Lo
: Uns32
) return Uns64
is
27 (Shift_Left
(Uns64
(Hi
), 32) or Uns64
(Lo
));
28 -- Concatenate hi, lo values to form 64-bit result
30 function "abs" (X
: Int64
) return Uns64
is
31 (if X
= Int64
'First then 2**63 else Uns64
(Int64
'(abs X)));
32 -- Convert absolute value of X to unsigned. Note that we can't just use
33 -- the expression of the Else, because it overflows for X = Int64'First.
35 function Lo (A : Uns64) return Uns32 is (Uns32 (A and 16#FFFF_FFFF#));
36 -- Low order half of 64-bit value
38 function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32)));
39 -- High order half of 64-bit value
45 procedure Double_Divide
50 Xu : constant Uns64 := abs X;
51 Yu : constant Uns64 := abs Y;
53 Yhi : constant Uns32 := Hi (Yu);
54 Ylo : constant Uns32 := Lo (Yu);
56 Zu : constant Uns64 := abs Z;
57 Zhi : constant Uns32 := Hi (Zu);
58 Zlo : constant Uns32 := Lo (Zu);
65 if Yu = 0 or else Zu = 0 then
66 raise Constraint_Error;
69 -- Compute Y * Z. Note that if the result overflows 64 bits unsigned,
70 -- then the rounded result is clearly zero (since the dividend is at
71 -- most 2**63 - 1, the extra bit of precision is nice here).
83 T2 := (if Zhi /= 0 then Ylo * Zhi else 0);
95 Du := Lo (T2) & Lo (T1);
97 -- Set final signs (RM 4.5.5(27-30))
99 Den_Pos := (Y < 0) = (Z < 0);
101 -- Check overflow case of largest negative number divided by 1
103 if X = Int64'First and then Du = 1 and then not Den_Pos then
104 raise Constraint_Error;
107 -- Perform the actual division
112 -- Deal with rounding case
114 if Round and then Ru > (Du - Uns64'(1)) / Uns64
'(2) then
115 Qu := Qu + Uns64'(1);
118 -- Case of dividend (X) sign positive
122 Q
:= (if Den_Pos
then To_Int
(Qu
) else -To_Int
(Qu
));
124 -- Case of dividend (X) sign negative
128 Q
:= (if Den_Pos
then -To_Int
(Qu
) else To_Int
(Qu
));