brzycki added a comment. > From what I understand, setting `-DLLVM_ENABLE_Z3_SOLVER=OFF` is supposed to > work
Hello @thakis, I have reduced it down to the minimal required flags on Ubuntu 18.04. I ran this on llvm-project SHA b0a227049fda9d0d229ea801ae77bf1b812f7328 <https://reviews.llvm.org/rGb0a227049fda9d0d229ea801ae77bf1b812f7328> from Feb 8, 2019. First, make sure Ubuntu has installed its version of Z3: sudo apt install libz3-4 libz3-dev dpkg -l | grep libz3 ii libz3-4:amd64 4.4.1-0.3build4 amd64 theorem prover from Microsoft Research - runtime libraries ii libz3-dev:amd64 4.4.1-0.3build4 amd64 theorem prover from Microsoft Research - development files Next, run CMake with the following arguments: mkdir build && cd build cmake \ -G Ninja \ -D LLVM_OPTIMIZED_TABLEGEN=ON \ -D LLVM_ENABLE_Z3_SOLVER=OFF \ /path/to/llvm-project/llvm First, you'll see that CMake detects a version of Z3: -- Found Z3: /usr/lib/x86_64-linux-gnu/libz3.so (Required is at least version "4.7.1") At around ninja command 600-700 a second CMake instance is spawned for the TableGen optimizations: [666/3618] cd /work/brzycki/b/NATIVE && /sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake -G Ninja -DCMAKE_MAKE_PROGRAM="/sarc-c/compiler_tmp/tools/build/ninja-1.8.2/ninja" -DCMAKE_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ /work/brzycki/llvm-project/llvm -DLLVM_TARGET_IS_CROSSCOMPILE_HOST=TRUE -DLLVM_TARGETS_TO_BUILD="AArch64;AMDGPU;ARM;BPF;Hexagon;Lanai;Mips;MSP430;NVPTX;PowerPC;Sparc;SystemZ;WebAssembly;X86;XCore" -DLLVM_EXPERIMENTAL_TARGETS_TO_BUILD="" -DLLVM_DEFAULT_TARGET_TRIPLE="x86_64-unknown-linux-gnu" -DLLVM_TARGET_ARCH="host" -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="OFF" -DCMAKE_BUILD_TYPE=Release -- The C compiler identification is GNU 7.3.0 -- The CXX compiler identification is GNU 7.3.0 -- The ASM compiler identification is GNU -- Found assembler: /usr/bin/cc -- Check for working C compiler: /usr/bin/cc -- Check for working C compiler: /usr/bin/cc -- works ... And shortly after that we fail: -- Build files have been written to: /work/brzycki/b/NATIVE [666/3618] cd /work/brzycki/b/NATIVE && /sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake --build /work/brzycki/b/NATIVE --target llvm-tblgen --config Release [72/187] Building CXX object lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o /usr/bin/c++ -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Support -I/work/brzycki/llvm-project/llvm/lib/Support -I/usr/include/libxml2 -Iinclude -I/work/brzycki/llvm-project/llvm/include -fPIC -fvisibility-inlines-hidden -Werror=date-time -std=c++11 -Wall -Wextra -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough -Wno-maybe-uninitialized -Wno-noexcept-type -Wdelete-non-virtual-dtor -Wno-comment -fdiagnostics-color -ffunction-sections -fdata-sections -O3 -DNDEBUG -fno-exceptions -fno-rtti -MD -MT lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -MF lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o.d -o lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o -c /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp: In function ‘void {anonymous}::Z3ErrorHandler(Z3_context, Z3_error_code)’: /work/brzycki/llvm-project/llvm/lib/Support/Z3Solver.cpp:44:71: error: cannot convert ‘Z3_context {aka _Z3_context* ’ to ‘Z3_error_code’ for argument ‘1’ to ‘const char* Z3_get_error_msg(Z3_error_code)’ llvm::Twine(Z3_get_error_msg(Context, Error))); ^ [183/187] Building CXX object utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o ninja: build stopped: subcommand failed. FAILED: NATIVE/bin/llvm-tblgen cd /work/brzycki/b/NATIVE && /sarc-c/compiler_tmp/tools/build/cmake-3.13.3/bin/cmake --build /work/brzycki/b/NATIVE --target llvm-tblgen --config Release ninja: build stopped: subcommand failed. I consider this to be 2 bugs: 1. CMake should not set Z3_FOUND when the library is too old. The llvm/CMakeLists.txt file correctly states `find_package(Z3 4.7.1)` but it doesn't work right and consideres the 4.4.1 one valid. It's why I'm in this mess in the first place. 2. There's some sort of interaction bug between the top-level llvm/CMakeLists.txt and the tablegen one when optimizations are turned on. It doesn't seem to respect the `LLVM_ENABLE_Z3_SOLVER` directive. Repository: rC Clang CHANGES SINCE LAST ACTION https://reviews.llvm.org/D54978/new/ https://reviews.llvm.org/D54978 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
