Author: mramalho Date: Wed Jul 25 05:49:43 2018 New Revision: 337922 URL: http://llvm.org/viewvc/llvm-project?rev=337922&view=rev Log: [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver
Summary: Third patch in the refactoring series, to decouple the SMT Solver from the Refutation Manager (1st: D49668, 2nd: D49767). The refutation API in the `SMTConstraintManager` was a hack to allow us to create an SMT solver and verify the constraints; it was conceptually wrong from the start. Now, we don't actually need to use the `SMTConstraintManager` and can create an SMT object directly, add the constraints and check them. While updating the Falsification visitor, I inlined the two functions that were used to collect the constraints and add them to the solver. As a result of this patch, we could move the SMT API elsewhere and as it's not really dependent on the CSA anymore. Maybe we can create a new dir (utils/smt) for Z3 and future solvers? Reviewers: NoQ, george.karpenkov Reviewed By: george.karpenkov Subscribers: xazax.hun, szepet, a.sidorin Differential Revision: https://reviews.llvm.org/D49768 Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=337922&r1=337921&r2=337922&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Jul 25 05:49:43 2018 @@ -54,14 +54,6 @@ public: const llvm::APSInt *getSymVal(ProgramStateRef State, SymbolRef Sym) const override; - /// Converts the ranged constraints of a set of symbols to SMT - /// - /// \param CR The set of constraints. - void addRangeConstraints(clang::ento::ConstraintRangeTy CR); - - /// Checks if the added constraints are satisfiable - clang::ento::ConditionTruthVal isModelFeasible(); - /// Dumps SMT formula LLVM_DUMP_METHOD void dump() const { Solver->dump(); } Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=337922&r1=337921&r2=337922&view=diff ============================================================================== --- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original) +++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Jul 25 05:49:43 2018 @@ -954,6 +954,8 @@ public: using SMTSolverRef = std::shared_ptr<SMTSolver>; +std::unique_ptr<SMTSolver> CreateZ3Solver(); + } // namespace ento } // namespace clang Modified: cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp?rev=337922&r1=337921&r2=337922&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp Wed Jul 25 05:49:43 2018 @@ -2370,34 +2370,6 @@ TaintBugVisitor::VisitNode(const Explode 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()) {} @@ -2406,8 +2378,26 @@ void FalsePositiveRefutationBRVisitor::f // Collect new constraints VisitNode(EndPathNode, nullptr, BRC, BR); - // Create a new refutation manager and check feasibility - if (areConstraintsUnfeasible(BRC, Constraints)) + // Create a refutation manager + std::unique_ptr<SMTSolver> RefutationSolver = CreateZ3Solver(); + ASTContext &Ctx = BRC.getASTContext(); + + // Add constraints to the solver + for (const auto &I : Constraints) { + SymbolRef Sym = I.first; + + SMTExprRef Constraints = RefutationSolver->fromBoolean(false); + for (const auto &Range : I.second) { + Constraints = RefutationSolver->mkOr( + Constraints, + RefutationSolver->getRangeExpr(Ctx, Sym, Range.From(), Range.To(), + /*InRange=*/true)); + } + RefutationSolver->addConstraint(Constraints); + } + + // And check for satisfiability + if (RefutationSolver->check().isConstrainedFalse()) BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); } @@ -2417,8 +2407,17 @@ FalsePositiveRefutationBRVisitor::VisitN BugReporterContext &BRC, BugReport &BR) { // Collect new constraints - addNewConstraints(Constraints, N->getState()->get<ConstraintRange>(), - N->getState()->get_context<ConstraintRange>()); + const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>(); + ConstraintRangeTy::Factory &CF = + N->getState()->get_context<ConstraintRange>(); + + // Add constraints if we don't have them yet + for (auto const &C : NewCs) { + const SymbolRef &Sym = C.first; + if (!Constraints.contains(Sym)) { + Constraints = CF.add(Constraints, Sym, C.second); + } + } return nullptr; } Modified: cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp?rev=337922&r1=337921&r2=337922&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp Wed Jul 25 05:49:43 2018 @@ -15,31 +15,6 @@ using namespace clang; using namespace ento; -void SMTConstraintManager::addRangeConstraints(ConstraintRangeTy CR) { - ASTContext &Ctx = getBasicVals().getContext(); - Solver->reset(); - - for (const auto &I : CR) { - SymbolRef Sym = I.first; - - SMTExprRef Constraints = Solver->fromBoolean(false); - for (const auto &Range : I.second) { - SMTExprRef SymRange = Solver->getRangeExpr(Ctx, Sym, Range.From(), - Range.To(), /*InRange=*/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); - } - Solver->addConstraint(Constraints); - } -} - -clang::ento::ConditionTruthVal SMTConstraintManager::isModelFeasible() { - return Solver->check(); -} - ProgramStateRef SMTConstraintManager::assumeSym(ProgramStateRef State, SymbolRef Sym, bool Assumption) { Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=337922&r1=337921&r2=337922&view=diff ============================================================================== --- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original) +++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Jul 25 05:49:43 2018 @@ -932,7 +932,7 @@ public: }; // end class Z3Solver class Z3ConstraintManager : public SMTConstraintManager { - SMTSolverRef Solver = std::make_shared<Z3Solver>(); + SMTSolverRef Solver = CreateZ3Solver(); public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) @@ -1043,6 +1043,17 @@ public: #endif +std::unique_ptr<SMTSolver> clang::ento::CreateZ3Solver() { +#if CLANG_ANALYZER_WITH_Z3 + return llvm::make_unique<Z3Solver>(); +#else + llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild " + "with -DCLANG_ANALYZER_BUILD_Z3=ON", + false); + return nullptr; +#endif +} + std::unique_ptr<ConstraintManager> ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { #if CLANG_ANALYZER_WITH_Z3 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
