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 
<> 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 \

First, you'll see that CMake detects a version of Z3:

  -- Found Z3: /usr/lib/x86_64-linux-gnu/ (Required is at least version 

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_C_COMPILER=/usr/bin/cc -DCMAKE_CXX_COMPILER=/usr/bin/c++ 
/work/brzycki/llvm-project/llvm -DLLVM_TARGET_IS_CROSSCOMPILE_HOST=TRUE 
  -- 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 
  FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
-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: 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 
  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.

  rC Clang


cfe-commits mailing list

Reply via email to