From: Mikhail R. Gadelha Date: Thu, 7 Feb 2019 03:17:36 +0000 (+0000) Subject: Generalised the SMT state constraints X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=617fd0c671765052789f8c1409d227fe56ee3199;p=clang 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 a407c77c32..7e7ec1267b 100644 --- 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> + ConstraintSMTTy; +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy) + namespace clang { namespace ento { -template 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( - std::make_pair(Sym, static_cast(*Exp))); + return State->add(std::make_pair(Sym, Exp)); return nullptr; } @@ -289,9 +292,9 @@ protected: 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); @@ -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( - std::make_pair(Sym, static_cast(*Exp))); + ProgramStateRef NewState = + State->add(std::make_pair(Sym, Exp)); llvm::FoldingSetNodeID ID; NewState->get().Profile(ID); diff --git a/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h b/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h index 1b975e1a43..b2cfba878d 100644 --- 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; +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 e5d71ade7d..d7b86789a8 100644 --- 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 cbafb8469e..933bc3ec74 100644 --- 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; +using SMTSortRef = const SMTSort *; } // namespace ento } // namespace clang diff --git a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp index 3681570da5..934f56ed6d 100644 --- a/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp +++ b/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp @@ -102,6 +102,11 @@ public: 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); } @@ -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> 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 CachedSorts; + + // Cache Exprs + std::set 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(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 { @@ -804,7 +814,7 @@ public: } }; // end class Z3Solver -class Z3ConstraintManager : public SMTConstraintManager { +class Z3ConstraintManager : public SMTConstraintManager { SMTSolverRef Solver = CreateZ3Solver(); public: