[PATCH] D54978: Move the SMT API to LLVM

[Brian Rzycki via Phabricator via cfe-commits]

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