# [Ada] Fix static computation of bounds using -gnato2 or -gnato3

## Commit Message

Arnaud Charlet Oct. 5, 2012, 2:26 p.m.
```The code for statically computing bounds for division and exponent was
incorrect in some cases, possibly leading to wrong results when -gnato2 or
-gnato3 was used. The code for mod and rem was not using optimal bounds, with
possible minor consequences on efficiency of the generated code with -gnato2 or
-gnato3.

Tested on x86_64-pc-linux-gnu, committed on trunk

for the division operation and exponent operation. Adjust bound
for the mod and rem operations.
```

## Patch

```Index: checks.adb
===================================================================
@@ -1209,7 +1209,7 @@

--  Here we know the result is Long_Long_Integer'Base, of that it has
--  been rewritten because the parent operation is a conversion. See
-      --  Conversion_Optimization.Apply_Arithmetic_Overflow_Checked_Suppressed.
+      --  Apply_Arithmetic_Overflow_Checked_Suppressed.Conversion_Optimization.

else
pragma Assert
@@ -7087,148 +7087,81 @@

when N_Op_Divide =>

-               --  Following seems awfully complex, can it be simplified ???
+               --  If the right operand can only be zero, set 0..0

-               Hi := No_Uint;
-               Lo := No_Uint;
+               if Rlo = 0 and then Rhi = 0 then
+                  Lo := Uint_0;
+                  Hi := Uint_0;

-               declare
-                  S : Uint;
+               --  Possible bounds of division must come from dividing end
+               --  values of the input ranges (four possibilities), provided
+               --  zero is not included in the possible values of the right
+               --  operand.

-               begin
-                  --  First work on finding big absolute result values. These
-                  --  come from dividing large numbers (which we have in Llo
-                  --  and Lhi) by small values, which we need to figure out.
+               --  Otherwise, we just consider two intervals of values for
+               --  the right operand: the interval of negative values (up to
+               --  -1) and the interval of positive values (starting at 1).
+               --  Since division by 1 is the identity, and division by -1
+               --  is negation, we get all possible bounds of division in that
+               --  case by considering:
+               --    - all values from the division of end values of input
+               --      ranges;
+               --    - the end values of the left operand;
+               --    - the negation of the end values of the left operand.

-                  --  Case where right operand can be positive
+               else
+                  declare
+                     Mrk : constant Uintp.Save_Mark := Mark;
+                     --  Mark so we can release the RR and Ev values

-                  if Rhi > 0 then
+                     Ev1 : Uint;
+                     Ev2 : Uint;
+                     Ev3 : Uint;
+                     Ev4 : Uint;

-                     --  Find smallest positive divisor
+                  begin
+                     --  Discard extreme values of zero for the divisor, since
+                     --  they will simply result in an exception in any case.

-                     if Rlo > 0 then
-                        S := Rlo;
-                     else
-                        S := Uint_1;
+                     if Rlo = 0 then
+                        Rlo := Uint_1;
+                     elsif Rhi = 0 then
+                        Rhi := -Uint_1;
end if;

-                     --  Big negative value divided by small positive value
-                     --  generates a candidate for lowest possible result.
+                     --  Compute possible bounds coming from dividing end
+                     --  values of the input ranges.

-                     if Llo < 0 then
-                        Min (Lo, Llo / S);
-                     end if;
+                     Ev1 := Llo / Rlo;
+                     Ev2 := Llo / Rhi;
+                     Ev3 := Lhi / Rlo;
+                     Ev4 := Lhi / Rhi;

-                     --  Big positive value divided by small positive value
-                     --  generates a candidate for highest possible result.
+                     Lo := UI_Min (UI_Min (Ev1, Ev2), UI_Min (Ev3, Ev4));
+                     Hi := UI_Max (UI_Max (Ev1, Ev2), UI_Max (Ev3, Ev4));

-                     if Lhi > 0 then
-                        Max (Hi, Lhi / S);
-                     end if;
-                  end if;
+                     --  If the right operand can be both negative or positive,
+                     --  include the end values of the left operand in the
+                     --  extreme values, as well as their negation.

-                  --  Case where right operand can be negative
+                     if Rlo < 0 and then Rhi > 0 then
+                        Ev1 := Llo;
+                        Ev2 := -Llo;
+                        Ev3 := Lhi;
+                        Ev4 := -Lhi;

-                  if Rlo < 0 then
-
-                     --  Find smallest absolute value negative divisor
-
-                     if Rhi < 0 then
-                        S := Rhi;
-                     else
-                        S := -Uint_1;
+                        Min (Lo,
+                             UI_Min (UI_Min (Ev1, Ev2), UI_Min (Ev3, Ev4)));
+                        Max (Hi,
+                             UI_Max (UI_Max (Ev1, Ev2), UI_Max (Ev3, Ev4)));
end if;

-                     --  Big negative value divided by small negative value
-                     --  generates a candidate for largest possible result.
+                     --  Release the RR and Ev values

-                     if Llo < 0 then
-                        Max (Hi, Llo / S);
-                     end if;
+                     Release_And_Save (Mrk, Lo, Hi);
+                  end;
+               end if;

-                     --  Big positive value divided by small negative value
-                     --  generates a candidate for lowest possible result.
-
-                     if Lhi > 0 then
-                        Min (Lo, Lhi / S);
-                     end if;
-                  end if;
-
-                  --  Now work on finding small absolute result values. These
-                  --  come from dividing small numbers, which we need to figure
-                  --  out, by large values (which we have in Rlo, Rhi).
-
-                  --  Case where left operand can be positive
-
-                  if Lhi > 0 then
-
-                     --  Find smallest positive dividend
-
-                     if Llo > 0 then
-                        S := Llo;
-                     else
-                        S := Uint_1;
-                     end if;
-
-                     --  Small positive values divided by large negative values
-                     --  generate candidates for low results.
-
-                     if Rlo < 0 then
-                        Min (Lo, S / Rlo);
-                     end if;
-
-                     --  Small positive values divided by large positive values
-                     --  generate candidates for high results.
-
-                     if Rhi > 0 then
-                        Max (Hi, S / Rhi);
-                     end if;
-                  end if;
-
-                  --  Case where left operand can be negative
-
-                  if Llo < 0 then
-
-                     --  Find smallest absolute value negative dividend
-
-                     if Lhi < 0 then
-                        S := Lhi;
-                     else
-                        S := -Uint_1;
-                     end if;
-
-                     --  Small negative value divided by large negative value
-                     --  generates a candidate for highest possible result.
-
-                     if Rlo < 0 then
-                        Max (Hi, Rlo / S);
-                     end if;
-
-                     --  Small negative value divided by large positive value
-                     --  generates a candidate for lowest possible result.
-
-                     if Rhi > 0 then
-                        Min (Lo, Rhi / S);
-                     end if;
-                  end if;
-
-                  --  Finally, if neither Lo or Hi set (happens if the right
-                  --  operand is always zero for example), then set 0 .. 0.
-
-                  if Lo = No_Uint and then Hi = No_Uint then
-                     Lo := Uint_0;
-                     Hi := Uint_0;
-
-                  --  If one bound set and not the other copy
-
-                  elsif Lo = No_Uint then
-                     Lo := Hi;
-
-                  elsif Hi = No_Uint then
-                     Hi := Lo;
-                  end if;
-               end;
-
--  Exponentiation

when N_Op_Expon =>
@@ -7264,14 +7197,15 @@

else
--  High bound comes either from exponentiation of largest
-                  --  positive value to largest exponent value, or from the
-                  --  exponentiation of most negative value to an odd exponent.
+                  --  positive value to largest exponent value, or from
+                  --  the exponentiation of most negative value to an
+                  --  even exponent.

declare
Hi1, Hi2 : Uint;

begin
-                     if Lhi >= 0 then
+                     if Lhi > 0 then
Hi1 := Lhi ** Rhi;
else
Hi1 := Uint_0;
@@ -7279,9 +7213,9 @@

if Llo < 0 then
if Rhi mod 2 = 0 then
-                           Hi2 := Llo ** (Rhi - 1);
-                        else
Hi2 := Llo ** Rhi;
+                        else
+                           Hi2 := Llo ** (Rhi - 1);
end if;
else
Hi2 := Uint_0;
@@ -7316,7 +7250,7 @@

when N_Op_Mod =>
declare
-                  Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi);
+                  Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi) - 1;
--  This is the maximum absolute value of the result

begin
@@ -7371,9 +7305,10 @@

when N_Op_Rem =>
declare
-                  Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi);
+                  Maxabs : constant Uint := UI_Max (abs Rlo, abs Rhi) - 1;
--  This is the maximum absolute value of the result. Note
-                  --  that the result range does not depend on the sign of B.
+                  --  that the result range does not depend on the sign of the
+                  --  right operand.

begin
Lo := Uint_0;

```