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,25 @@ BugReport &BR) override; }; +class FalsePositiveRefutationBRVisitor final + : public BugReporterVisitorImpl { + // Flag first node as seen by the visitor. + bool FirstNodeVisited = true; + +public: + FalsePositiveRefutationBRVisitor() = default; + + void Profile(llvm::FoldingSetNodeID &ID) const override { + static int Tag = 0; + ID.AddPointer(&Tag); + } + + 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 @@ -486,6 +486,7 @@ EnvironmentManager EnvMgr; std::unique_ptr StoreMgr; std::unique_ptr ConstraintMgr; + std::unique_ptr RefutationMgr; ProgramState::GenericDataMap::Factory GDMFactory; TaintedSubRegions::Factory TSRFactory; @@ -551,6 +552,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,35 @@ 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(); + + if (FirstNodeVisited) { + RefutationMgr.reset(); + RefutationMgr.addRangeConstraints(PrevCR, SuccCR, /*OnlyPurged=*/false); + FirstNodeVisited = false; + } + + auto K = Succ->getLocation().getKind(); + if (K == ProgramPoint::PreStmtPurgeDeadSymbolsKind || + K == ProgramPoint::PostStmtPurgeDeadSymbolsKind) { + RefutationMgr.addRangeConstraints(PrevCR, SuccCR, /*OnlyPurged=*/true); + } + + if (Prev->pred_size() == 0 && !RefutationMgr.isModelFeasible()) { + const LocationContext *LC = Succ->getLocationContext(); + BR.markInvalid("Infeasible constraints", LC); + } + + return nullptr; +} 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,57 @@ 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 (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { + SymbolRef Sym = I.getKey(); + + if (OnlyPurged && SuccCR.contains(Sym)) + continue; + + Z3Expr Constraints = Z3Expr::fromBoolean(false); + + for (const auto &Range : I.getData()) { + 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. //===------------------------------------------------------------------===//