[Ada] Fix evaluation of expressions in inlined code

[Ada] Fix evaluation of expressions in inlined code

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 1146 bytes --]

In GNATprove mode, inlining is used to make it easier to perform proof
without forcing the user to annotate all local subprograms with
contracts.  But the compiled code will not be similarly inlined, thus
the analysis should not assume that the compiler will have access to the
same extended precision for compile-time computations as is available on
inlined code.  The same is true for frontend inlining in the compiler
(only used with -gnatN or -gnatd.z), as Ada semantics requires in such a
case that run-time checks are still performed. For these reasons,
inlined expressions should always be checked for possible overflows.

Also add the missing compile-time checks for non-static unary
expressions and exponentiation of signed integer type (as unary minus,
absolute value and exponentiation can all lead to an overflow).

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

gcc/ada/

	* sem_eval.adb (Check_Non_Static_Context_For_Overflow): Apply
	compile-time checking for overflows in non-static contexts
	including inlined code.
	(Eval_Arithmetic_Op): Use the new procedure.
	(Eval_Unary_Op, Eval_Op_Expon): Add call to the new procedure.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 3652 bytes --]

diff --git a/gcc/ada/sem_eval.adb b/gcc/ada/sem_eval.adb
--- a/gcc/ada/sem_eval.adb
+++ b/gcc/ada/sem_eval.adb
@@ -142,6 +142,16 @@ package body Sem_Eval is
    -- Local Subprograms --
    -----------------------
 
+   procedure Check_Non_Static_Context_For_Overflow
+     (N      : Node_Id;
+      Stat   : Boolean;
+      Result : Uint);
+   --  For a signed integer type, check non-static overflow in Result when
+   --  Stat is False. This applies also inside inlined code, where the static
+   --  property may be an effect of the inlining, which should not be allowed
+   --  to remove run-time checks (whether during compilation, or even more
+   --  crucially in the special inlining-for-proof in GNATprove mode).
+
    function Choice_Matches
      (Expr   : Node_Id;
       Choice : Node_Id) return Match_Result;
@@ -649,6 +659,34 @@ package body Sem_Eval is
       end if;
    end Check_Non_Static_Context;
 
+   -------------------------------------------
+   -- Check_Non_Static_Context_For_Overflow --
+   -------------------------------------------
+
+   procedure Check_Non_Static_Context_For_Overflow
+     (N      : Node_Id;
+      Stat   : Boolean;
+      Result : Uint)
+   is
+   begin
+      if (not Stat or else In_Inlined_Body)
+        and then Is_Signed_Integer_Type (Etype (N))
+      then
+         declare
+            BT : constant Entity_Id := Base_Type (Etype (N));
+            Lo : constant Uint := Expr_Value (Type_Low_Bound (BT));
+            Hi : constant Uint := Expr_Value (Type_High_Bound (BT));
+         begin
+            if Result < Lo or else Result > Hi then
+               Apply_Compile_Time_Constraint_Error
+                 (N, "value not in range of }??",
+                  CE_Overflow_Check_Failed,
+                  Ent => BT);
+            end if;
+         end;
+      end if;
+   end Check_Non_Static_Context_For_Overflow;
+
    ---------------------------------
    -- Check_String_Literal_Length --
    ---------------------------------
@@ -2143,25 +2181,10 @@ package body Sem_Eval is
 
             if Is_Modular_Integer_Type (Ltype) then
                Result := Result mod Modulus (Ltype);
-
-               --  For a signed integer type, check non-static overflow
-
-            elsif (not Stat) and then Is_Signed_Integer_Type (Ltype) then
-               declare
-                  BT : constant Entity_Id := Base_Type (Ltype);
-                  Lo : constant Uint := Expr_Value (Type_Low_Bound (BT));
-                  Hi : constant Uint := Expr_Value (Type_High_Bound (BT));
-               begin
-                  if Result < Lo or else Result > Hi then
-                     Apply_Compile_Time_Constraint_Error
-                       (N, "value not in range of }??",
-                        CE_Overflow_Check_Failed,
-                        Ent => BT);
-                     return;
-                  end if;
-               end;
             end if;
 
+            Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
             --  If we get here we can fold the result
 
             Fold_Uint (N, Result, Stat);
@@ -3202,6 +3225,8 @@ package body Sem_Eval is
                      Result := Result mod Modulus (Etype (N));
                   end if;
 
+                  Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
                   Fold_Uint (N, Result, Stat);
                end if;
             end;
@@ -4375,6 +4400,8 @@ package body Sem_Eval is
                Result := abs Rint;
             end if;
 
+            Check_Non_Static_Context_For_Overflow (N, Stat, Result);
+
             Fold_Uint (N, Result, Stat);
          end;