Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
> > > Could you provide a minimal example where USRs are not generated? It might > be the case that there are other ways to fix it. > > Sure, I'll try to reduce our testcase, but basically we have an ASTFrontendAction [0] that adds a set of intrinsics [1] to the preprocessor [2]. [0] https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/AST/esbmc_action.h [1] https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/clang_c_language.cpp#L206 [2] https://github.com/esbmc/esbmc/blob/master/src/clang-c-frontend/AST/esbmc_action.h#L31 -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D45517: [analyzer] False positive refutation with Z3
Hi, > Just a bit of context and to have some expectation management regarding > this patch. The main purpose of this implementation was to back a thesis. > It was made under a very serious time pressure and the main goal was to be > able to measure on real world projects as soon as possible and in the > meantime to be flexible so we can measure multiple configurations (like > incremental solving). > > So the goal was a flexible proof of concept that is sensible to measure in > the shortest possible time. After the thesis was done, Reka started to work > an another GSoC project, so she had no time to review the code with the > requirements of upstreaming in mind. Nevertheless we found that sharing the > proof of concept could be useful for the community. So it is perfectly > reasonable if you disagree with some design decisions behind this patch, > because the requirements for the thesis (in the short time frame) was very > different from the requirements of upstreaming this work. In a different > context these decisions made perfect sense. > > Just want to comment here and give thanks again for the first version of the refutation code. It's being really helpful to develop the approach this code as a base; things would definitely be slower if I had to start it from scratch. Thanks! -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D45517: [analyzer] False positive refutation with Z3
> > > Awesome! Does it mean that the optimization for adding less constraints > was in fact buggy? > > I pretty sure it was not related to the optimizations, I removed them days ago (in the previous version of this patch) and the bug was still there. > > 2. Could it be something unrelated to your changes? Any given trunk > version can be buggy, but usually those are resolved very fast, so if you > update now the issue can go away. > > Watching cfe-commits mailing list might be helpful there. > > I update my repo every other day and it's been happening for the past two/three weeks :/ The compiler shows the following error: posix_spawn failed: Argument list too long There are some discussions in several places about it. -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
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&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>
> +ConstraintSMTTy;
> +REGISTER_TRAIT_WITH_PROGRAMSTATE(ConstraintSMT, ConstraintSMTTy)
> +
> namespace clang {
> namespace ento {
>
> -template 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(
> - 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
Re: [PATCH] D54978: Move the SMT API to LLVM
Hi,
Thank you for the discussion, I was finally able to reproduce the error.
> Hello @ddcc.
> I agree with your reasoning here and developed a patch based on this line
> of thought:
>
> diff --git a/llvm/cmake/modules/FindZ3.cmake
> b/llvm/cmake/modules/FindZ3.cmake
> index 5c6d3f0b427..b213342df37 100644
> --- a/llvm/cmake/modules/FindZ3.cmake
> +++ b/llvm/cmake/modules/FindZ3.cmake
> @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE)
>string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1"
> Z3_VERSION_STRING "${libz3_version_str}")
>unset(libz3_version_str)
> +else()
> +# The version could not be determined from running Z3_EXECUTABLE.
> Set the
> +# version Z3 to the lowest possible value such that all checks for a
> +# minimum version will fail.
> +set(Z3_VERSION_STRING "0.0.0")
>endif()
>
># handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
>
> This works for everything I could throw at it. If you think it's
> reasonable I can open another ticket and have the code reviewed as a
> separate fix.
>
>
This seems fine but I'm wondering if we can remove the binary requirement
all together: is it possible to run a small program that would return
EXIT_SUCCESS if the library is the correct version?
Something like:
```
#include
int main()
{
unsigned int major, minor, build, revision;
Z3_get_version(&major, &minor, &build, &revision);
if(major >= 4 && minor >= 7 && build >= 1)
return EXIT_SUCCESS;
return EXIT_FAILURE;
}
```
This would be part of FindZ3.cmake and would set Z3_FOUND.
Do you guys think it's possible? I'm almost certain it can be done with
autotools, but I'm clueless when it comes to cmake.
--
Mikhail Ramalho.
___
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
> > Why wasn't there a file for function parameter? Function parameters *are* > declared in some file, or am I missing something? > > They are declared in some file defined by the line markers; the file are not registered in the SourceManager as actual files, so getting the FileEntry will always fail, that's why I changed it to get the PresumedLoc. More general question is: how do we want USRs for function parameters to > work, specifically should USR of the same param of different declarations > be the same or different? > That's a good point, this patch will generated different names for the same function param if a function is first defined then declared somewhere else. I guess it should follow the USR generation pattern for FunctionDecls, what do you think? -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
Hi, > Or is the that whenever there's a `#line` directive we get into a > "virtual" file that's not registered in the `SourceManager`? > > The virtual file is actually registered in the SourceManager but the FileEntry for it is NULL (USRGeneration.cpp:33), which forces printLoc to return true (USRGeneration.cpp:38) and the USR is not generated. I believe the USR gen for params should have follow the functionDecl convention. I'm reworking the patch now. > int func(int param1); > int func(int param2); > // param1 and param2 could both have the same USR, but different names. > That might (or might not) be surprising. > I agree here, they should have the same USR. -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
Hi, > After thinking about this a bit, and use cases like rename and > find-declaration that could be USR based, I think including some location > information is the right way to go, which I think is the current behavior. > > What do you man by location information? Only the filename or filename + offset (current behaviour)? -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D36610: [Tooling] Add option to getFullyQualifiedName using a custom PritingPolicy
Last review asked to change the test case, I just want to make sure everything is fine this time. 2018-05-02 8:54 GMT+01:00 Manuel Klimek via Phabricator < revi...@reviews.llvm.org>: > klimek added a comment. > > I believe this was accepted by rnk - are you waiting for specific further > feedback? > > > https://reviews.llvm.org/D36610 > > > > -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
Hi, > Filename + offset for things like function parameters, where we have to > identify the particular function declaration they're part of. > For static functions themselveds, just the filename. I think this is > current behavior in both cases. > > But then we're back to the initial question, what to do when there are linemarkers that change the filename/line number? Should we ignore linemarkers and use filename + offset of the real file? Should we try to calculate the offset of the decl in the virtual file? Thank you, -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
Re: [PATCH] D42966: Fix USR generation in the presence of #line directives or linemarkes
Hi, > I would say "yes". Let's not rely on linemarkers, unless we can explain > why that's a good idea. > > Sounds reasonable to me, specially considering cases like rename and find-declaration. > > Where do virtual files come from in the first place? > > >From the linemarker: https://gcc.gnu.org/onlinedocs/cpp/Preprocessor-Output.html For instance: $ cat foo.c int f(int a); # 1 "file1.c" 1 int g(int b); clang generates: |-FunctionDecl 0x6866ff0 col:5 f 'int (int)' | `-ParmVarDecl 0x6866f30 col:11 a 'int' `-FunctionDecl 0x6867138 col:5 g 'int (int)' `-ParmVarDecl 0x68670b0 col:11 b 'int' Note that the location of f and g are different, despite being in the same file. The preprocessor inserts linemarkers by default: $ clang foo.c -E # 1 "foo.c" # 1 "" 1 # 1 "" 3 # 349 "" 3 # 1 "" 1 # 1 "" 2 # 1 "foo.c" 2 int f(int a); # 1 "file1.c" 1 int g(int b); unless you call it with -P: $ clang foo.c -E -P int f(int a); int g(int b); > Repository: > rC Clang > > https://reviews.llvm.org/D42966 > > > > -- Mikhail Ramalho. ___ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
