Page MenuHomePhabricator

Move the SMT API to LLVM
ClosedPublic

Authored by mikhail.ramalho on Nov 27 2018, 2:38 PM.

Diff Detail

Repository
rL LLVM

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
Herald added a project: Restricted Project. · View Herald TranscriptFeb 6 2019, 7:19 PM
Herald added a subscriber: cfe-commits. · View Herald Transcript

Looks like this (all all other related Z3 reviews - D54975, D54976, D54977) review has completely omitted
cfe-commits and llvm-commits lists during review, which means it was essentially not reviewed by the wider audience.

brzycki added a subscriber: brzycki.Feb 7 2019, 9:45 AM

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)));
                                       ^~~~~~~~~~~~~~~~

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.

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)));
                                       ^~~~~~~~~~~~~~~~

@mikhail.ramalho could you revert then?
In general, we should not use Z3 unless it's explicitly requested.

The ninja build also fails

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.)

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)));
                                       ^~~~~~~~~~~~~~~~

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.

brzycki added a comment.EditedFeb 8 2019, 8:22 AM

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/llvm

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.

Thanks for the analysis. I think it's fine if you revert, given that.

Thanks for the analysis. I think it's fine if you revert, given that.

I'm running in to conflict dependency issues when attempting to revert rL353373. There is at least one other conflicting commit rL353465 on top of this code already.

I don't feel comfortable reverting 2+ patches in a sub-section of the code I know little about on a Friday afternoon. :)

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?

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?

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?

I'm guessing you didn't add llvm-commits and cfe-commits as subscribers when sending this out?

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?

I'm guessing you didn't add llvm-commits and cfe-commits as subscribers when sending this out?

As far as I know, that happens automatically if you add LLVM or Clang as project, that usually works for me.

mikhail.ramalho reopened this revision.Feb 10 2019, 11:44 AM

Reopening the revision as it was reverted.

This revision is now accepted and ready to land.Feb 10 2019, 11:44 AM
mikhail.ramalho added a project: Restricted Project.Feb 10 2019, 11:46 AM
mikhail.ramalho added a subscriber: llvm-commits.

@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".

Shouldn't that be off by default?

@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.
ddcc added subscribers: delcypher, ddcc.EditedFeb 11 2019, 12:39 PM

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.

Shouldn't that be off by default?

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.

The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only.

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.

The likely reason for this versioning problem is that the current versioning implementation in FindZ3.cmake is best-effort only.

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.)

brzycki added a comment.EditedFeb 11 2019, 4:22 PM

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?

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.

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.

Got it now, sorry about being dense.

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.

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

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.

ddcc added a comment.Feb 12 2019, 12:30 PM

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.

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.

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.

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.

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.

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.

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.

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?

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

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?

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.

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).

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}

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 :)

ddcc added a comment.EditedFeb 12 2019, 8:06 PM

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.

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.

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

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'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?

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.

lsaba added a subscriber: lsaba.Feb 13 2019, 7:05 AM
brzycki added a comment.EditedFeb 13 2019, 8:32 AM

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()

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'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.

ddcc added a comment.Feb 13 2019, 12:34 PM

That is almost exactly what I was thinking about this morning. I'd prefer the following since it's more robust for older versions:

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?

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?

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

Update FindZ3.cmake to do a runtime check of the version.

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.

ddcc added a comment.Feb 13 2019, 3:36 PM

I just sent the first prototype of the solution. All the magic happens inside the CHECK_CXX_SOURCE_RUNS call.

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.

I just sent the first prototype of the solution. All the magic happens inside the CHECK_CXX_SOURCE_RUNS call.

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.

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.

brzycki added a comment.EditedFeb 14 2019, 3:43 PM

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()
+

Update Z3 script to use cmake's try_run in order to retrieve the version from the lib.

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:

  1. Update the regex to handle the new format for Z3_FULL_VERSION.
  2. 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.

ddcc added a comment.EditedMar 15 2019, 7:34 PM

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:

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"

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:

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"

Nope, I downloaded it from release page on github: https://github.com/Z3Prover/z3/releases

ddcc added a comment.Mar 15 2019, 7:39 PM

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.

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.

Indeed, it seems to be cmake specific (even the commit message says that the python scripts were not changed).

ddcc added a comment.Mar 16 2019, 2:23 AM
  1. 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.

Sounds like this might be the way to go, since the format seems to be more stable.

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.

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.

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)

This output means you built Z3 from source that was in a git repository and you used Z3's python build system.

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"

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.

ddcc added a comment.Mar 16 2019, 11:34 AM

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.

I've opened https://github.com/Z3Prover/z3/issues/2184 .

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.

That's strange, I have been building from a git repository.

  1. 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.

Since the differences in version string depending on the build system are intended behavior, it seems (2) would be preferable?

Fixes:

  • FindZ3.cmake format .
  • Wrong SMTExpr namespace in SMTConstraintManager.h.

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.

I've opened https://github.com/Z3Prover/z3/issues/2184 .

Thanks.

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.

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.

  1. 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.

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.

Updated script to parse Z3's headers and changed the workflow to handle cross compilation cases.

ddcc added inline comments.Mar 18 2019, 1:11 PM
llvm/cmake/modules/FindZ3.cmake
92 ↗(On Diff #191152)

Should be ${Z3_MAJOR}.${Z3_MINOR}.${Z3_BUILD_NUMBER}

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.

Fix copy-and-paste error.

mikhail.ramalho marked an inline comment as done.Mar 19 2019, 8:17 AM

Fixed.

ddcc added a comment.Mar 23 2019, 12:51 AM

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.

Thanks, sounds good to me.

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.

Do you know if this configuration builds fine now?

@mikhail.ramalho

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!

! 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.

gou4shi1 added a comment.EditedMar 25 2019, 7:31 AM

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

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

You can get the sort size by calling getBitvectorSortSize().

gou4shi1 added a comment.EditedMar 25 2019, 8:33 AM

! In D54978#1441547, @mikhail.ramalho wrote:
You can get the sort size by calling getBitvectorSortSize().

found, thx

This revision was automatically updated to reflect the committed changes.

I'm afraid this broke some bots that build with LLVM_ENABLE_MODULES=1.

For example:

http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4

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.

I'm afraid this broke some bots that build with LLVM_ENABLE_MODULES=1.

For example:

http://green.lab.llvm.org/green/view/LLDB/job/lldb-cmake/22411/consoleFull#710926295dd1929ea-7054-4089-b7ef-4624c3781fa4

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.

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.

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.

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.

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.

I can't reproduce the error, can you send me a small example?

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.

I can't reproduce the error, can you send me a small example?

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

NoQ added inline comments.Apr 7 2019, 1:22 AM
cfe/trunk/CMakeLists.txt
453

This message needs to be updated :)