[analyzer] False positive refutation with Z3

Summary: This is a prototype of a bug reporter visitor that invalidates bug reports by re-checking constraints of certain states on the bug path using the Z3 constraint manager backend. The functionality is available under the `crosscheck-with-z3` analyzer config flag.

Reviewers: george.karpenkov, NoQ, dcoughlin, rnkovacs

Reviewed By: george.karpenkov

Subscribers: rnkovacs, NoQ, george.karpenkov, dcoughlin, xbolva00, ddcc, mikhail.ramalho, MTC, fhahn, whisperity, baloghadamsoftware, szepet, a.sidorin, gsd, dkrupp, xazax.hun, cfe-commits

Differential Revision: https://reviews.llvm.org/D45517

llvm-svn: 333903

1 files changed, 51 insertions, 0 deletions

diff --git a/clang/test/Analysis/z3-crosscheck.c b/clang/test/Analysis/z3-crosscheck.c
new file mode 100644
index 00000000000..66f778de8a3
--- /dev/null
+++ b/clang/test/Analysis/z3-crosscheck.c
@@ -0,0 +1,51 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core,unix.Malloc,debug.ExprInspection -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+int foo(int x) 
+{
+  int *z = 0;
+  if ((x & 1) && ((x & 1) ^ 1))
+#ifdef NO_CROSSCHECK
+      return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
+#else
+      return *z; // no-warning
+#endif
+  return 0;
+}
+
+void g(int d);
+
+void f(int *a, int *b) {
+  int c = 5;
+  if ((a - b) == 0)
+    c = 0;
+  if (a != b)
+#ifdef NO_CROSSCHECK
+    g(3 / c); // expected-warning {{Division by zero}}
+#else
+    g(3 / c); // no-warning
+#endif
+}
+
+_Bool nondet_bool();
+
+void h(int d) {
+  int x, y, k, z = 1;
+#ifdef NO_CROSSCHECK
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#else
+  while (z < k) { // expected-warning {{The right operand of '<' is a garbage value}}
+#endif
+    z = 2 * z;
+  }
+}
+
+void i() {
+  _Bool c = nondet_bool();
+  if (c) {
+    h(1);
+  } else {
+    h(2);
+  }
+}