[analyzer] Removed API used by the Refutation Manager from SMTConstraintManager and replace by proper calls to SMTSolver

[mikhail.ramalho]

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?

[george.karpenkov]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1053

not sure whether it makes sense to return nullptr vs. crashing.

[mikhail.ramalho]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1053

True, I got it from CreateZ3ConstraintManager. Should I remove it from both?

[george.karpenkov]

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

1053

if it was there before, let's leave it for now

include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

public:
   // Implementation for interface from ConstraintManager.
   //===------------------------------------------------------------------===//
 
   ConditionTruthVal checkNull(ProgramStateRef State, SymbolRef Sym) override;
 
   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(); }
 
 protected:
   //===------------------------------------------------------------------===//
   // Internal implementation.
   //===------------------------------------------------------------------===//
 

include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h

public:
   /// Reset the solver and remove all constraints.
   virtual void reset() const = 0;
 
   virtual void print(raw_ostream &OS) const = 0;
 };
 
 using SMTSolverRef = std::shared_ptr<SMTSolver>;
 
+std::unique_ptr<SMTSolver> CreateZ3Solver();
+
 } // namespace ento
 } // namespace clang
 
 #endif

lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

TaintBugVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN,
   PathDiagnosticLocation L =
       PathDiagnosticLocation::createBegin(S, BRC.getSourceManager(), NCtx);
   if (!L.isValid() || !L.asLocation().isValid())
     return nullptr;
 
   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()) {}
 
 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))
+  // 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());
 }
 
 std::shared_ptr<PathDiagnosticPiece>
 FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N,
                                             const ExplodedNode *PrevN,
                                             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;
 }
 
 void FalsePositiveRefutationBRVisitor::Profile(
     llvm::FoldingSetNodeID &ID) const {
   static int Tag = 0;
   ID.AddPointer(&Tag);
 }

lib/StaticAnalyzer/Core/SMTConstraintManager.cpp

 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h"
 #include "clang/Basic/TargetInfo.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
 
 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) {
   ASTContext &Ctx = getBasicVals().getContext();
 
   QualType RetTy;
   bool hasComparison;
 

lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp

public:
   void reset() const override { Z3_solver_reset(Context.Context, Solver); }
 
   void print(raw_ostream &OS) const override {
     OS << Z3_solver_to_string(Context.Context, Solver);
   }
 }; // end class Z3Solver
 
 class Z3ConstraintManager : public SMTConstraintManager {
-  SMTSolverRef Solver = std::make_shared<Z3Solver>();
+  SMTSolverRef Solver = CreateZ3Solver();
 
 public:
   Z3ConstraintManager(SubEngine *SE, SValBuilder &SB)
       : SMTConstraintManager(SE, SB, Solver) {}
 
   void addStateConstraints(ProgramStateRef State) const override {
     // TODO: Don't add all the constraints, only the relevant ones
     ConstraintZ3Ty CZ = State->get<ConstraintZ3>();
void print(ProgramStateRef St, raw_ostream &OS, const char *nl,
     OS << nl;
   }
 }; // end class Z3ConstraintManager
 
 } // end anonymous namespace
 
 #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
   return llvm::make_unique<Z3ConstraintManager>(Eng, StMgr.getSValBuilder());
 #else
   llvm::report_fatal_error("Clang was not compiled with Z3 support, rebuild "
                            "with -DCLANG_ANALYZER_BUILD_Z3=ON",
                            false);
   return nullptr;
 #endif
 }