Z3 constraint solver is not supported by clangsa

[dilyanpalauzov]

According to https://codechecker.readthedocs.io/en/v6.11.0/analyzer/checker_and_analyzer_configuration/ ClangSA can utilize “Z3 refutation” or “Z3 constraint solver”. With Z3 constraint solver, Clang crashes. According to:

• static analyzer with ctu and z3 crashes 15.0.1 llvm/llvm-project#58118 and
• clang analyzer 15.0.1 fails with CTU and Z3 solver 4.11.2  llvm/llvm-project#58119

Z3 constraint solver is not supported and codechecker shall drop the support for it.

[whisperity]

Clang might not support Z3 officially, but CodeChecker supports several unofficial builds of Clang (and several experimental features, like statistics-based checkers). According to the same documentation, full Z3 constraint solving (instead of just refutation) is an opt-in feature that needs to be explicitly enabled when building Clang. If you did not enable this and Clang nevertheless exposes itself as-if it was Z3-capable (for constraint solving) then that is the problem, and the exposure of the associated flags should be turned off in Clang. Also, v6.11 of CodeChecker is very old, could you please try the same with a newer release? It could have been that Z3 support in Clang was better at the time when CodeChecker v6.11 was released, which was 3 years ago, December 2019. It is possible that a Clang release from that time is perfectly fine with Z3, but ever since the Clang releases (in the official repository) diverged and the people implementing the divergency did not care about making sure it works with Z3.

[dilyanpalauzov]

I compiled myself clang/llvm 15.0.1 with LLVM_ENABLE_Z3_SOLVER=ON. The documentation of the option is “Enable Support for the Z3 constraint solver in LLVM.”

If Z3 refutation is enabled, when this option is disabled, I cannot say.

I build clang/llvm with ccmake, which lists all available options. To be precise, it can hide some options, if other options are disabled. https://codechecker.readthedocs.io/en/v6.11.0/analyzer/checker_and_analyzer_configuration/#z3-theorem-prover suggests that in order to enable the Z3 Theorem Prover, the option CLANG_ANALYZER_BUILD_Z3=ON must be set. I do not see this option.

That said: while the documentation at https://codechecker.readthedocs.io/en/latest/analyzer/checker_and_analyzer_configuration/#z3-theorem-prover mentions CLANG_ANALYZER_BUILD_Z3=ON, I have instead LLVM_ENABLE_Z3_SOLVER=ON.

At llvm/llvm-project#58119 and llvm/llvm-project#58118 I have spelled the used version with 6.20, but referenced here the documentation of version 6.11. I have used v6.20

[whisperity]

The documentation of the option is “Enable Support for the Z3 constraint solver in LLVM.”

Yeah, Z3 in LLVM is not the same thing as Z3 in the Clang Static Analyser.

It should be investigated why the flags mentioned in the documentation is missing. There ought to be a patch that removed that flag for one reason or another.

What needs to be verified first is if you build Clang without Z3 support, then CodeChecker SHOULD not show the --z3 option. If this works, CodeChecker is working as expected. Third-party clients using a broken version or configuration of Clang is not inherently an issue with CodeChecker.

[dilyanpalauzov]

From https://github.com/llvm/llvm-project/releases/tag/llvmorg-15.0.2 → Downloads I fetch https://github.com/llvm/llvm-project/releases/download/llvmorg-15.0.2/llvm-project-15.0.2.src.tar.xz, unpack it, do grep -ri BUILD_Z3. It finds nothing. Therefore the option CLANG_ANALYZER_BUILD_Z3, mentioned at https://codechecker.readthedocs.io/en/latest/analyzer/checker_and_analyzer_configuration/#z3-theorem-prover, does not exist.

clang --help|grep -i z3 finds nothing, when LLVM is compiled with LLVM_ENABLE_Z3_SOLVER=ON. How can I find, if clang is compiled with Z3, and how does CodeChecker detects this?

[ryao]

One of the LLVM/Clang developers told people to use Z3:

https://llvm.org/devmtg/2020-09/slides/Using_the_clang_static_ananalyzer_to_find_bugs.pdf

Here the results of some quick tests based on those slides:

$ clang --analyze -Xclang -analyzer-constraints=z3 ~/test.c
error: analyzer constraint manager 'z3' is only available if LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON
$ clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true ~/test.c
$ 

Coincidentally, I am in the middle of recompiling my machine's LLVM installation to have Z3, so I was able to get the error that occurs when you try turning on the Z3 constraint solver without Z3 support.

You need to pass --z3 to CodeChecker to get it to tell LLVM to use the z3 constraint solver. The default is to use z3 based refution. You probably should continue using the default until the LLVM project has fixed this.

[ryao]

Some more tests based on those slides:

$ cat test-csa.c
unsigned int func(unsigned int a) {
        unsigned int *z = 0;
        if ((a & 1) && ((a & 1) ^1))
                return *z; // unreachable
        return 0;
}
$ clang --analyze ~/test-csa.c 
/home/richard/test-csa.c:4:10: warning: Dereference of null pointer (loaded from variable 'z') [core.NullDereference]
                return *z; // unreachable
                       ^~
