[PATCH] D54978: Move the SMT API to LLVM
Brian Rzycki via Phabricator via cfe-commits
cfe-commits at lists.llvm.org
Fri Feb 8 08:23:53 PST 2019
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
More information about the cfe-commits
mailing list