[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

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h

@@ -280,6 +280,9 @@ class AnalyzerOptions : public RefCountedBase<AnalyzerOptions> {
   /// \sa shouldSuppressFromCXXStandardLibrary
   Optional<bool> SuppressFromCXXStandardLibrary;
 
+  /// \sa shouldCrosscheckWithZ3
+  Optional<bool> CrosscheckWithZ3;
+
   /// \sa reportIssuesInMainSourceFile
   Optional<bool> ReportIssuesInMainSourceFile;
 
@@ -575,6 +578,13 @@ class AnalyzerOptions : public RefCountedBase<AnalyzerOptions> {
   /// which accepts the values "true" and "false".
   bool shouldSuppressFromCXXStandardLibrary();
 
+  /// Returns whether bug reports should be crosschecked with the Z3
+  /// constraint manager backend.
+  ///
+  /// This is controlled by the 'crosscheck-with-z3' config option,
+  /// which accepts the values "true" and "false".
+  bool shouldCrosscheckWithZ3();
+
   /// Returns whether or not the diagnostic report should be always reported
   /// in the main source file and not the headers.
   ///

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

@@ -16,6 +16,7 @@
 #define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_BUGREPORTERVISITORS_H
 
 #include "clang/Basic/LLVM.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "llvm/ADT/FoldingSet.h"
 #include "llvm/ADT/STLExtras.h"
@@ -359,6 +360,27 @@ class TaintBugVisitor final : public BugReporterVisitorImpl<TaintBugVisitor> {
                                                  BugReport &BR) override;
 };
 
+/// The bug visitor will walk all the nodes in a path and collect all the
+/// constraints. When it reaches the root node, will create a refutation
+/// manager and check if the constraints are satisfiable
+class FalsePositiveRefutationBRVisitor final
+    : public BugReporterVisitorImpl<FalsePositiveRefutationBRVisitor> {
+private:
+  /// Holds the constraints in a given path
+  // TODO: should we use a set?
+  llvm::SmallVector<ConstraintRangeTy, 32> Constraints;
+
+public:
+  FalsePositiveRefutationBRVisitor() = default;
+
+  void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+  std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N,
+                                                 const ExplodedNode *PrevN,
+                                                 BugReporterContext &BRC,
+                                                 BugReport &BR) override;
+};
+
 namespace bugreporter {
 
 /// Attempts to add visitors to trace a null or undefined value back to its

clang/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp

@@ -296,6 +296,12 @@ bool AnalyzerOptions::shouldSuppressFromCXXStandardLibrary() {
                           /* Default = */ true);
 }
 
+bool AnalyzerOptions::shouldCrosscheckWithZ3() {
+  return getBooleanOption(CrosscheckWithZ3,
+                          "crosscheck-with-z3",
+                          /* Default = */ false);
+}
+
 bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() {
   return getBooleanOption(ReportIssuesInMainSourceFile,
                           "report-in-main-source-file",

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

@@ -3143,10 +3143,15 @@ bool GRBugReporter::generatePathDiagnostic(PathDiagnostic& PD,
     PathDiagnosticBuilder PDB(*this, R, ErrorGraph.BackMap, &PC);
     const ExplodedNode *N = ErrorGraph.ErrorNode;
 
+    // Register refutation visitors first, if they mark the bug invalid no
+    // further analysis is required
+    R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
+    if (getAnalyzerOptions().shouldCrosscheckWithZ3())
+      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
     R->addVisitor(llvm::make_unique<ConditionBRVisitor>());
-    R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
     R->addVisitor(llvm::make_unique<CXXSelfAssignmentBRVisitor>());
 
     BugReport::VisitorList visitors;

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

@@ -44,6 +44,7 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/None.h"
 #include "llvm/ADT/Optional.h"
@@ -2354,3 +2355,46 @@ TaintBugVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN,
 
   return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
 }
+
+static bool
+areConstraintsUnfeasible(BugReporterContext &BRC,
+                         const llvm::SmallVector<ConstraintRangeTy, 32> &Cs) {
+  // Create a refutation manager
+  std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
+      BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
+
+  SMTConstraintManager *SMTRefutationMgr =
+      static_cast<SMTConstraintManager *>(RefutationMgr.get());
+
+  // Add constraints to the solver
+  for (const auto &C : Cs)
+    SMTRefutationMgr->addRangeConstraints(C);
+
+  // And check for satisfiability
+  return SMTRefutationMgr->isModelFeasible().isConstrainedFalse();
+}
+
+std::shared_ptr<PathDiagnosticPiece>
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+                                            const ExplodedNode *PrevN,
+                                            BugReporterContext &BRC,
+                                            BugReport &BR) {
+  // Collect the constraint for the current state
+  const ConstraintRangeTy &CR = N->getState()->get<ConstraintRange>();
+  Constraints.push_back(CR);
+
+  // If there are no predecessor, we reached the root node. In this point,
+  // a new refutation manager will be created and the path will be checked
+  // for reachability
+  if (PrevN->pred_size() == 0 && areConstraintsUnfeasible(BRC, Constraints)) {
+    BR.markInvalid("Infeasible constraints", N->getLocationContext());
+  }
+
+  return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+    llvm::FoldingSetNodeID &ID) const {
+  static int Tag = 0;
+  ID.AddPointer(&Tag);
+}

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);
+  }
+}