r353370 - Generalised the SMT state constraints
Mikhail R. Gadelha via cfe-commits
cfe-commits at lists.llvm.org
Wed Feb 6 19:17:36 PST 2019
Author: mramalho
Date: Wed Feb 6 19:17:36 2019
New Revision: 353370
URL: http://llvm.org/viewvc/llvm-project?rev=353370&view=rev
Log:
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
Modified:
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353370&r1=353369&r2=353370&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h Wed Feb 6 19:17:36 2019
@@ -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);
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=353370&r1=353369&r2=353370&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h Wed Feb 6 19:17:36 2019
@@ -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
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=353370&r1=353369&r2=353370&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h Wed Feb 6 19:17:36 2019
@@ -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;
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=353370&r1=353369&r2=353370&view=diff
==============================================================================
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (original)
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h Wed Feb 6 19:17:36 2019
@@ -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
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp
URL: http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=353370&r1=353369&r2=353370&view=diff
==============================================================================
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Feb 6 19:17:36 2019
@@ -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::fl
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:
More information about the cfe-commits
mailing list