Re: r353370 - Generalised the SMT state constraints
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, 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 clang::ento::SMTExpr *>,llvm::ImutContainerInfo> ConstraintSMTTy'
> with
> [
> ValT=std::pair 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 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=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=353369=353370=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>
> +ConstraintSMTTy;
> +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
> +
> namespace clang {
> namespace ento {
>
> -template class
> SMTConstraintManager : public clang::ento::SimpleConstraintManager {
>SMTSolverRef
>
> @@ -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 ) {
> // 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;
>
RE: r353370 - Generalised the SMT state constraints
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,llvm::ImutContainerInfo> ConstraintSMTTy'
with
[
ValT=std::pair
]
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 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=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=353369=353370=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>
+ConstraintSMTTy;
+REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
+
namespace clang {
namespace ento {
-template class
SMTConstraintManager : public clang::ento::SimpleConstraintManager {
SMTSolverRef
@@ -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 ) {
// 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 ) const {
-ProgramStateRef NewState = State->add(
-std::make_pair(Sym,
