r353370 - Generalised the SMT state constraints
Mikhail Ramalho via cfe-commits
cfe-commits at lists.llvm.org
Mon Feb 11 16:16:48 PST 2019
Hi Douglas, thank you for the report.
We are discussing the issue in https://reviews.llvm.org/D54975.
@michaelplatings said he found a solution and I asked him to run the tests
locally. If it indeed fixes the issue, I'd say we push it.
Em seg, 11 de fev de 2019 às 20:13, <douglas.yung at sony.com> escreveu:
> Hi Mikhail,
>
> Your commit seems to be causing a build failure on our internal Windows
> build bot that uses Visual Studio 2015. Can you take a look?
>
> C:\src\upstream\llvm_clean\tools\clang\include\clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23):
> error C2872: 'ConstraintSMTTy': ambiguous symbol
> [C:\src\upstream\353370-PS4-Release\tools\clang\lib\StaticAnalyzer\Core\clangStaticAnalyzerCore.vcxproj]
>
> C:\src\upstream\llvm_clean\tools\clang\include\clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(22):
> note: could be 'llvm::ImmutableSet<std::pair<clang::ento::SymbolRef,const
> clang::ento::SMTExpr *>,llvm::ImutContainerInfo<ValT>> ConstraintSMTTy'
> with
> [
> ValT=std::pair<clang::ento::SymbolRef,const
> clang::ento::SMTExpr *>
> ]
>
> C:\src\upstream\llvm_clean\tools\clang\include\clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23):
> note: or '`anonymous-namespace'::ConstraintSMTTy'
>
> I was able to reproduce the build failure locally on my Windows machine
> using Visual Studio 2015 Update 3 (version 19.00.24215.1). Here are the
> cmake and build commands I used:
>
> CMake.exe -G "Visual Studio 14 Win64" -DCMAKE_BUILD_TYPE=Release
> -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_DEFAULT_TARGET_TRIPLE=x86_64-scei-ps4
> -DLLVM_TOOL_COMPILER_RT_BUILD:BOOL=OFF -DLLVM_BUILD_TESTS:BOOL=ON
> -DLLVM_BUILD_EXAMPLES:BOOL=ON -DCLANG_BUILD_EXAMPLES:BOOL=ON
> -DLLVM_TARGETS_TO_BUILD=X86 -DLLVM_LIT_ARGS="-v -j8"
> C:\src\upstream\llvm_clean
>
> Douglas Yung
>
> -----Original Message-----
> From: cfe-commits <cfe-commits-bounces at lists.llvm.org> On Behalf Of
> Mikhail R. Gadelha via cfe-commits
> Sent: Wednesday, February 6, 2019 19:18
> To: cfe-commits at lists.llvm.org
> Subject: r353370 - Generalised the SMT state constraints
>
> 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/SMTConstra
> +++ intManager.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:
>
>
> _______________________________________________
> cfe-commits mailing list
> cfe-commits at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
>
--
Mikhail Ramalho.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-commits/attachments/20190211/7b6f8162/attachment-0001.html>
More information about the cfe-commits
mailing list