diff mbox series

[Ada] Fix folding of comparison operators in GNATprove mode

Message ID 20201130141711.GA117748@adacore.com
State New
Headers show
Series [Ada] Fix folding of comparison operators in GNATprove mode | expand

Commit Message

Pierre-Marie de Rodat Nov. 30, 2020, 2:17 p.m. UTC
Folding of comparison operators was disabled for GNATprove in assertion
expressions (except for some special cases). However, folding itself is
harmless. The problem was only in the current value optimizer, which
interferes with assertions that act as cut points for proof.

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

gcc/ada/

	* exp_util.adb (Get_Current_Value_Condition): Don't use current
	value tracking in GNATprove mode.
	* sem_res.adb (Resolve_Comparison_Op): Remove incomplete
	special-casing for folding in GNATprove mode.
diff mbox series

Patch

diff --git a/gcc/ada/exp_util.adb b/gcc/ada/exp_util.adb
--- a/gcc/ada/exp_util.adb
+++ b/gcc/ada/exp_util.adb
@@ -6360,6 +6360,17 @@  package body Exp_Util is
          return;
       end if;
 
+      --  In GNATprove mode we don't want to use current value optimizer, in
+      --  particular for loop invariant expressions and other assertions that
+      --  act as cut points for proof. The optimizer often folds expressions
+      --  into True/False where they trivially follow from the previous
+      --  assignments, but this deprives proof from the information needed to
+      --  discharge checks that are beyond the scope of the value optimizer.
+
+      if GNATprove_Mode then
+         return;
+      end if;
+
       --  Otherwise examine current value
 
       declare


diff --git a/gcc/ada/sem_res.adb b/gcc/ada/sem_res.adb
--- a/gcc/ada/sem_res.adb
+++ b/gcc/ada/sem_res.adb
@@ -7457,24 +7457,7 @@  package body Sem_Res is
 
       Analyze_Dimension (N);
 
-      --  Evaluate the relation (note we do this after the above check since
-      --  this Eval call may change N to True/False). Skip this evaluation
-      --  inside assertions, in order to keep assertions as written by users
-      --  for tools that rely on these, e.g. GNATprove for loop invariants.
-      --  Except evaluation is still performed even inside assertions for
-      --  comparisons between values of universal type, which are useless
-      --  for static analysis tools, and not supported even by GNATprove.
-      --  ??? It is suspicious to disable evaluation only for comparison
-      --  operators and not, let's say, for calls to static functions.
-
-      if not GNATprove_Mode
-        or else In_Assertion_Expr = 0
-        or else (Is_Universal_Numeric_Type (Etype (L))
-                   and then
-                 Is_Universal_Numeric_Type (Etype (R)))
-      then
-         Eval_Relational_Op (N);
-      end if;
+      Eval_Relational_Op (N);
    end Resolve_Comparison_Op;
 
    --------------------------------