diff mbox

[Ada] Further work on new overflow checking scheme

Message ID 20121001101810.GA20311@adacore.com
State New
Headers show

Commit Message

Arnaud Charlet Oct. 1, 2012, 10:18 a.m. UTC
This patch contains the initial implementation of Minimized/Eliminated
overflow checking mode, but it is quite preliminary, definitely not
ready for prime time. So no tests yet.

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

2012-10-01  Robert Dewar  <dewar@adacore.com>

	* checks.adb (Overflow_Check_Mode): New function
	(Apply_Overflow_Check): New procedure (Is_Check_Suppressed):
	Moved here from Sem, Overflow_Check case now specially treated.
	* checks.ads (Overflow_Check_Mode): New function
	(Is_Check_Suppressed): Moved here from Sem (more logical)
	* exp_ch4.adb (Substitute_Valid_Check): Suppress warning about
	optimization if we are in MINIMIZED or ELIMINATED overflow
	checking mode and within an assertiom expression.
	* rtsfind.ads: Add entries for Bignum stuff.
	* s-bignum.ads, s-bignum.adb: New files.
	* sem.ads, sem.adb (Is_Check_Suppressed): Moved to Checks, more logical.
	* sem_prag.adb (Process_Suppress_Unsuppress): New behavior for
	Unsuppress of Overflow_Check (sets Checked instead of Minimized)
	* sem_res.adb: Update comments.
	* sinfo.ads (N_Op): Add documentation on overflow handling.
	* tbuild.ads, tbuild.adb (Convert_To_And_Rewrite): New procedure.
	* types.ads (Minimized_Or_Eliminated): New subtype.
diff mbox

Patch

Index: sinfo.ads
===================================================================
--- sinfo.ads	(revision 191895)
+++ sinfo.ads	(working copy)
@@ -408,6 +408,14 @@ 
    --       Do_Overflow_Check        (Flag17-Sem) set if overflow check needed
    --       Has_Private_View         (Flag11-Sem) set in generic units.
 
+   --       Note on use of entity field. This field is set during analysis
+   --       and is used in carrying out semantic checking, but it has no
+   --       significance to the back end, which is driven by the Etype's
+   --       of the operands, and the Etype of the result. During processing
+   --       in the exapander for overflow checks, these types may be modified
+   --       and there is no point in trying to set a proper Entity value, so
+   --       it just gets cleared to Empty in this situation.
+
    --    "plus fields for unary operator"
    --       Chars                    (Name1)      Name_Id for the operator
    --       Right_Opnd               (Node3)      right operand expression
@@ -416,6 +424,8 @@ 
    --       Do_Overflow_Check        (Flag17-Sem) set if overflow check needed
    --       Has_Private_View         (Flag11-Sem) set in generic units.
 
+   --       See note on use of Entity field above (same situation).
+
    --    "plus fields for expression"
    --       Paren_Count                           number of parentheses levels
    --       Etype                    (Node5-Sem)  type of the expression
@@ -3849,6 +3859,22 @@ 
       --  point operands if the Treat_Fixed_As_Integer flag is set and will
       --  thus treat these nodes in identical manner, ignoring small values.
 
+      --  Note on overflow handling: When the overflow checking mode is set to
+      --  MINIMIZED or ELIMINATED, nodes for signed arithmetic operations may
+      --  be modified to use a larger type for the operands and result. In
+      --  these cases, the back end does not need the Entity field anyway, so
+      --  there is no point in setting it. In fact we reuse the Entity field to
+      --  record the possible range of the result. Entity points to an N_Range
+      --  node whose Low_Bound and High_Bound fields point to integer literal
+      --  nodes containing the computed bounds. These range nodes are only set
+      --  for intermediate nodes whose parents are themselves either arithmetic
+      --  operators, or comparison or membership tests. The computed ranges are
+      --  then used in processing the parent operation. In the case where the
+      --  computed range exceeds that of Long_Long_Integer, and we are running
+      --  in ELIMINATED mode, the operator node will be changed to be a call to
+      --  the appropriate routine in System.Bignums, and in this case we forget
+      --  about keeping track of the range.
+
       ---------------------------------
       -- 4.5.9 Quantified Expression --
       ---------------------------------
Index: types.ads
===================================================================
--- types.ads	(revision 191897)
+++ types.ads	(working copy)
@@ -735,6 +735,11 @@ 
       --  overflow. Again the final value of an expression must fit in the base
       --  type of the whole expression.
 
+   subtype Minimized_Or_Eliminated is
+     Overflow_Check_Type range Minimized .. Eliminated;
+   --  Definte subtypes so that clients don't need to know ordering. Note that
+   --  Overflow_Check_Type is not marked as an ordered enumeration type.
+
    --  The following structure captures the state of check suppression or
    --  activation at a particular point in the program execution.
 
Index: checks.adb
===================================================================
--- checks.adb	(revision 191910)
+++ checks.adb	(working copy)
@@ -201,6 +201,16 @@ 
    --  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
