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.y...@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-boun...@lists.llvm.org> On Behalf Of > Mikhail R. Gadelha via cfe-commits > Sent: Wednesday, February 6, 2019 19:18 > To: cfe-commits@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@lists.llvm.org > https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits > -- Mikhail Ramalho.
_______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
