FileCheck linking with Z3 despite -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF

[llvmbot]

Bugzilla Link	42921
Resolution	FIXED
Resolved on	Aug 08, 2019 01:52
Version	9.0
OS	All
Blocks	#41819
Reporter	LLVM Bugzilla Contributor
CC	@zmodem,@pogo59

Extended Description

In LLVM 8.0.0, support was added for Z3. In the FreeBSD port (think package) we added -DCLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF to the cmake arguments list to avoid requiring it. Somewhere between the 8.0 and 9.0 branch, that stopped being sufficient and libz3 is being found and FileCheck is being linked to it. On some of our platforms where our base compiler is still an ancient GCC, this is posing a bootstrapping challenge.

Here's an example ldd output (it seems to me that FileCheck may simply be being overlinked):
$ ldd work/stage/usr/local/bin/FileCheck90
work/stage/usr/local/bin/FileCheck90:
libthr.so.3 => /lib/libthr.so.3 (0x80089d000)
libz.so.6 => /lib/libz.so.6 (0x800ac5000)
librt.so.1 => /usr/lib/librt.so.1 (0x800cdd000)
libexecinfo.so.1 => /usr/lib/libexecinfo.so.1 (0x800ee3000)
libncurses.so.8 => /lib/libncurses.so.8 (0x8010e6000)
libm.so.5 => /lib/libm.so.5 (0x80133b000)
libz3.so.0 => /usr/local/lib/libz3.so.0 (0x801600000)
libc++.so.1 => /usr/lib/libc++.so.1 (0x802a9c000)
libcxxrt.so.1 => /lib/libcxxrt.so.1 (0x802d6a000)
libc.so.7 => /lib/libc.so.7 (0x802f89000)
libelf.so.2 => /lib/libelf.so.2 (0x803345000)
libgcc_s.so.1 => /lib/libgcc_s.so.1 (0x80355c000)

[pogo59]

After a bit of research it appears that CLANG_ANALYZER_ENABLE_Z3_SOLVER
was removed, and replaced with LLVM_ENABLE_Z3_SOLVER.
This change was made in March 2019 in r356929.

So, if you change the cmake argument in your port, that should make the
problem go away.

Please try this and let us know whether it works. If not, there is some
deeper problem.

[pogo59]

FTR, FileCheck is a victim here, not the culprit. All of the SMT-related
stuff was moved into llvm/lib/Support, along with the CMake code that
looks for and includes Z3 by default. Because that all moved from Clang
to LLVM, the name of the CMake parameter changed.

Separately, FileCheck was reorganized and most of its code was also moved
into lib/Support. So, by default it links against Z3 because the rest of
libSupport does, not because FileCheck itself has anything solver-related
in it.

See https://reviews.llvm.org/D54978 for details of the Z3 move.

[pogo59]

CC: Hans and making it a blocker for #41819 , because the CMake parameter
name change probably deserves a release note:

The CMake parameter CLANG_ANALYZER_ENABLE_Z3_SOLVER has been replaced by
LLVM_ENABLE_Z3_SOLVER.

[llvmbot]

After a bit of research it appears that CLANG_ANALYZER_ENABLE_Z3_SOLVER
was removed, and replaced with LLVM_ENABLE_Z3_SOLVER.
This change was made in March 2019 in r356929.

So, if you change the cmake argument in your port, that should make the
problem go away.

Please try this and let us know whether it works. If not, there is some
deeper problem.

That was easier than expected. :-) Making that change works. Thanks!

[zmodem]

CC: Hans and making it a blocker for #41819 , because the CMake parameter
name change probably deserves a release note:

The CMake parameter CLANG_ANALYZER_ENABLE_Z3_SOLVER has been replaced by
LLVM_ENABLE_Z3_SOLVER.

Thanks! Added a note in r368269.