Generalised the SMT state constraints

This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around.

We achieve this by not using shared_ptr  anymore, as llvm::ImmutableSet doesn't seem to like it.

The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around.

As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay!

Differential Revision: https://reviews.llvm.org/D54975

git-svn-id: https://llvm.org/svn/llvm-project/cfe/trunk@353370 91177308-0d34-0410-b5e6-96231b3b80d8

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index a407c77c32e43b8688e4b01ab53e2b0cdc559232..7e7ec1267beb488c952cf102ea7967eae8514f85 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
@@ -17,10 +17,14 @@
 #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 
+typedef llvm::ImmutableSet<
+    std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>>
+    ConstraintSMTTy;
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
+
 namespace clang {
 namespace ento {
 
-template <typename ConstraintSMT, typename SMTExprTy>
 class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
   SMTSolverRef &Solver;
 
@@ -212,7 +216,7 @@ public:
     OS << nl << sep << "Constraints:";
     for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {
       OS << nl << ' ' << I->first << " : ";
-      I->second.print(OS);
+      I->second->print(OS);
     }
     OS << nl;
   }
@@ -272,8 +276,7 @@ protected:
                                      const SMTExprRef &Exp) {
     // Check the model, avoid simplifying AST to save time
     if (checkModel(State, Sym, Exp).isConstrainedTrue())
-      return State->add<ConstraintSMT>(
-          std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+      return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     return nullptr;
   }
@@ -289,9 +292,9 @@ protected:
     if (I != IE) {
       std::vector<SMTExprRef> ASTs;
 
-      SMTExprRef Constraint = Solver->newExprRef(I++->second);
+      SMTExprRef Constraint = I++->second;
       while (I != IE) {
-        Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));
+        Constraint = Solver->mkAnd(Constraint, I++->second);
       }
 
       Solver->addConstraint(Constraint);
@@ -301,8 +304,8 @@ protected:
   // Generate and check a Z3 model, using the given constraint.
   ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,
                                const SMTExprRef &Exp) const {
-    ProgramStateRef NewState = State->add<ConstraintSMT>(
-        std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));
+    ProgramStateRef NewState =
+        State->add<ConstraintSMT>(std::make_pair(Sym, Exp));
 
     llvm::FoldingSetNodeID ID;
     NewState->get<ConstraintSMT>().Profile(ID);

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
index 1b975e1a43e4e5aa78e85216d21ee24b79ef0f3c..b2cfba878d5dcb169f272e0bb395606ce7d6b1da 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
@@ -33,10 +33,7 @@ public:
     return ID1 < ID2;
   }
 
-  virtual void Profile(llvm::FoldingSetNodeID &ID) const {
-    static int Tag = 0;
-    ID.AddPointer(&Tag);
-  }
+  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
 
   friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
     return LHS.equal_to(RHS);
@@ -53,7 +50,7 @@ protected:
 };
 
 /// Shared pointer for SMTExprs, used by SMTSolver API.
-using SMTExprRef = std::shared_ptr<SMTExpr>;
+using SMTExprRef = const SMTExpr *;
 
 } // namespace ento
 } // namespace clang

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
index e5d71ade7d46e49e834bbca90b6e0a66c7a26067..d7b86789a81dbfde6f4071c3e85dce7ba36b3c42 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
@@ -70,9 +70,6 @@ public:
   // Returns an appropriate sort for the given AST.
   virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
 
-  // Returns a new SMTExprRef from an SMTExpr
-  virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;
-
   /// Given a constraint, adds it to the solver
   virtual void addConstraint(const SMTExprRef &Exp) const = 0;
 

diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
index cbafb8469e5076d67bf0a5f402b1b03dfc6b49d8..933bc3ec74e29cff13fd977fd0d282a3909285ef 100644 (file)
--- a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
+++ b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
@@ -52,6 +52,15 @@ public:
     return Size;
   };
 
