diff mbox series

[committed] analyzer: handle comparisons against negated symbolic values [PR107948]

Message ID 20221202023554.3778168-1-dmalcolm@redhat.com
State Committed
Commit 0b737090a69624dea5318c380620283f0321a92e
Headers
Series [committed] analyzer: handle comparisons against negated symbolic values [PR107948] |

Commit Message

David Malcolm Dec. 2, 2022, 2:35 a.m. UTC 
  Successfully bootstrapped & regrtested on x86_64-pc-linux-gnu.
Pushed to trunk as r13-4456-g0b737090a69624.

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>
---
 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(+)
 create mode 100644 gcc/testsuite/gcc.dg/analyzer/feasibility-pr107948.c
diff mbox series

Patch

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" } */
+    }
+}