llvmbot
commented
1 year ago @llvm/issue-subscribers-clang-static-analyzer
Open dilyanpalauzov opened 1 year ago
llvmbot
commented
1 year ago @llvm/issue-subscribers-clang-static-analyzer
steakhal
commented
1 year ago The z3 constraint solver is not supported.
z3 refutation is supported though.
Ask CodeChecker about the --z3=on flag. I think they should simply drop it.
Can I close this?
dilyanpalauzov
commented
1 year ago I filled https://github.com/Ericsson/codechecker/issues/3757 about removing Z3 constraint solver from code checker.
The problem report is, that clang crashes. It is not codechecker’s fault, that clang crashes. The solution would be to fix clang, so that it does not crash.
dilyanpalauzov
commented
1 year ago If the z3 constraint solver is not supported, and is activated by -analyze -analyzer-constraints=z3, why do the files clang/test/Analysis/analyzer_test.py, clang/test/Analysis/missing-z3-nocrash.c, clang/test/Analysis/z3/pretty-dump.c, clang/test/Analysis/z3/enabled.c, and clang/test/Analysis/z3/D83660.c in llvm-project-15.0.2.src contain -analyzer-constraints=z3?
ryao
commented
1 year ago @mikhailramalho Is there any chance you could take a look?
dilyanpalauzov
commented
1 year ago llvm-project-15.0.2.src/clang/lib/Frontend/CompilerInvocation.cpp:ParseAnalyzerArgs() contains:
if (Value == NumConstraints) {
Diags.Report(diag::err_drv_invalid_value)
<< A->getAsString(Args) << Name;
} else {
#ifndef LLVM_WITH_Z3
if (Value == AnalysisConstraints::Z3ConstraintsModel) {
Diags.Report(diag::err_analyzer_not_built_with_z3);
}
#endif // LLVM_WITH_Z3
Opts.AnalysisConstraintsOpt = Value;
}I expect, when I pass -analyzer-constraints=z3 to clang, not compiled with Z3 to get the above “not build with z3 error”.
With Clang 14.0.5 (I have not checked it source code, if the above function is different), when it is not compiled with Z3, calling:
$ clang --analyze -Xclang -analyzer-constraints=z3 a.c
fatal error: error in backend: LLVM was not compiled with Z3 support, rebuild with -DLLVM_ENABLE_Z3_SOLVER=ON
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. Program arguments: clang --analyze -Xclang -analyzer-constraints=z3 a.c
1. <eof> parser at end of file
#0 0x00007fc682c0c975 llvm::sys::PrintStackTrace(llvm::raw_ostream&, int) (/lib64/libLLVM-14.so+0xc0c975)
#1 0x00007fc682c0cbfb (/lib64/libLLVM-14.so+0xc0cbfb)
#2 0x00007fc682c0a2b4 llvm::sys::RunSignalHandlers() (/lib64/libLLVM-14.so+0xc0a2b4)
#3 0x00007fc682c0be8b llvm::sys::CleanupOnSignal(unsigned long) (/lib64/libLLVM-14.so+0xc0be8b)
#4 0x00007fc682b1a439 (/lib64/libLLVM-14.so+0xb1a439)
#5 0x00007fc682b1a342 (/lib64/libLLVM-14.so+0xb1a342)
#6 0x00007fc682c067be llvm::sys::Process::Exit(int, bool) (/lib64/libLLVM-14.so+0xc067be) #7 0x00005561c5e92347 (/usr/bin/clang-14+0x15347)
#8 0x00007fc682b2c1b1 llvm::report_fatal_error(llvm::Twine const&, bool) (/lib64/libLLVM-14.so+0xb2c1b1) #9 0x00007fc682b2c07a (/lib64/libLLVM-14.so+0xb2c07a)
#10 0x00007fc682bf4946 (/lib64/libLLVM-14.so+0xbf4946) #11 0x00007fc68abc512a clang::ento::CreateZ3ConstraintManager(clang::ento::ProgramStateManager&, clang::ento::ExprEngine*) (/lib64/libclang-cpp.so.14+0x25c512a)
#12 0x00007fc68ab73d1f clang::ento::ProgramStateManager::ProgramStateManager(clang::ASTContext&, std::unique_ptr<clang::ento::StoreManager, std::default_delete<clang::ento::StoreManager> > (*)(clang::ento::ProgramStateManager&), std::unique_ptr<clang::ento::ConstraintManager, std::default_delete<clang::ento::ConstraintManager> > (*)(clang::ento::ProgramStateManager&, clang::ento::ExprEngine*), llvm::BumpPtrAllocatorImpl<llvm::MallocAllocator, 4096ul, 4096ul, 128ul>&, clang::ento::ExprEngine*) (/lib64/libclang-cpp.so.14+0x2573d1f)
#13 0x00007fc68ab1df92 clang::ento::ExprEngine::ExprEngine(clang::cross_tu::CrossTranslationUnitContext&, clang::ento::AnalysisManager&, llvm::DenseSet<clang::Decl const*, llvm::DenseMapInfo<clang::Decl const*, void> >*, clang::ento::FunctionSummariesTy*, clang::ento::ExprEngine::InliningModes) (/lib64/libclang-cpp.so.14+0x251df92)
#14 0x00007fc68aedc1d4 (/lib64/libclang-cpp.so.14+0x28dc1d4)
#15 0x00007fc68aeeb2cf (/lib64/libclang-cpp.so.14+0x28eb2cf)
#16 0x00007fc68aeebd63 (/lib64/libclang-cpp.so.14+0x28ebd63)
#17 0x00007fc688ff26c9 clang::ParseAST(clang::Sema&, bool, bool) (/lib64/libclang-cpp.so.14+0x9f26c9)
#18 0x00007fc68a8e15f9 clang::FrontendAction::Execute() (/lib64/libclang-cpp.so.14+0x22e15f9)
#19 0x00007fc68a8718a9 clang::CompilerInstance::ExecuteAction(clang::FrontendAction&) (/lib64/libclang-cpp.so.14+0x22718a9)
#20 0x00007fc68a94de5c clang::ExecuteCompilerInvocation(clang::CompilerInstance*) (/lib64/libclang-cpp.so.14+0x234de5c)
#21 0x00005561c5e935ee cc1_main(llvm::ArrayRef<char const*>, char const*, void*) (/usr/bin/clang-14+0x165ee)
#22 0x00005561c5e90623 (/usr/bin/clang-14+0x13623)
#23 0x00007fc68a57d1c9 (/lib64/libclang-cpp.so.14+0x1f7d1c9)
#24 0x00007fc682b1a315 llvm::CrashRecoveryContext::RunSafely(llvm::function_ref<void ()>) (/lib64/libLLVM-14.so+0xb1a315)
#25 0x00007fc68a57da31 (/lib64/libclang-cpp.so.14+0x1f7da31)
#26 0x00007fc68a55199b clang::driver::Compilation::ExecuteCommand(clang::driver::Command const&, clang::driver::Command const*&) const (/lib64/libclang-cpp.so.14+0x1f5199b)
#27 0x00007fc68a55213e clang::driver::Compilation::ExecuteJobs(clang::driver::JobList const&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) const (/lib64/libclang-cpp.so.14+0x1f5213e)
#28 0x00007fc68a55c5c2 clang::driver::Driver::ExecuteCompilation(clang::driver::Compilation&, llvm::SmallVectorImpl<std::pair<int, clang::driver::Command const*> >&) (/lib64/libclang-cpp.so.14+0x1f5c5c2)
#29 0x00005561c5e8da02 main (/usr/bin/clang-14+0x10a02)
#30 0x00007fc681829550 __libc_start_call_main (/lib64/libc.so.6+0x29550)
#31 0x00007fc681829609 __libc_start_main@GLIBC_2.2.5 (/lib64/libc.so.6+0x29609)
#32 0x00005561c5e8faa5 _start (/usr/bin/clang-14+0x12aa5)
Slide 27 of https://llvm.org/devmtg/2020-09/slides/Using_the_clang_static_ananalyzer_to_find_bugs.pdf contains:
Example of unhandled bitwise operations
▪ This program is safe, albeit brittle
1: unsigned int func(unsigned int a) {
2: unsigned int *z = 0;
3: if ((a & 1) && ((a & 1) ^1))
4: return *z; // unreachable
5: return 0;
6: }
$ clang --analyze test.cpp
test.cpp:5:16: warning: Dereference of null pointer (loaded from variable 'z') [core.NullDereference]
return *z;
^~
1 warning generated.
$ clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true test.cpp # Z3 Refutation, preferred
$ clang --analyze -Xclang -analyzer-constraints=z3 func.c # Z3 constraint manager, slowerWhen I try with b.c:
#include <stdio.h>
unsigned int func(unsigned int a) {
unsigned int *z = 0;
if ((a & 1) && ((a & 1) ^1))
return *z; // unreachable
return 0;
}
int main() {
printf("%i\n", func(7));
}all of
$ clang --analyzer-output text --analyze b.c
$ clang --analyzer-output text --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true b.c
$ clang --analyzer-output text --analyze -Xclang -analyzer-constraints=z3 b.cproduce no output with clang 15.0.1.
balazs-benics-sonarsource
commented
1 year ago If the
z3constraint solver is not supported, and is activated by-analyze -analyzer-constraints=z3, why do the files clang/test/Analysis/analyzer_test.py, clang/test/Analysis/missing-z3-nocrash.c, clang/test/Analysis/z3/pretty-dump.c, clang/test/Analysis/z3/enabled.c, and clang/test/Analysis/z3/D83660.c in llvm-project-15.0.2.src contain-analyzer-constraints=z3?
I believe, at some point, there was a push for having this, but I don't know anyone maintaining it now.
There are no build bots running any of those tests, I believe.
One can play with the (huge number of) crashes on the testsuite by running ./build/bin/llvm-lit --param USE_Z3_SOLVER=1 --show-unsupported --show-xfail clang/test/Analysis. This will not only run the tests by the original solver, but also with the z3-based solver.
I expect, when I pass -analyzer-constraints=z3 to clang, not compiled with Z3 to get the above “not build with z3 error”. With Clang 14.0.5 (I have not checked it source code, if the above function is different), when it is not compiled with Z3, calling:
Yes, previously the detection of the availability Z3 involved crashing clang. That was fixed by https://reviews.llvm.org/D120325
Slide 27 of https://llvm.org/devmtg/2020-09/slides/Using_the_clang_static_ananalyzer_to_find_bugs.pdf contains:
clang --analyze -Xclang -analyzer-constraints=z3 func.c
-analyzer-constraints=z3 is not only slower but also crashes a lot of times.
Could you elaborate on your last example? You said all of [...] produce no output with clang 15.0.1.
Well, the range-based solver is constantly being improved, making it smarter and smarter by the time.
It could be the case that in clang-15.0.1 the solver is smart enough to figure out that branch is unreachable.
However, by looking at the bitwise operations, I'm actually really surprised that we are not falling for it.
About the other two invocations:
Refutation is much cheaper than the z3-based solver, hence that brings value for production use. That is being actively maintained by the CodeChecker team AFAIK. So, I'm not surprised that we don't crash on that code, nor that we don't have a FP for it.
About the z3-based solver (-analyzer-constraints=z3), that is not maintained, and it could be the case that it happens to work for this example. Not crashing nor producing FP.
dilyanpalauzov
commented
1 year ago Could you elaborate on your last example? You said
all of [...] produce no output with clang 15.0.1.Well, the range-based solver is constantly being improved, making it smarter and smarter by the time. It could be the case that in clang-15.0.1 the solver is smart enough to figure out that branch is unreachable. However, by looking at the bitwise operations, I'm actually really surprised that we are not falling for it.
I mean what I said. The slide 27 above says that for the above input clang shall generate error (return *z dereferences NULL), when invoked without any form of Z3, but when I try it there is no error (the code is always detected to be unreachable, or for another reason).
ryao
commented
1 year ago That is odd. When I tried it last week, it was a false positive as reported in the slides. I believe that I tested against 15.0.2.
balazs-benics-sonarsource
commented
1 year ago I figured out what's going on.
1) We have a bug that we miss the null pointer dereference of *z if that not used (e.g. by some subexpression or initializes some variable) You can read more about why here. We should treat return statements as 'reads', we know about this.
2) Our range-based solver is now smart enough to deal with the bit-fiddling stuff. You can see that the value of the expressions is known to be constants, hence we can constant-fold them into a concrete decision that the branch should not be taken.
https://godbolt.org/z/57qqs5sKx
This range-based solver improvement was likely a recent improvement, which at the time of the mentioned presentation was not yet done.
EDIT: my first point might not be accurate, it seems like in return statements we detect null-derefs, as we should. I must have mixed this issue with something else.
dilyanpalauzov
commented
1 year ago Reading the previous comment, including the EDIT:, my understanding is that clangsa has a bug missing null pointer dereference of *z, and at the same time an improvement, detecting better the false messages.
Can you provide an example input, b.c (and possilbly other files), so that
$ clang --analyzer-output text --analyze b.c
$ clang --analyzer-output text --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true b.c
$ clang --analyzer-output text --analyze -Xclang -analyzer-constraints=z3 b.cproduces three different results?
balazs-benics-sonarsource
commented
1 year ago Can you provide an example input, b.c (and possilbly other files), so that $ clang --analyzer-output text --analyze b.c $ clang --analyzer-output text --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true b.c $ clang --analyzer-output text --analyze -Xclang -analyzer-constraints=z3 b.c produces three different results?
It seems like the example is from clang/test/Analysis/z3-crosscheck.c:
int foo(int x)
{
int *z = 0;
if ((x & 1) && ((x & 1) ^ 1))
#ifdef NO_CROSSCHECK
return *z; // expected-warning {{Dereference of null pointer (loaded from variable 'z')}}
#else
return *z; // no-warning
#endif
return 0;
}Any by reading that one might think that the range-based solver should report there a null dereference, while the z3 cross-checked invocation should not. Unfortunately, the tests with // REQUIRES: z3 are never run. The reason why they are never run, relates to the broken z3-based solver implementation. You can read more about that at D83677.
Since these tests are never run, they can get outdated; which probably happened with this one.
Coming back to your question, the difference between the three invocations. Let's have a look at this example:
void func(int a, int b) {
assert(a >= 1 && a <= 100);
assert(b >= 0 && b <= 100);
if (a*a == b*b && b == 0) {
// should be unreachable
clang_analyzer_warnIfReached();
}
clang_analyzer_warnIfReached();
}1) The range-based solver (right now) cannot conclude that the a*a == b*b && b == 0 is always false, hence it will reach the true branch.
2) The range-based solver with z3 cross-checking, it would still visit the seemingly feasible branch, find and construct the bugreport for the true-branch, but prior emitting the issue to the user we collect the constraints and create a SAT model for it which we pass to Z3 to see if there are contradictions; If there are, that means that the bugpath is infeasible, hence we discard the bug report without emitting it. The important thing is that we did spend time analysing an infeasible program path.
3) The z3-based solver could (and probably does) recognize that the true-branch is infeasible, so we simply don't spend time on analysing it - we just skip it. In theory, this could save analysis time, but in practice calling z3 for checking each condition is way to expensive; and this is why it runs so slow.
The bottom line is that, z3 crosscheck should have the benefit of the z3-based solver, without paying the price for calling z3 at each step during the analysis - only at the bug report construction.
haoNoQ
commented
1 year ago I filled Ericsson/codechecker#3757 about removing Z3 constraint solver from code checker.
The problem report is, that clang crashes. It is not codechecker’s fault, that clang crashes. The solution would be to fix clang, so that it does not crash.
If the
z3constraint solver is not supported, and is activated by-analyze -analyzer-constraints=z3, why do the files clang/test/Analysis/analyzer_test.py, clang/test/Analysis/missing-z3-nocrash.c, clang/test/Analysis/z3/pretty-dump.c, clang/test/Analysis/z3/enabled.c, and clang/test/Analysis/z3/D83660.c in llvm-project-15.0.2.src contain-analyzer-constraints=z3?
I want to chime in real quick about this confusion. I think your bug report is valuable, but the feature is indeed not supported, so we aren't likely to address it at the same rate as other crashes of this kind in supported use cases.
In case of LLVM, the word "supported" is not a synonym of "exists" or "implemented" or "available". The way LLVM is developed (which is very different from most open-source projects), every feature is supposed to be developed under a runtime flag. LLVM does not have feature branches. Developer policy explicitly forbids making feature branches. This leads to the situation where LLVM and Clang provide a lot of features that are available in the shipped binaries, covered with tests (because everything needs to be covered with tests), but not actually considered ready for everyday use aka "supported".
Static analysis with Z3 is one of such features. It was a valuable experiment which could have been successful in replacing the default constraint solver, it turned out to be unsuccessful (too slow), we're not removing it because it can be useful for gathering more experimental data for future research on constraint solvers (as this is still a difficult open problem), but we never claimed (or at least shouldn't have claimed) that we actually support it for any practical purposes.
When it comes to Clang, anything behind clang -cc1 or behind -Xclang isn't a supported interface. Only the Clang Driver is supported (alongside a few alternative drivers such as clang-cl).
With the static analyzer it's a bit of a mess because some actual features like -enable-checker don't have corresponding driver flags; they totally should have them. That said, such manual use of the static analyzer is also not recommended, the actual supported use case is with a GUI such as CodeChecker or scan-build or an IDE that integrates the static analyzer. This is because text output is inevitably terrible, you can't have basic quality of life in a non-visual tool.
So this presentation you're quoting, it just tells developers of the static analyzer how to access these guts of the implementation and experiment with them. This is absolutely not how users should use the static analyzer in their everyday life. I definitely think @vabridgers should have placed disclaimers about this all over the place! In other words, if you're not actively interested in addressing such crashes yourself, you're not supposed to touch these options.
So, this isn't about what you can or cannot do, this is about who's responsible for the outcome. In this sense, even though the compiler is crashing, this isn't a bug in the compiler. It's a bug in the interface that gives you access to a feature that doesn't exist. It becomes a bug in clang when we actually announce that it is supported, provide a proper user interface (CLI or GUI) to access it, or maybe make this the default behavior. But without all that, it's just a glorified never-shipped feature branch.
Yes, it's valuable to know that the feature has crashes on top of the slowdown. If somebody wants to use that feature, they have to worry not only about slowdowns, but also crashes, they'll have to recognize that the feature isn't fully implemented, and they'll have to work on its stability.
If this feature causes more confusion of this kind, we may choose to remove it entirely. Ideally, LLVM "branches" aren't supposed to be long-living. Maybe we should purge them more aggressively just to avoid confusion. For now it doesn't seem like it though, most of the time there's value in keeping that feature committed, especially in cases like this when it doesn't cost us anything, given that this feature mostly lives behind a compile-time cmake flag.
whisperity
commented
1 year ago given that this feature mostly lives behind a compile-time cmake flag.
The problem here is that, to the best of my understanding, both the Z3 as-a-constraint-solver and Z3 as-refutation live behind the same CMake flag, namely the one that builds LLVM with Z3 as a DSO to be loaded. So if I compile Clang with Z3 support, I will get both the (in CodeChecker parlance) --z3-refutation and --z3(-as-a-constraint-solver) options.
Either way, I've merged a patch to CodeChecker which emphasises that Z3 (as-a-constraint-solver) is a massively experimental and crash-laden feature. But there could be the chance that there are vendors who supply a build of Clang that has certain checks that rely on Z3 (as-a-constraint-solver) being available and those vendors take care of making sure their downstream checks do not crash.
The default behaviour (from CodeChecker's perspective) is: range-based constraint solver + Z3 refutation (if available).
ryao
commented
1 year ago The bottom line is that, z3 crosscheck should have the benefit of the z3-based solver, without paying the price for calling z3 at each step during the analysis - only at the bug report construction.
Are there no false negatives from the range based solver that z3 refution would have no chance to correct since it is only run on positive results?
balazs-benics-sonarsource
commented
1 year ago The bottom line is that, z3 crosscheck should have the benefit of the z3-based solver, without paying the price for calling z3 at each step during the analysis - only at the bug report construction.
Are there no false negatives from the range based solver that z3 refution would have no chance to correct since it is only run on positive results?
There could be false-negatives with both the range-based and the z3-based solver. During the analysis we might have hard-coded models for functions, where if we make a typo like this, then we will mismodel it and potentially cause FPs and FNs like. But there could be other situations, like the modeling of casts, and its shortcomings which are well demonstrated by D103096. Speaking of false-negatives, z3 refutation won't help with them, that's for sure.
ryao
commented
1 year ago The bottom line is that, z3 crosscheck should have the benefit of the z3-based solver, without paying the price for calling z3 at each step during the analysis - only at the bug report construction.
Are there no false negatives from the range based solver that z3 refution would have no chance to correct since it is only run on positive results?
There could be false-negatives with both the range-based and the z3-based solver. During the analysis we might have hard-coded models for functions, where if we make a typo like this, then we will mismodel it and potentially cause FPs and FNs like. But there could be other situations, like the modeling of casts, and its shortcomings which are well demonstrated by D103096. Speaking of false-negatives, z3 refutation won't help with them, that's for sure.
z3 refution would not help with false negatives since it is restricted to positive results. However, i was under the impression that the z3-based solver could from my read of this:
Speed comes at the expense of precision -- symbolic analysis does not handle some arithmetic and bitwise operations. Z3 can compensate for some of these shortcoming.
https://llvm.org/devmtg/2020-09/slides/Using_the_clang_static_ananalyzer_to_find_bugs.pdf
Because of that, I have been looking into adopting z3-based solver scans in OpenZFS alongside the regular scans with z3 refution as a result of that. However, there are two main drawbacks:
By the way, @balazs-benics-sonarsource, I notice that you are related to sonarsource. While it is offtopic here, one of the things I would like to do is adopt sonarcloud scans for OpenZFS, but the requirement that I give access to SonarCloud to act on my behalf without any explanation of what this meant has blocked me from doing it. I tried emailing sonarsource to ask for more information, but Evelyn Martinez sent me back a boilerplate email that had nothing to do with my inquiry (I asked about the security implications of adopting SonarCloud in an OSS project and received an email telling me that I could not get an evaluation for SonarQube).
A number of people trust me to safeguard my github account against compromise and it only takes a single incident to destroy people's trust, so I hope that it is understandable that I am very cautious about granting third parties permission to act on my behalf. The issue could be somewhat mitigated by making another github account, but if I recall, that is against Github's ToS, so I cannot do that.
Would you be willing to put me in contact with someone who could explain the security implications of signing up with sonarcloud (e.g. to what extent can a bad actor cause harm to my github projects if sonarcloud is compromised) and how I can mitigate them as much as possible? If you are willing to help, you should be able to find my email in my github profile, so we could take this conversation to email to avoid derailing this issue.
balazs-benics-sonarsource
commented
1 year ago 1) There are numerous crashes that reduce the number of reports that we receive from the z3 solver. Unfortunately, there is a segfault in the llvm-symbolizer that keeps me from getting good stack traces. I plan to investigate this some more as my time allows over the coming weeks (as while the crash issue is something others have too, they do not have the bad stack trace issue and I suspect that the way I build LLVM is responsible). The crash issue is something that I hope the wider LLVM community would be able to help solve with the aid of good bug reports, although if no one tackles it, I might end up trying to debug it myself at some point.
For bugreports, the best would be to have some catchy example. It could be semi-automatically generated by creduce under good hands. However, a stack-trace, platform, z3 version, llvm version (commit hash), and the preprocessed file should be enough to file and resolve any issues.
The best I can do for z3-based solver issues is to submit a test case to the repo so that we will have a reminder about the crashing case when we decide to resolve those crashes. Of course, for this, we would need a reduced reproducer. Feel free to contact me if you need help with this.
2) The computational requirements make this take days to run on my current development hardware, which is impractical since I cannot dedicate days of compute time to it on that. However, this is a solvable problem. [...]
Interesting and motivating to see.
[...] you should be able to find my email in my github profile, so we could take this conversation to email to avoid derailing this issue.
Done.
ryao
commented
1 year ago #9 0x00007fd99cf81f05 in clang::ento::SValBuilder::makeSymbolVal(clang::ento::SymExpr const*) () from /usr/local/bin/../lib/../lib/../lib/libclangStaticAnalyzerCore.so.15
This calls another function that has some issue that causes a signal that triggers CrashRecoverySignalHandler(). Unfortunately, on my machine, things crash in a way that prevent me from seeing any symbols in backtraces, so this is very difficult to examine for me.
That said, this appears to be in clang/include/clang/StaticAnalyzer/Core/PathSensitive/SValBuilder.h:
DefinedSVal makeSymbolVal(SymbolRef Sym) {
if (Loc::isLocType(Sym->getType()))
return makeLoc(Sym);
return nonloc::SymbolVal(Sym);
}Presumably, a runtime issue happened in one of the functions called in that function body.
I tried looking through coverity reports to see if the issue was reported there, but nothing looked related. For my sanity, I had coverity only show me defect reports whose file system paths that matched */StaticAnalyzer/Core/*. If the issue really was caught by Coverity, but its file path does not match that, then I would have missed it.
Tangentially, defect report CID-1490697 looked very interesting. What is interesting about it is that it says SSE->getRHS() is passed to a function argument named lhs and SSE->getLHS() is passed to a function argument named rhs. That kind of thing is usually a bug, but in rare circumstances, it could be intentional. Usually, those involve test cases that intentionally write incorrect code to check how it is handled, but I am not sure that there is no reason to ever do it. I am not familiar enough with the code to be certain if the report describes an actual bug and since it seems unrelated to this, I did not look at it very long.
This code is also difficult for me to navigate. My usual tool for navigating codebases is cscope and it usually is okay on C++ code, but it cannot find a global definition for SymbolRef. Looking at all "C symbols", it finds a struct named SymbolRef, but C++ structures do not have member functions, so that cannot be it unless the C++ standard changed to allow them since I last accquinted myself with C++. Searching for an implementation for getType() predictably returns an absurd amount of matches. I imagine that I could find it by doing a build, finding a build command relevant , modifying it to get the preprocessed code and then doing grep, but that requires more time than I have to look at this right now.
I am a little more successful with the other functions:
static bool isLocType(QualType T) {
return T->isAnyPointerType() || T->isBlockPointerType() ||
T->isReferenceType() || T->isNullPtrType();
} SymbolVal(SymbolRef sym) : NonLoc(SymbolValKind, sym) {
assert(sym);
assert(!Loc::isLocType(sym->getType()));
} loc::MemRegionVal makeLoc(SymbolRef sym) {
return loc::MemRegionVal(MemMgr.getSymbolicRegion(sym));
}Nothing there stands out to me as possible causes. Finding some way to get Clang's static analyzer to generate a core dump instead of handling whatever went wrong internally would probably be more useful in figuring out the cause here, since then I could reproduce the issue locally to generate the core dump and load it into a debugger to see where the runtime issue actually is.
I guess another option would be to reduce this to a minimal test case and then attach gdb to the clang invocation so that it hopefully intercepts the signal before clang's signal handler. That would involve getting the preprocessed source output and trimming it until there is nothing left to trim without making it stop triggering this. I do not have time to volunteer to do that.
Given that the only people who use this tool are software developers, I suspect that other people affected by it could volunteer to track this down. It might even be easier for them since their systems are producing decent backtraces, unlike mine.
dilyanpalauzov
commented
1 year ago Looking at all "C symbols", it finds a struct named SymbolRef, but C++ structures do not have member functions, so that cannot be it unless the C++ standard changed to allow them since I last accquinted myself with C++.
In C++ struct and class are almost the same. The only difference is that after struct { there is an implicit public:, while after class { there is an implicit private:.
whisperity
commented
1 year ago @ryao
Tangentially, defect report CID-1490697 looked very interesting. What is interesting about it is that it says
SSE->getRHS()is passed to a function argument namedlhsandSSE->getLHS()is passed to a function argument namedrhs. That kind of thing is usually a bug, but in rare circumstances, it could be intentional. Usually, those involve test cases that intentionally write incorrect code to check how it is handled, but I am not sure that there is no reason to ever do it. I am not familiar enough with the code to be certain if the report describes an actual bug and since it seems unrelated to this, I did not look at it very long.
(FYI: Clang-Tidy has a check named readability-suspicious-call-argument that hunts for such cases. IIRC, if the argument expression passed is a simple function call, it synthesises the "name" from the function name. Although the get might make Tidy itself not report this case. But know that we are working towards this in LLVM's own supplied tooling.)
This code is also difficult for me to navigate. My usual tool for navigating codebases is cscope and it usually is okay on C++ code, but it cannot find a global definition for SymbolRef.
LLVM's code is very complex because of all the template thingamajig that we are doing under the hood. However, I recommend trying clangd out. It integrates nicely into various editors that support LSP, both Vim and Emacs are covered. :wink:
Looking at all "C symbols", it finds a struct named SymbolRef, but C++ structures do not have member functions, so that cannot be it unless the C++ standard changed to allow them since I last accquinted myself with C++.
This seems a bit tangential, and I am confused here. Do you mean the C standard changing? In C++, struct and class mean the exact same thing, they both introduce a record type, and record types can have member functions. (It is as it has always been, all the way back to the original C++98.) The only difference is that if you use class then all members and inherited bases are private by default, and if you use struct they are public by default.
Searching for an implementation for
getType()predictably returns an absurd amount of matches. I imagine that I could find it by doing a build, finding a build command relevant , modifying it to get the preprocessed code and then doing grep, but that requires more time than I have to look at this right now.
(To navigate the code with Clangd, you do not even need to have a full build, only the compilation with CMake prepared. LLVM creates some generated code during the build which should be available so all the files are meaningfully preprocessed, but those codes are small, you only need to build the targets named tablegen or tblgen.)
Finding some way to get Clang's static analyzer to generate a core dump instead of handling whatever went wrong internally would probably be more useful in figuring out the cause here
Clang does the job of printing a stack trace and the invocation arguments when a deadly signal arrives, but does not invalidate the signal. That being said, a coredump should still be created once we returned from the signal handler. Did you set the ulimit appropriately? Clang's core dump will be huge...
balazs-benics-sonarsource
commented
1 year ago @rayo I assume you are still trying to use the z3-based solver, and the mentioned crash relates to that. Please confirm. I'll try to analyze OpenZFS to see if I have any crashes. Let me know how you invoked CodeChecker. Which TU fails, etc.
With CodeChecker 6.20.0, self-compiled clang 15.0.1, enabled Z3 solver 4.11.2 on openldap branch OPENLDAP_REL_ENG_2_6, calling
prints
/git/openldap/libraries/liblber/encode.cis https://git.openldap.org/openldap/openldap/-/blob/OPENLDAP_REL_ENG_2_6/libraries/liblber/encode.cFull backtrace, without debug symbols:
bprint.c.ast.gz io.c.ast.gz