+  virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
+
+  bool operator<(const SMTSort &Other) const {
+    llvm::FoldingSetNodeID ID1, ID2;
+    Profile(ID1);
+    Other.Profile(ID2);
+    return ID1 < ID2;
+  }
+
   friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
     return LHS.equal_to(RHS);
   }
@@ -82,7 +91,7 @@ protected:
 };
 
 /// Shared pointer for SMTSorts, used by SMTSolver API.
-using SMTSortRef = std::shared_ptr<SMTSort>;
+using SMTSortRef = const SMTSort *;
 
 } // namespace ento
 } // namespace clang

diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 3681570da5b563f890906a31bbf613e73f8dbf10..934f56ed6d15f5e5b5e0bac0ec246d9186888962 100644 (file)
--- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
@@ -102,6 +102,11 @@ public:
       Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
   }
 
+  void Profile(llvm::FoldingSetNodeID &ID) const {
+    ID.AddInteger(
+        Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
+  }
+
   bool isBitvectorSortImpl() const override {
     return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
   }
@@ -172,7 +177,7 @@ public:
   }
 
   void Profile(llvm::FoldingSetNodeID &ID) const override {
-    ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));
+    ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
   }
 
   /// Comparison of AST equality, not model equivalence.
@@ -253,13 +258,6 @@ static bool areEquivalent(const llvm::fltSemantics &LHS,
           llvm::APFloat::semanticsSizeInBits(RHS));
 }
 
-} // end anonymous namespace
-
-typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty;
-REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)
-
-namespace {
-
 class Z3Solver : public SMTSolver {
   friend class Z3ConstraintManager;
 
@@ -267,6 +265,12 @@ class Z3Solver : public SMTSolver {
 
   Z3_solver Solver;
 
+  // Cache Sorts
+  std::set<Z3Sort> CachedSorts;
+
+  // Cache Exprs
+  std::set<Z3Expr> CachedExprs;
+
 public:
   Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
     Z3_solver_inc_ref(Context.Context, Solver);
@@ -286,42 +290,48 @@ public:
     Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
   }
 
+  // Given an SMTSort, adds/retrives it from the cache and returns
+  // an SMTSortRef to the SMTSort in the cache
+  SMTSortRef newSortRef(const SMTSort &Sort) {
+    auto It = CachedSorts.insert(toZ3Sort(Sort));
+    return &(*It.first);
+  }
+
+  // Given an SMTExpr, adds/retrives it from the cache and returns
+  // an SMTExprRef to the SMTExpr in the cache
+  SMTExprRef newExprRef(const SMTExpr &Exp) {
+    auto It = CachedExprs.insert(toZ3Expr(Exp));
+    return &(*It.first);
+  }
+
   SMTSortRef getBoolSort() override {
-    return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
   }
 
   SMTSortRef getBitvectorSort(unsigned BitWidth) override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_bv_sort(Context.Context, BitWidth));
+    return newSortRef(
+        Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
   }
 
   SMTSortRef getSort(const SMTExprRef &Exp) override {
-    return std::make_shared<Z3Sort>(
-        Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));
+    return newSortRef(
+        Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
   }
 
   SMTSortRef getFloat16Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_16(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
   }
 
   SMTSortRef getFloat32Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_32(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
   }
 
   SMTSortRef getFloat64Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_64(Context.Context));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
   }
 
   SMTSortRef getFloat128Sort() override {
-    return std::make_shared<Z3Sort>(Context,
-                                    Z3_mk_fpa_sort_128(Context.Context));
-  }
-
-  SMTExprRef newExprRef(const SMTExpr &E) const override {
-    return std::make_shared<Z3Expr>(toZ3Expr(E));
+    return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
   }
 
   SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
@@ -804,7 +814,7 @@ public:
   }
 }; // end class Z3Solver
 
-class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {
+class Z3ConstraintManager : public SMTConstraintManager {
   SMTSolverRef Solver = CreateZ3Solver();
 
 public: