[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and...

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

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 6b44e02b3e18e3acbffc3c70c06b224ab59c5305..f593fcc39362b7886c81958cb9776d3724b20190 100644 (file)
--- 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 3a3adc044a4002b0cebb42380e9f6c2e461cfc03..bdd3505d621f8c370eb4c6a3f094eec9f4e960c0 100644 (file)
--- 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<SMTSolver>;
 
+std::unique_ptr<SMTSolver> CreateZ3Solver();
+
 } // namespace ento
 } // namespace clang
 

diff --git a/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index f17f41a7ac93265e47f104cc313748c14ff9b41d..6213fc0598a6ad054cdcba04ff3b2dedb97e3ae1 100644 (file)
--- 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<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::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<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::VisitNode(const ExplodedNode *N,
                                             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;
 }

diff --git a/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp b/lib/StaticAnalyzer/Core/SMTConstraintManager.cpp
index 542b3741be8deaa00772f55ce1576bc4b49f4bf5..8e31635dc9428fad0795163a42e59a8c3f81b9b3 100644 (file)
--- 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 10514932792e7fa01185f3f2c1692e247d6d8bc4..f15737bed4592e65a4e80ca5a50d7bd483c25d82 100644 (file)
--- 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<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