analyzer: handle comparisons against negated symbolic values [PR107948]

gcc/analyzer/ChangeLog:
	PR analyzer/107948
	* region-model-manager.cc
	(region_model_manager::maybe_fold_binop): Fold (0 - VAL) to -VAL.
	* region-model.cc (region_model::eval_condition): Handle e.g.
	"-X <= 0" as equivalent to X >= 0".

gcc/testsuite/ChangeLog:
	PR analyzer/107948
	* gcc.dg/analyzer/feasibility-pr107948.c: New test.

Signed-off-by: David Malcolm <dmalcolm@redhat.com>

diff --git a/gcc/analyzer/region-model-manager.cc b/gcc/analyzer/region-model-manager.cc
index ae63c664ae580ebd82babe5b6593fffe744cb0cf..471a9272e410aec35788267b43ed90ea070c58fe 100644 (file)
--- a/gcc/analyzer/region-model-manager.cc
+++ b/gcc/analyzer/region-model-manager.cc
@@ -620,6 +620,9 @@ region_model_manager::maybe_fold_binop (tree type, enum tree_code op,
       /* (VAL - 0) -> VAL.  */
       if (cst1 && zerop (cst1))
        return get_or_create_cast (type, arg0);
+      /* (0 - VAL) -> -VAL.  */
+      if (cst0 && zerop (cst0))
+       return get_or_create_unaryop (type, NEGATE_EXPR, arg1);
       break;
     case MULT_EXPR:
       /* (VAL * 0).  */

diff --git a/gcc/analyzer/region-model.cc b/gcc/analyzer/region-model.cc
index 91b868f7b168566ec59fdeb92150aa4a16bdb8ea..4f623fd6ca326d9f075f67d8bef6cb8bb17399cb 100644 (file)
--- a/gcc/analyzer/region-model.cc
+++ b/gcc/analyzer/region-model.cc
@@ -3339,6 +3339,19 @@ region_model::eval_condition (const svalue *lhs,
                  return lhs_ts;
              }
          }
+       else if (const unaryop_svalue *unaryop
+                  = lhs->dyn_cast_unaryop_svalue ())
+         {
+           if (unaryop->get_op () == NEGATE_EXPR)
+             {
+               /* e.g. "-X <= 0" is equivalent to X >= 0".  */
+               tristate lhs_ts = eval_condition (unaryop->get_arg (),
+                                                 swap_tree_comparison (op),
+                                                 rhs);
+               if (lhs_ts.is_known ())
+                 return lhs_ts;
+             }
+         }
       }
 
   /* Handle rejection of equality for comparisons of the initial values of

diff --git a/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c b/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c
new file mode 100644 (file)
index 0000000..5eb8b0a
--- /dev/null
+++ b/gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c
@@ -0,0 +1,49 @@
+#include "analyzer-decls.h"
+
+void foo(int width) {
+  int i = 0;
+  int base;
+  if (width > 0){
+    __analyzer_eval(i == 0); /* { dg-warning "TRUE" } */
+    __analyzer_eval(width > 0); /* { dg-warning "TRUE" } */
+    __analyzer_eval(width - i > 0); /* { dg-warning "TRUE" } */
+    __analyzer_eval(i - width <= 0); /* { dg-warning "TRUE" } */
+    if (i - width <= 0) {
+      base = 512;
+    }
+    else {
+      __analyzer_dump_path (); /* { dg-bogus "path" } */
+    }
+    base+=1; /* { dg-bogus "uninit" } */
+  }
+}
+
+void test_ge_zero (int x)
+{
+  if (x >= 0)
+    {
+      __analyzer_eval(x >= 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(x > 0); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval(x <= 0); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval(x < 0); /* { dg-warning "FALSE" } */
+      __analyzer_eval(-x <= 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(-x < 0); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval(-x >= 0); /* { dg-warning "UNKNOWN" } */
+      __analyzer_eval(-x > 0); /* { dg-warning "FALSE" } */
+    }
+}
+
+void test_gt_zero (int x)
+{
+  if (x > 0)
+    {
+      __analyzer_eval(x >= 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(x > 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(x <= 0); /* { dg-warning "FALSE" } */
+      __analyzer_eval(x < 0); /* { dg-warning "FALSE" } */
+      __analyzer_eval(-x <= 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(-x < 0); /* { dg-warning "TRUE" } */
+      __analyzer_eval(-x >= 0); /* { dg-warning "FALSE" } */
+      __analyzer_eval(-x > 0); /* { dg-warning "FALSE" } */
+    }
+}