Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -18,10 +18,14 @@ #include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h" #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" +typedef llvm::ImmutableSet< + std::pair> + ConstraintSMTTy; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy) + namespace clang { namespace ento { -template class SMTConstraintManager : public clang::ento::SimpleConstraintManager { SMTSolverRef &Solver; @@ -213,7 +217,7 @@ 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; } @@ -273,8 +277,7 @@ const SMTExprRef &Exp) { // Check the model, avoid simplifying AST to save time if (checkModel(State, Sym, Exp).isConstrainedTrue()) - return State->add( - std::make_pair(Sym, static_cast(*Exp))); + return State->add(std::make_pair(Sym, Exp)); return nullptr; } @@ -290,9 +293,9 @@ if (I != IE) { std::vector 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); @@ -302,8 +305,8 @@ // Generate and check a Z3 model, using the given constraint. ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym, const SMTExprRef &Exp) const { - ProgramStateRef NewState = State->add( - std::make_pair(Sym, static_cast(*Exp))); + ProgramStateRef NewState = + State->add(std::make_pair(Sym, Exp)); llvm::FoldingSetNodeID ID; NewState->get().Profile(ID); Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h @@ -34,10 +34,7 @@ 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); @@ -54,7 +51,7 @@ }; /// Shared pointer for SMTExprs, used by SMTSolver API. -using SMTExprRef = std::shared_ptr; +using SMTExprRef = const SMTExpr *; } // namespace ento } // namespace clang Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h @@ -71,9 +71,6 @@ // 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; Index: clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h =================================================================== --- clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h +++ clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h @@ -53,6 +53,15 @@ 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); } @@ -83,7 +92,7 @@ }; /// Shared pointer for SMTSorts, used by SMTSolver API. -using SMTSortRef = std::shared_ptr; +using SMTSortRef = const SMTSort *; } // namespace ento } // namespace clang Index: clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp =================================================================== --- clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ clang/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -103,6 +103,11 @@ Z3_dec_ref(Context.Context, reinterpret_cast(Sort)); } + void Profile(llvm::FoldingSetNodeID &ID) const { + ID.AddInteger( + Z3_get_ast_id(Context.Context, reinterpret_cast(Sort))); + } + bool isBitvectorSortImpl() const override { return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT); } @@ -173,7 +178,7 @@ } 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. @@ -254,13 +259,6 @@ llvm::APFloat::semanticsSizeInBits(RHS)); } -} // end anonymous namespace - -typedef llvm::ImmutableSet> ConstraintZ3Ty; -REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty) - -namespace { - class Z3Solver : public SMTSolver { friend class Z3ConstraintManager; @@ -268,6 +266,12 @@ Z3_solver Solver; + // Cache Sorts + std::set CachedSorts; + + // Cache Exprs + std::set CachedExprs; + public: Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { Z3_solver_inc_ref(Context.Context, Solver); @@ -287,42 +291,48 @@ 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(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(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( - 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(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(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(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(Context, - Z3_mk_fpa_sort_128(Context.Context)); - } - - SMTExprRef newExprRef(const SMTExpr &E) const override { - return std::make_shared(toZ3Expr(E)); + return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context))); } SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { @@ -805,7 +815,7 @@ } }; // end class Z3Solver -class Z3ConstraintManager : public SMTConstraintManager { +class Z3ConstraintManager : public SMTConstraintManager { SMTSolverRef Solver = CreateZ3Solver(); public: