Open rpfeiffer opened 3 weeks ago
@llvm/issue-subscribers-clang-static-analyzer
Author: René Pfeiffer (rpfeiffer)
Could you please try 19 or main
branch? https://godbolt.org should be helpful.
@NagyDonat @Xazax-hun @haoNoQ WDYT of renaming -analyzer-constraints=z3
to something like -analyzer-constraints=unsupported-z3
to reflect that no maintainer is interested in fixing any of the crashes of the Z3-based solver?
I never heard of anyone interested in that area, we don't have build bots testing that configuration, etc.
I think we should also disclaim this shortcoming in the docs too, even in the help text of that flag.
Should I bring this to discuss to get more visibility to this?
I will retry with 19 and report back. I didn't know that the z3 resolver wasn't supported. This is good to know, because I know developers who run the static analyzer with this option in test pipelines.
WDYT of renaming -analyzer-constraints=z3 to something like -analyzer-constraints=unsupported-z3 to reflect that no maintainer is interested in fixing any of the crashes of the Z3-based solver? I never heard of anyone interested in that area, we don't have build bots testing that configuration, etc.
I completely agree, we should document that it is unsupported.
I would even suggest renaming it to deprecated-z3 and removing it in e.g. 2027 if nobody starts to support it -- we should not keep unsupported logic in the codebase indefinitely. Obviously, we should emphasize in the documentation that improving/fixing it is not deprecated (or is it? would it be possible to fix and support z3, or are there tough blocker issues?), but users should not expect stable results from it.
Side note: The z3 stuff is used in security research and computer science (I teach at an university for applied sciences). This was the reason why I used it in the first place. Marking z3 not supported or clearly stating that it will be removed is a good idea. I didn't realise this.
clang-19 (installed from Debian package) yields the same or a similar error:
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace, preprocessed source, and associated run script. Stack dump:
LLVM_SYMBOLIZER_PATH
to point to it):
0 libLLVM.so.19.1 0x00007fd1724b7d06 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) + 54
1 libLLVM.so.19.1 0x00007fd1724b59b0 llvm::sys::RunSignalHandlers() + 80
2 libLLVM.so.19.1 0x00007fd1723fdb50
3 libc.so.6 0x00007fd17105b050
4 libLLVM.so.19.1 0x00007fd1723d1695 llvm::APSInt::Profile(llvm::FoldingSetNodeID&) const + 5
5 libclang-cpp.so.19.1 0x00007fd17c1690f0 clang::ento::BasicValueFactory::getValue(llvm::APSInt const&) + 80
6 libclang-cpp.so.19.1 0x00007fd17c2716ac
7 libclang-cpp.so.19.1 0x00007fd17c2710c1
8 libclang-cpp.so.19.1 0x00007fd17c270a99
9 libclang-cpp.so.19.1 0x00007fd17c26ef70
10 libclang-cpp.so.19.1 0x00007fd17c26c69a
11 libclang-cpp.so.19.1 0x00007fd17c27af87 clang::ento::SValBuilder::evalBinOp(llvm::IntrusiveRefCntPtrPLEASE ATTACH THE FOLLOWING FILES TO THE BUG REPORT: Preprocessed source(s) and associated run script(s) are located at: clang++-19: note: diagnostic msg: /tmp/minirng-34878d.cpp clang++-19: note: diagnostic msg: /tmp/minirng-34878d.sh clang++-19: note: diagnostic msg:
Given the similarity and the status of the z3 support I won't test the static analyzer with clang-20. There are a lot of other options for static analysis, so the crash has low priority. I can work around z3 in my projects.
WDYT of renaming -analyzer-constraints=z3 to something like -analyzer-constraints=unsupported-z3 to reflect that no maintainer is interested in fixing any of the crashes of the Z3-based solver?
I agree that we should not give the false impression of something being supported. At the same time, I wish someone stepped up, so I wonder if we could word it in a way that is more like a call to action. E.g., whenever someone is using the analyzer with Z3 as the constraint solver, we could emit a warning that we are actually looking for people interested in support this?
I would even suggest renaming it to deprecated-z3 and removing it in e.g. 2027 if nobody starts to support it
We could do it in stages. First unsupported, and later deprecated. But to make it clear, this is only applicable to using z3 as the main constraint solver, right? And it is not applicable to refutation.
WDYT of renaming -analyzer-constraints=z3 to something like -analyzer-constraints=unsupported-z3 to reflect that no maintainer is interested in fixing any of the crashes of the Z3-based solver? I never heard of anyone interested in that area, we don't have build bots testing that configuration, etc.
I completely agree, we should document that it is unsupported.
I would even suggest renaming it to deprecated-z3 and removing it in e.g. 2027 if nobody starts to support it -- we should not keep unsupported logic in the codebase indefinitely. Obviously, we should emphasize in the documentation that improving/fixing it is not deprecated (or is it? would it be possible to fix and support z3, or are there tough blocker issues?), but users should not expect stable results from it.
I think at bare minimum to say that it's supported, we should make it pass check-clang
and have a build bot enforcing that. Now, neither of these two holds. After this, we could say that it's experimental - but definitely not production ready.
Side note: The z3 stuff is used in security research and computer science (I teach at an university for applied sciences). This was the reason why I used it in the first place. Marking z3 not supported or clearly stating that it will be removed is a good idea. I didn't realise this.
No worries. You didn't know that this is not supported. Even bug reports could be useful for people picking this up. However, at the stage it is right now, it crashes so often that I don't think there is much value tracking them. That's why I'm pushing back here. We get reports like this time to time.
WDYT of renaming -analyzer-constraints=z3 to something like -analyzer-constraints=unsupported-z3 to reflect that no maintainer is interested in fixing any of the crashes of the Z3-based solver?
I agree that we should not give the false impression of something being supported. At the same time, I wish someone stepped up, so I wonder if we could word it in a way that is more like a call to action. E.g., whenever someone is using the analyzer with Z3 as the constraint solver, we could emit a warning that we are actually looking for people interested in support this?
I believe, it could be improved to be quite fast - but likely never as fast as the range-based solver. PRs are welcomed of course.
I would even suggest renaming it to deprecated-z3 and removing it in e.g. 2027 if nobody starts to support it
We could do it in stages. First unsupported, and later deprecated. But to make it clear, this is only applicable to using z3 as the main constraint solver, right? And it is not applicable to refutation.
Z3-crosschecking (refutation) is solid.
I ran the static analyzer with the following command line:
clang++-18 --analyze -Xclang -analyzer-constraints=z3 -Wall -Werror -I. -g -O0 -march=native -std=c++20 minirng.cpp
The output was as follows:
PLEASE submit a bug report to https://github.com/llvm/llvm-project/issues/ and include the crash backtrace, preprocessed source, and associated run script. Stack dump:
0 Calling std::uniform_int_distribution::_S_nd(class std::mersenne_twister_engine<unsigned long, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005> &, unsigned long) at line /usr/bin/../lib/gcc/x86_64-linux-gnu/12/../../../../include/c++/12/bits/uniform_int_dist.h:307:25
1 Calling std::uniform_int_distribution::operator()(class std::mersenne_twister_engine<unsigned long, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005> &, const param_type &) at line /usr/bin/../lib/gcc/x86_64-linux-gnu/12/../../../../include/c++/12/bits/uniform_int_dist.h:193:18
2 Calling std::uniform_int_distribution::operator()(class std::mersenne_twister_engine<unsigned long, 64, 312, 156, 31, 13043109905998158313, 29, 6148914691236517205, 17, 8202884508482404352, 37, 18444473444759240704, 43, 6364136223846793005> &) at line 171
3 Calling main(int, char **)::(anonymous class)::operator()()
LLVM_SYMBOLIZER_PATH
to point to it): 0 libLLVM-18.so.18.1 0x00007f1d0bd9f8b6 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) + 54 1 libLLVM-18.so.18.1 0x00007f1d0bd9d8e0 llvm::sys::RunSignalHandlers() + 80 2 libLLVM-18.so.18.1 0x00007f1d0bce9910 3 libc.so.6 0x00007f1d0ae5b050 4 libLLVM-18.so.18.1 0x00007f1d0bcbdb45 llvm::APSInt::Profile(llvm::FoldingSetNodeID&) const + 5 5 libclang-cpp.so.18.1 0x00007f1d153f9b60 clang::ento::BasicValueFactory::getValue(llvm::APSInt const&) + 80 6 libclang-cpp.so.18.1 0x00007f1d1550046f 7 libclang-cpp.so.18.1 0x00007f1d154ffe42 8 libclang-cpp.so.18.1 0x00007f1d154ff859 9 libclang-cpp.so.18.1 0x00007f1d154fdd80 10 libclang-cpp.so.18.1 0x00007f1d154fb45a 11 libclang-cpp.so.18.1 0x00007f1d15508017 clang::ento::SValBuilder::evalBinOp(llvm::IntrusiveRefCntPtrPLEASE ATTACH THE FOLLOWING FILES TO THE BUG REPORT: Preprocessed source(s) and associated run script(s) are located at: clang++-18: note: diagnostic msg: /tmp/minirng-896626.cpp clang++-18: note: diagnostic msg: /tmp/minirng-896626.sh clang++-18: note: diagnostic msg:
output.zip
Let me know if you need anything else.