Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h =================================================================== --- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -17,6 +17,7 @@ #include "clang/Basic/LLVM.h" #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" +#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "llvm/ADT/FoldingSet.h" #include "llvm/ADT/STLExtras.h" @@ -338,8 +339,11 @@ /// Holds the constraints in a given path ConstraintRangeTy Constraints; + /// Holds the Refutation Manager + ConstraintManager &RefutationMgr; + public: - FalsePositiveRefutationBRVisitor(); + FalsePositiveRefutationBRVisitor(ConstraintManager &R); void Profile(llvm::FoldingSetNodeID &ID) const override; Index: include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -24,6 +24,8 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SMTSolverRef &Solver; + llvm::SmallVector<ConstraintRangeTy, 32> AllPathConstraints; + public: SMTConstraintManager(clang::ento::SubEngine *SE, clang::ento::SValBuilder &SB, SMTSolverRef &S) @@ -60,7 +62,7 @@ void addRangeConstraints(clang::ento::ConstraintRangeTy CR); /// Checks if the added constraints are satisfiable - clang::ento::ConditionTruthVal isModelFeasible(); + clang::ento::ConditionTruthVal areConstraintsFeasible(); /// Dumps SMT formula LLVM_DUMP_METHOD void dump() const { Solver->dump(); } Index: lib/StaticAnalyzer/Core/BugReporter.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporter.cpp +++ lib/StaticAnalyzer/Core/BugReporter.cpp @@ -2586,18 +2586,24 @@ /// Find a non-invalidated report for a given equivalence class, /// and return together with a cache of visitors notes. /// If none found, return a nullptr paired with an empty cache. -static -std::pair<BugReport*, std::unique_ptr<VisitorsDiagnosticsTy>> findValidReport( - TrimmedGraph &TrimG, - ReportGraph &ErrorGraph, - ArrayRef<BugReport *> &bugReports, - AnalyzerOptions &Opts, - GRBugReporter &Reporter) { +static std::pair<BugReport *, std::unique_ptr<VisitorsDiagnosticsTy>> +findValidReport(TrimmedGraph &TrimG, ReportGraph &ErrorGraph, + ArrayRef<BugReport *> &bugReports, AnalyzerOptions &Opts, + GRBugReporter &Reporter) { + std::unique_ptr<ConstraintManager> RefutationMgr = nullptr; + if (Opts.shouldCrosscheckWithZ3()) { + RefutationMgr = + CreateZ3ConstraintManager(Reporter.getStateManager(), + Reporter.getStateManager().getOwningEngine()); + } + + BugReport *R = nullptr; + std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes = nullptr; while (TrimG.popNextReportGraph(ErrorGraph)) { // Find the BugReport with the original location. assert(ErrorGraph.Index < bugReports.size()); - BugReport *R = bugReports[ErrorGraph.Index]; + R = bugReports[ErrorGraph.Index]; assert(R && "No original report found for sliced graph."); assert(R->isValid() && "Report selected by trimmed graph marked invalid."); const ExplodedNode *ErrorNode = ErrorGraph.ErrorNode; @@ -2606,7 +2612,8 @@ // further analysis is required R->addVisitor(llvm::make_unique<LikelyFalsePositiveSuppressionBRVisitor>()); if (Opts.shouldCrosscheckWithZ3()) - R->addVisitor(llvm::make_unique<FalsePositiveRefutationBRVisitor>()); + R->addVisitor( + llvm::make_unique<FalsePositiveRefutationBRVisitor>(*RefutationMgr)); // Register additional node visitors. R->addVisitor(llvm::make_unique<NilReceiverBRVisitor>()); @@ -2616,12 +2623,24 @@ BugReporterContext BRC(Reporter, ErrorGraph.BackMap); // Run all visitors on a given graph, once. - std::unique_ptr<VisitorsDiagnosticsTy> visitorNotes = - generateVisitorsDiagnostics(R, ErrorNode, BRC); + visitorNotes = generateVisitorsDiagnostics(R, ErrorNode, BRC); if (R->isValid()) - return std::make_pair(R, std::move(visitorNotes)); + break; + } + + if (Opts.shouldCrosscheckWithZ3()) { + SMTConstraintManager *SMTRefutationMgr = + static_cast<SMTConstraintManager *>(RefutationMgr.get()); + + if (SMTRefutationMgr->areConstraintsFeasible().isConstrainedFalse()) + R->markInvalid("Infeasible constraints", + R->getErrorNode()->getLocationContext()); } + + if (R->isValid()) + return std::make_pair(R, std::move(visitorNotes)); + return std::make_pair(nullptr, llvm::make_unique<VisitorsDiagnosticsTy>()); } Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -44,7 +44,6 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SubEngine.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h" #include "llvm/ADT/ArrayRef.h" #include "llvm/ADT/None.h" #include "llvm/ADT/Optional.h" @@ -2370,45 +2369,22 @@ return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here"); } -static bool areConstraintsUnfeasible(BugReporterContext &BRC, - const ConstraintRangeTy &Cs) { - // Create a refutation manager - std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager( - BRC.getStateManager(), BRC.getStateManager().getOwningEngine()); - - SMTConstraintManager *SMTRefutationMgr = - static_cast<SMTConstraintManager *>(RefutationMgr.get()); - - // Add constraints to the solver - SMTRefutationMgr->addRangeConstraints(Cs); - - // And check for satisfiability - return SMTRefutationMgr->isModelFeasible().isConstrainedFalse(); -} - -static void addNewConstraints(ConstraintRangeTy &Cs, - const ConstraintRangeTy &NewCs, - ConstraintRangeTy::Factory &CF) { - // Add constraints if we don't have them yet - for (auto const &C : NewCs) { - const SymbolRef &Sym = C.first; - if (!Cs.contains(Sym)) { - Cs = CF.add(Cs, Sym, C.second); - } - } -} - -FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() - : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {} +FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor( + ConstraintManager &R) + : Constraints(ConstraintRangeTy::Factory().getEmptyMap()), + RefutationMgr(R) {} void FalsePositiveRefutationBRVisitor::finalizeVisitor( BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) { // Collect new constraints VisitNode(EndPathNode, nullptr, BRC, BR); - // Create a new refutation manager and check feasibility - if (areConstraintsUnfeasible(BRC, Constraints)) - BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); + // Adds constraints to the Solver + SMTConstraintManager &SMTRefutationMgr = + static_cast<SMTConstraintManager &>(RefutationMgr); + + // Add constraints to the solver + SMTRefutationMgr.addRangeConstraints(Constraints); } std::shared_ptr<PathDiagnosticPiece> @@ -2416,9 +2392,17 @@ const ExplodedNode *PrevN, BugReporterContext &BRC, BugReport &BR) { - // Collect new constraints - addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(), - N->getState()->get_context<ConstraintRange>()); + const ConstraintRangeTy &Cs = N->getState()->get<ConstraintRange>(); + ConstraintRangeTy::Factory &CF = + N->getState()->get_context<ConstraintRange>(); + + // Collect new constraints, if we don't have them yet + for (auto const &C : Cs) { + const SymbolRef &Sym = C.first; + if (!Constraints.contains(Sym)) { + Constraints = CF.add(Constraints, Sym, C.second); + } + } return nullptr; } Index: lib/StaticAnalyzer/Core/SMTConstraintManager.cpp =================================================================== --- lib/StaticAnalyzer/Core/SMTConstraintManager.cpp +++ lib/StaticAnalyzer/Core/SMTConstraintManager.cpp @@ -16,26 +16,42 @@ using namespace ento; void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { - Solver->reset(); + AllPathConstraints.push_back(CR); +} + +clang::ento::ConditionTruthVal SMTConstraintManager::areConstraintsFeasible() { - for (const auto &I : CR) { - SymbolRef Sym = I.first; + // Will hold all the constraints of all path + SMTExprRef AllPathFormula = Solver->fromBoolean(true); - SMTExprRef Constraints = Solver->fromBoolean(false); - for (const auto &Range : I.second) { - SMTExprRef SymRange = - getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true); + for (const auto &CR : AllPathConstraints) { + SMTExprRef PathConstraints = Solver->fromBoolean(true); - // FIXME: the last argument (isSigned) is not used when generating the - // or expression, as both arguments are booleans - Constraints = - Solver->fromBinOp(Constraints, BO_LOr, SymRange, /*IsSigned=*/true); + // This loop will add all the constraints of a given path + for (const auto &I : CR) { + SymbolRef Sym = I.first; + + // Collect all the ranges for a given symbol + SMTExprRef SymbolConstraints = Solver->fromBoolean(false); + for (const auto &Range : I.second) { + SymbolConstraints = Solver->mkOr( + SymbolConstraints, + getRangeExpr(Sym, Range.From(), Range.To(), /*InRange=*/true)); + } + + // Collect all the ranges for all symbol + PathConstraints = Solver->mkAnd(PathConstraints, SymbolConstraints); } - Solver->addConstraint(Constraints); + + // At this point, we have all the constraints of a given path in + // PathConstraints, so add them to AllPathFormula + AllPathFormula = Solver->mkAnd(AllPathFormula, PathConstraints); } -} -clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() { + // All now holds all the constraints, of all paths + Solver->addConstraint(AllPathFormula); + + // Check for satisfiability return Solver->check(); }