From 36751338e321f66a58055bfa313da52b8e91039d Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Fri, 10 Mar 2023 18:42:50 -0500 Subject: [PATCH 1/2] Build CVC{4,5} natively on Windows This patch: * Upgrades CVC5 to version 1.0.5, which contains several key bugfixes and a new `--win64-native` flag, which allows CVC5 to be build natively on Windows. * Backports the `--win64-native` flag to CVC4, thereby allowing it to be built natively as well. * Tweaks the CI configuration to clean up how Python dependencies are installed, which are important to building CVC4 and CVC5. Fixes #4. By upgrading the CVC5 version, this also fixes #31. --- .github/ci.sh | 49 +++++++++++++------- .github/workflows/ci.yml | 22 ++++++--- README.md | 2 +- patches/cvc4-no-ld-gold.patch | 24 ++++++++++ patches/cvc4-win64-native.patch | 82 +++++++++++++++++++++++++++++++++ patches/cvc5-no-ld-gold.patch | 24 ++++++++++ patches/cvc5-win64-native.patch | 20 ++++++++ repos/cvc5 | 2 +- 8 files changed, 199 insertions(+), 26 deletions(-) create mode 100644 patches/cvc4-no-ld-gold.patch create mode 100644 patches/cvc4-win64-native.patch create mode 100644 patches/cvc5-no-ld-gold.patch create mode 100644 patches/cvc5-win64-native.patch diff --git a/.github/ci.sh b/.github/ci.sh index f89d1b4..2b090a8 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -62,18 +62,25 @@ build_boolector() { build_cvc4() { pushd repos/CVC4-archived + ./contrib/get-antlr-3.4 + ./contrib/get-symfpu if $IS_WIN ; then - echo "Downloading pre-built CVC4 binary for Windows" - curl -o cvc4$EXT -sL "https://github.com/CVC4/CVC4/releases/download/1.8/cvc4-1.8-win64-opt.exe" - cp cvc4$EXT $BIN + # Backport changes from https://github.com/cvc5/cvc5/pull/7512 needed to + # build CVC4 natively on Windows. + patch -p1 -i $PATCHES/cvc4-win64-native.patch + # GitHub Actions comes preinstalled with Chocolatey's mingw package, which + # includes the ld.gold linker. This does not play nicely with MSYS2's + # mingw-w64-x86_64-gcc, so we must prevent CMake from using ld.gold. + # (Ideally, there would be a CMake configuration option to accomplish this, + # but I have not found one.) + patch -p1 -i $PATCHES/cvc4-no-ld-gold.patch + ./configure.sh --static --static-binary --symfpu --win64-native production else - ./contrib/get-antlr-3.4 - ./contrib/get-symfpu ./configure.sh --static --no-static-binary --symfpu production - cd build - make -j4 - cp bin/cvc4$EXT $BIN fi + cd build + make -j4 + cp bin/cvc4$EXT $BIN (cd $BIN && ./cvc4$EXT --version && deps cvc4$EXT && ./cvc4$EXT $PROBLEM) popd cleanup_bins @@ -82,17 +89,25 @@ build_cvc4() { build_cvc5() { pushd repos/cvc5 if $IS_WIN ; then - # TODO: Once https://github.com/cvc5/cvc5/pull/7512 lands, build a native - # Windows version of CVC5 instead. - echo "Downloading pre-built CVC5 binary for Windows" - curl -o cvc5$EXT -sL "https://github.com/cvc5/cvc5/releases/download/cvc5-1.0.2/cvc5-Win64.exe" - cp cvc5$EXT $BIN + # Work around https://github.com/cvc5/cvc5/issues/9564 + patch -p1 -i $PATCHES/cvc5-win64-native.patch + # GitHub Actions comes preinstalled with Chocolatey's mingw package, which + # includes the ld.gold linker. This does not play nicely with MSYS2's + # mingw-w64-x86_64-gcc, so we must prevent CMake from using ld.gold. + # (Ideally, there would be a CMake configuration option to accomplish this, + # but I have not found one.) + patch -p1 -i $PATCHES/cvc5-no-ld-gold.patch + # Why do we manually override Python_EXECUTABLE below? GitHub Actions comes + # with multiple versions of Python pre-installed, and for some bizarre + # reason, CMake always tries to pick the latest version, even if it is not + # on the PATH. Manually overriding this option avoids this oddity. + ./configure.sh -DPython_EXECUTABLE=${pythonLocation}/python${EXT} --static --static-binary --auto-download --win64-native production else - ./configure.sh --static --no-static-binary --auto-download production - cd build - make -j4 - cp bin/cvc5$EXT $BIN + ./configure.sh -DPython_EXECUTABLE=${pythonLocation}/python${EXT} --static --no-static-binary --auto-download production fi + cd build + make -j4 + cp bin/cvc5$EXT $BIN (cd $BIN && ./cvc5$EXT --version && deps cvc5$EXT && ./cvc5$EXT $PROBLEM) popd cleanup_bins diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 87b1f95..3489086 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -27,13 +27,13 @@ jobs: - name: Install dependencies (Ubuntu) run: | sudo apt-get update - sudo apt-get install gperf automake autoconf lzip ninja-build + sudo apt-get install libfl-dev gperf automake autoconf lzip ninja-build if: runner.os == 'Linux' - name: Install dependencies (macOS) run: | brew update - brew install gperf automake autoconf ninja gnu-sed + brew install flex gperf automake autoconf ninja gnu-sed # macOS's version of sed lacks the -r option, which CVC5 requires. To # work around this, we install put GNU sed before macOS's sed on the # PATH. @@ -45,11 +45,13 @@ jobs: with: update: true msystem: MINGW64 + path-type: inherit install: | autoconf automake curl dos2unix + flex git gperf lzip @@ -59,19 +61,25 @@ jobs: mingw-w64-x86_64-gcc mingw-w64-x86_64-ninja patch - python tar unzip if: runner.os == 'Windows' - - uses: actions/setup-python@v2 + - name: Install Python + uses: actions/setup-python@v4 with: python-version: '3.9' - - uses: BSFishy/pip-action@v1 + - name: Install Python libraries + run: | + python -m pip install --upgrade pip + pip install pyparsing toml + + - name: Install Java + uses: actions/setup-java@v3 with: - packages: | - toml + distribution: 'temurin' + java-version: '17' - name: build_solver (non-Windows) shell: bash diff --git a/README.md b/README.md index e7e6ff6..9acd6b5 100644 --- a/README.md +++ b/README.md @@ -12,7 +12,7 @@ Currently, `what4-solvers` offers the following solver versions: * ABC - [99ab99bf](https://github.com/berkeley-abc/abc/tree/99ab99bfa6d1c2cc11d59af16aa26b273f611674) * Boolector - [3.2.2](https://github.com/Boolector/boolector/tree/e7aba964f69cd52dbe509e46e818a4411b316cd3) * CVC4 - [1.8](https://github.com/CVC4/CVC4-archived/tree/5247901077efbc7b9016ba35fded7a6ab459a379) -* CVC5 - [1.0.2](https://github.com/cvc5/cvc5/tree/ef35c1131976e5a3d981dace510d90aed2d11cef) +* CVC5 - [1.0.5](https://github.com/cvc5/cvc5/tree/4cb2ab9eb36f64295272a50f61dd1c62903aca4b) * Yices - [2.6.2](https://github.com/SRI-CSL/yices2/tree/8509cfb5c294df3c0ac3a4814483f39c58879606) * Z3 - [4.8.8](https://github.com/Z3Prover/z3/tree/ad55a1f1c617a7f0c3dd735c0780fc758424c7f1) and [4.8.14](https://github.com/Z3Prover/z3/tree/df8f9d7dcb8b9f9b3de1072017b7c2b7f63f0af8) diff --git a/patches/cvc4-no-ld-gold.patch b/patches/cvc4-no-ld-gold.patch new file mode 100644 index 0000000..03b4ff6 --- /dev/null +++ b/patches/cvc4-no-ld-gold.patch @@ -0,0 +1,24 @@ +diff --git a/CMakeLists.txt b/CMakeLists.txt +index e4d4aaeda..c604ba989 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -238,19 +238,6 @@ if (WIN32) + set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000") + endif () + +-#-----------------------------------------------------------------------------# +-# Use ld.gold if available +- +-execute_process(COMMAND ${CMAKE_C_COMPILER} +- -fuse-ld=gold +- -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION) +-if ("${LD_VERSION}" MATCHES "GNU gold") +- string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold") +- string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold") +- string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold") +- message(STATUS "Using GNU gold linker.") +-endif () +- + #-----------------------------------------------------------------------------# + # Option defaults (three-valued options (cvc4_option(...))) + # diff --git a/patches/cvc4-win64-native.patch b/patches/cvc4-win64-native.patch new file mode 100644 index 0000000..ffd1a2a --- /dev/null +++ b/patches/cvc4-win64-native.patch @@ -0,0 +1,82 @@ +diff --git a/configure.sh b/configure.sh +index 21a444082..8b30c8b14 100755 +--- a/configure.sh ++++ b/configure.sh +@@ -23,6 +23,7 @@ General options; + --best turn on dependencies known to give best performance + --gpl permit GPL dependencies, if available + --win64 cross-compile for Windows 64 bit ++ --win64-native natively compile for Windows 64 bit + --ninja use Ninja build system + + +@@ -146,6 +147,7 @@ ubsan=default + unit_testing=default + valgrind=default + win64=default ++win64_native=default + + language_bindings_java=default + language_bindings_python=default +@@ -238,6 +240,9 @@ do + --win64) win64=ON;; + --no-win64) win64=OFF;; + ++ --win64-native) win64_native=ON;; ++ --no-win64-native) win64_native=OFF;; ++ + --ninja) ninja=ON;; + + --glpk) glpk=ON;; +@@ -387,6 +392,9 @@ cmake_opts="" + && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" + [ $win64 != default ] \ + && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" ++# Because 'MSYS Makefiles' has a space in it, we set the variable vs. adding to 'cmake_opts' ++[ $win64_native != default ] \ ++ && [ $ninja == default ] && export CMAKE_GENERATOR="MSYS Makefiles" + [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja" + [ $muzzle != default ] \ + && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" +diff --git a/src/expr/mkexpr b/src/expr/mkexpr +index c5f12f487..b47c66753 100755 +--- a/src/expr/mkexpr ++++ b/src/expr/mkexpr +@@ -14,6 +14,9 @@ + # + # Output is to standard out. + # ++# Required to disable this option for bash >=5.2 to avoid automatically ++# replacing & by the substituted text. ++shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement + + copyright=2010-2014 + +diff --git a/src/expr/mkkind b/src/expr/mkkind +index fbf37eff4..aabc70afe 100755 +--- a/src/expr/mkkind ++++ b/src/expr/mkkind +@@ -13,6 +13,9 @@ + # + # Output is to standard out. + # ++# Required to disable this option for bash >=5.2 to avoid automatically ++# replacing & by the substituted text. ++shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement + + copyright=2010-2014 + +diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind +index e2a733ec8..e56d076d7 100755 +--- a/src/expr/mkmetakind ++++ b/src/expr/mkmetakind +@@ -16,6 +16,9 @@ + # + # Output is to standard out. + # ++# Required to disable this option for bash >=5.2 to avoid automatically ++# replacing & by the substituted text. ++shopt | grep -q '^patsub_replacement\b' && shopt -u patsub_replacement + + copyright=2010-2014 + diff --git a/patches/cvc5-no-ld-gold.patch b/patches/cvc5-no-ld-gold.patch new file mode 100644 index 0000000..233629e --- /dev/null +++ b/patches/cvc5-no-ld-gold.patch @@ -0,0 +1,24 @@ +diff --git a/CMakeLists.txt b/CMakeLists.txt +index bbd49612a..fb9b416f9 100644 +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -229,19 +229,6 @@ if (WIN32) + add_check_c_cxx_flag("-Wno-error=unknown-pragmas") + endif () + +-#-----------------------------------------------------------------------------# +-# Use ld.gold if available +- +-execute_process(COMMAND ${CMAKE_C_COMPILER} +- -fuse-ld=gold +- -Wl,--version ERROR_QUIET OUTPUT_VARIABLE LD_VERSION) +-if ("${LD_VERSION}" MATCHES "GNU gold") +- string(APPEND CMAKE_EXE_LINKER_FLAGS " -fuse-ld=gold") +- string(APPEND CMAKE_SHARED_LINKER_FLAGS " -fuse-ld=gold") +- string(APPEND CMAKE_MODULE_LINKER_FLAGS " -fuse-ld=gold") +- message(STATUS "Using GNU gold linker.") +-endif () +- + #-----------------------------------------------------------------------------# + # Use interprocedural optimization if requested + diff --git a/patches/cvc5-win64-native.patch b/patches/cvc5-win64-native.patch new file mode 100644 index 0000000..3b3eed3 --- /dev/null +++ b/patches/cvc5-win64-native.patch @@ -0,0 +1,20 @@ +diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt +index 3ff605948..d9dd4b70d 100644 +--- a/src/parser/CMakeLists.txt ++++ b/src/parser/CMakeLists.txt +@@ -107,15 +107,6 @@ flex_target(Lexer + ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp) + set_source_files_properties(${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp PROPERTIES GENERATED TRUE) + +-# The FlexLexer.h header is installed to /usr/include/, but is not found by the +-# cross-compilation environment. As a workaround we'll copy the header to the +-# current build directory and set the FLEX_INCLUDE_DIRS variable accordingly. +-if(WIN32) +- file(MAKE_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/flex) +- file(COPY /usr/include/FlexLexer.h DESTINATION ${CMAKE_CURRENT_BINARY_DIR}/flex) +- set(FLEX_INCLUDE_DIRS ${CMAKE_CURRENT_BINARY_DIR}/flex) +-endif() +- + # We don't want to enable -Wall for code generated by Flex. + set(gen_src_files ${CMAKE_CURRENT_BINARY_DIR}/smt2/smt2_lexer.cpp) + set(GEN_SRC_FLAGS "") diff --git a/repos/cvc5 b/repos/cvc5 index ef35c11..4cb2ab9 160000 --- a/repos/cvc5 +++ b/repos/cvc5 @@ -1 +1 @@ -Subproject commit ef35c1131976e5a3d981dace510d90aed2d11cef +Subproject commit 4cb2ab9eb36f64295272a50f61dd1c62903aca4b From 974d4a0479a6b8a8d4f91f621151e4c698872923 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 Mar 2023 20:21:13 -0400 Subject: [PATCH 2/2] Build Z3 using CMake/Ninja Unfortunately, using a native Windows version of Python causes Z3's `mk_make.py` script to generate a `Makefile` tailored specifically for Visual Studio, which is annoying to deal with in GitHub Actions. We instead use Z3's CMake/Ninja-based build, which avoids this. --- .github/ci.sh | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/.github/ci.sh b/.github/ci.sh index 2b090a8..9a3d6dd 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -195,11 +195,15 @@ build_z3-4.8.14() { build_z3() { Z3_BIN="z3-$1" pushd repos/$Z3_BIN + mkdir build + cd build if $IS_WIN ; then - sed -i.bak -e 's/STATIC_BIN=False/STATIC_BIN=True/' scripts/mk_util.py + cmake .. -DCMAKE_BUILD_TYPE=Release -DCMAKE_EXE_LINKER_FLAGS:STRING='-static' -GNinja + else + cmake .. -DCMAKE_BUILD_TYPE=Release -GNinja fi - python scripts/mk_make.py - (cd build && make -j4 && cp z3$EXT $BIN/$Z3_BIN$EXT) + ninja -j4 + cp z3$EXT $BIN/$Z3_BIN$EXT popd (cd $BIN && ./$Z3_BIN$EXT --version && deps $Z3_BIN$EXT && ./$Z3_BIN$EXT $PROBLEM) cleanup_bins