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

llvm-svn: 353370

1 files changed, 36 insertions, 26 deletions

diff --git a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
index 3681570da5b..934f56ed6d1 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
+++ b/clang/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: