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 SuppressFromCXXStandardLibrary; + /// \sa shouldCrosscheckWithZ3 + Optional CrosscheckWithZ3; + /// \sa reportIssuesInMainSourceFile Optional 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. /// 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 @@ -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 { +private: + /// Holds the constraints in a given path + // TODO: should we use a set? + llvm::SmallVector Constraints; + +public: + FalsePositiveRefutationBRVisitor() = default; + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + std::shared_ptr 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/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 @@ -33,9 +34,12 @@ namespace ento { class ProgramStateManager; +class RangeSet; class SubEngine; class SymbolReaper; +using ConstraintRangeTy = llvm::ImmutableMap; + class ConditionTruthVal { Optional 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/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; template <> struct ProgramStateTrait 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: 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()); + if (getAnalyzerOptions().shouldCrosscheckWithZ3()) + R->addVisitor(llvm::make_unique()); + // Register additional node visitors. R->addVisitor(llvm::make_unique()); R->addVisitor(llvm::make_unique()); - R->addVisitor(llvm::make_unique()); R->addVisitor(llvm::make_unique()); BugReport::VisitorList visitors; Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -2354,3 +2354,48 @@ return std::make_shared(L, "Taint originated here"); } + +std::shared_ptr +FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N, + const ExplodedNode *PrevN, + BugReporterContext &BRC, + BugReport &BR) { + const ConstraintRangeTy &CR = N->getState()->get(); + 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 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/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/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/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(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: 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); + } +} +