r333903 - [analyzer] False positive refutation with Z3
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Mon Jun 4 07:40:44 PDT 2018
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);
+ }
+}
More information about the cfe-commits
mailing list