<div dir="ltr"><div dir="ltr"><div dir="ltr">Hi Douglas, thank you for the report.<div><br></div><div>We are discussing the issue in <a href="https://reviews.llvm.org/D54975">https://reviews.llvm.org/D54975</a>. </div><div><br></div><div>@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.</div><div><br></div><div><br></div></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Em seg, 11 de fev de 2019 às 20:13, <<a href="mailto:douglas.yung@sony.com">douglas.yung@sony.com</a>> escreveu:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Hi Mikhail,<br>
<br>
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?<br>
<br>
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]<br>
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'<br>
with<br>
[<br>
ValT=std::pair<clang::ento::SymbolRef,const clang::ento::SMTExpr *><br>
]<br>
C:\src\upstream\llvm_clean\tools\clang\include\clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h(23): note: or '`anonymous-namespace'::ConstraintSMTTy'<br>
<br>
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:<br>
<br>
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<br>
<br>
Douglas Yung<br>
<br>
-----Original Message-----<br>
From: cfe-commits <<a href="mailto:cfe-commits-bounces@lists.llvm.org" target="_blank">cfe-commits-bounces@lists.llvm.org</a>> On Behalf Of Mikhail R. Gadelha via cfe-commits<br>
Sent: Wednesday, February 6, 2019 19:18<br>
To: <a href="mailto:cfe-commits@lists.llvm.org" target="_blank">cfe-commits@lists.llvm.org</a><br>
Subject: r353370 - Generalised the SMT state constraints<br>
<br>
Author: mramalho<br>
Date: Wed Feb 6 19:17:36 2019<br>
New Revision: 353370<br>
<br>
URL: <a href="http://llvm.org/viewvc/llvm-project?rev=353370&view=rev" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project?rev=353370&view=rev</a><br>
Log:<br>
Generalised the SMT state constraints<br>
<br>
This patch moves the ConstraintSMT definition to the SMTConstraintManager header to make it easier to move the Z3 backend around.<br>
<br>
We achieve this by not using shared_ptr anymore, as llvm::ImmutableSet doesn't seem to like it.<br>
<br>
The solver specific exprs and sorts are cached in the Z3Solver object now and we move pointers to those objects around.<br>
<br>
As a nice side-effect, SMTConstraintManager doesn't have to be a template anymore. Yay!<br>
<br>
Differential Revision: <a href="https://reviews.llvm.org/D54975" rel="noreferrer" target="_blank">https://reviews.llvm.org/D54975</a><br>
<br>
Modified:<br>
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h<br>
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h<br>
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h<br>
cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h<br>
cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp<br>
<br>
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353370&r1=353369&r2=353370&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h?rev=353370&r1=353369&r2=353370&view=diff</a><br>
==============================================================================<br>
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (original)<br>
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstra<br>
+++ intManager.h Wed Feb 6 19:17:36 2019<br>
@@ -17,10 +17,14 @@<br>
#include "clang/StaticAnalyzer/Core/PathSensitive/RangedConstraintManager.h"<br>
#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"<br>
<br>
+typedef llvm::ImmutableSet<<br>
+ std::pair<clang::ento::SymbolRef, const clang::ento::SMTExpr *>><br>
+ ConstraintSMTTy;<br>
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)<br>
+<br>
namespace clang {<br>
namespace ento {<br>
<br>
-template <typename ConstraintSMT, typename SMTExprTy> class SMTConstraintManager : public clang::ento::SimpleConstraintManager {<br>
SMTSolverRef &Solver;<br>
<br>
@@ -212,7 +216,7 @@ public:<br>
OS << nl << sep << "Constraints:";<br>
for (auto I = CZ.begin(), E = CZ.end(); I != E; ++I) {<br>
OS << nl << ' ' << I->first << " : ";<br>
- I->second.print(OS);<br>
+ I->second->print(OS);<br>
}<br>
OS << nl;<br>
}<br>
@@ -272,8 +276,7 @@ protected:<br>
const SMTExprRef &Exp) {<br>
// Check the model, avoid simplifying AST to save time<br>
if (checkModel(State, Sym, Exp).isConstrainedTrue())<br>
- return State->add<ConstraintSMT>(<br>
- std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));<br>
+ return State->add<ConstraintSMT>(std::make_pair(Sym, Exp));<br>
<br>
return nullptr;<br>
}<br>
@@ -289,9 +292,9 @@ protected:<br>
if (I != IE) {<br>
std::vector<SMTExprRef> ASTs;<br>
<br>
- SMTExprRef Constraint = Solver->newExprRef(I++->second);<br>
+ SMTExprRef Constraint = I++->second;<br>
while (I != IE) {<br>
- Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second));<br>
+ Constraint = Solver->mkAnd(Constraint, I++->second);<br>
}<br>
<br>
Solver->addConstraint(Constraint);<br>
@@ -301,8 +304,8 @@ protected:<br>
// Generate and check a Z3 model, using the given constraint.<br>
ConditionTruthVal checkModel(ProgramStateRef State, SymbolRef Sym,<br>
const SMTExprRef &Exp) const {<br>
- ProgramStateRef NewState = State->add<ConstraintSMT>(<br>
- std::make_pair(Sym, static_cast<const SMTExprTy &>(*Exp)));<br>
+ ProgramStateRef NewState =<br>
+ State->add<ConstraintSMT>(std::make_pair(Sym, Exp));<br>
<br>
llvm::FoldingSetNodeID ID;<br>
NewState->get<ConstraintSMT>().Profile(ID);<br>
<br>
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=353370&r1=353369&r2=353370&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h?rev=353370&r1=353369&r2=353370&view=diff</a><br>
==============================================================================<br>
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h (original)<br>
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTExpr.h <br>
+++ Wed Feb 6 19:17:36 2019<br>
@@ -33,10 +33,7 @@ public:<br>
return ID1 < ID2;<br>
}<br>
<br>
- virtual void Profile(llvm::FoldingSetNodeID &ID) const {<br>
- static int Tag = 0;<br>
- ID.AddPointer(&Tag);<br>
- }<br>
+ virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;<br>
<br>
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {<br>
return LHS.equal_to(RHS);<br>
@@ -53,7 +50,7 @@ protected:<br>
};<br>
<br>
/// Shared pointer for SMTExprs, used by SMTSolver API.<br>
-using SMTExprRef = std::shared_ptr<SMTExpr>;<br>
+using SMTExprRef = const SMTExpr *;<br>
<br>
} // namespace ento<br>
} // namespace clang<br>
<br>
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=353370&r1=353369&r2=353370&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h?rev=353370&r1=353369&r2=353370&view=diff</a><br>
==============================================================================<br>
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.h (original)<br>
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSolver.<br>
+++ h Wed Feb 6 19:17:36 2019<br>
@@ -70,9 +70,6 @@ public:<br>
// Returns an appropriate sort for the given AST.<br>
virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;<br>
<br>
- // Returns a new SMTExprRef from an SMTExpr<br>
- virtual SMTExprRef newExprRef(const SMTExpr &E) const = 0;<br>
-<br>
/// Given a constraint, adds it to the solver<br>
virtual void addConstraint(const SMTExprRef &Exp) const = 0;<br>
<br>
<br>
Modified: cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=353370&r1=353369&r2=353370&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project/cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h?rev=353370&r1=353369&r2=353370&view=diff</a><br>
==============================================================================<br>
--- cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h (original)<br>
+++ cfe/trunk/include/clang/StaticAnalyzer/Core/PathSensitive/SMTSort.h <br>
+++ Wed Feb 6 19:17:36 2019<br>
@@ -52,6 +52,15 @@ public:<br>
return Size;<br>
};<br>
<br>
+ virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;<br>
+<br>
+ bool operator<(const SMTSort &Other) const {<br>
+ llvm::FoldingSetNodeID ID1, ID2;<br>
+ Profile(ID1);<br>
+ Other.Profile(ID2);<br>
+ return ID1 < ID2;<br>
+ }<br>
+<br>
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {<br>
return LHS.equal_to(RHS);<br>
}<br>
@@ -82,7 +91,7 @@ protected:<br>
};<br>
<br>
/// Shared pointer for SMTSorts, used by SMTSolver API.<br>
-using SMTSortRef = std::shared_ptr<SMTSort>;<br>
+using SMTSortRef = const SMTSort *;<br>
<br>
} // namespace ento<br>
} // namespace clang<br>
<br>
Modified: cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp<br>
URL: <a href="http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=353370&r1=353369&r2=353370&view=diff" rel="noreferrer" target="_blank">http://llvm.org/viewvc/llvm-project/cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp?rev=353370&r1=353369&r2=353370&view=diff</a><br>
==============================================================================<br>
--- cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp (original)<br>
+++ cfe/trunk/lib/StaticAnalyzer/Core/Z3ConstraintManager.cpp Wed Feb 6 <br>
+++ 19:17:36 2019<br>
@@ -102,6 +102,11 @@ public:<br>
Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));<br>
}<br>
<br>
+ void Profile(llvm::FoldingSetNodeID &ID) const {<br>
+ ID.AddInteger(<br>
+ Z3_get_ast_id(Context.Context, <br>
+ reinterpret_cast<Z3_ast>(Sort))); }<br>
+<br>
bool isBitvectorSortImpl() const override {<br>
return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);<br>
}<br>
@@ -172,7 +177,7 @@ public:<br>
}<br>
<br>
void Profile(llvm::FoldingSetNodeID &ID) const override {<br>
- ID.AddInteger(Z3_get_ast_hash(Context.Context, AST));<br>
+ ID.AddInteger(Z3_get_ast_id(Context.Context, AST));<br>
}<br>
<br>
/// Comparison of AST equality, not model equivalence.<br>
@@ -253,13 +258,6 @@ static bool areEquivalent(const llvm::fl<br>
llvm::APFloat::semanticsSizeInBits(RHS));<br>
}<br>
<br>
-} // end anonymous namespace<br>
-<br>
-typedef llvm::ImmutableSet<std::pair<SymbolRef, Z3Expr>> ConstraintZ3Ty; -REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintZ3, ConstraintZ3Ty)<br>
-<br>
-namespace {<br>
-<br>
class Z3Solver : public SMTSolver {<br>
friend class Z3ConstraintManager;<br>
<br>
@@ -267,6 +265,12 @@ class Z3Solver : public SMTSolver {<br>
<br>
Z3_solver Solver;<br>
<br>
+ // Cache Sorts<br>
+ std::set<Z3Sort> CachedSorts;<br>
+<br>
+ // Cache Exprs<br>
+ std::set<Z3Expr> CachedExprs;<br>
+<br>
public:<br>
Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {<br>
Z3_solver_inc_ref(Context.Context, Solver); @@ -286,42 +290,48 @@ public:<br>
Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);<br>
}<br>
<br>
+ // Given an SMTSort, adds/retrives it from the cache and returns // <br>
+ an SMTSortRef to the SMTSort in the cache SMTSortRef newSortRef(const <br>
+ SMTSort &Sort) {<br>
+ auto It = CachedSorts.insert(toZ3Sort(Sort));<br>
+ return &(*It.first);<br>
+ }<br>
+<br>
+ // Given an SMTExpr, adds/retrives it from the cache and returns // <br>
+ an SMTExprRef to the SMTExpr in the cache SMTExprRef newExprRef(const <br>
+ SMTExpr &Exp) {<br>
+ auto It = CachedExprs.insert(toZ3Expr(Exp));<br>
+ return &(*It.first);<br>
+ }<br>
+<br>
SMTSortRef getBoolSort() override {<br>
- return std::make_shared<Z3Sort>(Context, Z3_mk_bool_sort(Context.Context));<br>
+ return newSortRef(Z3Sort(Context, <br>
+ Z3_mk_bool_sort(Context.Context)));<br>
}<br>
<br>
SMTSortRef getBitvectorSort(unsigned BitWidth) override {<br>
- return std::make_shared<Z3Sort>(Context,<br>
- Z3_mk_bv_sort(Context.Context, BitWidth));<br>
+ return newSortRef(<br>
+ Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));<br>
}<br>
<br>
SMTSortRef getSort(const SMTExprRef &Exp) override {<br>
- return std::make_shared<Z3Sort>(<br>
- Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST));<br>
+ return newSortRef(<br>
+ Z3Sort(Context, Z3_get_sort(Context.Context, <br>
+ toZ3Expr(*Exp).AST)));<br>
}<br>
<br>
SMTSortRef getFloat16Sort() override {<br>
- return std::make_shared<Z3Sort>(Context,<br>
- Z3_mk_fpa_sort_16(Context.Context));<br>
+ return newSortRef(Z3Sort(Context, <br>
+ Z3_mk_fpa_sort_16(Context.Context)));<br>
}<br>
<br>
SMTSortRef getFloat32Sort() override {<br>
- return std::make_shared<Z3Sort>(Context,<br>
- Z3_mk_fpa_sort_32(Context.Context));<br>
+ return newSortRef(Z3Sort(Context, <br>
+ Z3_mk_fpa_sort_32(Context.Context)));<br>
}<br>
<br>
SMTSortRef getFloat64Sort() override {<br>
- return std::make_shared<Z3Sort>(Context,<br>
- Z3_mk_fpa_sort_64(Context.Context));<br>
+ return newSortRef(Z3Sort(Context, <br>
+ Z3_mk_fpa_sort_64(Context.Context)));<br>
}<br>
<br>
SMTSortRef getFloat128Sort() override {<br>
- return std::make_shared<Z3Sort>(Context,<br>
- Z3_mk_fpa_sort_128(Context.Context));<br>
- }<br>
-<br>
- SMTExprRef newExprRef(const SMTExpr &E) const override {<br>
- return std::make_shared<Z3Expr>(toZ3Expr(E));<br>
+ return newSortRef(Z3Sort(Context, <br>
+ Z3_mk_fpa_sort_128(Context.Context)));<br>
}<br>
<br>
SMTExprRef mkBVNeg(const SMTExprRef &Exp) override { @@ -804,7 +814,7 @@ public:<br>
}<br>
}; // end class Z3Solver<br>
<br>
-class Z3ConstraintManager : public SMTConstraintManager<ConstraintZ3, Z3Expr> {<br>
+class Z3ConstraintManager : public SMTConstraintManager {<br>
SMTSolverRef Solver = CreateZ3Solver();<br>
<br>
public:<br>
<br>
<br>
_______________________________________________<br>
cfe-commits mailing list<br>
<a href="mailto:cfe-commits@lists.llvm.org" target="_blank">cfe-commits@lists.llvm.org</a><br>
<a href="https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits" rel="noreferrer" target="_blank">https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits</a><br>
</blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr"><div><br></div><div>Mikhail Ramalho.</div></div></div>