# [Ada] Division/Rem/Mod work with extended overflow checks

## Commit Message

Arnaud Charlet Oct. 1, 2012, 1:18 p.m.
```This patch implements extended overflow checking modes
with the division, rem, and mod operators. This completes
the work on extended overflow checking.

The following is a test program:

1. with Text_IO; use Text_IO;
2. procedure Overflowm5 is
3.    function r1 (a, b, c : Integer)
4.      return Integer is
5.    begin
6.       return a / b - c;
7.    end;
8.    function r2 (a, b, c : Long_Long_Integer)
9.      return Long_Long_Integer is
10.    begin
11.       return a / b - c;
12.    end;
13. begin
14.    begin
15.       Put_Line
16.         ("r1 returns" &
17.            Integer'Image
18.            (r1 (Integer'First, - 1, Integer'Last)));
19.    exception
20.       when Constraint_Error =>
21.          Put_Line ("r1 raises exception");
22.    end;
23.
24.    begin
25.       Put_Line
26.         ("r2 returns" &
27.            Long_Long_Integer'Image
28.            (r2 (Long_Long_Integer'First, -1,
29.             Long_Long_Integer'Last)));
30.    exception
31.       when Constraint_Error =>
32.          Put_Line ("r2 raises exception");
33.    end;
34. end Overflowm5;

In CHECKED mode (-gnato1) we get:

r1 raises exception
r2 raises exception

since in both cases we are dividing the largest negative integer
by minus one, which generates a value one greater than the
largest positive value.

In MINIMIZED mode (-gnato2) we get:

r1 returns 1
r2 raises exception

since we can now compute the division and subtraction for r1
in Long_Long_Integer mode, but that's not true for r2.

In ELIMINATE mode (-gnato3) we get:

r1 returns 1
r2 returns 1

Because now we use Bignum arithmetic for the division and
subtraction operations in r2.

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

* checks.adb (Apply_Divide_Checks): New name for
Apply_Divide_Check (Minimize_Eliminate_Overflow_Checks):
Add code to handle division (and rem and mod) properly.
(Apply_Division_Check): New procedure (Apply_Divide_Checks):
Use Apply_Division_Check (Apply_Divide_Checks): Use
Apply_Arithmetic_Overflow_Minimized_Eliminated.
* checks.ads (Apply_Divide_Checks): New name for
Apply_Divide_Check, also add clearer documentation for this
routine and put in alfa order.
* exp_ch4.adb (Apply_Divide_Checks): New name for
Apply_Divide_Check.
* s-bignum.adb (To_Bignum): Handle largest negative integer
properly.
* sem.adb (Analyze): Handle overflow suppression correctly
(Analyze_List): Handle overflow suppression correctly
* sem_res.adb (Analyze_And_Resolve): Handle overflow suppression
correctly.
```

## Patch

