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 @@ -359,6 +359,20 @@ BugReport &BR) override; }; +class FalsePositiveRefutationBRVisitor final + : public BugReporterVisitorImpl { + +public: + FalsePositiveRefutationBRVisitor() = default; + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + std::shared_ptr VisitNode(const ExplodedNode *Succ, + const ExplodedNode *Prev, + 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,12 @@ return checkNull(State, Sym); } + virtual void reset() {} + virtual bool isModelFeasible() { return true; } + virtual void addRangeConstraints(ConstraintRangeTy PrevCR, + ConstraintRangeTy SuccCR, + bool OnlyPurged) {} + 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/ProgramState.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h @@ -493,6 +493,7 @@ EnvironmentManager EnvMgr; std::unique_ptr StoreMgr; std::unique_ptr ConstraintMgr; + std::unique_ptr RefutationMgr; ProgramState::GenericDataMap::Factory GDMFactory; TaintedSubRegions::Factory TSRFactory; @@ -558,6 +559,11 @@ StoreManager& getStoreManager() { return *StoreMgr; } ConstraintManager& getConstraintManager() { return *ConstraintMgr; } + + ConstraintManager& getRefutationManager() { + return *RefutationMgr; + } + SubEngine* getOwningEngine() { return Eng; } ProgramStateRef removeDeadBindings(ProgramStateRef St, 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 @@ -3149,6 +3149,9 @@ R->addVisitor(llvm::make_unique()); R->addVisitor(llvm::make_unique()); + if (getAnalyzerOptions().shouldCrosscheckWithZ3()) + R->addVisitor(llvm::make_unique()); + BugReport::VisitorList visitors; unsigned origReportConfigToken, finalReportConfigToken; LocationContextMap LCM; Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -41,6 +41,7 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState_Fwd.h" +#include "RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" @@ -2354,3 +2355,38 @@ return std::make_shared(L, "Taint originated here"); } + +std::shared_ptr +FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *Succ, + const ExplodedNode *Prev, + BugReporterContext &BRC, + BugReport &BR) { + + const ConstraintRangeTy SuccCR = Succ->getState()->get(); + const ConstraintRangeTy PrevCR = Prev->getState()->get(); + + ConstraintManager &RefutationMgr = + BRC.getStateManager().getRefutationManager(); + + RefutationMgr.addRangeConstraints(PrevCR, SuccCR, + Succ->getLocation().isPurgeKind()); + + // Reached root node, encode the path and check for satisfatiability + if (Prev->pred_size() == 0) { + if (!RefutationMgr.isModelFeasible()) { + // If the bug is not reachable, mark it as invalid + BR.markInvalid("Infeasible constraints", Succ->getLocationContext()); + } + + // Reset the solver + RefutationMgr.reset(); + } + + return nullptr; +} + +void FalsePositiveRefutationBRVisitor::Profile( + llvm::FoldingSetNodeID &ID) const { + static int Tag = 0; + ID.AddPointer(&Tag); +} Index: lib/StaticAnalyzer/Core/ProgramState.cpp =================================================================== --- lib/StaticAnalyzer/Core/ProgramState.cpp +++ lib/StaticAnalyzer/Core/ProgramState.cpp @@ -13,6 +13,8 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" #include "clang/Analysis/CFG.h" +#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/AnalysisManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/CallEvent.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramStateTrait.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" @@ -78,6 +80,10 @@ CallEventMgr(new CallEventManager(alloc)), Alloc(alloc) { StoreMgr = (*CreateSMgr)(*this); ConstraintMgr = (*CreateCMgr)(*this, SubEng); + AnalyzerOptions &Opts = SubEng->getAnalysisManager().getAnalyzerOptions(); + RefutationMgr = Opts.shouldCrosscheckWithZ3() + ? CreateZ3ConstraintManager(*this, SubEng) + : nullptr; } Index: lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -7,6 +7,7 @@ // //===----------------------------------------------------------------------===// +#include "RangedConstraintManager.h" #include "clang/Basic/TargetInfo.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h" #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h" @@ -915,6 +916,13 @@ void print(ProgramStateRef St, raw_ostream &Out, const char *nl, const char *sep) override; + void reset() override; + + bool isModelFeasible() override; + + void addRangeConstraints(ConstraintRangeTy PrevCR, ConstraintRangeTy SuccCR, + bool OnlyPurged) override; + //===------------------------------------------------------------------===// // Implementation for interface from SimpleConstraintManager. //===------------------------------------------------------------------===// @@ -1235,6 +1243,58 @@ return State->set(CZ); } +void Z3ConstraintManager::reset() { Solver.reset(); } + +bool Z3ConstraintManager::isModelFeasible() { + return Solver.check() != Z3_L_FALSE; +} + +void Z3ConstraintManager::addRangeConstraints(ConstraintRangeTy PrevCR, + ConstraintRangeTy SuccCR, + bool OnlyPurged) { + if (OnlyPurged && PrevCR.isEmpty()) + return; + if (!OnlyPurged && SuccCR.isEmpty()) + return; + ConstraintRangeTy CR = OnlyPurged ? PrevCR : SuccCR; + + for (auto const &I : CR) { + SymbolRef Sym = I.first; + + if (OnlyPurged && SuccCR.contains(Sym)) + continue; + + 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. + 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/analyzer-config.c =================================================================== --- test/Analysis/analyzer-config.c +++ test/Analysis/analyzer-config.c @@ -18,6 +18,7 @@ // CHECK-NEXT: cfg-rich-constructors = true // CHECK-NEXT: cfg-scopes = false // CHECK-NEXT: cfg-temporary-dtors = true +// CHECK-NEXT: crosscheck-with-z3 = false // CHECK-NEXT: exploration_strategy = unexplored_first_queue // CHECK-NEXT: faux-bodies = true // CHECK-NEXT: graph-trim-interval = 1000 @@ -35,4 +36,4 @@ // CHECK-NEXT: unroll-loops = false // CHECK-NEXT: widen-loops = false // CHECK-NEXT: [stats] -// CHECK-NEXT: num-entries = 23 +// CHECK-NEXT: num-entries = 24 Index: test/Analysis/analyzer-config.cpp =================================================================== --- test/Analysis/analyzer-config.cpp +++ test/Analysis/analyzer-config.cpp @@ -32,6 +32,7 @@ // CHECK-NEXT: cfg-rich-constructors = true // CHECK-NEXT: cfg-scopes = false // CHECK-NEXT: cfg-temporary-dtors = true +// CHECK-NEXT: crosscheck-with-z3 = false // CHECK-NEXT: experimental-enable-naive-ctu-analysis = false // CHECK-NEXT: exploration_strategy = unexplored_first_queue // CHECK-NEXT: faux-bodies = true @@ -50,4 +51,4 @@ // CHECK-NEXT: unroll-loops = false // CHECK-NEXT: widen-loops = false // CHECK-NEXT: [stats] -// CHECK-NEXT: num-entries = 30 +// CHECK-NEXT: num-entries = 31 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); + } +} +