[PATCH] D54978: Move the SMT API to LLVM

[Brian Rzycki via Phabricator via cfe-commits]

brzycki added a comment.

The following patch:

  diff --git a/llvm/cmake/modules/CrossCompile.cmake b/llvm/cmake/modules/CrossCompile.cmake
  index bc3b210f018..0c30b88f80f 100644
  --- a/llvm/cmake/modules/CrossCompile.cmake
  +++ b/llvm/cmake/modules/CrossCompile.cmake
  @@ -53,6 +53,7 @@ function(llvm_create_cross_target_internal target_name toolchain buildtype)
           -DLLVM_DEFAULT_TARGET_TRIPLE="${TARGET_TRIPLE}"
           -DLLVM_TARGET_ARCH="${LLVM_TARGET_ARCH}"
           -DLLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN="${LLVM_TEMPORARILY_ALLOW_OLD_TOOLCHAIN}"
  +        -DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
           ${build_type_flags} ${linker_flag} ${external_clang_dir}
       WORKING_DIRECTORY ${LLVM_${target_name}_BUILD}
       DEPENDS CREATE_LLVM_${target_name}

fixes the build break when CMake is called in the following manner:

  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF ../llvm-project/llvm

However, the custom command sub-call to CMake always fails in the same way with either of these invocations:

  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=ON ../llvm-project/llvm
  cmake -v -G Ninja  -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm

The error is the following:

  [209/2543] /usr/bin/c++  -DGTEST_HAS_RTTI=0 -D_DEBUG -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Iutils/TableGen -I/work/brzycki/llvm-project/llvm/utils/TableGen -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 -g    -fno-exceptions -fno-rtti -MD -MT utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o -MF utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o.d -o utils/TableGen/CMakeFiles/llvm-tblgen.dir/GlobalISelEmitter.cpp.o -c /work/brzycki/llvm-project/llvm/utils/TableGen/GlobalISelEmitter.cpp
  [210/2543] cd /work/brzycki/build/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" -DLLVM_ENABLE_Z3_SOLVER="ON" -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
  ...
  ...
  -- Performing Test HAVE_GNU_POSIX_REGEX -- failed to compile
  -- Performing Test HAVE_POSIX_REGEX
  -- Performing Test HAVE_POSIX_REGEX
  -- Performing Test HAVE_POSIX_REGEX -- success
  -- Performing Test HAVE_STEADY_CLOCK
  -- Performing Test HAVE_STEADY_CLOCK
  -- Performing Test HAVE_STEADY_CLOCK -- success
  -- Configuring done
  -- Generating done
  -- Build files have been written to: /work/brzycki/build/NATIVE
  ninja: build stopped: subcommand failed.

I tried passing more information to the sub CMake call, but it yielded the exact same results:

  +        -DLLVM_ENABLE_Z3_SOLVER="${LLVM_ENABLE_Z3_SOLVER}"
  +        -DLLVM_Z3_INSTALL_DIR="${LLVM_Z3_INSTALL_DIR}"
  +        -DZ3_EXECUTABLE="${Z3_EXECUTABLE}"
  +        -DZ3_INCLUDE_DIR="${Z3_INCLUDE_DIR}"
  +        -DZ3_LIBRARIES="${Z3_LIBRARIES}"

When I diff the successful sub-CMake with the failing one, the only difference is the detection of the Z3 solver library:

  $ diff -u good_submake.txt bad_submake.txt
  --- good_submake.txt    2019-02-12 11:41:54.638892191 -0600
  +++ bad_submake.txt     2019-02-12 11:43:30.096484824 -0600
  @@ -14,7 +14,7 @@
   -- Detecting CXX compiler ABI info - done
   -- Detecting CXX compile features
   -- Detecting CXX compile features - done
  --- Could NOT find Z3 (missing: Z3_LIBRARIES Z3_INCLUDE_DIR) (Required is at least version "4.7.1")
  +-- Found Z3: /usr/lib/x86_64-linux-gnu/libz3.so (Required is at least version "4.7.1")
   -- Looking for dlfcn.h
   -- Looking for dlfcn.h - found
   -- Looking for errno.h


Repository:
  rC Clang

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D54978/new/

https://reviews.llvm.org/D54978