Author: mramalho Date: Mon Jun 4 07:40:44 2018 New Revision: 333903 URL: http://llvm.org/viewvc/llvm-project?rev=333903&view=rev Log: [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 Added: cfe/trunk/test/Analysis/z3-crosscheck.c Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h?rev=333903&r1=333902&r2=333903&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/AnalyzerOptions.h Mon Jun 4 07:40:44 2018 @@ -280,6 +280,9 @@ private: /// \sa shouldSuppressFromCXXStandardLibrary Optional<bool> SuppressFromCXXStandardLibrary; + /// \sa shouldCrosscheckWithZ3 + Optional<bool> CrosscheckWithZ3; + /// \sa reportIssuesInMainSourceFile Optional<bool> ReportIssuesInMainSourceFile; @@ -575,6 +578,13 @@ public: /// 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. /// Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h?rev=333903&r1=333902&r2=333903&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h Mon Jun 4 07:40:44 2018 @@ -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" @@ -355,6 +356,27 @@ public: std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN, + BugReporterContext &BRC, + 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; }; Modified: cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp?rev=333903&r1=333902&r2=333903&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/AnalyzerOptions.cpp Mon Jun 4 07:40:44 2018 @@ -296,6 +296,12 @@ bool AnalyzerOptions::shouldSuppressFrom /* Default = */ true); } +bool AnalyzerOptions::shouldCrosscheckWithZ3() { + return getBooleanOption(CrosscheckWithZ3, + "crosscheck-with-z3", + /* Default = */ false); +} + bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() { return getBooleanOption(ReportIssuesInMainSourceFile, "report-in-main-source-file", Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp?rev=333903&r1=333902&r2=333903&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporter.cpp Mon Jun 4 07:40:44 2018 @@ -3143,10 +3143,15 @@ bool GRBugReporter::generatePathDiagnost 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; Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=333903&r1=333902&r2=333903&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Mon Jun 4 07:40:44 2018 @@ -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 Explode 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); +} Added: cfe/trunk/test/Analysis/z3-crosscheck.c URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/test/Analysis/z3-crosscheck.c?rev=333903&view=auto ============================================================================== --- cfe/trunk/test/Analysis/z3-crosscheck.c (added) +++ cfe/trunk/test/Analysis/z3-crosscheck.c Mon Jun 4 07:40:44 2018 @@ -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); + } +} _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