```Index: checks.adb
===================================================================
@@ -193,14 +193,6 @@
-- Local Subprograms --
-----------------------

-   procedure Apply_Float_Conversion_Check
-     (Ck_Node    : Node_Id;
-      Target_Typ : Entity_Id);
-   --  The checks on a conversion from a floating-point type to an integer
-   --  type are delicate. They have to be performed before conversion, they
-   --  have to raise an exception when the operand is a NaN, and rounding must
-   --  be taken into account to determine the safe bounds of the operand.
-
procedure Apply_Arithmetic_Overflow_Normal (N : Node_Id);
--  Used to apply arithmetic overflow checks for all cases except operators
--  on signed arithmetic types in Minimized/Eliminate case (for which we
@@ -211,6 +203,24 @@
--  checking mode is Minimized or Eliminated (and the Do_Overflow_Check flag
--  is known to be set) and we have an signed integer arithmetic op.

+   procedure Apply_Division_Check
+     (N   : Node_Id;
+      Rlo : Uint;
+      Rhi : Uint;
+      ROK : Boolean);
+   --  N is an N_Op_Div, N_Op_Rem, or N_Op_Mod node. This routine applies
+   --  division checks as required if the Do_Division_Check flag is set.
+   --  Rlo and Rhi give the possible range of the right operand, these values
+   --  can be referenced and trusted only if ROK is set True.
+
+   procedure Apply_Float_Conversion_Check
+     (Ck_Node    : Node_Id;
+      Target_Typ : Entity_Id);
+   --  The checks on a conversion from a floating-point type to an integer
+   --  type are delicate. They have to be performed before conversion, they
+   --  have to raise an exception when the operand is a NaN, and rounding must
+   --  be taken into account to determine the safe bounds of the operand.
+
procedure Apply_Selected_Length_Checks
(Ck_Node    : Node_Id;
Target_Typ : Entity_Id;
@@ -1641,52 +1651,69 @@
Reason    => CE_Discriminant_Check_Failed));
end Apply_Discriminant_Check;

-   ------------------------
-   -- Apply_Divide_Check --
-   ------------------------
+   -------------------------
+   -- Apply_Divide_Checks --
+   -------------------------

-   procedure Apply_Divide_Check (N : Node_Id) is
+   procedure Apply_Divide_Checks (N : Node_Id) is
Loc   : constant Source_Ptr := Sloc (N);
Typ   : constant Entity_Id  := Etype (N);
Left  : constant Node_Id    := Left_Opnd (N);
Right : constant Node_Id    := Right_Opnd (N);

+      Mode : constant Overflow_Check_Type := Overflow_Check_Mode (Typ);
+      --  Current overflow checking mode
+
LLB : Uint;
Llo : Uint;
Lhi : Uint;
LOK : Boolean;
Rlo : Uint;
Rhi : Uint;
-      ROK   : Boolean;
+      ROK : Boolean;

pragma Warnings (Off, Lhi);
--  Don't actually use this value

begin
+      --  If we are operating in MINIMIZED or ELIMINATED mode, and the
+      --  Do_Overflow_Check flag is set and we are operating on signed
+      --  integer types, then the only thing this routine does is to call
+      --  Apply_Arithmetic_Overflow_Minimized_Eliminated. That procedure will
+      --  (possibly later on during recursive downward calls), make sure that
+      --  any needed overflow and division checks are properly applied.
+
+      if Mode in Minimized_Or_Eliminated
+        and then Do_Overflow_Check (N)
+        and then Is_Signed_Integer_Type (Typ)
+      then
+         Apply_Arithmetic_Overflow_Minimized_Eliminated (N);
+         return;
+      end if;
+
+      --  Proceed here in SUPPRESSED or CHECKED modes
+
if Full_Expander_Active
and then not Backend_Divide_Checks_On_Target
and then Check_Needed (Right, Division_Check)
then
Determine_Range (Right, ROK, Rlo, Rhi, Assume_Valid => True);

-         --  See if division by zero possible, and if so generate test. This
-         --  part of the test is not controlled by the -gnato switch.
+         --  Deal with division check

-         if Do_Division_Check (N) then
-            if (not ROK) or else (Rlo <= 0 and then 0 <= Rhi) then
-               Insert_Action (N,
-                 Make_Raise_Constraint_Error (Loc,
-                   Condition =>
-                     Make_Op_Eq (Loc,
-                       Left_Opnd  => Duplicate_Subexpr_Move_Checks (Right),
-                       Right_Opnd => Make_Integer_Literal (Loc, 0)),
-                   Reason => CE_Divide_By_Zero));
-            end if;
+         if Do_Division_Check (N)
+           and then not Division_Checks_Suppressed (Typ)
+         then
+            Apply_Division_Check (N, Rlo, Rhi, ROK);
end if;

-         --  Test for extremely annoying case of xxx'First divided by -1
+         --  Deal with overflow check

-         if Do_Overflow_Check (N) then
+         if Do_Overflow_Check (N) and then Mode /= Suppressed then
+
+            --  Test for extremely annoying case of xxx'First divided by -1
+            --  for division of signed integer types (only overflow case).
+
if Nkind (N) = N_Op_Divide
and then Is_Signed_Integer_Type (Typ)
then
@@ -1694,31 +1721,69 @@
LLB := Expr_Value (Type_Low_Bound (Base_Type (Typ)));

if ((not ROK) or else (Rlo <= (-1) and then (-1) <= Rhi))
-                 and then
-                 ((not LOK) or else (Llo = LLB))
+                     and then
+                  ((not LOK) or else (Llo = LLB))
then
Insert_Action (N,
Make_Raise_Constraint_Error (Loc,
Condition =>
Make_And_Then (Loc,
+                          Left_Opnd  =>
+                            Make_Op_Eq (Loc,
+                              Left_Opnd  =>
+                                Duplicate_Subexpr_Move_Checks (Left),
+                              Right_Opnd => Make_Integer_Literal (Loc, LLB)),

-                           Make_Op_Eq (Loc,
-                             Left_Opnd  =>
-                               Duplicate_Subexpr_Move_Checks (Left),
-                             Right_Opnd => Make_Integer_Literal (Loc, LLB)),
+                          Right_Opnd =>
+                            Make_Op_Eq (Loc,
+                              Left_Opnd  => Duplicate_Subexpr (Right),
+                              Right_Opnd => Make_Integer_Literal (Loc, -1))),

-                           Make_Op_Eq (Loc,
-                             Left_Opnd =>
-                               Duplicate_Subexpr (Right),
-                             Right_Opnd =>
-                               Make_Integer_Literal (Loc, -1))),
Reason => CE_Overflow_Check_Failed));
end if;
end if;
end if;
end if;
-   end Apply_Divide_Check;
+   end Apply_Divide_Checks;

+   --------------------------
+   -- Apply_Division_Check --
+   --------------------------
+
+   procedure Apply_Division_Check
+     (N   : Node_Id;
+      Rlo : Uint;
+      Rhi : Uint;
+      ROK : Boolean)
+   is
+      pragma Assert (Do_Division_Check (N));
+
+      Loc   : constant Source_Ptr := Sloc (N);
+      Right : constant Node_Id    := Right_Opnd (N);
+
+   begin
+      if Full_Expander_Active
+        and then not Backend_Divide_Checks_On_Target
+        and then Check_Needed (Right, Division_Check)
+      then
+         --  See if division by zero possible, and if so generate test. This
+         --  part of the test is not controlled by the -gnato switch, since
+         --  it is a Division_Check and not an Overflow_Check.
+
+         if Do_Division_Check (N) then
+            if (not ROK) or else (Rlo <= 0 and then 0 <= Rhi) then
+               Insert_Action (N,
+                 Make_Raise_Constraint_Error (Loc,
+                   Condition =>
+                     Make_Op_Eq (Loc,
+                       Left_Opnd  => Duplicate_Subexpr_Move_Checks (Right),
+                       Right_Opnd => Make_Integer_Literal (Loc, 0)),
+                   Reason => CE_Divide_By_Zero));
+            end if;
+         end if;
+      end if;
+   end Apply_Division_Check;
+
----------------------------------
-- Apply_Float_Conversion_Check --
----------------------------------
@@ -6496,6 +6561,36 @@
OK : Boolean;
--  Used in call to Determine_Range

+      procedure Max (A : in out Uint; B : Uint);
+      --  If A is No_Uint, sets A to B, else to UI_Max (A, B);
+
+      procedure Min (A : in out Uint; B : Uint);
+      --  If A is No_Uint, sets A to B, else to UI_Min (A, B);
+
+      ---------
+      -- Max --
+      ---------
+
+      procedure Max (A : in out Uint; B : Uint) is
+      begin
+         if A = No_Uint or else B > A then
+            A := B;
+         end if;
+      end Max;
+
+      ---------
+      -- Min --
+      ---------
+
+      procedure Min (A : in out Uint; B : Uint) is
+      begin
+         if A = No_Uint or else B < A then
+            A := B;
+         end if;
+      end Min;
+
+   --  Start of processing for Minimize_Eliminate_Overflow_Checks
+
begin
--  Case where we do not have an arithmetic operator.

@@ -6559,8 +6654,149 @@
--  Division

when N_Op_Divide =>
-               raise Program_Error;

+               --  Following seems awfully complex, can it be simplified ???
+
+               Hi := No_Uint;
+               Lo := No_Uint;
+
+               declare
+                  S : Uint;
+
+               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.
+
+                  --  Case where right operand can be positive
+
+                  if Rhi > 0 then
+
+                     --  Find smallest positive divisor
+
+                     if Rlo > 0 then
+                        S := Rlo;
+                     else
+                        S := Uint_1;
+                     end if;
+
+                     --  Big negative value divided by small positive value
+                     --  generates a candidate for lowest possible result.
+
+                     if Llo < 0 then
+                        Min (Lo, Llo / S);
+                     end if;
+
+                     --  Big positive value divided by small positive value
+                     --  generates a candidate for highest possible result.
+
+                     if Lhi > 0 then
+                        Max (Hi, Lhi / S);
+                     end if;
+                  end if;
+
+                  --  Case where right operand can be negative
+
+                  if Rlo < 0 then
+
+                     --  Find smallest absolute value negative divisor
+
+                     if Rhi < 0 then
+                        S := Rhi;
+                     else
+                        S := -Uint_1;
+                     end if;
+
+                     --  Big negative value divided by small negative value
+                     --  generates a candidate for largest possible result.
+
+                     if Llo < 0 then
+                        Max (Hi, Llo / S);
+                     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 =>
@@ -6647,8 +6883,27 @@
--  Mod

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

+               begin
+                  Lo := Uint_0;
+                  Hi := Uint_0;
+
+                  --  The result depends only on the sign and magnitude of
+                  --  the right operand, it does not depend on the sign or
+                  --  magnitude of the left operand.
+
+                  if Rlo < 0 then
+                     Lo := -Maxabs;
+                  end if;
+
+                  if Rhi > 0 then
+                     Hi := Maxabs;
+                  end if;
+               end;
+
--  Multiplication

when N_Op_Multiply =>
@@ -6683,8 +6938,30 @@
--  Remainder

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

+               begin
+                  Lo := Uint_0;
+                  Hi := Uint_0;
+
+                  --  Case of left operand negative, which results in a range
+                  --  of -Maxabs .. 0 for those negative values. If there are
+                  --  no negative values then Lo value of result is always 0.
+
+                  if Llo < 0 then
+                     Lo := -Maxabs;
+                  end if;
+
+                  --  Case of left operand positive
+
+                  if Lhi > 0 then
+                     Hi := Maxabs;
+                  end if;
+               end;
+
--  Subtract

when N_Op_Subtract =>
@@ -6819,16 +7096,21 @@
Set_Etype (N, Empty);
Set_Entity (N, Empty);

-      --  Now analyze this new node
+      --  Now analyze this new node. This reanalysis will complete processing
+      --  for the node. In particular we will complete the expansion of an
+      --  exponentiation operator (e.g. changing A ** 2 to A * A), and also
+      --  we will complete any division checks (since we have not changed the
+      --  setting of the Do_Division_Check flag).

-      --  If no overflow check, suppress all checks
+      --  If no overflow check, suppress overflow check to avoid an infinite
+      --  recursion into this procedure.

if not Do_Overflow_Check (N) then
-         Analyze_And_Resolve (N, LLIB, Suppress => All_Checks);
+         Analyze_And_Resolve (N, LLIB, Suppress => Overflow_Check);

--  If an overflow check is required, do it in normal CHECKED mode.
-      --  That avoids an infinite recursion, makes sure we get a normal
-      --  overflow check, and also completes expansion of Exponentiation.
+      --  That avoids an infinite recursion, making sure we get a normal
+      --  overflow check.

else
declare
===================================================================
@@ -166,6 +166,13 @@
--  formals, the check is performed only if the corresponding actual is
--  constrained, i.e., whether Lhs'Constrained is True.

+   procedure Apply_Divide_Checks (N : Node_Id);
+   --  The node kind is N_Op_Divide, N_Op_Mod, or N_Op_Rem if either of the
+   --  flags Do_Division_Check or Do_Overflow_Check is set, then this routine
+   --  ensures that the appropriate checks are made. Note that overflow can
+   --  occur in the signed case for the case of the largest negative number
+   --  divided by minus one.
+
procedure Apply_Parameter_Aliasing_And_Validity_Checks (Subp : Entity_Id);
--  Given a subprogram Subp, add both a pre and post condition pragmas that
--  detect aliased objects and verify the proper initialization of scalars
@@ -176,12 +183,6 @@
--  for Typ, if Typ has a predicate function. The check is applied only
--  if the type of N does not match Typ.

-   procedure Apply_Divide_Check (N : Node_Id);
-   --  The node kind is N_Op_Divide, N_Op_Mod, or N_Op_Rem. An appropriate
-   --  check is generated to ensure that the right operand is non-zero. In
-   --  the divide case, we also check that we do not have the annoying case
-   --  of the largest negative number divided by minus one.
-
procedure Apply_Type_Conversion_Checks (N : Node_Id);
--  N is an N_Type_Conversion node. A type conversion actually involves
--  two sorts of checks. The first check is the checks that ensures that
===================================================================
@@ -730,6 +730,20 @@
Scope_Suppress := Svg;
end;

+      elsif Suppress = Overflow_Check then
+         declare
+            Svg : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_General;
+            Sva : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_Assertions;
+         begin
+            Scope_Suppress.Overflow_Checks_General    := Suppressed;
+            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Analyze (N);
+            Scope_Suppress.Overflow_Checks_General    := Svg;
+            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+         end;
+
else
declare
Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
@@ -769,6 +783,20 @@
Scope_Suppress := Svg;
end;

+      elsif Suppress = Overflow_Check then
+         declare
+            Svg : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_General;
+            Sva : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_Assertions;
+         begin
+            Scope_Suppress.Overflow_Checks_General    := Suppressed;
+            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Analyze_List (L);
+            Scope_Suppress.Overflow_Checks_General    := Svg;
+            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+         end;
+
else
declare
Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
===================================================================
@@ -322,7 +322,7 @@
Resolve (N, Typ);
end Analyze_And_Resolve;

-   --  Version withs check(s) suppressed
+   --  Versions with check(s) suppressed

procedure Analyze_And_Resolve
(N        : Node_Id;
@@ -341,6 +341,20 @@
Scope_Suppress := Svg;
end;

+      elsif Suppress = Overflow_Check then
+         declare
+            Svg : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_General;
+            Sva : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_Assertions;
+         begin
+            Scope_Suppress.Overflow_Checks_General    := Suppressed;
+            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Analyze_And_Resolve (N, Typ);
+            Scope_Suppress.Overflow_Checks_General    := Svg;
+            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+         end;
+
else
declare
Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
@@ -381,6 +395,20 @@
Scope_Suppress := Svg;
end;

+      elsif Suppress = Overflow_Check then
+         declare
+            Svg : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_General;
+            Sva : constant Overflow_Check_Type :=
+                    Scope_Suppress.Overflow_Checks_Assertions;
+         begin
+            Scope_Suppress.Overflow_Checks_General    := Suppressed;
+            Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
+            Analyze_And_Resolve (N);
+            Scope_Suppress.Overflow_Checks_General    := Svg;
+            Scope_Suppress.Overflow_Checks_Assertions := Sva;
+         end;
+
else
declare
Svg : constant Boolean := Scope_Suppress.Suppress (Suppress);
===================================================================
@@ -6584,7 +6584,7 @@
--  Non-fixed point cases, do integer zero divide and overflow checks

elsif Is_Integer_Type (Typ) then
-         Apply_Divide_Check (N);
+         Apply_Divide_Checks (N);

--  Deal with Vax_Float

@@ -7836,7 +7836,7 @@

else
if Is_Integer_Type (Etype (N)) then
-            Apply_Divide_Check (N);
+            Apply_Divide_Checks (N);
end if;

--  Apply optimization x mod 1 = 0. We don't really need that with
@@ -8469,7 +8469,7 @@
Binary_Op_Validity_Checks (N);

if Is_Integer_Type (Etype (N)) then
-         Apply_Divide_Check (N);
+         Apply_Divide_Checks (N);
end if;

--  Apply optimization x rem 1 = 0. We don't really need that with gcc,
===================================================================
@@ -1024,10 +1024,21 @@
if X = 0 then
R := Allocate_Bignum (0);

+      --  One word result
+
elsif X in -(2 ** 32 - 1) .. +(2 ** 32 - 1) then
R := Allocate_Bignum (1);
R.D (1) := SD (abs (X));

+      --  Largest negative number annoyance
+
+      elsif X = Long_Long_Integer'First then
+         R := Allocate_Bignum (2);
+         R.D (1) := 2 ** 31;
+         R.D (2) := 0;
+
+      --  Normal two word case
+
else
R := Allocate_Bignum (2);
R.D (2) := SD (abs (X) mod Base);

```