Re: [committed] analyzer: reject ((i + 1 > 0) && (i < 0)) for integers [PR94362]

[Mikael Morin]

Hello,

Le 21/01/2022 à 00:59, David Malcolm via Gcc-patches a écrit :
diff --git a/gcc/analyzer/constraint-manager.cc 
b/gcc/analyzer/constraint-manager.cc
index 568e7150ea7..7c4a85bbb24 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -301,6 +301,80 @@ range::above_upper_bound (tree rhs_const) const
                            m_upper_bound.m_constant).is_true ();
  }
  
+/* Attempt to add B to the bound of the given kind of this range.
+   Return true if feasible; false if infeasible.  */
+
+bool
+range::add_bound (bound b, enum bound_kind bound_kind)
+{
+  b.ensure_closed (bound_kind);
+
+  switch (bound_kind)
+    {
+    default:
+      gcc_unreachable ();
+    case BK_LOWER:
+      /* Discard redundant bounds.  */
+      if (m_lower_bound.m_constant)
+       {
+         m_lower_bound.ensure_closed (BK_LOWER);
+         if (!tree_int_cst_lt (b.m_constant,
+                               m_lower_bound.m_constant))
+           return true;

isn’t this condition reversed?

+       }
+      m_lower_bound = b;
+      break;
+    case BK_UPPER:
+      /* Discard redundant bounds.  */
+      if (m_upper_bound.m_constant)
+       {
+         m_upper_bound.ensure_closed (BK_UPPER);
+         if (tree_int_cst_le (b.m_constant,
+                              m_upper_bound.m_constant))
+           return true;

same here.

All the tests added have just one lower and one upper bound, so they 
don’t use the short-circuit code, but amending one of them as follows 
makes the problem appear as the test starts to fails.  It should 
continue to work, shouldn’t it?


diff --git a/gcc/analyzer/constraint-manager.cc 
b/gcc/analyzer/constraint-manager.cc
index 7c4a85bbb24..3f38b857722 100644
--- a/gcc/analyzer/constraint-manager.cc
+++ b/gcc/analyzer/constraint-manager.cc
@@ -3697,6 +3697,7 @@ test_constant_comparisons ()
     region_model_manager mgr;
     {
       region_model model (&mgr);
+      ADD_SAT_CONSTRAINT (model, int_1, LT_EXPR, a);
       ADD_SAT_CONSTRAINT (model, int_3, LT_EXPR, a);
       ADD_UNSAT_CONSTRAINT (model, a, LT_EXPR, int_4);
     }