From 7179078a7a3501a27cc18d911079025a3865e134 Mon Sep 17 00:00:00 2001 From: "Mikhail R. Gadelha" Date: Wed, 25 Jul 2018 12:49:43 +0000 Subject: [PATCH] [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 git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@337922 91177308-0d34-0410-b5e6-96231b3b80d8 --- .../Core/PathSensitive/SMTConstraintManager.h | 8 --- .../Core/PathSensitive/SMTSolver.h | 2 + .../Core/BugReporterVisitors.cpp | 63 +++++++++---------- .../Core/SMTConstraintManager.cpp | 25 -------- .../Core/Z3ConstraintManager.cpp | 13 +++- 5 files changed, 45 insertions(+), 66 deletions(-) diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 6b44e02b3e..f593fcc393 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -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(); } diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h index 3a3adc044a..bdd3505d62 100644 --- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -954,6 +954,8 @@ public: using SMTSolverRef = std::shared_ptr; +std::unique_ptr CreateZ3Solver(); + } // namespace ento } // namespace clang diff --git a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp index f17f41a7ac..6213fc0598 100644 --- a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -2370,34 +2370,6 @@ TaintBugVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN, return std::make_shared(L, "Taint originated here"); } -static bool areConstraintsUnfeasible(BugReporterContext &BRC, - const ConstraintRangeTy &Cs) { - // Create a refutation manager - std::unique_ptr RefutationMgr = CreateZ3ConstraintManager( - BRC.getStateManager(), BRC.getStateManager().getOwningEngine()); - - SMTConstraintManager *SMTRefutationMgr = - static_cast(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::finalizeVisitor( // 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 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::VisitNode(const ExplodedNode *N, BugReporterContext &BRC, BugReport &BR) { // Collect new constraints - addNewConstraints(Constraints, N->getState()->get(), - N->getState()->get_context()); + const ConstraintRangeTy &NewCs = N->getState()->get(); + ConstraintRangeTy::Factory &CF = + N->getState()->get_context(); + + // 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; } diff --git a/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp index 542b3741be..8e31635dc9 100644 --- a/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp @@ -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) { diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 1051493279..f15737bed4 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -932,7 +932,7 @@ public: }; // end class Z3Solver class Z3ConstraintManager : public SMTConstraintManager { - SMTSolverRef Solver = std::make_shared(); + SMTSolverRef Solver = CreateZ3Solver(); public: Z3ConstraintManager(SubEngine *SE, SValBuilder &SB) @@ -1043,6 +1043,17 @@ public: #endif +std::unique_ptr clang::ento::CreateZ3Solver() { +#if CLANG_ANALYZER_WITH_Z3 + return llvm::make_unique(); +#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 ento::CreateZ3ConstraintManager(ProgramStateManager &StMgr, SubEngine *Eng) { #if CLANG_ANALYZER_WITH_Z3 -- 2.40.0