Moved everything SMT-related to LLVM and updated the cmake scripts.
Details
Details
- Reviewers
NoQ george.karpenkov alexandre.isoard serge-sans-paille - Commits
- rGdb695c834f2c: Moved everything SMT-related to LLVM and updated the cmake scripts.
rC356929: Moved everything SMT-related to LLVM and updated the cmake scripts.
rL356929: Moved everything SMT-related to LLVM and updated the cmake scripts.
rGeac500f0c340: Move the SMT API to LLVM
rL353373: Move the SMT API to LLVM
rC353373: Move the SMT API to LLVM
Diff Detail
Diff Detail
Event Timeline
Comment Actions
Great! I have some use cases for verifiers, and in general for research purposes it can be quite useful.
LGTM
| llvm/lib/Support/Z3Solver.cpp | ||
|---|---|---|
| 821 | Maybe say LLVM instead of Clang as this is a file in the LLVM folder now? | |
Comment Actions
Cool! Are there any other Z3 clients expected any time soon?
| clang/CMakeLists.txt | ||
|---|---|---|
| 433–435 | If anybody uses Z3 for anything else in LLVM, it would immediately make sense to enable Z3 without static analyzer. Is this check even justified? Unlike ARCMT, these two aren't dependencies of each other. I think if we detach Z3 from clang, we should also detach it from the analyzer. | |
Comment Actions
We indeed have a user of Z3 for LLVM coming soon. (it is not upstreamed yet because the binding with Z3 was botched, it would never have been accepted)
To spill the beans: we wrote a more aggressive SCEV Canonicalizer, as a support class. It does not rely on Z3 to perform the transformation itself, but it uses Z3 into the verifier. (mostly to find potential mistakes, but we could use it to find missed opportunities too)
I suspect we could benefit a lot from Z3 if we were to use it in our verifiers in general.
| clang/CMakeLists.txt | ||
|---|---|---|
| 433–435 | I agree. The goal is to use Z3 in LLVM, independently from Clang or its static analyzer. | |
| llvm/include/llvm/Support/SMTAPI.h | ||
| 14–16 | Need to update the guards. | |
| llvm/lib/Support/Z3Solver.cpp | ||
| 20 | I find it weird to have using namespace llvm inside the #if LLVM_WITH_Z3 guard. I would put it outside. | |
Comment Actions
Updates:
- Don't abort cmake if enabling Z3 but not the CSA.
- Fixed guards in llvm/Support/SMTAPI.h
- Moved using namespace llvm; to outside the #if
Comment Actions
This commit is causing a build-break for our nightly cross compilers of arm and aarch64. The immediately preceding commit of D54977 does not break with the exact same invocation.
The problem is our build machine (Ubuntu 18.04 LTS) installs an old version of Z3 that is incompatible with LLVM's tip of tree. To deal with this we add -D CLANG_ANALYZER_ENABLE_Z3_SOLVER=OFF to force disabling Z3 even if CMake detects the library is installed.
With this patch I am unable to disable Z3 because CLANG_ANALYZER_ENABLE_Z3_SOLVER is no longer in the codebase and setting -D LLVM_ENABLE_Z3_SOLVER=OFF still builds Z3 support (which fails):
[74/187] Building CXX object lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
FAILED: lib/Support/CMakeFiles/LLVMSupport.dir/Z3Solver.cpp.o
/usr/bin/clang++-6.0 -DGTEST_HAS_RTTI=0 -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Support -I/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support -I/usr/include/libxml2 -Iinclude -I/tmp/tmp.UCDOJjmgJ1/src/llvm/include -fPIC -fvisibility-inlines-hidden -Werror=date-time -Werror=unguarded-availability-new -std=c++11 -Wall -Wextra -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wmissing-field-initializers -pedantic -Wno-long-long -Wimplicit-fallthrough -Wcovered-switch-default -Wno-noexcept-type -Wnon-virtual-dtor -Wdelete-non-virtual-dtor -Wstring-conversion -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 /tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp
/tmp/tmp.UCDOJjmgJ1/src/llvm/lib/Support/Z3Solver.cpp:44:40: error: no matching function for call to 'Z3_get_error_msg'
llvm::Twine(Z3_get_error_msg(Context, Error)));
^~~~~~~~~~~~~~~~Comment Actions
The ninja build also fails
ninja -C out/gn
ninja: Entering directory `out/gn'
[1/3182] ACTION clang/test:lit_site_cfg(llvm/utils/gn/build/toolchain:unix)
FAILED: gen/clang/test/lit.site.cfg.py
python ../../llvm/utils/gn/build/write_cmake_config.py -o gen/clang/test/lit.site.cfg.py ../../clang/test/lit.site.cfg.py.in LIT_SITE_CFG_IN_HEADER=\#\#\ Autogenerated\ from\ //clang/test/lit.site.cfg.py.in,\ do\ not\ edit CLANG_BINARY_DIR=/home/shakeel/devel/llvm-project/out/gn/obj/clang CLANG_SOURCE_DIR=/home/shakeel/devel/llvm-project/clang ENABLE_SHARED=0 LLVM_BINARY_DIR=/home/shakeel/devel/llvm-project/out/gn/obj/llvm LLVM_LIBS_DIR= LLVM_SOURCE_DIR=/home/shakeel/devel/llvm-project/llvm LLVM_TOOLS_DIR=/home/shakeel/devel/llvm-project/out/gn/bin TARGET_TRIPLE=x86_64-unknown-linux-gnu SHLIBDIR=/home/shakeel/devel/llvm-project/out/gn/lib CLANG_ANALYZER_WITH_Z3= CLANG_BUILD_EXAMPLES=0 CLANG_DEFAULT_CXX_STDLIB= CLANG_TOOLS_DIR=/home/shakeel/devel/llvm-project/out/gn/bin CMAKE_CXX_COMPILER=c++ ENABLE_BACKTRACES=1 LLVM_HOST_TRIPLE=x86_64-unknown-linux-gnu LLVM_LIT_TOOLS_DIR= LLVM_USE_SANITIZER= PYTHON_EXECUTABLE=python USE_Z3_SOLVER= CLANG_ENABLE_ARCMT=1 CLANG_ENABLE_STATIC_ANALYZER=1 HAVE_LIBZ=1 HOST_ARCH=x86_64 LLVM_PLUGIN_EXT=.so
Traceback (most recent call last):
File "../../llvm/utils/gn/build/write_cmake_config.py", line 108, in <module> sys.exit(main()) File "../../llvm/utils/gn/build/write_cmake_config.py", line 72, in main in_line = var_re.sub(repl, in_line) File "../../llvm/utils/gn/build/write_cmake_config.py", line 71, in repl return values[key]
KeyError: 'LLVM_WITH_Z3'
[2/3182] ACTION llvm/include/llvm/Config:config(llvm/utils/gn/build/toolchain:unix)
FAILED: gen/llvm/include/llvm/Config/config.h
python ../../llvm/utils/gn/build/write_cmake_config.py -o gen/llvm/include/llvm/Config/config.h ../../llvm/include/llvm/Config/config.h.cmake BUG_REPORT_URL=https://bugs.llvm.org/ ENABLE_BACKTRACES=1 ENABLE_CRASH_OVERRIDES=1 BACKTRACE_HEADER=execinfo.h HAVE_CRASHREPORTERCLIENT_H= HAVE_DECL_FE_ALL_EXCEPT=1 HAVE_DECL_FE_INEXACT=1 LLVM_ENABLE_DIA_SDK= LLVM_ENABLE_CRASH_DUMPS= HAVE_ERRNO_H=1 HAVE_FCNTL_H=1 HAVE_FENV_H=1 HAVE_FFI_CALL= HAVE_FFI_FFI_H= HAVE_FFI_H= HAVE_LIBPFM= HAVE_LIBPSAPI= HAVE_MALLCTL= HAVE_SIGNAL_H=1 HAVE_STD_IS_TRIVIALLY_COPYABLE=1 HAVE_STRERROR=1 HAVE_SYS_STAT_H=1 HAVE_SYS_TYPES_H=1 HAVE_VALGRIND_VALGRIND_H= HAVEALLOCA= HAVE_ALLOCA= HAVE___ASHLDI3= HAVE___ASHRDI3= HAVE___CHKSTK= HAVE___CHKSTK_MS= HAVE___CMPDI2= HAVE___DIVDI3= HAVE___FIXDFDI= HAVE___FIXSFDI= HAVE___FLOATDIDF= HAVE___LSHRDI3= HAVE___MAIN= HAVE___MODDI3= HAVE___UDIVDI3= HAVE___UMODDI3= HAVE____CHKSTK= HAVE____CHKSTK_MS= HOST_LINK_VERSION= LLVM_TARGET_TRIPLE_ENV= LLVM_VERSION_INFO= LLVM_VERSION_PRINTER_SHOW_HOST_TARGET_INFO=1 PACKAGE_BUGREPORT=https://bugs.llvm.org/ PACKAGE_NAME=LLVM PACKAGE_STRING=LLVM\ 9.0.0svn PACKAGE_VERSION=9.0.0svn PACKAGE_VENDOR= RETSIGTYPE=void LLVM_GISEL_COV_ENABLED= LLVM_GISEL_COV_PREFIX= LLVM_DEFAULT_TARGET_TRIPLE=x86_64-unknown-linux-gnu HAVE_FUTIMENS=1 HAVE_LINK_H=1 HAVE_LSEEK64=1 HAVE_MALLINFO=1 HAVE_POSIX_FALLOCATE=1 HAVE_SCHED_GETAFFINITY=1 HAVE_CPU_COUNT=1 HAVE_STRUCT_STAT_ST_MTIM_TV_NSEC=1 HAVE_CRASHREPORTER_INFO= HAVE_DECL_ARC4RANDOM= HAVE_DLADDR= HAVE_MACH_MACH_H= HAVE_MALLOC_MALLOC_H= HAVE_MALLOC_ZONE_STATISTICS= HAVE_STRUCT_STAT_ST_MTIMESPEC_TV_NSEC= HAVE_BACKTRACE=1 HAVE_POSIX_SPAWN=1 HAVE_PTHREAD_GETNAME_NP=1 HAVE_DECL_STRERROR_S= HAVE_DLFCN_H=1 HAVE_DLOPEN=1 HAVE_FUTIMES=1 HAVE_GETPAGESIZE=1 HAVE_GETRLIMIT=1 HAVE_GETRUSAGE=1 HAVE_ISATTY=1 HAVE_LIBPTHREAD=1 HAVE_PTHREAD_SETNAME_NP=1 HAVE_LIBZ=1 HAVE_PREAD=1 HAVE_PTHREAD_GETSPECIFIC=1 HAVE_PTHREAD_H=1 HAVE_PTHREAD_MUTEX_LOCK=1 HAVE_PTHREAD_RWLOCK_INIT=1 HAVE_REALPATH=1 HAVE_SBRK=1 HAVE_SETENV=1 HAVE_SETRLIMIT=1 HAVE_SIGALTSTACK=1 HAVE_STRERROR_R=1 HAVE_SYSCONF=1 HAVE_SYS_IOCTL_H=1 HAVE_SYS_MMAN_H=1 HAVE_SYS_PARAM_H=1 HAVE_SYS_RESOURCE_H=1 HAVE_SYS_TIME_H=1 HAVE_TERMIOS_H=1 HAVE_UNISTD_H=1 HAVE_ZLIB_H=1 HAVECHSIZE_S= HAVEUNWIND_BACKTRACE=1 stricmp= strdup= LTDL_SHLIB_EXT=.so HAVE_LIBEDIT= HAVE_LIBXAR= HAVE_TERMINFO= LLVM_ENABLE_ZLIB=1 LLVM_LIBXML2_ENABLED=1
Traceback (most recent call last):
File "../../llvm/utils/gn/build/write_cmake_config.py", line 108, in <module> sys.exit(main()) File "../../llvm/utils/gn/build/write_cmake_config.py", line 72, in main in_line = var_re.sub(repl, in_line) File "../../llvm/utils/gn/build/write_cmake_config.py", line 71, in repl return values[key]
KeyError: 'LLVM_WITH_Z3'
[3/3182] ACTION clang/include/clang/Config:Config(llvm/utils/gn/build/toolchain:unix)
FAILED: gen/clang/include/clang/Config/config.h
python ../../llvm/utils/gn/build/write_cmake_config.py -o gen/clang/include/clang/Config/config.h ../../clang/include/clang/Config/config.h.cmake BUG_REPORT_URL=https://bugs.llvm.org/ CLANG_DEFAULT_LINKER= CLANG_DEFAULT_STD_C= CLANG_DEFAULT_STD_CXX= CLANG_DEFAULT_CXX_STDLIB= CLANG_DEFAULT_RTLIB= CLANG_DEFAULT_OBJCOPY=objcopy CLANG_DEFAULT_OPENMP_RUNTIME=libomp CLANG_OPENMP_NVPTX_DEFAULT_ARCH=sm_35 CLANG_LIBDIR_SUFFIX= CLANG_RESOURCE_DIR= C_INCLUDE_DIRS= CLANG_CONFIG_FILE_SYSTEM_DIR= CLANG_CONFIG_FILE_USER_DIR= DEFAULT_SYSROOT= GCC_INSTALL_PREFIX= CLANG_ANALYZER_WITH_Z3= BACKEND_PACKAGE_STRING=LLVM\ 9.0.0svn ENABLE_LINKER_BUILD_ID= ENABLE_X86_RELAX_RELOCATIONS= ENABLE_EXPERIMENTAL_NEW_PASS_MANAGER= CLANG_ENABLE_OBJC_REWRITER=1 CLANG_ENABLE_ARCMT=1 CLANG_ENABLE_STATIC_ANALYZER=1 CLANG_HAVE_RLIMITS=1 CLANG_HAVE_LIBXML=1 HOST_LINK_VERSION=
unused values args:
CLANG_ANALYZER_WITH_Z3
ninja: build stopped: subcommand failed.
Comment Actions
@mikhail.ramalho could you revert then?
In general, we should not use Z3 unless it's explicitly requested.
Comment Actions
That's not the ninja build, that's the GN build. If you use that, please read llvm/utils/gn/README.rst. If something like this happens, it's on you (and other people using then gn build) to fix this. If you're not comfortable with that, please don't use the GN build. (I just merged this to the GN build in r353518, so syncing will make things go again for you.)
Comment Actions
From what I understand, setting -DLLVM_ENABLE_Z3_SOLVER=OFF is supposed to work – the contents of Z3Solver.cpp are wrapped in a #if LLVM_WITH_Z3, and the logic in the llvm cmake file looks identical to the logic in the clang cmake file previously. Can you maybe debug a bit to see what goes wrong on your bot?
lebedev.ri's point about this not being reviewed properly is a good one though.
Comment Actions
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 .
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/llvmCMake 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:
- 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.
- 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.
Comment Actions
There is at least one other conflicting commit rL353465 on top of this code already.
Sorry about that. I think it would be fine to revert both or to replay the other commit on top of reverted version of this one.
@mikhail.ramalho could you take a look?
Comment Actions
Hi everyone, I just saw your messages and reverted the commits.
Sorry for the inconvenience, but for some reason I didn't get any email from the bots. Could you send me the link with the failure?
@brzycki, I'm using Ubuntu 18.04.2 and I'll try to reproduce the error.
@thakis, do you have any idea why this was not sent to the llvm mailing lists?
Comment Actions
I'm guessing you didn't add llvm-commits and cfe-commits as subscribers when sending this out?
Comment Actions
As far as I know, that happens automatically if you add LLVM or Clang as project, that usually works for me.
Comment Actions
@brzycki, I can't reproduce your error. Maybe you're missing -DLLVM_ENABLE_Z3_SOLVER=OFF?
$ cmake -GNinja ../llvm -DLLVM_ENABLE_PROJECTS=clang -DBUILD_SHARED_LIBS=ON -DCMAKE_INSTALL_PREFIX=/home/mgadelha/myclang -DCMAKE_LINKER=/usr/bin/ld.gold -DLLVM_ENABLE_BACKTRACES=OFF -DLLVM_TARGETS_TO_BUILD=host -DLLVM_ENABLE_Z3_SOLVER=ON -DCMAKE_BUILD_TYPE=RelWithDebInfo -- clang project is enabled -- compiler-rt project is disabled -- debuginfo-tests project is disabled -- libclc project is disabled -- libcxx project is disabled -- libcxxabi project is disabled -- libunwind project is disabled -- lld project is disabled -- lldb project is disabled -- llgo project is disabled -- llvm project is disabled -- openmp project is disabled -- parallel-libs project is disabled -- polly project is disabled -- pstl project is disabled -- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so) CMake Error at CMakeLists.txt:406 (message): LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available. -- Configuring incomplete, errors occurred! See also "/home/mgadelha/llvm/build/CMakeFiles/CMakeOutput.log".
Comment Actions
@brzycki, I can't reproduce your error. Maybe you're missing -DLLVM_ENABLE_Z3_SOLVER=OFF?
Hello @mikhail.ramalho, here are my exact reproduction steps. I just verified them about 5 minutes ago.
# Setup Ubuntu's Z3 lsb_release -a No LSB modules are available. Distributor ID: Ubuntu Description: Ubuntu 18.04.1 LTS Release: 18.04 Codename: bionic sudo apt install -y libz3-4 libz3-dev # Clone llvm-project and checkout the test SHA tmpd=$(mktemp -d) cd $tmpd git clone https://github.com/llvm/llvm-project.git git checkout b0a227049fda # Setup symlinks under llvm to compile correctly cd $tmpd/llvm-project/llvm ln -s ../../clang ln -s ../../polly ln -s ../../libcxx ln -s ../../libcxxabi # CMake and Ninja mkdir $tmpd/build cd $tmpd/build cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF ../llvm-project/llvm ninja -v
These steps produce the error:
[70/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)));
^If I remove -D LLVM_ENABLE_Z3_SOLVER=OFF the actual TableGen CMake fails to succeed:
cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm ninja -v
And here's the TableGen CMake error:
[218/3618] 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" -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 -- Detecting C compiler ABI info -- Detecting C compiler ABI info - done -- Detecting C compile features -- Detecting C compile features - done -- Check for working CXX compiler: /usr/bin/c++ -- Check for working CXX compiler: /usr/bin/c++ -- works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- 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 -- Looking for errno.h - found -- Looking for fcntl.h -- Looking for fcntl.h - found -- Looking for link.h -- Looking for link.h - found -- Looking for malloc/malloc.h -- Looking for malloc/malloc.h - not found -- Looking for pthread.h -- Looking for pthread.h - found -- Looking for signal.h -- Looking for signal.h - found -- Looking for sys/ioctl.h -- Looking for sys/ioctl.h - found -- Looking for sys/mman.h -- Looking for sys/mman.h - found -- Looking for sys/param.h -- Looking for sys/param.h - found -- Looking for sys/resource.h -- Looking for sys/resource.h - found -- Looking for sys/stat.h -- Looking for sys/stat.h - found -- Looking for sys/time.h -- Looking for sys/time.h - found -- Looking for sys/types.h -- Looking for sys/types.h - found -- Looking for termios.h -- Looking for termios.h - found -- Looking for unistd.h -- Looking for unistd.h - found -- Looking for valgrind/valgrind.h -- Looking for valgrind/valgrind.h - found -- Looking for zlib.h -- Looking for zlib.h - found -- Looking for fenv.h -- Looking for fenv.h - found -- Looking for FE_ALL_EXCEPT -- Looking for FE_ALL_EXCEPT - found -- Looking for FE_INEXACT -- Looking for FE_INEXACT - found -- Looking for mach/mach.h -- Looking for mach/mach.h - not found -- Looking for histedit.h -- Looking for histedit.h - not found -- Looking for CrashReporterClient.h -- Looking for CrashReporterClient.h - not found -- Looking for linux/magic.h -- Looking for linux/magic.h - found -- Looking for pthread_create in pthread -- Looking for pthread_create in pthread - found -- Looking for pthread_getspecific in pthread -- Looking for pthread_getspecific in pthread - found -- Looking for pthread_rwlock_init in pthread -- Looking for pthread_rwlock_init in pthread - found -- Looking for pthread_mutex_lock in pthread -- Looking for pthread_mutex_lock in pthread - found -- Looking for dlopen in dl -- Looking for dlopen in dl - found -- Looking for clock_gettime in rt -- Looking for clock_gettime in rt - found -- Looking for pfm_initialize in pfm -- Looking for pfm_initialize in pfm - not found -- Looking for pthread.h -- Looking for pthread.h - found -- Looking for pthread_create -- Looking for pthread_create - not found -- Looking for pthread_create in pthreads -- Looking for pthread_create in pthreads - not found -- Looking for pthread_create in pthread -- Looking for pthread_create in pthread - found -- Found Threads: TRUE -- Looking for compress2 in z -- Looking for compress2 in z - found -- Looking for setupterm in terminfo -- Looking for setupterm in terminfo - not found -- Looking for setupterm in tinfo -- Looking for setupterm in tinfo - found -- Found LibXml2: /usr/lib/x86_64-linux-gnu/libxml2.so (found version "2.9.4") -- Looking for xar_open in xar -- Looking for xar_open in xar - not found -- Looking for arc4random -- Looking for arc4random - not found -- Looking for backtrace -- Looking for backtrace - found -- backtrace facility detected in default set of libraries -- Found Backtrace: /usr/include -- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW -- Performing Test C_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Failed -- Looking for _Unwind_Backtrace -- Looking for _Unwind_Backtrace - found -- Looking for getpagesize -- Looking for getpagesize - found -- Looking for sysconf -- Looking for sysconf - found -- Looking for getrusage -- Looking for getrusage - found -- Looking for setrlimit -- Looking for setrlimit - found -- Looking for isatty -- Looking for isatty - found -- Looking for futimens -- Looking for futimens - found -- Looking for futimes -- Looking for futimes - found -- Looking for posix_fallocate -- Looking for posix_fallocate - found -- Looking for sigaltstack -- Looking for sigaltstack - found -- Looking for lseek64 -- Looking for lseek64 - found -- Looking for mallctl -- Looking for mallctl - not found -- Looking for mallinfo -- Looking for mallinfo - found -- Looking for malloc_zone_statistics -- Looking for malloc_zone_statistics - not found -- Looking for getrlimit -- Looking for getrlimit - found -- Looking for posix_spawn -- Looking for posix_spawn - found -- Looking for pread -- Looking for pread - found -- Looking for realpath -- Looking for realpath - found -- Looking for sbrk -- Looking for sbrk - found -- Looking for strerror -- Looking for strerror - found -- Looking for strerror_r -- Looking for strerror_r - found -- Looking for strerror_s -- Looking for strerror_s - not found -- Looking for setenv -- Looking for setenv - found -- Looking for dlopen -- Looking for dlopen - found -- Looking for dladdr -- Looking for dladdr - not found -- Performing Test HAVE_STRUCT_STAT_ST_MTIMESPEC_TV_NSEC -- Performing Test HAVE_STRUCT_STAT_ST_MTIMESPEC_TV_NSEC - Failed -- Performing Test HAVE_STRUCT_STAT_ST_MTIM_TV_NSEC -- Performing Test HAVE_STRUCT_STAT_ST_MTIM_TV_NSEC - Success -- Looking for __GLIBC__ -- Looking for __GLIBC__ - found -- Looking for sched_getaffinity -- Looking for sched_getaffinity - found -- Looking for CPU_COUNT -- Looking for CPU_COUNT - found -- Looking for pthread_getname_np -- Looking for pthread_getname_np - found -- Looking for pthread_setname_np -- Looking for pthread_setname_np - found -- Performing Test HAVE_STD_IS_TRIVIALLY_COPYABLE -- Performing Test HAVE_STD_IS_TRIVIALLY_COPYABLE - Success -- Performing Test HAVE_CXX_ATOMICS_WITHOUT_LIB -- Performing Test HAVE_CXX_ATOMICS_WITHOUT_LIB - Success -- Performing Test HAVE_CXX_ATOMICS64_WITHOUT_LIB -- Performing Test HAVE_CXX_ATOMICS64_WITHOUT_LIB - Success -- Performing Test LLVM_HAS_ATOMICS -- Performing Test LLVM_HAS_ATOMICS - Success -- Performing Test SUPPORTS_VARIADIC_MACROS_FLAG -- Performing Test SUPPORTS_VARIADIC_MACROS_FLAG - Success -- Performing Test SUPPORTS_GNU_ZERO_VARIADIC_MACRO_ARGUMENTS_FLAG -- Performing Test SUPPORTS_GNU_ZERO_VARIADIC_MACRO_ARGUMENTS_FLAG - Failed -- Performing Test HAS_MAYBE_UNINITIALIZED -- Performing Test HAS_MAYBE_UNINITIALIZED - Success -- Native target architecture is X86 -- Threads enabled. -- Doxygen disabled. -- Go bindings disabled. -- Could NOT find OCaml (missing: OCAMLFIND OCAML_VERSION OCAML_STDLIB_PATH) -- Could NOT find OCaml (missing: OCAMLFIND OCAML_VERSION OCAML_STDLIB_PATH) -- OCaml bindings disabled. -- Could NOT find Python module pygments -- Could NOT find Python module pygments.lexers.c_cpp -- Could NOT find Python module yaml -- LLVM host triple: x86_64-unknown-linux-gnu -- LLVM default target triple: x86_64-unknown-linux-gnu -- Performing Test C_SUPPORTS_FPIC -- Performing Test C_SUPPORTS_FPIC - Success -- Performing Test CXX_SUPPORTS_FPIC -- Performing Test CXX_SUPPORTS_FPIC - Success -- Building with -fPIC -- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG -- Performing Test SUPPORTS_FVISIBILITY_INLINES_HIDDEN_FLAG - Success -- Performing Test C_SUPPORTS_WERROR_DATE_TIME -- Performing Test C_SUPPORTS_WERROR_DATE_TIME - Success -- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME -- Performing Test CXX_SUPPORTS_WERROR_DATE_TIME - Success -- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW -- Performing Test CXX_SUPPORTS_WERROR_UNGUARDED_AVAILABILITY_NEW - Failed -- Performing Test CXX_SUPPORTS_CXX11 -- Performing Test CXX_SUPPORTS_CXX11 - Success -- Performing Test CXX_SUPPORTS_MISSING_FIELD_INITIALIZERS_FLAG -- Performing Test CXX_SUPPORTS_MISSING_FIELD_INITIALIZERS_FLAG - Success -- Performing Test C_SUPPORTS_IMPLICIT_FALLTHROUGH_FLAG -- Performing Test C_SUPPORTS_IMPLICIT_FALLTHROUGH_FLAG - Success -- Performing Test CXX_SUPPORTS_IMPLICIT_FALLTHROUGH_FLAG -- Performing Test CXX_SUPPORTS_IMPLICIT_FALLTHROUGH_FLAG - Success -- Performing Test C_SUPPORTS_COVERED_SWITCH_DEFAULT_FLAG -- Performing Test C_SUPPORTS_COVERED_SWITCH_DEFAULT_FLAG - Failed -- Performing Test CXX_SUPPORTS_COVERED_SWITCH_DEFAULT_FLAG -- Performing Test CXX_SUPPORTS_COVERED_SWITCH_DEFAULT_FLAG - Failed -- Performing Test CXX_SUPPORTS_CLASS_MEMACCESS_FLAG -- Performing Test CXX_SUPPORTS_CLASS_MEMACCESS_FLAG - Failed -- Performing Test CXX_SUPPORTS_NOEXCEPT_TYPE_FLAG -- Performing Test CXX_SUPPORTS_NOEXCEPT_TYPE_FLAG - Success -- Performing Test C_SUPPORTS_DELETE_NON_VIRTUAL_DTOR_FLAG -- Performing Test C_SUPPORTS_DELETE_NON_VIRTUAL_DTOR_FLAG - Failed -- Performing Test CXX_SUPPORTS_DELETE_NON_VIRTUAL_DTOR_FLAG -- Performing Test CXX_SUPPORTS_DELETE_NON_VIRTUAL_DTOR_FLAG - Success -- Performing Test C_WCOMMENT_ALLOWS_LINE_WRAP -- Performing Test C_WCOMMENT_ALLOWS_LINE_WRAP - Failed -- Performing Test C_SUPPORTS_STRING_CONVERSION_FLAG -- Performing Test C_SUPPORTS_STRING_CONVERSION_FLAG - Failed -- Performing Test CXX_SUPPORTS_STRING_CONVERSION_FLAG -- Performing Test CXX_SUPPORTS_STRING_CONVERSION_FLAG - Failed -- Performing Test LINKER_SUPPORTS_COLOR_DIAGNOSTICS -- Performing Test LINKER_SUPPORTS_COLOR_DIAGNOSTICS - Failed -- Performing Test C_SUPPORTS_FNO_FUNCTION_SECTIONS -- Performing Test C_SUPPORTS_FNO_FUNCTION_SECTIONS - Success -- Performing Test C_SUPPORTS_FFUNCTION_SECTIONS -- Performing Test C_SUPPORTS_FFUNCTION_SECTIONS - Success -- Performing Test CXX_SUPPORTS_FFUNCTION_SECTIONS -- Performing Test CXX_SUPPORTS_FFUNCTION_SECTIONS - Success -- Performing Test C_SUPPORTS_FDATA_SECTIONS -- Performing Test C_SUPPORTS_FDATA_SECTIONS - Success -- Performing Test CXX_SUPPORTS_FDATA_SECTIONS -- Performing Test CXX_SUPPORTS_FDATA_SECTIONS - Success -- Found PythonInterp: /usr/bin/python2.7 (found version "2.7.15") -- Constructing LLVMBuild project information -- Found Git: /usr/local/bin/git (found version "2.20.1") -- Linker detection: GNU ld -- Targeting AArch64 -- Targeting AMDGPU -- Targeting ARM -- Targeting BPF -- Targeting Hexagon -- Targeting Lanai -- Targeting Mips -- Targeting MSP430 -- Targeting NVPTX -- Targeting PowerPC -- Targeting Sparc -- Targeting SystemZ -- Targeting WebAssembly -- Targeting X86 -- Targeting XCore -- ISL version: isl-0.20-65-gb822a210 -- Performing Test HAS_ATTRIBUTE_WARN_UNUSED_RESULT -- Performing Test HAS_ATTRIBUTE_WARN_UNUSED_RESULT - Success -- Performing Test HAVE___ATTRIBUTE__ -- Performing Test HAVE___ATTRIBUTE__ - Success -- Performing Test HAVE_DECL_FFS -- Performing Test HAVE_DECL_FFS - Success -- Performing Test HAVE_DECL___BUILTIN_FFS -- Performing Test HAVE_DECL___BUILTIN_FFS - Success -- Performing Test HAVE_DECL__BITSCANFORWARD -- Performing Test HAVE_DECL__BITSCANFORWARD - Failed -- Performing Test HAVE_DECL_STRCASECMP -- Performing Test HAVE_DECL_STRCASECMP - Success -- Performing Test HAVE_DECL__STRICMP -- Performing Test HAVE_DECL__STRICMP - Failed -- Performing Test HAVE_DECL_STRNCASECMP -- Performing Test HAVE_DECL_STRNCASECMP - Success -- Performing Test HAVE_DECL__STRNICMP -- Performing Test HAVE_DECL__STRNICMP - Failed -- Performing Test HAVE_DECL_SNPRINTF -- Performing Test HAVE_DECL_SNPRINTF - Success -- Performing Test HAVE_DECL__SNPRINTF -- Performing Test HAVE_DECL__SNPRINTF - Failed -- Performing Test HAVE_UINT8T -- Performing Test HAVE_UINT8T - Failed -- Performing Test HAVE_STDINT_H -- Performing Test HAVE_STDINT_H - Success -- Performing Test HAVE_INTTYPES_H -- Performing Test HAVE_INTTYPES_H - Success -- Performing Test HAVE_SYS_INTTYPES_H -- Performing Test HAVE_SYS_INTTYPES_H - Failed -- PPCG version: ppcg-0.07 -- Looking for sys/resource.h -- Looking for sys/resource.h - found -- Clang version: 9.0.0 -- Performing Test CXX_SUPPORTS_NO_NESTED_ANON_TYPES_FLAG -- Performing Test CXX_SUPPORTS_NO_NESTED_ANON_TYPES_FLAG - Failed -- Failed to find LLVM FileCheck -- git Version: v0.0.0 -- Version: 0.0.0 -- Performing Test HAVE_CXX_FLAG_STD_CXX11 -- Performing Test HAVE_CXX_FLAG_STD_CXX11 - Success -- Performing Test HAVE_CXX_FLAG_WALL -- Performing Test HAVE_CXX_FLAG_WALL - Success -- Performing Test HAVE_CXX_FLAG_WEXTRA -- Performing Test HAVE_CXX_FLAG_WEXTRA - Success -- Performing Test HAVE_CXX_FLAG_WSHADOW -- Performing Test HAVE_CXX_FLAG_WSHADOW - Success -- Performing Test HAVE_CXX_FLAG_PEDANTIC -- Performing Test HAVE_CXX_FLAG_PEDANTIC - Success -- Performing Test HAVE_CXX_FLAG_PEDANTIC_ERRORS -- Performing Test HAVE_CXX_FLAG_PEDANTIC_ERRORS - Success -- Performing Test HAVE_CXX_FLAG_WSHORTEN_64_TO_32 -- Performing Test HAVE_CXX_FLAG_WSHORTEN_64_TO_32 - Failed -- Performing Test HAVE_CXX_FLAG_WFLOAT_EQUAL -- Performing Test HAVE_CXX_FLAG_WFLOAT_EQUAL - Success -- Performing Test HAVE_CXX_FLAG_FSTRICT_ALIASING -- Performing Test HAVE_CXX_FLAG_FSTRICT_ALIASING - Success -- Performing Test HAVE_CXX_FLAG_FNO_EXCEPTIONS -- Performing Test HAVE_CXX_FLAG_FNO_EXCEPTIONS - Success -- Performing Test HAVE_CXX_FLAG_WSTRICT_ALIASING -- Performing Test HAVE_CXX_FLAG_WSTRICT_ALIASING - Success -- Performing Test HAVE_CXX_FLAG_WD654 -- Performing Test HAVE_CXX_FLAG_WD654 - Failed -- Performing Test HAVE_CXX_FLAG_WTHREAD_SAFETY -- Performing Test HAVE_CXX_FLAG_WTHREAD_SAFETY - Failed -- Performing Test HAVE_CXX_FLAG_COVERAGE -- Performing Test HAVE_CXX_FLAG_COVERAGE - Success -- Performing Test HAVE_GNU_POSIX_REGEX -- Performing Test HAVE_GNU_POSIX_REGEX -- 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.
Comment Actions
The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only: among other conditions, if the z3 binary is available, it will execute it and parse out the version number from standard output, otherwise, it fails silently. This is because upstream Z3 doesn't define the API version in a header file, and uses a homebrew python-based build system that also doesn't export the version. I believe @delcypher 's CMake-based build system for upstream Z3 might solve this problem, but I haven't looked at it in a long time, and it it appears to be stalled ( https://github.com/Z3Prover/z3/issues/986 ).
I also agree that more notice about this patch would have been appreciated; I didn't hear about it until I read LLVM weekly today.
Comment Actions
The default for LLVM_ENABLE_Z3_SOLVER depends entirely on what CMake detects from find_package(). Here is the relevant code in llvm/CMakeLists.txt:
find_package(Z3 4.7.1)
...
set(LLVM_ENABLE_Z3_SOLVER_DEFAULT "${Z3_FOUND}")
option(LLVM_ENABLE_Z3_SOLVER
"Enable Support for the Z3 constraint solver in LLVM."
${LLVM_ENABLE_Z3_SOLVER_DEFAULT}
)If find_package() idenfiies a suitable Z3_FOUND the default is to enable builds with the Z3 framework. In other words the entire Z3 feature is manual opt-out and implicit opt-in when CMake thinks a suitable Z3 library is found.
Thank you @ddcc for this explanation. If that's the case I'd really prefer if LLVM_ENABLE_Z3_SOLVER was explicit opt-in and defaulted to OFF regardless of what find_package returned.
Comment Actions
Thank you @ddcc for this explanation. If that's the case I'd really prefer if LLVM_ENABLE_Z3_SOLVER was explicit opt-in and defaulted to OFF regardless of what find_package returned.
Do you understand why the default matters for you? You seem to explicitly disable the setting, and you still get Z3 as part of your build. Did you make a clean build dir before turning it to OFF? If so, I don't understand why the default setting is important to you and why this doesn't work for you. (I don't disagree with the default being off, I'm just confused why things don't work for you.)
Comment Actions
Yes, Please see my recreation instructions above. I created a new, empty build directory.
If so, I don't understand why the default setting is important to you and why this doesn't work for you. (I don't disagree with the default being off, I'm just confused why things don't work for you.)
As I have stated several times, the CMake option -D LLVM_OPTIMIZED_TABLEGEN=ON spawns a sub-command of CMake and is required for the break to occur. I don't know how to make this any more clear: if you build with optimized tablegen, it breaks. I strongly suspect an interaction between LLVM's top-level CMake and the TableGen one but I haven't had time to debug it down to the exact cause.
It is important to me because the detection of the correct version of Z3 is imprecise, at best. If a Z3 library is found I have no way to guarantee a build I run will not attempt to include the library.
Comment Actions
If so, I don't understand why the default setting is important to you and why this doesn't work for you. (I don't disagree with the default being off, I'm just confused why things don't work for you.)
As I have stated several times, the CMake option -D LLVM_OPTIMIZED_TABLEGEN=ON spawns a sub-command of CMake and is required for the break to occur. I don't know how to make this any more clear: if you build with optimized tablegen, it breaks. I strongly suspect an interaction between LLVM's top-level CMake and the TableGen one but I haven't had time to debug it down to the exact cause.
It is important to me because the detection of the correct version of Z3 is imprecise, at best. If a Z3 library is found I have no way to guarantee a build I run will not attempt to include the library.
Got it now, sorry about being dense.
mikhail.ramalho: My guess is that we need to pass on LLVM_OPTIMIZED_TABLEGEN to the child cmake invocation in http://llvm-cs.pcc.me.uk/cmake/modules/CrossCompile.cmake#50 (like we pass on a few other variables) to fix this.
Comment Actions
No problem, I appreciate you looking into this. :)
I hope to have some time in the next few days to help out and debug this further.
Comment Actions
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
Comment Actions
I think I found why others are struggling to recreate this issue. I did not have the package z3/bionic installed. This provides the /usr/bin/z3 executable which llvm/cmake/modules/FindZ3.cmake relies upon to determine the correct Z3_VERSION_STRING.
If I perform the following on an unpatched checkout of sha b0a227049fda the build works :
sudo apt install -y z3 libz3-4 libz3-dev mkdir build && cd build
Either of the following CMake commands build successfully:
cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON ../llvm-project/llvm cmake -G Ninja -D LLVM_OPTIMIZED_TABLEGEN=ON -D LLVM_ENABLE_Z3_SOLVER=OFF ../llvm-project/llvm
And if I try -D LLVM_ENABLE_Z3_SOLVER=ON I receive a top-leve CMake error immediately:
-- Could NOT find Z3: Found unsuitable version "4.4.1", but required is at least "4.7.1" (found /usr/lib/x86_64-linux-gnu/libz3.so) CMake Error at CMakeLists.txt:406 (message): LLVM_ENABLE_Z3_SOLVER cannot be enabled when Z3 is not available. -- Configuring incomplete, errors occurred! See also "/work/brzycki/build/CMakeFiles/CMakeOutput.log". ninja: error: loading 'build.ninja': No such file or directory
Unfortunately it's completely valid to install packages libz3-4 and libz3-dev without pulling in z3 on Ubuntu 18.04. I've added this to my internal build notes.
I'm also looking to see if there's a way to better handle this case inside the find_package(Z3 ...) subsystem of llvm.
Comment Actions
Yeah, that's what I meant by best-effort only. Due to upstream Z3's design, without the binary, there is no easy way to retrieve the current installed version, so when I originally wrote the Z3 integration, it seemed fine to let the version check pass. Given the issues that have come up, it might make more sense to at least emit a warning, or explicitly fail if the version can't be determined, and prompt the user to install the binary.
Comment Actions
Hello @ddcc.
I agree with your reasoning here and developed a patch based on this line of thought:
diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake index 5c6d3f0b427..b213342df37 100644 --- a/llvm/cmake/modules/FindZ3.cmake +++ b/llvm/cmake/modules/FindZ3.cmake @@ -39,6 +39,11 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) string(REGEX REPLACE "^Z3 version ([0-9.]+)" "\\1" Z3_VERSION_STRING "${libz3_version_str}") unset(libz3_version_str) +else() + # The version could not be determined from running Z3_EXECUTABLE. Set the + # version Z3 to the lowest possible value such that all checks for a + # minimum version will fail. + set(Z3_VERSION_STRING "0.0.0") endif() # handle the QUIETLY and REQUIRED arguments and set Z3_FOUND to TRUE if
This works for everything I could throw at it. If you think it's reasonable I can open another ticket and have the code reviewed as a separate fix.
Comment Actions
I found a CHECK_CXX_SOURCE_COMPILES, which seems to be used in a number of places in LLVM. I'll give it a try.
Comment Actions
Looks like my last email got lost:
I'm wondering if we can remove the binary requirement all together: is it possible to run a small program that would return EXIT_SUCCESS if the library is the correct version?
Something like:
#include <z3.h>
int main()
{
unsigned int major, minor, build, revision;
Z3_get_version(&major, &minor, &build, &revision);
if(major >= 4 && minor >= 7 && build >= 1)
return EXIT_SUCCESS;
return EXIT_FAILURE;
}This would be part of FindZ3.cmake and would set Z3_FOUND.
Do you guys think it's possible? I'm almost certain it can be done with autotools, but I'm clueless when it comes to cmake.
Comment Actions
Hi @mikhail.ramalho, I don't think this is feasible unfortunately. If we're using a cross-compiler the emitted binary won't be native to the platform. In other words, you cannot test for Z3 as a run-time property.
I looked at the Z3 source and they do have a z3_version.h file now and was added in version 4.4.2.0. You may be able to use the header directly, but I'm not sure how find_package() parses for library versions and if this is useful or not. The generated header is named src/util/version.h in this initial commit:
https://github.com/Z3Prover/z3/commit/251527603df01904f70ed884f8695fedab5caed9
and was renamed last September to src/util/z3_version.h in this commit:
https://github.com/Z3Prover/z3/commit/0c4754d94bdfaf07077120f5cbff780d8fb0971d
Comment Actions
Hi @brzycki, but isn't it exactly what we want? I mean, if we try to cross-compile and it fails for any reason (non-native library, wrong version), then Z3_FOUND shouldn't be set.
I just finished a small patch that checks the version as a run-time property. Please, let me know your thoughts.
If you agree with this approach I'll create a separate revision for it (it seems to work on ubuntu and fedora for me).
Comment Actions
Independent of the rest of the discussion, this patch should be part of the reland, to make sure that explicitly turning off Z3 works reliably. Thanks for coming up with that, and thanks everyone for the good discussion here :)
Comment Actions
Sounds good to me, although I think it'd be good to emit a warning or at least a message about assuming the version due to a missing executable.
You're right, it looks like it was originally internal-only, but then became exposed as part of the interface with the second commit, starting around the release of z3 4.8.1. It's been a while since I've used CMake, but perhaps something like this:
if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h")
file(STRINGS "${Z3_INCLUDE_DIR }/z3_version.h" z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
endif()I see other projects do something similar; e.g. https://github.com/SRI-CSL/sally/blob/master/cmake/FindZ3.cmake#L20 . I'm less fond of that approach because it involves even more moving parts, but then again, parsing C header files with regular expressions isn't particularly robust either.
Comment Actions
perhaps something like this:
if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h") file(STRINGS "${Z3_INCLUDE_DIR }/z3_version.h" z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"") string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" Z3_VERSION_STRING "${z3_version_str}") unset(z3_version_str) endif()
That is almost exactly what I was thinking about this morning. I'd prefer the following since it's more robust for older versions:
if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/z3_version.h")
# For 4.8.0 or newer
file(STRINGS "${Z3_INCLUDE_DIR }/z3_version.h" z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
elseif(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR }/version.h")
file(STRINGS "${Z3_INCLUDE_DIR }/version.h" z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"")
string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"Z3 ([0-9\.]+)\".*$" "\\1" Z3_VERSION_STRING "${z3_version_str}")
unset(z3_version_str)
else()
message(WARNING "Unable to locate the Z3 version.h/z3_version.h header. Setting the found version to 0.0.0.")
set(Z3_VERSION_STRING "0.0.0")
endif()Comment Actions
I'm not sure, cross-compilation is tricky to get right.
I just finished a small patch that checks the version as a run-time property. Please, let me know your thoughts.
If you agree with this approach I'll create a separate revision for it (it seems to work on ubuntu and fedora for me).
I'd be interested in seeing it and I'll happily provide feedback. I'm not sure if this method is better or worse than regex parsing of headers that @ddcc suggested.
No matter what algorithm chosen I'd strongly prefer the case when we are unable to ascertain the correct Z3_VERSION_STRING we should conservatively set this to "0.0.0" with a warning to inform the users early on something is strange with the version of Z3 being tested.
Comment Actions
The old version.h header isn't externally exposed, only the newer z3_version.h header starting with version 4.8.1. I built a copy of 4.7.1 from source, and I don't see it, so unfortunately I think the second check for version.h is superfluous. Instead, I think it'd be ok to still query the executable as the primary, then fallback to this header as the secondary?
Comment Actions
Thanks @ddcc for checking on version.h, I meant to do so but got side-tracked with other items today.
I think your suggestion is a good compromise, possibly something like the following as pseudo-code:
if z3_version.h: use_regex_parsed_version if version_not_valid and z3_executable: use_z3_execution output_version if version_not_valid z3_include_dir: try_mikhail.ramalho_runtime_check if version_not_valid: warning "Z3 is not installed correctly or too old to detect its version" version = 0.0.0
Comment Actions
Hi guys,
I just sent the first prototype of the solution. All the magic happens inside the CHECK_CXX_SOURCE_RUNS call.
There is still one thing to do: currently, the program is hard-coded to check for version 4.7.1. We should either get it from the find_package call or remove the minimum version from the find_package call and rely only on the program. I'm not a big fan of the latter.
Comment Actions
I think hardcoding the version into the binary is too brittle. Instead, your program can just print out the current z3 version (much like the current execution of the z3 binary), and the remaining logic can remain in CMake, with the fallbacks as suggested above by @brzycki.
Comment Actions
I don't think there is a mechanism to do so easily within CMake. The CHECK_CXX_SOURCE_RUNS call only returns a boolean answer, not stdout. You have to use the underlying try_run() command along with RUN_OUTPUT_VARIABLE to obtain a given version. This interface seems less simple than the CHECK_CXX_* macros.
Comment Actions
Here's my proposed logic as actual CMake code. @mikhail.ramalho if you can get your code to emit the version string I made a TODO placeholder for it in the 3rd block below.
diff --git a/llvm/cmake/modules/FindZ3.cmake b/llvm/cmake/modules/FindZ3.cmake index 5c6d3f0..f913686 100644 --- a/llvm/cmake/modules/FindZ3.cmake +++ b/llvm/cmake/modules/FindZ3.cmake @@ -30,7 +30,23 @@ find_program(Z3_EXECUTABLE z3 PATH_SUFFIXES bin ) -if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) +# Searching for the version of the Z3 library is a best-effort task. The version +# is only recently added to a public header. +unset(Z3_VERSION_STRING) + +if(Z3_INCLUDE_DIR AND EXISTS "${Z3_INCLUDE_DIR}/z3_version.h") + # Z3 4.8.1+ has the version is in a public header. + file(STRINGS "${Z3_INCLUDE_DIR}/z3_version.h" + z3_version_str REGEX "^#define[\t ]+Z3_FULL_VERSION[\t ]+\".*\"") + + string(REGEX REPLACE "^.*Z3_FULL_VERSION[\t ]+\"([0-9\.]+)\".*$" "\\1" + Z3_VERSION_STRING "${z3_version_str}") + unset(z3_version_str) +endif() + +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES AND + Z3_EXECUTABLE)) + # Run the found z3 executable and parse the version string output. execute_process (COMMAND ${Z3_EXECUTABLE} -version OUTPUT_VARIABLE libz3_version_str ERROR_QUIET @@ -41,6 +57,20 @@ if(Z3_INCLUDE_DIR AND Z3_LIBRARIES AND Z3_EXECUTABLE) unset(libz3_version_str) endif() +if(NOT Z3_VERSION_STRING AND (Z3_INCLUDE_DIR AND Z3_LIBRARIES)) + # We do not have the Z3 binary to query for a version. Try to use + # a small C++ program to detect it via the Z3_get_version() API call. + # TODO: add code from Mikhail Ramalho to obtain the version. + # TODO: set(Z3_VERSION_STRING) if successful. +endif() + +if(NOT Z3_VERSION_STRING) + # Give up: we are unable to obtain a version of the Z3 library. Be + # conservative and force the found version to 0.0.0 to make version + # checks always fail. + set(Z3_VERSION_STRING "0.0.0") +endif() +
Comment Actions
Update Z3 script to use cmake's try_run in order to retrieve the version from the lib.
Comment Actions
Hi all,
Sorry for the massive delay, but I just updated the FindZ3 script to retrieve the version from the lib. I changed it to use try_run instead of try_compile so we can get the version number.
I tried to use @brzycki code to get the version from the header, however, it's not working for Z3 4.8.4. In Z3 4.8.3 the FULL_VERSION is a nice "Z3 4.8.3.0" but in version 4.8.4 it's "Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4" and cmake fails with the following message:
-- Could NOT find Z3: Found unsuitable version "#define Z3_FULL_VERSION "Z3 4.8.4.10272 d6df51951f4c master z3-4.8.4"", but required is at least "4.7.1" (found /home/mgadelha/z3/bin/libz3.so)
I believe we have a few options here:
- Update the regex to handle the new format for Z3_FULL_VERSION.
- Instead of parsing Z3_FULL_VERSION, we can parse Z3_MAJOR_VERSION, Z3_MINOR_VERSION and Z3_BUILD_NUMBER which are also available in the same header.
But, we'll still face the same problem of them changing the string format and breaking the scripts.
Comment Actions
Thanks for making the changes! Is this being parsed from e.g. /usr/include/z3_version.h? I checked their code, and I have a local build of z3 4.8.5.0, but I'm not seeing those changes to the version string:
#define Z3_FULL_VERSION "Z3 4.8.5.0"
Comment Actions
Nope, I downloaded it from release page on github: https://github.com/Z3Prover/z3/releases
Comment Actions
The only relevant commit that I can find is https://github.com/Z3Prover/z3/commit/2cb4223979cc94e2ebc4e49a9e83adbdcd2b6979 , but it first landed in z3 4.6.0. It looks like it's specific to CMake though, so is it different if you use the python build? I haven't tried the CMake build.
Comment Actions
Indeed, it seems to be cmake specific (even the commit message says that the python scripts were not changed).
Comment Actions
Hmm this looks like there are some bugs in the different Z3 build systems.
So for the CMake build the value of Z3_FULL_VERSION_STR is used to populate the Z3_FULL_VERSION macro in the header file. Initially this is "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}" but then
If the git has is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L96
and if the git description is available we append to it https://github.com/Z3Prover/z3/blob/c0f7afacc497e7e2e1a2a28bcebf1173933f5bab/CMakeLists.txt#L109
This was my attempt at mimicking the get_full_version_string() function ( https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L3065 ) when I added Z3's CMake build system.
Unfortunately this doesn't quite match what Z3's python build system does.
- In the python build system the VER_REVISION global (used to set Z3_REVISION_NUMBER macro and is the forth integer in Z3_FULL_VERSION, i.e. d in a.b.c.d) tries to count the number of commits reachable from the current git HEAD (see https://github.com/Z3Prover/z3/blob/038f992ff485d0bf93f962dc9e45330ff1e2e47d/scripts/mk_util.py#L561 ). The CMake build system doesn't mimic this. Personally I don't think the python build system makes sense here at all given that this integer goes in the 4th position in the version output (i.e. d in a.b.c.d).
- In the CMake build system the 4th integer in Z3_FULL_VERSION is always whatever Z3_VERSION_TWEAK is set to in the root CMakeLists.txt file. So far, I think has always been 0.
So the bug here is that the CMake and python build systems don't agree on the meaning of the 4th version field. Personally I think the implementation of Z3's CMake build system makes more sense given where it is placed in the version string but that means the name Z3_REVISION_NUMBER macro name isn't very appropriate.
None of this really mattered until the version header file became public
Would one of you be able to file a bug against Z3 to fix this? I am no longer in a position to contribute to Z3 so I can't do this.
Comment Actions
This output means you built Z3 from source that was in a git repository and you used Z3's python build system.
This output means you built Z3 from source that was not in a git repository. In this case the header file should look the same for both Z3's CMake and Python build systems.
Comment Actions
I've opened https://github.com/Z3Prover/z3/issues/2184 .
That's strange, I have been building from a git repository.
Since the differences in version string depending on the build system are intended behavior, it seems (2) would be preferable?
Comment Actions
Thanks.
That's strange, I have been building from a git repository.
Hmm I misread the python code. I inferred that because the extra text from
def get_full_version_string(major, minor, build, revision): global GIT_HASH, GIT_DESCRIBE res = "Z3 %s.%s.%s.%s" % (major, minor, build, revision) if GIT_HASH: res += " " + GIT_HASH if GIT_DESCRIBE: branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD']) res += " " + branch + " " + check_output(['git', 'describe']) return '"' + res + '"'
wasn't in your output. However, I didn't actually check to see how GIT_HASH and GIT_DESCRIBE are set. It looks like you need to pass --githash and --gitdescribe respectively to the Python build system configure scripts to get those. They are false by default.
The Z3 CMake build system is different. It will add the git hash and description by default if it detects you're using git ( see https://github.com/Z3Prover/z3/blob/057151c7a80dac44d610f5286799ad7b727b5d2c/CMakeLists.txt#L67 ). You can switch this off by passing
-DINCLUDE_GIT_HASH=OFF -DINCLUDE_GIT_DESCRIBE=OFF to the CMake invocation you use when configuring Z3.
Since the differences in version string depending on the build system are intended behavior, it seems (2) would be preferable?
Yeah, that's the way I would go.
Comment Actions
Updated script to parse Z3's headers and changed the workflow to handle cross compilation cases.
| llvm/cmake/modules/FindZ3.cmake | ||
|---|---|---|
| 92 | Should be ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD_NUMBER} | |
Comment Actions
Hi all,
I just updated the CMake script to get the version by parsing the header, however, I just found a potential issue in the previous approach: if we have incompatible libs in the path (32-bits libs when compiling in 64-bit mode) the CMake config will succeed but the compilation will fail.
To fix that, I changed the script slightly: we first try to dinamically get the Z3's version, if we fail and we are cross compiling, then we try to parse the headers. Right now, it should just work but I'd like to add a message to warn the user that we found the lib but we don't know if it'll link.
Let me know your thoughts.
Comment Actions
Can you plz add some wrappers of overflow predicates like Z3_mk_bvadd_no_overflow, Z3_mk_bvadd_no_underflow, ... to SMTAPI.h and Z3Solver.cpp?
It could help me, thanks!
Comment Actions
! In D54978#1440464, @ddcc wrote:
Do you know if this configuration builds fine now?
It's working fine now, I'll push it later today.
! In D54978#1441355, @gou4shi1 wrote:
Can you plz add some wrappers of overflow predicates like Z3_mk_bvadd_no_overflow, Z3_mk_bvadd_no_underflow, ... to SMTAPI.h and Z3Solver.cpp?
It could help me, thanks!
Sure, I'll create a new revision with the added functions tonight.
Comment Actions
! In D54978#1441417, @mikhail.ramalho wrote:
Sure, I'll create a new revision with the added functions tonight.
I am very happy with your quickly reply.
btw, Z3_get_bv_sort_size is also needed :)
Thanks for your nice job!
Comment Actions
! In D54978#1441547, @mikhail.ramalho wrote:
You can get the sort size by calling getBitvectorSortSize().
found, thx
Comment Actions
I'm afraid this broke some bots that build with LLVM_ENABLE_MODULES=1.
For example:
Undefined symbols for architecture x86_64:
"llvm::errs()", referenced from:
llvm::SMTExpr::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTSolver::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTSort::dump() const in liblldbDebugserverCommon.a(RNBSocket.cpp.o)
llvm::SMTExpr::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)
llvm::SMTSolver::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)
llvm::SMTSort::dump() const in liblldbDebugserverCommon.a(SocketAddress.cpp.o)Long story short: You can't have an LLVM_DUMP_METHOD defined inline inside of a module.
One way to fix this would be to move the function body of the various
LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }functions into .cpp files.
Comment Actions
Unfortunately, I was not able to reproduce the bug locally (when I enable modules, clang complains about some std::shared_ptr<msf::MappedBlockStream>), however, I just pushed r356994 and I'll keep an eye on the bot.
Thanks for the report.
Comment Actions
Thanks!
The problem with these methods is that LLVM_DUMP_METHOD forces the function to be emitted even if it is not used and Clang modules without local submodule visibility will implicitly include all header files in a module, which will then cause the missing symbol error.
Comment Actions
My own out-of-tree pass #include <llvm/Support/SMTAPI.h> and use cmake's add_llvm_library to compile it into a .so
However, opt -load-pass-plugin=my-pass.so -passes="foo" bar.ll fails:
opt: symbol lookup error: Passes/libStackPasses.so: undefined symbol: _ZN4llvm14CreateZ3SolverEv
(c++filt: llvm::CreateZ3Solver())
If I move the content of Z3Solver.cpp into another file of llvm/Support (like llvm/Support/raw_ostream.cpp)
everything works.
Comment Actions
I build llvm with cmake -DCMAKE_BUILD_TYPE=Debug -DLLVM_TARGETS_TO_BUILD=X86 -DLLVM_ENABLE_PROJECTS=clang ../llvm
I have make a mini reproduce example at https://github.com/gou4shi1/mini-repro-pass
you can build this example with mkdir build && cd build && cmake -DCMAKE_BUILD_TYPE=Debug .. && make
you can run this example with opt -load-pass-plugin=ttttt/ttttt.so -passes="ttttt" ../test/add100.ll
| cfe/trunk/CMakeLists.txt | ||
|---|---|---|
| 453 ↗ | (On Diff #192151) | This message needs to be updated :) |
If anybody uses Z3 for anything else in LLVM, it would immediately make sense to enable Z3 without static analyzer. Is this check even justified? Unlike ARCMT, these two aren't dependencies of each other. I think if we detach Z3 from clang, we should also detach it from the analyzer.