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

login
register
mail settings
Submitter Arnaud Charlet
Date Oct. 5, 2012, 2:26 p.m.
Message ID <20121005142644.GA8783@adacore.com>
Download mbox | patch
Permalink /patch/189493/
State New
Headers show

Comments

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

2012-10-05  Yannick Moy  <moy@adacore.com>

	* checks.adb (Minimize_Eliminate_Overflow_Checks): Correct code
	for the division operation and exponent operation. Adjust bound
	for the mod and rem operations.

Patch

Index: checks.adb
===================================================================
--- checks.adb	(revision 192125)
+++ checks.adb	(working copy)
@@ -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;