r337922 - [analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Jul 25 05:49:43 PDT 2018
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
More information about the cfe-commits
mailing list