[Ada] Improper optimization of range checks

[Ada] Improper optimization of range checks

[Arnaud Charlet]

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

Several static evaluation routines use Determine_Range to establish the bounds
of a non-static expression. If overflow cheks are enabled, the range of the
result of unary and binary operations may raise an exception, and cannot be
assumed to evaluate correctly without a run-time check. This patch prevents
unwarranted optimizations on boolean expressions appearing in preconditions
and other contexts.

The following must execute quietly;

   gcc -c -gnato -gnatDG -gnatc add.ads
   grep true gnat.ads.dg

---
package Add is
   function AddTwo (X, Y : Integer) return Integer;
      Pragma Precondition (X + Y <= Integer'Last);
      Pragma Postcondition (AddTwo'Result = X + Y);
end Add;

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

2011-08-03  Ed Schonberg  <schonberg@adacore.com>

	* checks.adb (Determine_Range): If a computed bound of an operation is
	outside the range of the base type of the expression, and overflow
	checks are enabled, the result is unknown and cannot be used for any
	subsequent constant folding.
	* sem_eval.adb (Compile_Time_Compare): if the bounds of one operand are
	unknown, so is the result of the comparison.


[-- Attachment #2: difs --]
[-- Type: text/plain, Size: 2620 bytes --]

Index: checks.adb
===================================================================
--- checks.adb	(revision 177274)
+++ checks.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -3457,6 +3457,18 @@
       --  the computed expression is in the range Lor .. Hir. We can use this
       --  to restrict the possible range of results.
 
+      --  If one of the computed bounds is outside the range of the base type,
+      --  the expression may raise an exception and we better indicate that
+      --  the evaluation has failed, at least if checks are enabled.
+
+      if Enable_Overflow_Checks
+        and then not Is_Entity_Name (N)
+        and then  (Lor < Lo or else Hir > Hi)
+      then
+         OK := False;
+         return;
+      end if;
+
       if OK1 then
 
          --  If the refined value of the low bound is greater than the type
Index: sem_eval.adb
===================================================================
--- sem_eval.adb	(revision 177274)
+++ sem_eval.adb	(working copy)
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 B o d y                                  --
 --                                                                          --
---          Copyright (C) 1992-2010, Free Software Foundation, Inc.         --
+--          Copyright (C) 1992-2011, 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- --
@@ -964,6 +964,12 @@
                      return Unknown;
                   end if;
                end if;
+            else
+
+               --  If the range of either operand cannot be determined,
+               --  nothing further can be inferred.
+
+               return Unknown;
             end if;
          end;