1 warning generated.
$ clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true ~/test-csa.c 
$ clang --analyze -Xclang -analyzer-constraints=z3 ~/test-csa.c
error: analyzer constraint manager 'z3' is only available if LLVM was built with -DLLVM_ENABLE_Z3_SOLVER=ON
$

The z3 refution seems to be working. My LLVM build with Z3 support finished, but Clang still does not seem to have realized it, so I am now rebuilding Clang.

[whisperity]

@dilyanpalauzov Would it be alright if CodeChecker's help text indicated that Z3 as a constraint solver is a highly experimental feature that may or may not be generally available in a stable way?

CodeChecker detects Z3 compatibility by invoking Clang SA with the flags -Xclang -analyzer-constraints=z3. If this invocation succeeds, then the compiler is deemed to have the feature support ready.

codechecker/analyzer/codechecker_analyzer/analyzers/analyzer_types.py

Lines 83 to 98 in a8cb930

	def is_z3_capable(context):
	""" Detects if the current clang is Z3 compatible. """
	enabled_analyzers, _ = \
	check_supported_analyzers([ClangSA.ANALYZER_NAME], context)
	if not enabled_analyzers:
	return False
	analyzer_binary = context.analyzer_binaries.get(ClangSA.ANALYZER_NAME)
	analyzer_env = env.extend(context.path_env_extra,
	context.ld_lib_path_extra)
	return host_check.has_analyzer_option(analyzer_binary,
	['-Xclang',
	'-analyzer-constraints=z3'],
	analyzer_env)

[whisperity]

clang --help|grep -i z3

Some flags are hidden, or "really hidden", so there is --help, --help-hidden, --help-developer, and Clang (the top-level binary) is a generic frontend, so some flags are only available in different frontend modes, so --help and -cc1 --help (or -Xclang --help) might yield vastly different results.

[whisperity]

Further information, I found the culprit. So in LLVM 9.0.0, specifically in D54978 (landed as llvm/llvm-project@db695c8) all Z3-related stuff was moved to become an LLVM-level thing (as opposed to being just a Clang-level thing). So that's why you can no longer toggle it for Clang or Clang SA specifically.

That said: while the documentation at https://codechecker.readthedocs.io/en/latest/analyzer/checker_and_analyzer_configuration/#z3-theorem-prover mentions CLANG_ANALYZER_BUILD_Z3=ON, I have instead LLVM_ENABLE_Z3_SOLVER=ON.

This is a good catch, and now I think I understand why.

So, in essence, there is indeed a regression in our documentation, that people using Clang >= 9.0 should use the newer (LLVM_ENABLE_Z3_SOLVER) flag instead of CLANG_.... @dkrupp

[dilyanpalauzov]

Would it be alright if CodeChecker's help text indicated that Z3 as a constraint solver is a highly experimental feature that may or may not be generally available in a stable way?

Page 27 of https://llvm.org/devmtg/2020-09/slides/Using_the_clang_static_ananalyzer_to_find_bugs.pdf provides an example, where Z3 makes a difference compared to no Z3. With clang 15.0.1 this example is no more valid, as I explained at llvm/llvm-project#58118 (comment).

CodeChecker could state, that Z3 constraint solver is available, but not supported, if there exists an example b.c, which for the calls:

$ 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 and clang does not crash on that example.

The precise wording shall then be not “highly experimental”, but “contained in the LLVM source code, albeit not supported by LLVM”. The difference is that “highly experimental” suggests that bugs are fixed, while “not supported” does not imply this.

[ryao]

I think calling it "highly experimental" is a good compromise, but I do worry that there appears to be no one at LLVM working on these bugs right now. I have plans to adopt CodeChecker + LLVM/Clang + Z3, but the lack of attention to these bugs is concerning. Where did the people working on this go and can we get them back / find new people to work on them?

[whisperity]

@ryao You can still adopt Z3 as the refutator, or use the default range-based constraint solver, so you're covered from CodeChecker's angle.

LLVM itself is a non-profit foundation. Contributions the LLVM project are from individuals doing it as a hobby, or by people whose daily job involves working with LLVM and their employer pays for this (and allows giving back to the community by making patches public). Unfortunately, research and opensource isn't the best way to make money in this industry... 🙁

This is purely to make a point that there is no such thing as "at LLVM" just like how there's no such thing as "at Wikipedia". There's a few people working (for LLVM and Wikipedia, either officially or volunteering) directly on keeping things alive (mostly servers and governance) but those people don't directly write C++ code (or Wikipedia articles) on a daily basis.

[ryao]

@whisperity Z3 as a bounds checker is supposed to catch some false negatives that occur with Z3 as a refuter, so I am trying to run both.

That being said, I work on OpenZFS (mostly as a volunteer) and I would consider myself to be at OpenZFS. I think our definitions of being "at a project" are somewhat different.

[whisperity]

@dilyanpalauzov

$ 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 and clang does not crash on that example.

The problem with this is that such a test logic could get very costly (we're doing complex Clang invocations every time someone asks for --help!), and also flaky because now the contents of the help depends not only on whether Clang accepts something on its interface, but the internal logic of the checkers themselves. If a (hypothetical) checker is improved so much that they find the example in b.c with the default range-based CS engine and do not have a different with Z3, then we are once again at the point of running after heavily LLVM-specific details... just to generate a help?