static analyzer with ctu and z3 crashes 15.0.1 #58118
Comments
EugeneZelenko
added
clang:static analyzer
crash
|
@llvm/issue-subscribers-clang-static-analyzer |
|
The Ask CodeChecker about the Can I close this? |
|
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 |
|
@mikhailramalho Is there any chance you could take a look? |
|
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 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: When I try with b.c: all of produce no output with clang 15.0.1. |
I believe, at some point, there was a push for having this, but I don't know anyone maintaining it now.
Yes, previously the detection of the availability
Could you elaborate on your last example? You said About the other two invocations: |
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). |
|
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. |
|
I figured out what's going on.
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. |
|
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? |
It seems like the example is from 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 Coming back to your question, the difference between the three invocations. 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();
}
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. |
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 With the static analyzer it's a bit of a mess because some actual features like 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. |
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) 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). |
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. |
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:
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. |
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.
Interesting and motivating to see.
Done. |
This calls another function that has some issue that causes a signal that triggers That said, this appears to be in 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 Tangentially, defect report CID-1490697 looked very interesting. What is interesting about it is that it says 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 I am a little more successful with the other functions: 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. |
In C++ |
(FYI: Clang-Tidy has a check named
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. 😉
This seems a bit tangential, and I am confused here. Do you mean the C standard changing? In C++,
(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
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 |
|
@rayo I assume you are still trying to use the z3-based solver, and the mentioned crash relates to that. Please confirm. |
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
> CodeChecker analyze ./compile_commands.json --ctu --z3=on --output ./reportsprints
/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
The text was updated successfully, but these errors were encountered: