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 shouldPostProcessBugReports + Optional PostProcessBugReports; + /// \sa reportIssuesInMainSourceFile Optional ReportIssuesInMainSourceFile; @@ -575,6 +578,13 @@ /// which accepts the values "true" and "false". bool shouldSuppressFromCXXStandardLibrary(); + /// Returns whether bug reports should be postprocessed using the Z3 + /// constraint manager backend. + /// + /// This is controlled by the 'postprocess-reports' config option, + /// which accepts the values "true" and "false". + bool shouldPostProcessBugReports(); + /// 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 @@ -343,6 +343,24 @@ BugReport &BR) override; }; +class FalsePositiveRefutationBRVisitor final + : public BugReporterVisitorImpl { + bool isInvalidated = false; + +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 @@ -175,6 +175,10 @@ return checkNull(State, Sym); } + virtual bool checkRangedStateConstraints(ProgramStateRef State) { + return true; + } + 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 @@ -475,6 +475,7 @@ EnvironmentManager EnvMgr; std::unique_ptr StoreMgr; std::unique_ptr ConstraintMgr; + std::unique_ptr RefutationMgr; ProgramState::GenericDataMap::Factory GDMFactory; TaintedSubRegions::Factory TSRFactory; @@ -540,6 +541,7 @@ 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::shouldPostProcessBugReports() { + return getBooleanOption(PostProcessBugReports, + "postprocess-reports", + /* 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().shouldPostProcessBugReports()) + 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 @@ -2333,3 +2333,26 @@ return std::move(Piece); } + +std::shared_ptr +FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *Succ, + const ExplodedNode *Prev, + BugReporterContext &BRC, + BugReport &BR) { + if (isInvalidated) + return nullptr; + + if (Succ->getLocation().getKind() != ProgramPoint::BlockEdgeKind) + return nullptr; + + ConstraintManager &RefutationMgr = + BRC.getStateManager().getRefutationManager(); + + if (!RefutationMgr.checkRangedStateConstraints(Succ->getState())) { + const LocationContext *LC = Succ->getLocationContext(); + BR.markInvalid("Infeasible constraints", LC); + isInvalidated = true; + } + + 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.shouldPostProcessBugReports() + ? 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,8 @@ void print(ProgramStateRef St, raw_ostream &Out, const char *nl, const char *sep) override; + bool checkRangedStateConstraints(ProgramStateRef State) override; + //===------------------------------------------------------------------===// // Implementation for interface from SimpleConstraintManager. //===------------------------------------------------------------------===// @@ -1235,6 +1238,47 @@ return State->set(CZ); } +bool Z3ConstraintManager::checkRangedStateConstraints(ProgramStateRef State) { + Solver.reset(); + ConstraintRangeTy CR = State->get(); + + for (ConstraintRangeTy::iterator I = CR.begin(), E = CR.end(); I != E; ++I) { + SymbolRef Sym = I.getKey(); + + 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); + + if (From == To) { + Z3Expr Eq = getZ3BinExpr(Exp, SymTy, BO_EQ, FromExp, RangeTy, nullptr); + Solver.addConstraint(Eq); + } else { + Z3Expr LHS = getZ3BinExpr(Exp, SymTy, BO_GE, FromExp, RangeTy, nullptr); + Z3Expr RHS = getZ3BinExpr(Exp, SymTy, BO_LE, ToExp, RangeTy, nullptr); + Solver.addConstraint(Z3Expr::fromBinOp(LHS, BO_LOr, RHS, isSignedTy)); + } + } + } + // If Z3 timeouts, Z3_L_UNDEF is returned, and we assume that the state + // is feasible. + return Solver.check() != Z3_L_FALSE; +} + //===------------------------------------------------------------------===// // Internal implementation. //===------------------------------------------------------------------===//