+   --  call Apply_Arithmetic_Overflow_Minimized_Eliminated below).
+
+   procedure Apply_Arithmetic_Overflow_Minimized_Eliminated (Op : Node_Id);
+   --  Used to apply arithmetic overflow checks for the case where the overflow
+   --  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_Selected_Length_Checks
      (Ck_Node    : Node_Id;
       Target_Typ : Entity_Id;
@@ -289,6 +299,11 @@ 
    --  Called by Apply_{Length,Range}_Checks to rewrite the tree with the
    --  Constraint_Error node.
 
+   function Is_Signed_Integer_Arithmetic_Op (N : Node_Id) return Boolean;
+   --  Returns True if node N is for an arithmetic operation with signed
+   --  integer operands. This is the kind of node for which special handling
+   --  applies in MINIMIZED or EXTENDED overflow checking mode.
+
    function Range_Or_Validity_Checks_Suppressed
      (Expr : Node_Id) return Boolean;
    --  Returns True if either range or validity checks or both are suppressed
@@ -731,6 +746,32 @@ 
    -- Apply_Arithmetic_Overflow_Check --
    -------------------------------------
 
+   procedure Apply_Arithmetic_Overflow_Check (N : Node_Id) is
+   begin
+      --  Use old routine in almost all cases (the only case we are treating
+      --  specially is the case of an signed integer arithmetic op with the
+      --  Do_Overflow_Check flag set on the node, and the overflow checking
+      --  mode is either Minimized_Or_Eliminated.
+
+      if Overflow_Check_Mode (Etype (N)) not in Minimized_Or_Eliminated
+        or else not Do_Overflow_Check (N)
+        or else not Is_Signed_Integer_Arithmetic_Op (N)
+      then
+         Apply_Arithmetic_Overflow_Normal (N);
+
+      --  Otherwise use the new routine for Minimized/Eliminated modes for
+      --  the case of a signed integer arithmetic op, with Do_Overflow_Check
+      --  set True, and the checking mode is Minimized_Or_Eliminated.
+
+      else
+         Apply_Arithmetic_Overflow_Minimized_Eliminated (N);
+      end if;
+   end Apply_Arithmetic_Overflow_Check;
+
+   --------------------------------------
+   -- Apply_Arithmetic_Overflow_Normal --
+   --------------------------------------
+
    --  This routine is called only if the type is an integer type, and a
    --  software arithmetic overflow check may be needed for op (add, subtract,
    --  or multiply). This check is performed only if Software_Overflow_Checking
@@ -738,7 +779,16 @@ 
    --  operation into a more complex sequence of tests that ensures that
    --  overflow is properly caught.
 
-   procedure Apply_Arithmetic_Overflow_Check (N : Node_Id) is
+   --  This is used in SUPPRESSED/CHECKED modes. It is identical to the
+   --  code for these cases before the big overflow earthquake, thus ensuring
+   --  that in these modes we have compatible behavior (and realibility) to
+   --  what was there before. It is also called for types other than signed
+   --  integers, and if the Do_Overflow_Check flag is off.
+
+   --  Note: we also call this routine if we decide in the MINIMIZED case
+   --  to give up and just generate an overflow check without any fuss.
+
+   procedure Apply_Arithmetic_Overflow_Normal (N : Node_Id) is
       Loc   : constant Source_Ptr := Sloc (N);
       Typ   : constant Entity_Id  := Etype (N);
       Rtyp  : constant Entity_Id  := Root_Type (Typ);
@@ -1001,8 +1051,149 @@ 
          when RE_Not_Available =>
             return;
       end;
-   end Apply_Arithmetic_Overflow_Check;
+   end Apply_Arithmetic_Overflow_Normal;
 
+   ----------------------------------------------------
+   -- Apply_Arithmetic_Overflow_Minimized_Eliminated --
+   ----------------------------------------------------
+
+   procedure Apply_Arithmetic_Overflow_Minimized_Eliminated (Op : Node_Id) is
+      pragma Assert (Is_Signed_Integer_Arithmetic_Op (Op));
+      pragma Assert (Do_Overflow_Check (Op));
+
+      Loc : constant Source_Ptr := Sloc (Op);
+      P   : constant Node_Id    := Parent (Op);
+
+      Result_Type : constant Entity_Id := Etype (Op);
+      --  Original result type
+
+      Check_Mode : constant Overflow_Check_Type :=
+        Overflow_Check_Mode (Etype (Op));
+      pragma Assert (Check_Mode in Minimized_Or_Eliminated);
+
+      Lo, Hi : Uint;
+      --  Ranges of values for result
+
+   begin
+      --  Nothing to do if our parent is one of the following:
+
+      --    Another signed integer arithmetic operation
+      --    A membership operation
+      --    A comparison operation
+
+      --  In all these cases, we will process at the higher level (and then
+      --  this node will be processed during the downwards recursion that
+      --  is part of the processing in Minimize_Eliminate_Overflow_Checks.
+
+      if Is_Signed_Integer_Arithmetic_Op (P)
+        or else Nkind (Op) in N_Membership_Test
+        or else Nkind (Op) in N_Op_Compare
+      then
+         return;
+      end if;
+
+      --  Otherwise, we have a top level arithmetic operator node, and this
+      --  is where we commence the special processing for minimize/eliminate.
+
+      Minimize_Eliminate_Overflow_Checks (Op, Lo, Hi);
+
+      --  That call may but does not necessarily change the result type of Op.
+      --  It is the job of this routine to undo such changes, so that at the
+      --  top level, we have the proper type. This "undoing" is a point at
+      --  which a final overflow check may be applied.
+
+      --  If the result type was not fiddled we are all set
+
+      if Etype (Op) = Result_Type then
+         return;
+
+      --  Bignum case
+
+      elsif Etype (Op) = RTE (RE_Bignum) then
+
+         --  We need a sequence that looks like
+
+         --    Rnn : Result_Type;
+
+         --    declare
+         --       M   : Mark_Id := SS_Mark;
+         --    begin
+         --       Rnn := Long_Long_Integer (From_Bignum (Op));
+         --       SS_Release (M);
+         --    end;
+
+         --  This block is inserted (using Insert_Actions), and then the node
+         --  is replaced with a reference to Rnn.
+
+         --  A special case arises if our parent is a conversion node. In this
+         --  case no point in generating a conversion to Result_Type, we will
+         --  let the parent handle this. Note that this special case is not
+         --  just about optimization. Consider
+
+         --      A,B,C : Integer;
+         --      ...
+         --      X := Long_Long_Integer (A * (B ** C));
+
+         --  Now the product may fit in Long_Long_Integer but not in Integer.
+         --  In Minimize/Eliminate mode, we don't want to introduce an overflow
+         --  exception for this intermediate value.
+
+         declare
+            Blk  : constant Node_Id  := Make_Bignum_Block (Loc);
+            Rnn : constant Entity_Id := Make_Temporary (Loc, 'R', Op);
+            RHS : Node_Id;
+
+            Rtype : Entity_Id;
+
+         begin
+            RHS := Convert_From_Bignum (Op);
+
+            if Nkind (P) /= N_Type_Conversion then
+               RHS := Convert_To (Result_Type, Op);
+               Rtype := Result_Type;
+
+               --  Interesting question, do we need a check on that conversion
+               --  operation. Answer, not if we know the result is in range.
+               --  At the moment we are not taking advantage of this. To be
+               --  looked at later ???
+
+            else
+               Rtype := Standard_Long_Long_Integer;
+            end if;
+
+            Insert_Before
+              (First (Statements (Handled_Statement_Sequence (Blk))),
+               Make_Assignment_Statement (Loc,
+                 Name       => New_Occurrence_Of (Rnn, Loc),
+                 Expression => RHS));
+
+            Insert_Actions (Op, New_List (
+              Make_Object_Declaration (Loc,
+                Defining_Identifier => Rnn,
+                Object_Definition   => New_Occurrence_Of (Rtype, Loc)),
+              Blk));
+
+            Rewrite (Op, New_Occurrence_Of (Rnn, Loc));
+            Analyze_And_Resolve (Op);
+         end;
+
+         --  Here if the result is Long_Long_Integer
+
+      else
+         pragma Assert (Etype (Op) = Standard_Long_Long_Integer);
+
+         --  All we need to do here is to convert the result to the proper
+         --  result type. As explained above for the Bignum case, we can
+         --  omit this if our parent is a type conversion.
+
+         if Nkind (P) /= N_Type_Conversion then
+            Convert_To_And_Rewrite (Result_Type, Op);
+         end if;
+
+         Analyze_And_Resolve (Op);
+      end if;
+   end Apply_Arithmetic_Overflow_Minimized_Eliminated;
+
    ----------------------------
    -- Apply_Constraint_Check --
    ----------------------------
@@ -1418,8 +1609,8 @@ 
 
       Cond := Build_Discriminant_Checks (N, T_Typ);
 
-      --  If Lhs is set and is a parameter, then the condition is
-      --  guarded by: lhs'constrained and then (condition built above)
+      --  If Lhs is set and is a parameter, then the condition is guarded by:
+      --  lhs'constrained and then (condition built above)
 
       if Present (Param_Entity (Lhs)) then
          Cond :=
@@ -3358,6 +3549,52 @@ 
       Saved_Checks_TOS := Saved_Checks_TOS - 1;
    end Conditional_Statements_End;
 
+   -------------------------
+   -- Convert_From_Bignum --
+   -------------------------
+
+   function Convert_From_Bignum (N : Node_Id) return Node_Id is
+      Loc : constant Source_Ptr := Sloc (N);
+
+   begin
+      pragma Assert (Is_RTE (Etype (N), RE_Bignum));
+
+      --  Construct call From Bignum
+
+      return
+        Make_Function_Call (Loc,
+          Name                   =>
+            New_Occurrence_Of (RTE (RE_From_Bignum), Loc),
+          Parameter_Associations => New_List (Relocate_Node (N)));
+   end Convert_From_Bignum;
+
+   -----------------------
+   -- Convert_To_Bignum --
+   -----------------------
+
+   function Convert_To_Bignum (N : Node_Id) return Node_Id is
+      Loc : constant Source_Ptr := Sloc (N);
+
+   begin
+      --  Nothing to do if Bignum already
+
+      if Is_RTE (Etype (N), RE_Bignum) then
+         return Relocate_Node (N);
+
+         --  Otherwise construct call to To_Bignum, converting the operand to
+         --  the required Long_Long_Integer form.
+
+      else
+         pragma Assert (Is_Signed_Integer_Type (Etype (N)));
+         return
+           Make_Function_Call (Loc,
+             Name                   =>
+               New_Occurrence_Of (RTE (RE_To_Bignum), Loc),
+             Parameter_Associations => New_List (
+               Convert_To (Standard_Long_Long_Integer, Relocate_Node (N))));
+      end if;
+   end Convert_To_Bignum;
+
    ---------------------
    -- Determine_Range --
    ---------------------
@@ -3945,13 +4182,14 @@ 
    ---------------------------
 
    procedure Enable_Overflow_Check (N : Node_Id) is
-      Typ : constant Entity_Id  := Base_Type (Etype (N));
-      Chk : Nat;
-      OK  : Boolean;
-      Ent : Entity_Id;
-      Ofs : Uint;
-      Lo  : Uint;
-      Hi  : Uint;
+      Typ  : constant Entity_Id           := Base_Type (Etype (N));
+      Mode : constant Overflow_Check_Type := Overflow_Check_Mode (Etype (N));
+      Chk  : Nat;
+      OK   : Boolean;
+      Ent  : Entity_Id;
+      Ofs  : Uint;
+      Lo   : Uint;
+      Hi   : Uint;
 
    begin
       if Debug_Flag_CC then
@@ -3963,22 +4201,48 @@ 
 
       --  No check if overflow checks suppressed for type of node
 
-      if Present (Etype (N))
-        and then Overflow_Checks_Suppressed (Etype (N))
-      then
+      if Mode = Suppressed then
          return;
 
       --  Nothing to do for unsigned integer types, which do not overflow
 
       elsif Is_Modular_Integer_Type (Typ) then
          return;
+      end if;
 
+      --  This is the point at which processing for CHECKED mode diverges from
+      --  processing for MINIMIZED/ELIMINATED mode. This divergence is probably
+      --  more extreme that it needs to be, but what is going on here is that
+      --  when we introduced MINIMIZED/ELININATED modes, we wanted to leave the
+      --  processing for CHECKED mode untouched. There were two reasons for
+      --  this. First it avoided any incomptible change of behavior. Second,
+      --  it guaranteed that CHECKED mode continued to be legacy reliable.
+
+      --  The big difference is that in CHECKED mode there is a fair amount of
+      --  circuitry to try to avoid setting the Do_Overflow_Check flag if we
+      --  know that no check is needed. We skip all that in the two new modes,
+      --  since really overflow checking happens over a whole subtree, and we
+      --  do the corresponding optimizations later on when applying the checks.
+
+      if Mode in Minimized_Or_Eliminated then
+         Activate_Overflow_Check (N);
+
+         if Debug_Flag_CC then
+            w ("Minimized/Eliminated mode");
+         end if;
+
+         return;
+      end if;
+
+      --  Remainder of processing is for Checked case, and is unchanged from
+      --  earlier versions preceding the addition of Minimized/Eliminated.
+
       --  Nothing to do if the range of the result is known OK. We skip this
       --  for conversions, since the caller already did the check, and in any
       --  case the condition for deleting the check for a type conversion is
       --  different.
 
-      elsif Nkind (N) /= N_Type_Conversion then
+      if Nkind (N) /= N_Type_Conversion then
          Determine_Range (N, OK, Lo, Hi, Assume_Valid => True);
 
          --  Note in the test below that we assume that the range is not OK
@@ -5755,6 +6019,23 @@ 
       end;
    end Insert_Valid_Check;
 
+   -------------------------------------
+   -- Is_Signed_Integer_Arithmetic_Op --
+   -------------------------------------
+
+   function Is_Signed_Integer_Arithmetic_Op (N : Node_Id) return Boolean is
+   begin
+      case Nkind (N) is
+         when N_Op_Abs   | N_Op_Add      | N_Op_Divide   | N_Op_Expon |
+              N_Op_Minus | N_Op_Mod      | N_Op_Multiply | N_Op_Plus  |
+              N_Op_Rem   | N_Op_Subtract =>
+            return Is_Signed_Integer_Type (Etype (N));
+
+         when others =>
+            return False;
+      end case;
+   end Is_Signed_Integer_Arithmetic_Op;
+
    ----------------------------------
    -- Install_Null_Excluding_Check --
    ----------------------------------
@@ -6022,6 +6303,61 @@ 
       Possible_Local_Raise (R_Cno, Standard_Constraint_Error);
    end Install_Static_Check;
 
+   -------------------------
+   -- Is_Check_Suppressed --
+   -------------------------
+
+   function Is_Check_Suppressed (E : Entity_Id; C : Check_Id) return Boolean is
+      Ptr : Suppress_Stack_Entry_Ptr;
+
+   begin
+      --  First search the local entity suppress stack. We search this from the
+      --  top of the stack down so that we get the innermost entry that applies
+      --  to this case if there are nested entries.
+
+      Ptr := Local_Suppress_Stack_Top;
+      while Ptr /= null loop
+         if (Ptr.Entity = Empty or else Ptr.Entity = E)
+           and then (Ptr.Check = All_Checks or else Ptr.Check = C)
+         then
+            return Ptr.Suppress;
+         end if;
+
+         Ptr := Ptr.Prev;
+      end loop;
+
+      --  Now search the global entity suppress table for a matching entry.
+      --  We also search this from the top down so that if there are multiple
+      --  pragmas for the same entity, the last one applies (not clear what
+      --  or whether the RM specifies this handling, but it seems reasonable).
+
+      Ptr := Global_Suppress_Stack_Top;
+      while Ptr /= null loop
+         if (Ptr.Entity = Empty or else Ptr.Entity = E)
+           and then (Ptr.Check = All_Checks or else Ptr.Check = C)
+         then
+            return Ptr.Suppress;
+         end if;
+
+         Ptr := Ptr.Prev;
+      end loop;
+
+      --  If we did not find a matching entry, then use the normal scope
+      --  suppress value after all (actually this will be the global setting
+      --  since it clearly was not overridden at any point). For a predefined
+      --  check, we test the specific flag. For a user defined check, we check
+      --  the All_Checks flag. The Overflow flag requires special handling to
+      --  deal with the General vs Assertion case
+
+      if C = Overflow_Check then
+         return Overflow_Checks_Suppressed (Empty);
+      elsif C in Predefined_Check_Id then
+         return Scope_Suppress.Suppress (C);
+      else
+         return Scope_Suppress.Suppress (All_Checks);
+      end if;
+   end Is_Check_Suppressed;
+
    ---------------------
    -- Kill_All_Checks --
    ---------------------
@@ -6080,27 +6416,331 @@ 
       end if;
    end Length_Checks_Suppressed;
 
-   --------------------------------
-   -- Overflow_Checks_Suppressed --
-   --------------------------------
+   -----------------------
+   -- Make_Bignum_Block --
+   -----------------------
 
-   function Overflow_Checks_Suppressed (E : Entity_Id) return Boolean is
+   function Make_Bignum_Block (Loc : Source_Ptr) return Node_Id is
+      M : constant Entity_Id := Make_Defining_Identifier (Loc, Name_uM);
+
    begin
+      return
+        Make_Block_Statement (Loc,
+          Declarations => New_List (
+            Make_Object_Declaration (Loc,
+              Defining_Identifier => M,
+              Object_Definition   =>
+                New_Occurrence_Of (RTE (RE_Mark_Id), Loc),
+              Expression          =>
+                Make_Function_Call (Loc,
+                  Name => New_Reference_To (RTE (RE_SS_Mark), Loc)))),
+
+          Handled_Statement_Sequence =>
+            Make_Handled_Sequence_Of_Statements (Loc,
+              Statements => New_List (
+                Make_Procedure_Call_Statement (Loc,
+                  Name => New_Occurrence_Of (RTE (RE_SS_Release), Loc),
+                  Parameter_Associations => New_List (
+                    New_Reference_To (M, Loc))))));
+   end Make_Bignum_Block;
+
+   ----------------------------------------
+   -- Minimize_Eliminate_Overflow_Checks --
+   ----------------------------------------
+
+   procedure Minimize_Eliminate_Overflow_Checks
+     (N  : Node_Id;
+      Lo : out Uint;
+      Hi : out Uint)
+   is
+      pragma Assert (Is_Signed_Integer_Type (Etype (N)));
+
+      Check_Mode : constant Overflow_Check_Type := Overflow_Check_Mode (Empty);
+      pragma Assert (Check_Mode in Minimized_Or_Eliminated);
+
+      Loc : constant Source_Ptr := Sloc (N);
+
+      Rlo, Rhi : Uint;
+      --  Ranges of values for right operand
+
+      Llo, Lhi : Uint;
+      --  Ranges of values for left operand
+
+      LLLo, LLHi : Uint;
+      --  Bounds of Long_Long_Integer
+
+      Binary : constant Boolean := Nkind (N) in N_Binary_Op;
+      --  Indicates binary operator case
+
+      OK : Boolean;
+      --  Used in call to Determine_Range
+
+   begin
+      --  Case where we do not have an arithmetic operator.
+
+      if not Is_Signed_Integer_Arithmetic_Op (N) then
+
+         --  Use the normal Determine_Range routine to get the range. We
+         --  don't require operands to be valid, invalid values may result in
+         --  rubbish results where the result has not been properly checked for
+         --  overflow, that's fine!
+
+         Determine_Range (N, OK, Lo, Hi, Assume_Valid => False);
+
+         --  If Deterine_Range did not work (can this in fact happen? Not
+         --  clear but might as well protect), use type bounds.
+
+         if not OK then
+            Lo := Intval (Type_Low_Bound  (Base_Type (Etype (N))));
+            Hi := Intval (Type_High_Bound (Base_Type (Etype (N))));
+         end if;
+
+         --  If we don't have a binary operator, all we have to do is to set
+         --  the Hi/Lo range, so we are done
+
+         return;
+
+      --  If we have an arithmetic oeprator we make recursive calls on the
+      --  operands to get the ranges (and to properly process the subtree
+      --  that lies below us!)
+
+      else
+         Minimize_Eliminate_Overflow_Checks (Right_Opnd (N), Rlo, Rhi);
+
+         if Binary then
+            Minimize_Eliminate_Overflow_Checks (Left_Opnd (N), Llo, Lhi);
+         end if;
+      end if;
+
+      --  If either operand is a bignum, then result will be a bignum
+
+      if Rlo = No_Uint or else (Binary and then Llo = No_Uint) then
+         Lo := No_Uint;
+         Hi := No_Uint;
+
+      --  Otherwise compute result range
+
+      else
+         case Nkind (N) is
+
+            --  Absolute value
+
+            when N_Op_Abs =>
+               Lo := Uint_0;
+               Hi := UI_Max (UI_Abs (Rlo), UI_Abs (Rhi));
+
+            --  Addition
+
+            when N_Op_Add =>
+               Lo := Llo + Rlo;
+               Hi := Lhi + Rhi;
+
+            --  Division
+
+            when N_Op_Divide =>
+               raise Program_Error;
+
+            --  Exponentiation
+
+            when N_Op_Expon =>
+               raise Program_Error;
+
+            --  Negation
+
+            when N_Op_Minus =>
+               Lo := -Rhi;
+               Hi := -Rlo;
+
+            --  Mod
+
+            when N_Op_Mod =>
+               raise Program_Error;
+
+            --  Multiplication
+
+            when N_Op_Multiply =>
+               raise Program_Error;
+
+            --  Plus operator (affirmation)
+
+            when N_Op_Plus =>
+               Lo := Rlo;
+               Hi := Rhi;
+
+            --  Remainder
+
+            when N_Op_Rem =>
+               raise Program_Error;
+
+            --  Subtract
+
+            when N_Op_Subtract =>
+               Lo := Llo - Rhi;
+               Hi := Lhi - Rlo;
+
+            --  Nothing else should be possible
+
+            when others =>
+               raise Program_Error;
+
+         end case;
+      end if;
+
+      --  Case where we do the operation in Bignum mode. This happens either
+      --  because one of our operands is in Bignum mode already, or because
+      --  the computed bounds are outside the bounds of Long_Long_Integer.
+
+      --  Note: we could do better here and in some cases switch back from
+      --  Bignum mode to normal mode, e.g. big mod 2 must be in the range
+      --  0 .. 1, but the cases are rare and it is not worth the effort.
+      --  Failing to do this switching back is only an efficiency issue.
+
+      LLLo := Intval (Type_Low_Bound  (Standard_Long_Long_Integer));
+      LLHi := Intval (Type_High_Bound (Standard_Long_Long_Integer));
+
+      if Lo = No_Uint or else Lo < LLLo or else Hi > LLHi then
+
+         --  In MINIMIZED mode, just give up and apply an overflow check
+         --  Note that we know we don't have a Bignum, since Bignums only
+         --  appear in Eliminated mode.
+
+         if Check_Mode = Minimized then
+            pragma Assert (Lo /= No_Uint);
+            Enable_Overflow_Check (N);
+
+            --  It's fine to just return here, we may generate an overflow
+            --  exception, but this is the case in MINIMIZED mode where we
+            --  can't avoid this possibility.
+
+            Apply_Arithmetic_Overflow_Normal (N);
+            return;
+
+         --  Otherwise we are in ELIMINATED mode, switch to bignum
+
+         else
+            pragma Assert (Check_Mode = Eliminated);
+
+            declare
+               Fent : Entity_Id;
+               Args : List_Id;
+
+            begin
+               case Nkind (N) is
+                  when N_Op_Abs      =>
+                     Fent := RTE (RE_Big_Abs);
+
+                  when N_Op_Add      =>
+                     Fent := RTE (RE_Big_Add);
+
+                  when N_Op_Divide   =>
+                     Fent := RTE (RE_Big_Div);
+
+                  when N_Op_Expon    =>
+                     Fent := RTE (RE_Big_Exp);
+
+                  when N_Op_Minus    =>
+                     Fent := RTE (RE_Big_Neg);
+
+                  when N_Op_Mod      =>
+                     Fent := RTE (RE_Big_Mod);
+
+                  when N_Op_Multiply =>
+                     Fent := RTE (RE_Big_Mul);
+
+                  when N_Op_Rem      =>
+                     Fent := RTE (RE_Big_Rem);
+
+                  when N_Op_Subtract =>
+                     Fent := RTE (RE_Big_Sub);
+
+                  --  Anything else is an internal error, this includes the
+                  --  N_Op_Plus case, since how can plus cause the result
+                  --  to be out of range if the operand is in range?
+
+                  when others =>
+                     raise Program_Error;
+               end case;
+
+               --  Construct argument list for Bignum call, converting our
+               --  operands to Bignum form if they are not already there.
+
+               Args := New_List;
+
+               if Binary then
+                  Append_To (Args, Convert_To_Bignum (Left_Opnd (N)));
+               end if;
+
+               Append_To (Args, Convert_To_Bignum (Right_Opnd (N)));
+
+               --  Now rewrite the arithmetic operator with a call to the
+               --  corresponding bignum function.
+
+               Rewrite (N,
+                 Make_Function_Call (Loc,
+                   Name                   => New_Occurrence_Of (Fent, Loc),
+                   Parameter_Associations => Args));
+               Analyze_And_Resolve (N, RTE (RE_Bignum));
+            end;
+         end if;
+
+      --  Otherwise we are in range of Long_Long_Integer, so no overflow
+      --  check is required, at least not yet. Adjust the operands to
+      --  Long_Long_Integer and mark the result type as Long_Long_Integer.
+
+      else
+         Convert_To_And_Rewrite
+           (Standard_Long_Long_Integer, Right_Opnd (N));
+
+         if Binary then
+            Convert_To_And_Rewrite
+              (Standard_Long_Long_Integer, Left_Opnd (N));
+         end if;
+
+         Set_Etype (N, Standard_Long_Long_Integer);
+
+         --  Clear entity field, since we have modified the type and mark
+         --  the node as analyzed to prevent junk infinite recursion
+
+         Set_Entity (N, Empty);
+         Set_Analyzed (N, True);
+
+         --  Turn off the overflow check flag, since this is precisely the
+         --  case where we have avoided an intermediate overflow check.
+
+         Set_Do_Overflow_Check (N, False);
+      end if;
+   end Minimize_Eliminate_Overflow_Checks;
+
+   -------------------------
+   -- Overflow_Check_Mode --
+   -------------------------
+
+   function Overflow_Check_Mode (E : Entity_Id) return Overflow_Check_Type is
+   begin
       --  Check overflow suppressed on entity
 
       if Present (E) and then Checks_May_Be_Suppressed (E) then
          if Is_Check_Suppressed (E, Overflow_Check) then
-            return True;
+            return Suppressed;
          end if;
       end if;
 
       --  Else return appropriate scope setting
 
       if In_Assertion_Expr = 0 then
-         return Scope_Suppress.Overflow_Checks_General = Suppressed;
+         return Scope_Suppress.Overflow_Checks_General;
       else
-         return Scope_Suppress.Overflow_Checks_Assertions = Suppressed;
+         return Scope_Suppress.Overflow_Checks_Assertions;
       end if;
+   end Overflow_Check_Mode;
+
+   --------------------------------
+   -- Overflow_Checks_Suppressed --
+   --------------------------------
+
+   function Overflow_Checks_Suppressed (E : Entity_Id) return Boolean is
+   begin
+      return Overflow_Check_Mode (E) = Suppressed;
    end Overflow_Checks_Suppressed;
 
    -----------------------------
Index: checks.ads
===================================================================
--- checks.ads	(revision 191900)
+++ checks.ads	(working copy)
@@ -67,6 +67,18 @@ 
    --  reason we insist on specifying Empty is to force the caller to think
    --  about whether there is any relevant entity that should be checked.
 
+   function Is_Check_Suppressed (E : Entity_Id; C : Check_Id) return Boolean;
+   --  This function is called if Checks_May_Be_Suppressed (E) is True to
+   --  determine whether check C is suppressed either on the entity E or
+   --  as the result of a scope suppress pragma. If Checks_May_Be_Suppressed
+   --  is False, then the status of the check can be determined simply by
+   --  examining Scope_Checks (C), so this routine is not called in that case.
+
+   function Overflow_Check_Mode (E : Entity_Id) return Overflow_Check_Type;
+   --  Returns current overflow checking mode, taking into account whether
+   --  we are inside an assertion expression. Always returns Suppressed if
+   --  overflow checks are suppressed for entity E.
+
    -------------------------------------------
    -- Procedures to Activate Checking Flags --
    -------------------------------------------
@@ -164,14 +176,6 @@ 
    --  for Typ, if Typ has a predicate function. The check is applied only
    --  if the type of N does not match Typ.
 
-   function Build_Discriminant_Checks
-     (N     : Node_Id;
-      T_Typ : Entity_Id)
-      return  Node_Id;
-   --  Subsidiary routine for Apply_Discriminant_Check. Builds the expression
-   --  that compares discriminants of the expression with discriminants of the
-   --  type. Also used directly for membership tests (see Exp_Ch4.Expand_N_In).
-
    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
@@ -194,6 +198,25 @@ 
    --  result type. This routine deals with range and overflow checks needed
    --  to make sure that the universal result is in range.
 
+   function Build_Discriminant_Checks
+     (N     : Node_Id;
+      T_Typ : Entity_Id)
+      return  Node_Id;
+   --  Subsidiary routine for Apply_Discriminant_Check. Builds the expression
+   --  that compares discriminants of the expression with discriminants of the
+   --  type. Also used directly for membership tests (see Exp_Ch4.Expand_N_In).
+
+   function Convert_From_Bignum (N : Node_Id) return Node_Id;
+   --  Returns result of converting node N from Bignum. The returned value is
+   --  not analyzed, the caller takes responsibility for this. Node N must be
+   --  a subexpression node of type Bignum. The result is Long_Long_Integer.
+
+   function Convert_To_Bignum (N : Node_Id) return Node_Id;
+   --  Returns result of converting node N to Bignum. The returned value is not
+   --  analyzed, the caller takes responsibility for this. Node N must be a
+   --  subexpression node of a signed integer type or Bignum type (if it is
+   --  already a Bignnum, the returned value is Relocate_Node (N).
+
    procedure Determine_Range
      (N            : Node_Id;
       OK           : out Boolean;
@@ -218,6 +241,86 @@ 
    --  Determines whether an access node requires a runtime access check and
    --  if so inserts the appropriate run-time check.
 
+   function Make_Bignum_Block (Loc : Source_Ptr) return Node_Id;
+   --  This function is used by top level overflow checking routines to do a
+   --  mark/release operation on the secondary stack around bignum operations.
+   --  The block created looks like:
+   --
+   --    declare
+   --       M : Mark_Id := SS_Mark;
+   --    begin
+   --       SS_Release (M);
+   --    end;
+   --
+   --  The idea is that the caller will insert any needed extra declarations
+   --  after the declaration of M, and any needed statements (in particular
+   --  the bignum operations) before the call to SS_Release, and then do an
+   --  Insert_Action of the whole block (it is returned unanalyzed). The Loc
+   --  parameter is used to supply Sloc values for the constructed tree.
+
+   procedure Minimize_Eliminate_Overflow_Checks
+     (N  : Node_Id;
+      Lo : out Uint;
+      Hi : out Uint);
+   --  This is the main routine for handling MINIMIZED and ELIMINATED overflow
+   --  checks. On entry N is a node whose result is a signed integer subtype.
+   --  If the node is an artihmetic operation, then a range analysis is carried
+   --  out, and there are three possibilities:
+   --
+   --    The node is left unchanged (apart from expansion of an exponentiation
+   --    operation). This happens if the routine can determine that the result
+   --    is definitely in range. The Do_Overflow_Check flag is turned off in
+   --    this case.
+   --
+   --    The node is transformed into an arithmetic operation with a result
+   --    type of Long_Long_Integer.
+   --
+   --    The node is transformed into a function call that calls an appropriate
+   --    function in the System.Bignums package to compute a Bignum result.
+   --
+   --  In the first two cases, Lo and Hi are set to the bounds of the possible
+   --  range of results, computed as accurately as possible. In the third case
+   --  Lo and Hi are set to No_Uint (there are some cases where we cold get an
+   --  advantage from keeping result ranges for Bignum values, but it could use
+   --  a lot of space and is very unlikely to be valuable).
+   --
+   --  If the node is not an arithmetic operation, then it is unchanged but
+   --  Lo and Hi are still set (to the bounds of the result subtype if nothing
+   --  better can be determined.
+   --
+   --  Note: this function is recursive, if called with an arithmetic operator,
+   --  recursive calls are made to process the operands using this procedure.
+   --  So we end up doing things top down. Nothing happens to an arithmetic
+   --  expression until this procedure is called on the top level node and
+   --  then the recursive calls process all the children. We have to do it
+   --  this way. If we try to do it bottom up in natural expansion order, then
+   --  there are two problems. First, where do we stash the bounds, and more
+   --  importantly, semantic processing will be messed up. Consider A+B+C where
+   --  A,B,C are all of type integer, if we processed A+B before doing semantic
+   --  analysis of the addition of this result to C, that addition could end up
+   --  with a Long_Long_Integer left operand and an Integer right operand, and
+   --  we would get a semantic error.
+   --
+   --  The routine is called in three situations if we are operating in
+   --  either MINIMIZED or ELIMINATED modes.
+   --
+   --    Overflow checks applied to the top node of an expression tree when
+   --    that node is an arithmetic operator. In this case the result is
+   --    converted to the appropriate result type (there is special processing
+   --    when the parent is a conversion, see body for details).
+   --
+   --    Overflow checks are applied to the operands of a comparison operation.
+   --    In this case, the comparison is done on the result Long_Long_Integer
+   --    or Bignum values, without raising any exceptions.
+   --
+   --    Overflow checks are applied to the left operand of a membership test.
+   --    In this case no exception is raised if a Long_Long_Integer or Bignum
+   --    result is outside the range of the type of that left operand (it is
+   --    just that the result of IN is false in that case).
+   --
+   --  Note that if Bignum values appear, the caller must take care of doing
+   --  the appropriate mark/release operation on the secondary stack.
+
    -------------------------------------------------------
    -- Control and Optimization of Range/Overflow Checks --
    -------------------------------------------------------
@@ -248,7 +351,9 @@ 
    --  has no effect. If a check is needed then this routine sets the flag
    --  Do_Overflow_Check in node N to True, unless it can be determined that
    --  the check is not needed. The only condition under which this is the
-   --  case is if there was an identical check earlier on.
+   --  case is if there was an identical check earlier on. These optimziations
+   --  apply to CHECKED mode, but not to MINIMIZED/ELIMINATED modes. See the
+   --  body for a full explanation.
 
    procedure Enable_Range_Check (N : Node_Id);
    --  Set Do_Range_Check flag in node N True, unless it can be determined
Index: sem_prag.adb
===================================================================
--- sem_prag.adb	(revision 191910)
+++ sem_prag.adb	(working copy)
@@ -5685,8 +5685,8 @@ 
                Scope_Suppress.Overflow_Checks_General    := Suppressed;
                Scope_Suppress.Overflow_Checks_Assertions := Suppressed;
             else
-               Scope_Suppress.Overflow_Checks_General    := Minimized;
-               Scope_Suppress.Overflow_Checks_Assertions := Minimized;
+               Scope_Suppress.Overflow_Checks_General    := Checked;
+               Scope_Suppress.Overflow_Checks_Assertions := Checked;
             end if;
          end if;
 
Index: sem.adb
===================================================================
--- sem.adb	(revision 191895)
+++ sem.adb	(working copy)
@@ -1218,59 +1218,6 @@ 
       end if;
    end Insert_List_Before_And_Analyze;
 
-   -------------------------
-   -- Is_Check_Suppressed --
-   -------------------------
-
-   function Is_Check_Suppressed (E : Entity_Id; C : Check_Id) return Boolean is
-
-      Ptr : Suppress_Stack_Entry_Ptr;
-
-   begin
-      --  First search the local entity suppress stack. We search this from the
-      --  top of the stack down so that we get the innermost entry that applies
-      --  to this case if there are nested entries.
-
-      Ptr := Local_Suppress_Stack_Top;
-      while Ptr /= null loop
-         if (Ptr.Entity = Empty or else Ptr.Entity = E)
-           and then (Ptr.Check = All_Checks or else Ptr.Check = C)
-         then
-            return Ptr.Suppress;
-         end if;
-
-         Ptr := Ptr.Prev;
-      end loop;
-
-      --  Now search the global entity suppress table for a matching entry.
-      --  We also search this from the top down so that if there are multiple
-      --  pragmas for the same entity, the last one applies (not clear what
-      --  or whether the RM specifies this handling, but it seems reasonable).
-
-      Ptr := Global_Suppress_Stack_Top;
-      while Ptr /= null loop
-         if (Ptr.Entity = Empty or else Ptr.Entity = E)
-           and then (Ptr.Check = All_Checks or else Ptr.Check = C)
-         then
-            return Ptr.Suppress;
-         end if;
-
-         Ptr := Ptr.Prev;
-      end loop;
-
-      --  If we did not find a matching entry, then use the normal scope
-      --  suppress value after all (actually this will be the global setting
-      --  since it clearly was not overridden at any point). For a predefined
-      --  check, we test the specific flag. For a user defined check, we check
-      --  the All_Checks flag.
-
-      if C in Predefined_Check_Id then
-         return Scope_Suppress.Suppress (C);
-      else
-         return Scope_Suppress.Suppress (All_Checks);
-      end if;
-   end Is_Check_Suppressed;
-
    ----------
    -- Lock --
    ----------
Index: sem.ads
===================================================================
--- sem.ads	(revision 191897)
+++ sem.ads	(working copy)
@@ -641,13 +641,6 @@ 
    --  This function returns True if an explicit pragma Suppress for check C
    --  is present in the package defining E.
 
-   function Is_Check_Suppressed (E : Entity_Id; C : Check_Id) return Boolean;
-   --  This function is called if Checks_May_Be_Suppressed (E) is True to
-   --  determine whether check C is suppressed either on the entity E or
-   --  as the result of a scope suppress pragma. If Checks_May_Be_Suppressed
-   --  is False, then the status of the check can be determined simply by
-   --  examining Scope_Checks (C), so this routine is not called in that case.
-
    procedure Preanalyze (N : Node_Id);
    --  Performs a pre-analysis of node N. During pre-analysis no expansion is
    --  carried out for N or its children. For more info on pre-analysis read
Index: tbuild.adb
===================================================================
--- tbuild.adb	(revision 191888)
+++ tbuild.adb	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -129,6 +129,15 @@ 
       end if;
    end Convert_To;
 
+   ----------------------------
+   -- Convert_To_And_Rewrite --
+   ----------------------------
+
+   procedure Convert_To_And_Rewrite (Typ : Entity_Id; Expr : Node_Id) is
+   begin
+      Rewrite (Expr, Convert_To (Typ, Expr));
+   end Convert_To_And_Rewrite;
+
    ------------------
    -- Discard_List --
    ------------------
Index: tbuild.ads
===================================================================
--- tbuild.ads	(revision 191888)
+++ tbuild.ads	(working copy)
@@ -6,7 +6,7 @@ 
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 1992-2011, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2012, Free Software Foundation, Inc.         --
 --                                                                          --
 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
 -- terms of the  GNU General Public License as published  by the Free Soft- --
@@ -48,6 +48,12 @@ 
    --  Exp. This means that it is safe to replace a node by a Convert_To
    --  of itself to some other type.
 
+   procedure Convert_To_And_Rewrite (Typ : Entity_Id; Expr : Node_Id);
+   pragma Inline (Convert_To_And_Rewrite);
+   --  Like the function, except that there is an extra step of calling
+   --  Rewrite on the Expr node and replacing it with the converted result.
+   --  As noted above, this is safe, because Relocate_Node is called.
+
    procedure Discard_Node (N : Node_Or_Entity_Id);
    pragma Inline (Discard_Node);
    --  This is a dummy procedure that simply returns and does nothing. It is
Index: rtsfind.ads
===================================================================
--- rtsfind.ads	(revision 191888)
+++ rtsfind.ads	(working copy)
@@ -213,6 +213,7 @@ 
       System_Assertions,
       System_Atomic_Primitives,
       System_Aux_DEC,
+      System_Bignums,
       System_Bit_Ops,
       System_Boolean_Array_Operations,
       System_Byte_Swapping,
@@ -759,6 +760,27 @@ 
      RE_Type_Class_Task,                 -- System.Aux_DEC
      RE_Type_Class_Address,              -- System.Aux_DEC
 
+     RE_Big_Abs,                         -- System.Bignums
+     RE_Big_Add,                         -- System.Bignums
+     RE_Big_Div,                         -- System.Bignums
+     RE_Big_Exp,                         -- System.Bignums
+     RE_Big_Mod,                         -- System.Bignums
+     RE_Big_Mul,                         -- System.Bignums
+     RE_Big_Neg,                         -- System.Bignums
+     RE_Big_Rem,                         -- System.Bignums
+     RE_Big_Sub,                         -- System.Bignums
+
+     RE_Big_EQ,                          -- System.Bignums
+     RE_Big_GE,                          -- System.Bignums
+     RE_Big_GT,                          -- System.Bignums
+     RE_Big_LE,                          -- System.Bignums
+     RE_Big_LT,                          -- System.Bignums
+     RE_Big_NE,                          -- System.Bignums
+
+     RE_Bignum,                          -- System.Bignums
+     RE_To_Bignum,                       -- System.Bignums
+     RE_From_Bignum,                     -- System.Bignums
+
      RE_Bit_And,                         -- System.Bit_Ops
      RE_Bit_Eq,                          -- System.Bit_Ops
      RE_Bit_Not,                         -- System.Bit_Ops
@@ -783,18 +805,14 @@ 
      RE_Compare_Array_S8_Unaligned,      -- System.Compare_Array_Signed_8
 
      RE_Compare_Array_S16,               -- System.Compare_Array_Signed_16
-
      RE_Compare_Array_S32,               -- System.Compare_Array_Signed_16
-
      RE_Compare_Array_S64,               -- System.Compare_Array_Signed_16
 
      RE_Compare_Array_U8,                -- System.Compare_Array_Unsigned_8
      RE_Compare_Array_U8_Unaligned,      -- System.Compare_Array_Unsigned_8
 
      RE_Compare_Array_U16,               -- System.Compare_Array_Unsigned_16
-
      RE_Compare_Array_U32,               -- System.Compare_Array_Unsigned_16
-
      RE_Compare_Array_U64,               -- System.Compare_Array_Unsigned_16
 
      RE_Str_Concat_2,                    -- System.Concat_2
@@ -1985,6 +2003,27 @@ 
      RE_Type_Class_Task                  => System_Aux_DEC,
      RE_Type_Class_Address               => System_Aux_DEC,
 
+     RE_Big_Abs                          => System_Bignums,
+     RE_Big_Add                          => System_Bignums,
+     RE_Big_Div                          => System_Bignums,
+     RE_Big_Exp                          => System_Bignums,
+     RE_Big_Mod                          => System_Bignums,
+     RE_Big_Mul                          => System_Bignums,
+     RE_Big_Neg                          => System_Bignums,
+     RE_Big_Rem                          => System_Bignums,
+     RE_Big_Sub                          => System_Bignums,
+
+     RE_Big_EQ                           => System_Bignums,
+     RE_Big_GE                           => System_Bignums,
+     RE_Big_GT                           => System_Bignums,
+     RE_Big_LE                           => System_Bignums,
+     RE_Big_LT                           => System_Bignums,
+     RE_Big_NE                           => System_Bignums,
+
+     RE_Bignum                           => System_Bignums,
+     RE_To_Bignum                        => System_Bignums,
+     RE_From_Bignum                      => System_Bignums,
+
      RE_Bit_And                          => System_Bit_Ops,
      RE_Bit_Eq                           => System_Bit_Ops,
      RE_Bit_Not                          => System_Bit_Ops,
Index: sem_res.adb
===================================================================
--- sem_res.adb	(revision 191910)
+++ sem_res.adb	(working copy)
@@ -4965,10 +4965,7 @@ 
            ("operation should be qualified or explicitly converted", N);
       end if;
 
-      --  Set overflow and division checking bit. Much cleverer code needed
-      --  here eventually and perhaps the Resolve routines should be separated
-      --  for the various arithmetic operations, since they will need
-      --  different processing. ???
+      --  Set overflow and division checking bit
 
       if Nkind (N) in N_Op then
          if not Overflow_Checks_Suppressed (Etype (N)) then
Index: exp_ch4.adb
===================================================================
--- exp_ch4.adb	(revision 191910)
+++ exp_ch4.adb	(working copy)
@@ -4867,9 +4867,16 @@ 
 
          Analyze_And_Resolve (N, Restyp);
 
-         Error_Msg_N ("?explicit membership test may be optimized away", N);
-         Error_Msg_N -- CODEFIX
-           ("\?use ''Valid attribute instead", N);
+         --  Give warning unless overflow checking is MINIMIZED or ELIMINATED,
+         --  in which case, this usage makes sense, and in any case, we have
+         --  actually eliminated the danger of optimization above.
+
+         if Overflow_Check_Mode (Restyp) not in Minimized_Or_Eliminated then
+            Error_Msg_N ("?explicit membership test may be optimized away", N);
+            Error_Msg_N -- CODEFIX
+              ("\?use ''Valid attribute instead", N);
+         end if;
+
          return;
       end Substitute_Valid_Check;
 
Index: s-bignum.ads
===================================================================
--- s-bignum.ads	(revision 0)
+++ s-bignum.ads	(revision 0)
@@ -0,0 +1,102 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                       S Y S T E M . B I G N U M S                        --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--            Copyright (C) 2012, Free Software Foundation, Inc.            --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package provides arbitrary precision signed integer arithmetic for
+--  use in computing intermediate values in expressions for the case where
+--  pragma Overflow_Check (Eliminate) is in effect.
+
+with Interfaces;
+
+package System.Bignums is
+
+   subtype Length is Natural range 0 .. 2 ** 23 - 1;
+   --  Represent number of words in Digit_Vector
+
+   Base : constant := 2 ** 32;
+   --  Digit vectors use this base
+
+   subtype SD is Interfaces.Unsigned_32;
+   --  Single length digit
+
+   type Digit_Vector is array (Length range <>) of SD;
+   --  Represent digits of a number (most significant digit first)
+
+   type Bignum_Data (Len : Length) is record
+      Neg : Boolean;
+      --  Set if value is negative, never set for zero
+
+      D : Digit_Vector (1 .. Len);
+      --  Digits of number, most significant first, represented in base
+      --  2**Base. No leading zeroes are stored, and the value of zero is
+      --  represented using an empty vector for D.
+   end record;
+
+   for Bignum_Data use record
+      Len at 0 range 0 .. 23;
+      Neg at 3 range 0 .. 7;
+   end record;
+
+   type Bignum is access all Bignum_Data;
+
+   --  Note: none of the subprograms in this package modify the Bignum_Data
+   --  records referenced by Bignum arguments of mode IN.
+
+   function Big_Add (X, Y : Bignum) return Bignum;  --  "+"
+   function Big_Sub (X, Y : Bignum) return Bignum;  --  "-"
+   function Big_Mul (X, Y : Bignum) return Bignum;  --  "*"
+   function Big_Div (X, Y : Bignum) return Bignum;  --  "/"
+   function Big_Exp (X, Y : Bignum) return Bignum;  --  "**"
+   function Big_Mod (X, Y : Bignum) return Bignum;  --  "mod"
+   function Big_Rem (X, Y : Bignum) return Bignum;  --  "rem"
+   function Big_Neg (X    : Bignum) return Bignum;  --  "-"
+   function Big_Abs (X    : Bignum) return Bignum;  --  "abs"
+   --  Perform indicated arithmetic operation on bignum values. No exception
+   --  raised except for Div/Mod/Rem by 0 which raises Constraint_Error with
+   --  an appropriate message.
+
+   function Big_EQ  (X, Y : Bignum) return Boolean;  -- "="
+   function Big_NE  (X, Y : Bignum) return Boolean;  -- "/="
+   function Big_GE  (X, Y : Bignum) return Boolean;  -- ">="
+   function Big_LE  (X, Y : Bignum) return Boolean;  -- "<="
+   function Big_GT  (X, Y : Bignum) return Boolean;  --  ">"
+   function Big_LT  (X, Y : Bignum) return Boolean;  --  "<"
+   --  Perform indicated comparison on bignums, returning result as Boolean.
+   --  No exception raised for any input arguments.
+
+   function To_Bignum (X : Long_Long_Integer) return Bignum;
+   --  Convert Long_Long_Integer to Bignum. No exception can be raised for any
+   --  input argument.
+
+   function From_Bignum (X : Bignum) return Long_Long_Integer;
+   --  Convert Bignum to Long_Long_Integer. Constraint_Error raised with
+   --  appropriate message if value is out of range of Long_Long_Integer.
+
+end System.Bignums;
Index: s-bignum.adb
===================================================================
--- s-bignum.adb	(revision 0)
+++ s-bignum.adb	(revision 0)
@@ -0,0 +1,1005 @@ 
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                       S Y S T E M . B I G N U M S                        --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--            Copyright (C) 2012, Free Software Foundation, Inc.            --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+--                                                                          --
+-- GNAT was originally developed  by the GNAT team at  New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package provides arbitrary precision signed integer arithmetic for
+--  use in computing intermediate values in expressions for the case where
+--  pragma Overflow_Check (Eliminate) is in effect.
+
+with System;                  use System;
+with System.Secondary_Stack;  use System.Secondary_Stack;
+with System.Storage_Elements; use System.Storage_Elements;
+
+with Unchecked_Conversion;
+
+package body System.Bignums is
+
+   use Interfaces;
+   --  So that operations on Unsigned_32 are available
+
+   type DD is mod SD'Modulus ** 2;
+   --  Double length digit used for intermediate computations
+
+   function MSD (X : DD) return SD is (SD (X / Base));
+   function LSD (X : DD) return SD is (SD (X mod Base));
+   --  Most significant and least significant digit of double digit value
+
+   function "&" (X, Y : SD) return DD is (DD (X) * Base + DD (Y));
+   --  Compose double digit value from two single digit values
+
+   subtype LLI is Long_Long_Integer;
+
+   One_Data : constant Digit_Vector (1 .. 1) := (1 => 1);
+   --  Constant one
+
+   Zero_Data : constant Digit_Vector (1 .. 0) := (1 .. 0 => 0);
+   --  Constant zero
+
+   -----------------------
+   -- Local Subprograms --
+   -----------------------
+
+   function Add (X, Y : Digit_Vector; X_Neg, Y_Neg : Boolean) return Bignum
+   with Pre => X'First = 1 and then Y'First = 1;
+   --  This procedure adds two signed numbers returning the Sum, it is used
+   --  for both addition and subtraction. The value computed is X + Y, with
+   --  X_Neg and Y_Neg giving the signs of the operands.
+
+   function Allocate_Bignum (Len : Length) return Bignum
+   with Post => Allocate_Bignum'Result.Len = Len;
+   --  Allocate Bignum value of indicated length on secondary stack. On return
+   --  the Neg and D fields are left uninitialized.
+
+   type Compare_Result is (LT, EQ, GT);
+   --  Indicates result of comparison in following call
+
+   function Compare
+     (X, Y         : Digit_Vector;
+      X_Neg, Y_Neg : Boolean) return Compare_Result
+   with Pre => X'First = 1 and then X'Last = 1;
+   --  Compare (X with sign X_Neg) with (Y with sign Y_Neg), and return the
+   --  result of the signed comparison.
+
+   procedure Div_Rem
+     (X, Y              : Bignum;
+      Quotient          : out Bignum;
+      Remainder         : out Bignum;
+      Discard_Quotient  : Boolean := False;
+      Discard_Remainder : Boolean := False);
+   --  Returns the Quotient and Remainder from dividing abs (X) by abs (Y). The
+   --  values of X and Y are not modified. If Discard_Quotient is True, then
+   --  Quotient is undefined on return, and if Discard_Remainder is True, then
+   --  Remainder is undefined on return. Service routine for Big_Div/Rem/Mod.
+
+   procedure Free_Bignum (X : Bignum) is null;
+   --  Called to free a Bignum value used in intermediate computations. In
+   --  this implementation using the secondary stack, does nothing at all,
+   --  because we rely on Mark/Release, but it may be of use for some
+   --  alternative implementation.
+
+   function Normalize
+     (X   : Digit_Vector;
+      Neg : Boolean := False) return Bignum
+   with Pre  => X'First = 1;
+   --  Given a digit vector and sign, allocate and construct a Bignum value.
+   --  Note that X may have leading zeroes which must be removed, and if the
+   --  result is zero, the sign is forced positive.
+
+   ---------
+   -- Add --
+   ---------
+
+   function Add (X, Y : Digit_Vector; X_Neg, Y_Neg : Boolean) return Bignum is
+   begin
+      --  If signs are the same we are doing an addition, it is convenient to
+      --  ensure that the first operand is the longer of the two,
+
+      if X_Neg = Y_Neg then
+         if X'Last < Y'Last then
+            return Add (Y => X, X => Y, X_Neg => Y_Neg, Y_Neg => X_Neg);
+
+         --  Here signs are the same, and the first operand is the longer
+
+         else
+            pragma Assert (X_Neg = Y_Neg and then X'Last >= Y'Last);
+
+            --  Do addition, putting result in Sum (allowing for carry)
+
+            declare
+               Sum : Digit_Vector (0 .. X'Last);
+               RD  : DD;
+
+            begin
+               RD := 0;
+               for J in reverse 1 .. X'Last loop
+                  RD := RD + DD (X (J));
+
+                  if J >= 1 + (X'Last - Y'Last)  then
+                     RD := RD + DD (Y (J - (X'Last - Y'Last)));
+                  end if;
+
+                  Sum (J) := LSD (RD);
+                  RD := RD / Base;
+               end loop;
+
+               Sum (0) := SD (RD);
+               return Normalize (Sum, X_Neg);
+            end;
+         end if;
+
+         --  Signs are different so really this is an subtraction, we want to
+         --  make sure that the largest magnitude operand is the first one, and
+         --  then the result will have the sign of the first operand.
+
+      else
+         declare
+            CR : constant Compare_Result := Compare (X, Y, False, False);
+
+         begin
+            if CR = EQ then
+               return Normalize (Zero_Data);
+
+            elsif CR = LT then
+               return Add (Y => X, X => Y, X_Neg => Y_Neg, Y_Neg => X_Neg);
+
+            else
+               pragma Assert (X_Neg /= Y_Neg and then CR = GT);
+
+               --  Do subtraction, putting result in Diff
+
+               declare
+                  Diff : Digit_Vector (1 .. X'Length);
+                  RD    : DD;
+
+               begin
+                  RD := 0;
+                  for J in reverse 1 .. X'Last loop
+                     RD := RD + DD (X (J));
+
+                     if J >= 1 + (X'Last - Y'Last)  then
+                        RD := RD - DD (Y (J - (X'Last - Y'Last)));
+                     end if;
+
+                     Diff (J) := LSD (RD);
+                     RD := (if RD < Base then 0 else -1);
+                  end loop;
+
+                  return Normalize (Diff, X_Neg);
+               end;
+            end if;
+         end;
+      end if;
+   end Add;
+
+   ---------------------
+   -- Allocate_Bignum --
+   ---------------------
+
+   function Allocate_Bignum (Len : Length) return Bignum is
+      Addr : Address;
+
+      --  The following definitions are to allow us to set the discriminant
+
+      type Header is record
+         Len : Length;
+         Neg : Boolean;
+      end record;
+
+      for Header use record
+         Len at 0 range 0 .. 23;
+         Neg at 3 range 0 .. 7;
+      end record;
+
+      type Header_Ptr is access all Header;
+
+      function To_Header_Ptr is new Unchecked_Conversion (Address, Header_Ptr);
+      function To_Bignum     is new Unchecked_Conversion (Address, Bignum);
+
+   begin
+      if True then
+         declare
+            B : Bignum;
+         begin
+            B := new Bignum_Data'(Len, False, (others => 0));
+            return B;
+         end;
+
+      else
+         SS_Allocate (Addr, Storage_Offset (4 + 4 * Len));
+         To_Header_Ptr (Addr).Len := Len;
+         return To_Bignum (Addr);
+      end if;
+   end Allocate_Bignum;
+
+   -------------
+   -- Big_Abs --
+   -------------
+
+   function Big_Abs (X : Bignum) return Bignum is
+   begin
+      return Normalize (X.D);
+   end Big_Abs;
+
+   -------------
+   -- Big_Add --
+   -------------
+
+   function Big_Add  (X, Y : Bignum) return Bignum is
+   begin
+      return Add (X.D, Y.D, X.Neg, Y.Neg);
+   end Big_Add;
+
+   -------------
+   -- Big_Div --
+   -------------
+
+   --  This table is excerpted from RM 4.5.5(28-30) and shows how the result
+   --  varies with the signs of the operands.
+
+   --   A      B   A/B      A     B    A/B
+   --
+   --   10     5    2      -10    5    -2
+   --   11     5    2      -11    5    -2
+   --   12     5    2      -12    5    -2
+   --   13     5    2      -13    5    -2
+   --   14     5    2      -14    5    -2
+   --
+   --   A      B   A/B      A     B    A/B
+   --
+   --   10    -5   -2      -10   -5     2
+   --   11    -5   -2      -11   -5     2
+   --   12    -5   -2      -12   -5     2
+   --   13    -5   -2      -13   -5     2
+   --   14    -5   -2      -14   -5     2
+
+   function Big_Div  (X, Y : Bignum) return Bignum is
+      Q, R : Bignum;
+   begin
+      Div_Rem (X, Y, Q, R, Discard_Remainder => True);
+      Q.Neg := Q.Len > 0 and then (X.Neg xor Y.Neg);
+      return Q;
+   end Big_Div;
+
+   -------------
+   -- Big_Exp --
+   -------------
+
+   function Big_Exp  (X, Y : Bignum) return Bignum is
+
+      function "**" (X : Bignum; Y : SD) return Bignum;
+      --  Internal routine where we know right operand is one word
+
+      ----------
+      -- "**" --
+      ----------
+
+      function "**" (X : Bignum; Y : SD) return Bignum is
+      begin
+         case Y is
+
+            --  X ** 0 is 1
+
+            when 0 =>
+               return Normalize (One_Data);
+
+            --  X ** 1 is X
+
+            when 1 =>
+               return Normalize (X.D);
+
+            --  X ** 2 is X * X
+
+            when 2 =>
+               return Big_Mul (X, X);
+
+            --  For X greater than 2, use the recursion
+
+            --  X even, X ** Y = (X ** (Y/2)) ** 2;
+            --  X odd,  X ** Y = (X ** (Y/2)) ** 2 * X;
+
+            when others =>
+               declare
+                  XY2  : constant Bignum := X ** (Y / 2);
+                  XY2S : constant Bignum := Big_Mul (XY2, XY2);
+                  Res  : Bignum;
+
+               begin
+                  Free_Bignum (XY2);
+
+                  if (Y and 1) = 0 then
+                     return XY2S;
+
+                  else
+                     Res := Big_Mul (XY2S, X);
+                     Free_Bignum (XY2S);
+                     return Res;
+                  end if;
+               end;
+         end case;
+      end "**";
+
+   --  Start of processing for Big_Exp
+
+   begin
+      --  Error if right operand negative
+
+      if Y.Neg then
+         raise Constraint_Error with "exponentiation to negative power";
+
+      --  0 ** X is always 0
+
+      elsif X.Len = 0 then
+         return Normalize (Zero_Data);
+
+      --  (+1) ** Y = 1
+      --  (-1) ** Y = +/-1 depending on whether Y is even or odd
+
+      elsif X.Len = 1 and then X.D (1) = 1 then
+         return Normalize
+           (X.D, Neg => X.Neg and then ((Y.D (Y.Len) and 1) = 1));
+
+      --  If the absolute value of the base is greater than 1, then the
+      --  exponent must not be bigger than one word, otherwise the result
+      --  is ludicrously large, and we just signal Storage_Error right away.
+
+      elsif Y.Len > 1 then
+         raise Storage_Error with "exponentiation result is too large";
+
+      --  Special case (+/-)2 ** K, where K is 31 or less using a shift
+
+      elsif X.Len = 1 and then X.D (1) = 2 and then Y.D (1) < 32 then
+         declare
+            D : constant Digit_Vector (1 .. 1) :=
+                  (1 => Shift_Left (SD'(1), Natural (Y.D (1) - 1)));
+         begin
+            return Normalize (D, X.Neg);
+         end;
+
+      --  Remaining cases have right operand of one word
+
+      else
+         return X ** Y.D (1);
+      end if;
+   end Big_Exp;
+
+   ------------
+   -- Big_EQ --
+   ------------
+
+   function Big_EQ  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) = EQ;
+   end Big_EQ;
+
+   ------------
+   -- Big_GE --
+   ------------
+
+   function Big_GE  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) /= LT;
+   end Big_GE;
+
+   ------------
+   -- Big_GT --
+   ------------
+
+   function Big_GT  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) = GT;
+   end Big_GT;
+
+   ------------
+   -- Big_LE --
+   ------------
+
+   function Big_LE  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) /= GT;
+   end Big_LE;
+
+   ------------
+   -- Big_LT --
+   ------------
+
+   function Big_LT  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) = LT;
+   end Big_LT;
+
+   -------------
+   -- Big_Mod --
+   -------------
+
+   --  This table is excerpted from RM 4.5.5(28-30) and shows how the result
+   --  of Rem and Mod vary with the signs of the operands.
+
+   --   A      B    A mod B  A rem B     A     B    A mod B  A rem B
+
+   --   10     5       0        0       -10    5       0        0
+   --   11     5       1        1       -11    5       4       -1
+   --   12     5       2        2       -12    5       3       -2
+   --   13     5       3        3       -13    5       2       -3
+   --   14     5       4        4       -14    5       1       -4
+
+   --   A      B    A mod B  A rem B     A     B    A mod B  A rem B
+
+   --   10    -5       0        0       -10   -5       0        0
+   --   11    -5      -4        1       -11   -5      -1       -1
+   --   12    -5      -3        2       -12   -5      -2       -2
+   --   13    -5      -2        3       -13   -5      -3       -3
+   --   14    -5      -1        4       -14   -5      -4       -4
+
+   function Big_Mod  (X, Y : Bignum) return Bignum is
+      Q, R : Bignum;
+
+   begin
+      --  If signs are same, result is same as Rem
+
+      if X.Neg = Y.Neg then
+         return Big_Rem (X, Y);
+
+      --  Case where mod is different
+
+      else
+         --  Do division
+
+         Div_Rem (X, Y, Q, R, Discard_Quotient => True);
+
+         --  Zero result is unchanged
+
+         if R.Len = 0 then
+            return R;
+
+         --  Otherwise adjust result
+
+         else
+            declare
+               T1 : constant Bignum := Big_Sub (Y, R);
+            begin
+               T1.Neg := X.Neg;
+               Free_Bignum (R);
+               return T1;
+            end;
+         end if;
+      end if;
+   end Big_Mod;
+
+   -------------
+   -- Big_Mul --
+   -------------
+
+   function Big_Mul (X, Y : Bignum) return Bignum is
+      Result : Digit_Vector (1 .. X.Len + Y.Len) := (others => 0);
+      --  Accumulate result (max length of result is sum of operand lengths)
+
+      L : Length;
+      --  Current result digit
+
+      D : DD;
+      --  Result digit
+
+   begin
+      for J in 1 .. X.Len loop
+         for K in 1 .. Y.Len loop
+            L := Result'Last - (X.Len - J) - (Y.Len - K);
+            D := DD (X.D (J)) * DD (Y.D (K)) + DD (Result (L));
+            Result (L) := LSD (D);
+            D := D / Base;
+
+            --  D is carry which must be propagated
+
+            while D /= 0 and then L >= 1 loop
+               L := L - 1;
+               D := D + DD (Result (L));
+               Result (L) := LSD (D);
+               D := D / Base;
+            end loop;
+
+            --  Must not have a carry trying to extend max length
+
+            pragma Assert (D = 0);
+         end loop;
+      end loop;
+
+      --  Return result
+
+      return Normalize (Result, X.Neg xor Y.Neg);
+   end Big_Mul;
+
+   ------------
+   -- Big_NE --
+   ------------
+
+   function Big_NE  (X, Y : Bignum) return Boolean is
+   begin
+      return Compare (X.D, Y.D, X.Neg, Y.Neg) /= EQ;
+   end Big_NE;
+
+   -------------
+   -- Big_Neg --
+   -------------
+
+   function Big_Neg (X : Bignum) return Bignum is
+   begin
+      return Normalize (X.D, not X.Neg);
+   end Big_Neg;
+
+   -------------
+   -- Big_Rem --
+   -------------
+
+   --  This table is excerpted from RM 4.5.5(28-30) and shows how the result
+   --  varies with the signs of the operands.
+
+   --   A      B   A rem B   A     B   A rem B
+
+   --   10     5      0     -10    5      0
+   --   11     5      1     -11    5     -1
+   --   12     5      2     -12    5     -2
+   --   13     5      3     -13    5     -3
+   --   14     5      4     -14    5     -4
+
+   --   A      B  A rem B    A     B   A rem B
+
+   --   10    -5     0      -10   -5      0
+   --   11    -5     1      -11   -5     -1
+   --   12    -5     2      -12   -5     -2
+   --   13    -5     3      -13   -5     -3
+   --   14    -5     4      -14   -5     -4
+
+   function Big_Rem  (X, Y : Bignum) return Bignum is
+      Q, R : Bignum;
+   begin
+      Div_Rem (X, Y, Q, R, Discard_Quotient => True);
+      R.Neg :=  R.Len > 0 and then X.Neg;
+      return R;
+   end Big_Rem;
+
+   -------------
+   -- Big_Sub --
+   -------------
+
+   function Big_Sub (X, Y : Bignum) return Bignum is
+   begin
+      --  If right operand zero, return left operand
+
+      if Y.Len = 0 then
+         return Normalize (X.D, X.Neg);
+
+      --  Otherwise add negative of right operand
+
+      else
+         return Add (X.D, Y.D, X.Neg, not Y.Neg);
+      end if;
+   end Big_Sub;
+
+   -------------
+   -- Compare --
+   -------------
+
+   function Compare
+     (X, Y         : Digit_Vector;
+      X_Neg, Y_Neg : Boolean) return Compare_Result
+   is
+   begin
+      --  Signs are different, that's decisive, since 0 is always plus
+
+      if X_Neg /= Y_Neg then
+         return (if X_Neg then LT else GT);
+
+      --  Lengths are different, that's decisive since no leading zeroes
+
+      elsif X'Last /= Y'Last then
+         return (if (X'Last > Y'Last) xor X_Neg then GT else LT);
+
+      --  Need to compare data
+
+      else
+         for J in X'Range loop
+            if X (J) /= Y (J) then
+               return (if (X (J) > Y (J)) xor X_Neg then GT else LT);
+            end if;
+         end loop;
+
+         return EQ;
+      end if;
+   end Compare;
+
+   -------------
+   -- Div_Rem --
+   -------------
+
+   procedure Div_Rem
+     (X, Y              : Bignum;
+      Quotient          : out Bignum;
+      Remainder         : out Bignum;
+      Discard_Quotient  : Boolean := False;
+      Discard_Remainder : Boolean := False)
+   is
+   begin
+      --  Error if division by zero
+
+      if Y.Len = 0 then
+         raise Constraint_Error with "division by zero";
+      end if;
+
+      --  Handle simple cases with special tests
+
+      --  If X < Y then quotient is zero and remainder is X
+
+      if Compare (X.D, Y.D, False, False) = LT then
+         Remainder := Normalize (X.D);
+         Quotient := Normalize (Zero_Data);
+         return;
+
+      --  If both X and Y are comfortably less than 2**63-1 we can just use
+      --  Long_Long_Integer arithmetic. Note it is good not to do an accurate
+      --  range check here since -2**63 / -1 overflows!
+
+      elsif (X.Len <= 1 or else (X.Len = 2 and then X.D (1) <= 2**31))
+              and then
+            (Y.Len <= 1 or else (Y.Len = 2 and then Y.D (1) <= 2**31))
+      then
+         declare
+            A : constant LLI := abs (From_Bignum (X));
+            B : constant LLI := abs (From_Bignum (Y));
+         begin
+            Quotient  := To_Bignum (A / B);
+            Remainder := To_Bignum (A rem B);
+            return;
+         end;
+
+      --  Easy case if divisor is one digit
+
+      elsif Y.Len = 1 then
+         declare
+            ND  : DD;
+            Div : constant DD := DD (Y.D (1));
+
+            Result : Digit_Vector (1 .. X.Len);
+            Remdr  : Digit_Vector (1 .. 1);
+
+         begin
+            ND := 0;
+            for J in 1 .. X.Len loop
+               ND := Base * ND + DD (X.D (J));
+               Result (J) := SD (ND / Div);
+               ND := ND rem Div;
+            end loop;
+
+            Quotient := Normalize (Result);
+            Remdr (1) := SD (ND);
+            Remainder := Normalize (Remdr);
+            return;
+         end;
+      end if;
+
+      --  The complex full multi-precision case. We will employ algorithm
+      --  D defined in the section "The Classical Algorithms" (sec. 4.3.1)
+      --  of Donald Knuth's "The Art of Computer Programming", Vol. 2. The
+      --  terminology is adjusted for this section to match that reference.
+
+      --  We are dividing X.Len digits of X (called u here) by Y.Len digits
+      --  of Y (called v here), developing the quotient and remainder. The
+      --  numbers are represented using Base, which was chosen so that we have
+      --  the operations of multiplying to single digits (SD) to form a double
+      --  digit (DD), and dividing a double digit (DD) by a single digit (SD)
+      --  to give a single digit quotient and a single digit remainder.
+
+      --  Algorithm D from Knuth
+
+      --  Comments here with square brackets are directly from Knuth
+
+      Algorithm_D : declare
+
+         --  The following lower case variables correspond exactly to the
+         --  terminology used in algorithm D.
+
+         m : constant Length := X.Len - Y.Len;
+         n : constant Length := Y.Len;
+         b : constant DD     := Base;
+
+         u : Digit_Vector (0 .. m + n);
+         v : Digit_Vector (1 .. n);
+         q : Digit_Vector (0 .. m);
+         r : Digit_Vector (1 .. n);
+
+         u0 : SD renames u (0);
+         v1 : SD renames v (1);
+         v2 : SD renames v (2);
+
+         d    : DD;
+         j    : Length;
+         qhat : SD;
+
+      begin
+         --  Initialize data of left and right operands
+
+         for J in 1 .. m + n loop
+            u (J) := X.D (J);
+         end loop;
+
+         for J in 1 .. n loop
+            v (J) := Y.D (J);
+         end loop;
+
+         --  [Division of nonnegative integers]. Given nonnegative integers u
+         --  = (ul,u2..um+n) and v = (v1,v2..vn), where v1 /= 0 and n > 1, we
+         --  form the quotient u / v = (q0,ql..qm) and the remainder u mod v =
+         --  (r1,r2..rn).
+
+         pragma Assert (v (1) /= 0);
+         pragma Assert (n > 1);
+
+         --  Dl. [Normalize.] Set d = b/(vl + 1). Then set (u0,u1,u2..um+n)
+         --  equal to (u1,u2..um+n) times d, and set (v1,v2..vn) equal to
+         --  (v1,v2..vn) times d. Note the introduction of a new digit position
+         --  u0 at the left of u1; if d = 1 all we need to do in this step is
+         --  to set u0 = 0.
+
+         d := b / DD (v1 + 1);
+
+         if d = 1 then
+            u0 := 0;
+
+         else
+            declare
+               Carry : DD;
+               Tmp   : DD;
+
+            begin
+               --  Multiply Dividend (u) by d
+
+               Carry := 0;
+               for J in reverse 1 .. m + n loop
+                  Tmp   := DD (u (J)) * d + Carry;
+                  u (J) := LSD (Tmp);
+                  Carry := Tmp / Base;
+               end loop;
+
+               u0 := SD (Carry);
+
+               --  Multiply Divisor (v) by d
+
+               Carry := 0;
+               for J in reverse 1 .. n loop
+                  Tmp    := DD (v (J)) * d + Carry;
+                  v (J)  := LSD (Tmp);
+                  Carry  := Tmp / Base;
+               end loop;
+
+               pragma Assert (Carry = 0);
+            end;
+         end if;
+
+         --  D2. [Initialize j.] Set j = 0. The loop on j, steps D2 through D7,
+         --  will be essentially a division of (uj, uj+1..uj+n) by (v1,v2..vn)
+         --  to get a single quotient digit qj;
+
+         j := 0;
+
+         --  Loop through digits
+
+         loop
+            --  D3. [Calculate qhat] If uj = v1, set qhat to b-l; otherwise set
+            --  qhat to (uj,uj+1)/v1.
+
+            if u (j) = v1 then
+               qhat := -1;
+            else
+               qhat := SD ((u (j) & u (j + 1)) / DD (v1));
+            end if;
+
+            --  D3 (continued). Now test if v2 * qhat is greater than (uj*b +
+            --  uj+1 - qhat*v1)*b + uj+2. If so, decrease qhat by 1 and repeat
+            --  this test, which determines at high speed most of the cases in
+            --  which the trial value qhat is one too large, and it eliminates
+            --  all cases where qhat is two too large.
+
+            while DD (v2) * DD (qhat) >
+                   ((u (j) & u (j + 1)) -
+                     DD (qhat) * DD (v1)) * b + DD (u (j + 2))
+            loop
+               qhat := qhat - 1;
+            end loop;
+
+            --  D4. [Multiply and subtract.] Replace (uj,uj+1..uj+n) by
+            --  (uj,uj+1..uj+n) minus qhat times (v1,v2..vn). This step
+            --  consists of a simple multiplication by a one-place number,
+            --  combined with a subtraction.
+
+            --  The digits (uj,uj+1..uj+n) are always kept positive; if the
+            --  result of this step is actually negative then (uj,uj+1..uj+n)
+            --  is left as the true value plus b**(n+1), i.e. as the b's
+            --  complement of the true value, and a "borrow" to the left is
+            --  remembered.
+
+            declare
+               Borrow : SD;
+               Carry  : DD;
+               Temp   : DD;
+
+               Negative : Boolean;
+               --  Records if subtraction causes a negative result, requiring
+               --  an add back (case where qhat turned out to be 1 too large).
+
+            begin
+               Borrow := 0;
+               for K in reverse 1 .. n loop
+                  Temp := DD (qhat) * DD (v (K)) + DD (Borrow);
+                  Borrow := MSD (Temp);
+
+                  if LSD (Temp) > u (j + K) then
+                     Borrow := Borrow + 1;
+                  end if;
+
+                  u (j + K) := u (j + K) - LSD (Temp);
+               end loop;
+
+               Negative := u (j) < Borrow;
+               u (j) := u (j) - Borrow;
+
+               --  D5. [Test remainder.] Set qj = qhat. If the result of step
+               --  D4 was negative, we will do the add back step (step D6).
+
+               q (j) := qhat;
+
+               if Negative then
+
+                  --  D6. [Add back.] Decrease qj by 1, and add (0,v1,v2..vn)
+                  --  to (uj,uj+1,uj+2..uj+n). (A carry will occur to the left
+                  --  of uj, and it is be ignored since it cancels with the
+                  --  borrow that occurred in D4.)
+
+                  q (j) := q (j) - 1;
+
+                  Carry := 0;
+                  for K in reverse 1 .. n loop
+                     Temp := DD (v (K)) + DD (u (j + K)) + Carry;
+                     u (j + K) := LSD (Temp);
+                     Carry := Temp / Base;
+                  end loop;
+
+                  u (j) := u (j) + SD (Carry);
+               end if;
+            end;
+
+            --  D7. [Loop on j.] Increase j by one. Now if j <= m, go back to
+            --  D3 (the start of the loop on j).
+
+            j := j + 1;
+            exit when not (j <= m);
+         end loop;
+
+         --  D8. [Unnormalize.] Now (qo,ql..qm) is the desired quotient, and
+         --  the desired remainder may be obtained by dividing (um+1..um+n)
+         --  by d.
+
+         if not Discard_Quotient then
+            Quotient := Normalize (q);
+         end if;
+
+         if not Discard_Remainder then
+            declare
+               Remdr : DD;
+
+            begin
+               Remdr := 0;
+               for K in 1 .. n loop
+                  Remdr := Base * Remdr + DD (u (m + K));
+                  r (K) := SD (Remdr / d);
+                  Remdr := Remdr rem d;
+               end loop;
+
+               pragma Assert (Remdr = 0);
+            end;
+
+            Remainder := Normalize (r);
+         end if;
+      end Algorithm_D;
+   end Div_Rem;
+
+   -----------------
+   -- From_Bignum --
+   -----------------
+
+   function From_Bignum (X : Bignum) return Long_Long_Integer is
+   begin
+      if X.Len = 0 then
+         return 0;
+
+      elsif X.Len = 1 then
+         return (if X.Neg then -LLI (X.D (1)) else LLI (X.D (1)));
+
+      elsif X.Len = 2 then
+         declare
+            Mag : constant DD := X.D (1) & X.D (2);
+         begin
+            if X.Neg and then Mag <= 2 ** 63 then
+               return -LLI (Mag);
+            elsif Mag < 2 ** 63 then
+               return LLI (Mag);
+            end if;
+         end;
+      end if;
+
+      raise Constraint_Error with "expression value out of range";
+   end From_Bignum;
+
+   ---------------
+   -- Normalize --
+   ---------------
+
+   function Normalize
+     (X   : Digit_Vector;
+      Neg : Boolean := False) return Bignum
+   is
+      B : Bignum;
+      J : Length;
+
+   begin
+      J := X'First;
+      while J <= X'Last and then X (J) = 0 loop
+         J := J + 1;
+      end loop;
+
+      B := Allocate_Bignum (X'Last - J + 1);
+      B.Neg :=  B.Len > 0 and then Neg;
+      B.D := X (J .. X'Last);
+      return B;
+   end Normalize;
+
+   ---------------
+   -- To_Bignum --
+   ---------------
+
+   function To_Bignum (X : Long_Long_Integer) return Bignum is
+      R : Bignum;
+
+   begin
+      if X = 0 then
+         R := Allocate_Bignum (0);
+
+      elsif X in -(2 ** 32 - 1) .. +(2 ** 32 - 1) then
+         R := Allocate_Bignum (1);
+         R.D (1) := SD (abs (X));
+
+      else
+         R := Allocate_Bignum (2);
+         R.D (2) := SD (abs (X) mod Base);
+         R.D (1) := SD (abs (X) / Base);
+      end if;
+
+      R.Neg := X < 0;
+      return R;
+   end To_Bignum;
+
+end System.Bignums;