[gcc r13-4456] analyzer: handle comparisons against negated symbolic values [PR107948]

[gcc r13-4456] analyzer: handle comparisons against negated symbolic values [PR107948]

[David Malcolm]

https://gcc.gnu.org/g:0b737090a69624dea5318c380620283f0321a92e

commit r13-4456-g0b737090a69624dea5318c380620283f0321a92e
Author: David Malcolm <dmalcolm@redhat.com>
Date:   Thu Dec 1 21:28:55 2022 -0500

    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:
---
 gcc/analyzer/region-model-manager.cc               |  3 ++
 gcc/analyzer/region-model.cc                       | 13 ++++++
 .../gcc.dg/analyzer/feasibility-pr107948.c         | 49 ++++++++++++++++++++++
 3 files changed, 65 insertions(+)

diff --git a/gcc/analyzer/region-model-manager.cc b/gcc/analyzer/region-model-manager.cc
index ae63c664ae5..471a9272e41 100644
--- 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 91b868f7b16..4f623fd6ca3 100644
--- 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
index 00000000000..5eb8b0aef22
--- /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" } */
+    }
+}