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>()); } _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
