[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, 6 insertions, 1 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index 91d601b360d..854e405fb9c 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/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;