mikhail.ramalho updated this revision to Diff 149317.
mikhail.ramalho marked 6 inline comments as not done.
mikhail.ramalho added a comment.
- Simplified refutation process: it now collects all the constraints in a given
path and, only when it reaches the root node, the refutation manager is created
and the constraints are checked for reachability. All the optimizations were
removed.
- Moved RangedConstraintManager.h to include/
- Moved refutation check to be the first in the list of BugVisitors
- Added dump method to Z3Solver (to print the formula)
- Added more documentation/comments
https://reviews.llvm.org/D45517
Files:
include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
lib/StaticAnalyzer/Core/BugReporter.cpp
lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
lib/StaticAnalyzer/Core/RangedConstraintManager.h
lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
test/Analysis/z3-crosscheck.c
Index: test/Analysis/z3-crosscheck.c
===================================================================
--- /dev/null
+++ test/Analysis/z3-crosscheck.c
@@ -0,0 +1,57 @@
+// 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
+
+#ifndef NO_CROSSCHECK
+// expected-no-diagnostics
+#endif
+
+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
+ // FIXME: Should warn about 'k' being a garbage value
+ while (z < k) { // no-warning
+#endif
+ z = 2 * z;
+ }
+}
+
+void i() {
+ _Bool c = nondet_bool();
+ if (c) {
+ h(1);
+ } else {
+ h(2);
+ }
+}
+
Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -10,6 +10,7 @@
#include "clang/Basic/TargetInfo.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SimpleConstraintManager.h"
#include "clang/Config/config.h"
@@ -880,6 +881,12 @@
/// Reset the solver and remove all constraints.
void reset() { Z3_solver_reset(Z3Context::ZC, Solver); }
+
+ void print(raw_ostream &OS) const {
+ OS << Z3_solver_to_string(Z3Context::ZC, Solver);
+ }
+
+ LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
}; // end class Z3Solver
void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
@@ -915,6 +922,17 @@
void print(ProgramStateRef St, raw_ostream &Out, const char *nl,
const char *sep) override;
+ void reset() override { Solver.reset(); }
+
+ bool isModelFeasible() override {
+ return Solver.check() != Z3_L_FALSE;
+ }
+
+ /// Converts the ranged constraints of a set of symbols to SMT
+ ///
+ /// \param CR The set of constraints.
+ void addRangeConstraints(ConstraintRangeTy CR) override;
+
//===------------------------------------------------------------------===//
// Implementation for interface from SimpleConstraintManager.
//===------------------------------------------------------------------===//
@@ -1235,6 +1253,42 @@
return State->set<ConstraintZ3>(CZ);
}
+void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy CR) {
+ for (const auto &I : CR) {
+ SymbolRef Sym = I.first;
+
+ Z3Expr Constraints = Z3Expr::fromBoolean(false);
+
+ for (const auto &Range : I.second) {
+ const llvm::APSInt &From = Range.From();
+ const llvm::APSInt &To = Range.To();
+
+ assert((getAPSIntType(From) == getAPSIntType(To)) &&
+ "Range values have different types!");
+ QualType RangeTy = getAPSIntType(From);
+ // Skip ranges whose endpoints cannot be converted to APSInts with
+ // a valid APSIntType.
+ // FIXME: fix available in D35450
+ if (RangeTy.isNull())
+ continue;
+
+ QualType SymTy;
+ Z3Expr Exp = getZ3Expr(Sym, &SymTy);
+ bool IsSignedTy = SymTy->isSignedIntegerOrEnumerationType();
+
+ Z3Expr FromExp = Z3Expr::fromAPSInt(From);
+ Z3Expr ToExp = Z3Expr::fromAPSInt(To);
+
+ Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr);
+ Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr);
+ Z3Expr SymRange = Z3Expr::fromBinOp(LHS, BO_LAnd, RHS, IsSignedTy);
+ Constraints =
+ Z3Expr::fromBinOp(Constraints, BO_LOr, SymRange, IsSignedTy);
+ }
+ Solver.addConstraint(Constraints);
+ }
+}
+
//===------------------------------------------------------------------===//
// Internal implementation.
//===------------------------------------------------------------------===//
Index: lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangedConstraintManager.cpp
@@ -12,8 +12,8 @@
//
//===----------------------------------------------------------------------===//
-#include "RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
namespace clang {
Index: lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
===================================================================
--- lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
+++ lib/StaticAnalyzer/Core/RangeConstraintManager.cpp
@@ -12,10 +12,10 @@
//
//===----------------------------------------------------------------------===//
-#include "RangedConstraintManager.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/APSIntType.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
#include "llvm/ADT/FoldingSet.h"
#include "llvm/ADT/ImmutableSet.h"
#include "llvm/Support/raw_ostream.h"
Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2354,3 +2354,48 @@
return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
}
+
+std::shared_ptr<PathDiagnosticPiece>
+FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
+ const ExplodedNode *PrevN,
+ BugReporterContext &BRC,
+ BugReport &BR) {
+ 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) {
+ // Get the set of options
+ AnalyzerOptions &Opts = BRC.getStateManager()
+ .getOwningEngine()
+ ->getAnalysisManager()
+ .getAnalyzerOptions();
+
+ // Try to create the refutation manager, using Z3
+ std::unique_ptr<ConstraintManager> RefutationMgr =
+ Opts.shouldCrosscheckWithZ3()
+ ? CreateZ3ConstraintManager(BRC.getStateManager(),
+ BRC.getStateManager().getOwningEngine())
+ : nullptr;
+ assert((RefutationMgr != nullptr) &&
+ "Could not create a refutation manager");
+
+ // Add constraints to the solver
+ for (const auto &C : Constraints)
+ RefutationMgr->addRangeConstraints(C);
+
+ // And check for satisfiability
+ if (!RefutationMgr->isModelFeasible())
+ BR.markInvalid("Infeasible constraints", N->getLocationContext());
+ }
+
+ return nullptr;
+}
+
+void FalsePositiveRefutationBRVisitor::Profile(
+ llvm::FoldingSetNodeID &ID) const {
+ static int Tag = 0;
+ ID.AddPointer(&Tag);
+}
Index: lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- lib/StaticAnalyzer/Core/BugReporter.cpp
+++ lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -3143,10 +3143,15 @@
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;
Index: lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
===================================================================
--- lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
+++ lib/StaticAnalyzer/Core/AnalyzerOptions.cpp
@@ -296,6 +296,12 @@
/* Default = */ true);
}
+bool AnalyzerOptions::shouldCrosscheckWithZ3() {
+ return getBooleanOption(CrosscheckWithZ3,
+ "crosscheck-with-z3",
+ /* Default = */ false);
+}
+
bool AnalyzerOptions::shouldReportIssuesInMainSourceFile() {
return getBooleanOption(ReportIssuesInMainSourceFile,
"report-in-main-source-file",
Index: include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h
@@ -124,7 +124,6 @@
class ConstraintRange {};
-using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
template <>
struct ProgramStateTrait<ConstraintRange>
Index: include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
===================================================================
--- include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
+++ include/clang/StaticAnalyzer/Core/PathSensitive/ConstraintManager.h
@@ -18,6 +18,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SymExpr.h"
+#include "llvm/ADT/ImmutableMap.h"
#include "llvm/ADT/Optional.h"
#include "llvm/Support/SaveAndRestore.h"
#include <memory>
@@ -33,9 +34,12 @@
namespace ento {
class ProgramStateManager;
+class RangeSet;
class SubEngine;
class SymbolReaper;
+using ConstraintRangeTy = llvm::ImmutableMap<SymbolRef, RangeSet>;
+
class ConditionTruthVal {
Optional<bool> Val;
@@ -175,6 +179,10 @@
return checkNull(State, Sym);
}
+ virtual void reset() {}
+ virtual bool isModelFeasible() { return true; }
+ virtual void addRangeConstraints(ConstraintRangeTy) {}
+
protected:
/// A flag to indicate that clients should be notified of assumptions.
/// By default this is the case, but sometimes this needs to be restricted
Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -16,8 +16,10 @@
#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/SmallSet.h"
#include "llvm/ADT/STLExtras.h"
#include "llvm/ADT/StringRef.h"
#include <memory>
@@ -359,6 +361,27 @@
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;
+};
+
namespace bugreporter {
/// Attempts to add visitors to trace a null or undefined value back to its
Index: include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
===================================================================
--- include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
+++ include/clang/StaticAnalyzer/Core/AnalyzerOptions.h
@@ -280,6 +280,9 @@
/// \sa shouldSuppressFromCXXStandardLibrary
Optional<bool> SuppressFromCXXStandardLibrary;
+ /// \sa shouldCrosscheckWithZ3
+ Optional<bool> CrosscheckWithZ3;
+
/// \sa reportIssuesInMainSourceFile
Optional<bool> ReportIssuesInMainSourceFile;
@@ -575,6 +578,13 @@
/// 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.
///
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
