r337920 - [analyzer] Try to minimize the number of equivalent bug reports evaluated by the refutation manager

[Mikhail R. Gadelha via cfe-commits]

Author: mramalho
Date: Wed Jul 25 05:49:32 2018
New Revision: 337920

URL: http://llvm.org/viewvc/llvm-project?rev=337920&view=rev
Log:
[analyzer] Try to minimize the number of equivalent bug reports evaluated by the refutation manager

Summary:
This patch changes how the SMT bug refutation runs in an equivalent bug report class.

Now, all other visitor are executed until they find a valid bug or mark all bugs as invalid. When the one valid bug is found (and crosscheck is enabled), the SMT refutation checks the satisfiability of this single bug.

If the bug is still valid after checking with Z3, it is returned and a bug report is created. If the bug is found to be invalid, the next bug report in the equivalent class goes through the same process, until we find a valid bug or all bugs are marked as invalid.

Massive speedups when verifying redis/src/rax.c, from 1500s to 10s.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: xazax.hun, szepet, a.sidorin

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

Modified:
    cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp

Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp?rev=337920&r1=337919&r2=337920&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp Wed Jul 25 05:49:32 2018
@@ -2605,8 +2605,6 @@ std::pair<BugReport*, std::unique_ptr<Vi
     // Register refutation visitors first, if they mark the bug invalid no
     // further analysis is required
     R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>());
-    if (Opts.shouldCrosscheckWithZ3())
-      R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
 
     // Register additional node visitors.
     R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>());
@@ -2619,9 +2617,24 @@ std::pair<BugReport*, std::unique_ptr<Vi
     std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes =
         generateVisitorsDiagnostics(R, ErrorNode, BRC);
 
-    if (R->isValid())
-      return std::make_pair(R, std::move(visitorNotes));
+    if (R->isValid()) {
+      if (Opts.shouldCrosscheckWithZ3()) {
+        // If crosscheck is enabled, remove all visitors, add the refutation
+        // visitor and check again
+        R->clearVisitors();
+        R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>());
+
+        // We don't overrite the notes inserted by other visitors because the
+        // refutation manager does not add any new note to the path
+        generateVisitorsDiagnostics(R, ErrorGraph.ErrorNode, BRC);
+      }
+
+      // Check if the bug is still valid
+      if (R->isValid())
+        return std::make_pair(R, std::move(visitorNotes));
+    }
   }
+
   return std::make_pair(nullptr, llvm::make_unique<VisitorsDiagnosticsTy>());
 }