From 0d5ab1705324e91d9788185cd16e1d4e6bf54fbe Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 2 Mar 2021 00:26:29 -0800 Subject: [PATCH] Add aarch64 (ARM64) cross-compile support. (#6033) This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64. Fixes #1479 #5769. --- INSTALL.md | 5 +- cmake/Toolchain-aarch64.cmake | 31 +++++ configure.sh | 22 +++- contrib/get-antlr-3.4 | 79 ++++++------- contrib/get-gmp-dev | 13 +- contrib/get-win-dependencies | 111 ------------------ src/parser/CMakeLists.txt | 1 - .../quantifiers/fmf/bounded_integers.cpp | 3 +- 8 files changed, 102 insertions(+), 163 deletions(-) create mode 100644 cmake/Toolchain-aarch64.cmake delete mode 100755 contrib/get-win-dependencies diff --git a/INSTALL.md b/INSTALL.md index 75538d7cf..fc19dc946 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -30,7 +30,6 @@ To build a static binary for macOS, use: Cross-compiling CVC4 with Mingw-w64 can be done as follows: ``` - HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies ./configure.sh --win64 --static cd # default is ./build @@ -80,8 +79,8 @@ We recommend using a GCC version > 4.5.1. Do **not** install GMP via the provided script `contrib/get-gmp-dev` unless your distribution * does not ship with the GMP configuration you need, e.g., - script `contrib/get-win-dependencies` uses `contrib/get-gmp-dev` when - cross-compiling GMP for Windows. + `contrib/get-gmp-dev` is used in `configure.sh` when cross-compiling GMP for + Windows. * does not ship with static GMP libraries (e.g., Arch Linux) and you want to build CVC4 statically. diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake new file mode 100644 index 000000000..1db18e745 --- /dev/null +++ b/cmake/Toolchain-aarch64.cmake @@ -0,0 +1,31 @@ +##################### +## Toolchain-aarch64.cmake +## Top contributors (to current version): +## Mathias Preiner +## This file is part of the CVC4 project. +## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS +## in the top-level source directory and their institutional affiliations. +## All rights reserved. See the file COPYING in the top-level source +## directory for licensing information. +## +# Toolchain file for building for ARM on Ubuntu host. +# +# Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake + +SET(CMAKE_SYSTEM_NAME Linux) +SET(CMAKE_SYSTEM_PROCESSOR arm) + +set(TOOLCHAIN_PREFIX aarch64-linux-gnu) + +SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc) +SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++) + +# Set target environment path +SET(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX}) + +# Adjust the default behaviour of the find_XXX() commands: +# search headers and libraries in the target environment, search +# programs in the host environment +set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) +set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY BOTH) +set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE BOTH) diff --git a/configure.sh b/configure.sh index 1e036e548..e7a858486 100755 --- a/configure.sh +++ b/configure.sh @@ -22,6 +22,7 @@ General options; --name=STR use custom build directory name (optionally: +path) --best turn on dependencies known to give best performance --gpl permit GPL dependencies, if available + --arm64 cross-compile for Linux ARM 64 bit --win64 cross-compile for Windows 64 bit --ninja use Ninja build system @@ -151,6 +152,7 @@ ubsan=default unit_testing=default valgrind=default win64=default +arm64=default werror=default abc_dir=default @@ -244,7 +246,8 @@ do --no-kissat) kissat=OFF;; --win64) win64=ON;; - --no-win64) win64=OFF;; + + --arm64) arm64=ON;; --ninja) ninja=ON;; @@ -357,6 +360,20 @@ do shift done +#--------------------------------------------------------------------------# +# Automatically set up dependencies based on configure options +#--------------------------------------------------------------------------# + +if [ "$arm64" == "ON" ]; then + echo "Setting up dependencies for ARM 64-bit build" + HOST="aarch64-linux-gnu" contrib/get-antlr-3.4 || exit 1 + HOST="aarch64-linux-gnu" contrib/get-gmp-dev || exit 1 +elif [ "$win64" == "ON" ]; then + echo "Setting up dependencies for Windows 64-bit build" + HOST="x86_64-w64-mingw32" contrib/get-antlr-3.4 || exit 1 + HOST="x86_64-w64-mingw32" contrib/get-gmp-dev || exit 1 +fi + #--------------------------------------------------------------------------# if [ $werror != default ]; then @@ -393,6 +410,8 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl" [ $win64 != default ] \ && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-mingw64.cmake" +[ $arm64 != default ] \ + && cmake_opts="$cmake_opts -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake" [ $ninja != default ] && cmake_opts="$cmake_opts -G Ninja" [ $muzzle != default ] \ && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" @@ -478,6 +497,7 @@ root_dir=$(pwd) # The cmake toolchain can't be changed once it is configured in $build_dir. # Thus, remove $build_dir and create an empty directory. [ $win64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir" +[ $arm64 = ON ] && [ -e "$build_dir" ] && rm -r "$build_dir" mkdir -p "$build_dir" cd "$build_dir" diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 index 45dc86583..ed7d02496 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 @@ -2,9 +2,13 @@ # source "$(dirname "$0")/get-script-header.sh" ANTLR_HOME_DIR="$DEPS_DIR/antlr-3.4" +rm -rf "$ANTLR_HOME_DIR" -if [ -z "${BUILD_TYPE}" ]; then - BUILD_TYPE="--disable-shared --enable-static" +[ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static" +if [ -n "$HOST" ]; then + ANTLR_CONFIGURE_ARGS="--host=$HOST" + MACHINE_TYPE="$(echo "$HOST" | cut -d '-' -f 1)" + echo "Using MACHINE_TYPE=$MACHINE_TYPE for HOST=$HOST" fi if [ -z "${MACHINE_TYPE}" ]; then @@ -34,7 +38,7 @@ webget \ mkdir -p "$ANTLR_HOME_DIR/bin" tee "$ANTLR_HOME_DIR/bin/antlr3" < config.sub.new +mv config.sub.new config.sub # Make antlr3debughandlers.c empty to avoid unreferenced symbols rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c -if [ "${MACHINE_TYPE}" == 'x86_64' ]; then - # 64-bit stuff here - ./configure --enable-64bit --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE + +# Enable 64-bit build +if [[ "${MACHINE_TYPE}" == *"64" ]]; then + ANTLR_CONFIGURE_ARGS="$ANTLR_CONFIGURE_ARGS --enable-64bit" + echo "============== WARNING ====================" + echo "The script guessed that this machine is 64 bit." + echo "If ANTLR should be built as 32 bit \(i.e. -m32\)," + echo "please rerun the script as" + echo " MACHINE_TYPE=\"x86\" ./get-antlr-3.4" else - # 32-bit stuff here - ./configure --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE + echo "============== WARNING ====================" + echo "The script guessed that this machine is 32 bit." + echo "If ANTLR should be built as 64 bit \(i.e. -m64\)," + echo "please rerun the script as" + echo " MACHINE_TYPE=\"x86_64\" ./get-antlr-3.4" fi +# Build static ANTLR library + +./configure --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE + cp Makefile Makefile.orig sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig > Makefile make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" make install -if [[ $WINDOWS_BUILD == "yes" ]]; then - exit 0 -fi +# Build shared ANTLR library + +# On some systems the library may be installed to lib64/ instead of lib/ +LIB_DIR="$(dirname "$(find "$INSTALL_DIR" -name libantlr3c.a)")" -mv "$INSTALL_LIB_DIR/libantlr3c.a" "$INSTALL_LIB_DIR/libantlr3c-static.a" +mv "$LIB_DIR/libantlr3c.a" "$LIB_DIR/libantlr3c-static.a" make clean -if [ "${MACHINE_TYPE}" == 'x86_64' ]; then - # 64-bit stuff here - ./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE -else - # 32-bit stuff here - ./configure --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE -fi +./configure --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE cp Makefile Makefile.orig sed 's,^\(CFLAGS = .*\),\1 -fexceptions,' Makefile.orig > Makefile make CFLAGS="${MAKE_CFLAGS}" CXXFLAGS="${MAKE_CXXFLAGS}" LDFLAGS="${MAKE_LDFLAGS}" make install -mv "$INSTALL_LIB_DIR/libantlr3c.la" "$INSTALL_LIB_DIR/libantlr3c.la.orig" - -awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < "$INSTALL_LIB_DIR/libantlr3c.la.orig" > "$INSTALL_LIB_DIR/libantlr3c.la" -rm "$INSTALL_LIB_DIR/libantlr3c.la.orig" +mv "$LIB_DIR/libantlr3c.la" "$LIB_DIR/libantlr3c.la.orig" -if [ "${MACHINE_TYPE}" == 'x86_64' ]; then - # 64-bit stuff here - echo ============== WARNING ==================== - echo The script guessed that this machine is 64 bit. - echo If antlr should be built as 32 bit \(i.e. -m32\), - echo please rerun the script as - echo MACHINE_TYPE=\"x86\" ./get-antlr3.4 - -else - # 32-bit stuff here - echo ============== WARNING ==================== - echo The script guessed that this machine is 32 bit. - echo If antlr should be built as 64 bit \(i.e. -m64\), - echo please rerun the script as - echo MACHINE_TYPE=\"x86_64\" ./get-antlr3.4 -fi +awk '/^old_library=/ {print "old_library='\''libantlr3c-static.a'\''"} /^library_names=/ {print "library_names='\''libantlr3c.a'\''"} !/^old_library=/ && !/^library_names=/ {print}' < "$LIB_DIR/libantlr3c.la.orig" > "$LIB_DIR/libantlr3c.la" +rm "$LIB_DIR/libantlr3c.la.orig" echo echo ===================== Now configure CVC4 with ===================== diff --git a/contrib/get-gmp-dev b/contrib/get-gmp-dev index 3fc913a7d..d0ce045e4 100755 --- a/contrib/get-gmp-dev +++ b/contrib/get-gmp-dev @@ -1,8 +1,8 @@ #!/usr/bin/env bash # # This script should only be used if your distribution does not ship with the -# GMP configuration you need. For example, contrib/get-win-dependencies -# cross-compiles GMP for Windows. You can also use the script if your +# GMP configuration you need. For example, for cross-compiling GMP for Windows +# or Linux ARM platforms. You can also use the script if your # distribution does not ship with static GMP libraries (e.g., Arch Linux) and # you want to build CVC4 statically. # In most of the cases the GMP version installed on your system is the one you @@ -16,14 +16,15 @@ source "$(dirname "$0")/get-script-header.sh" [ -z "$GMPVERSION" ] && GMPVERSION=6.2.0 GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION" +rm -rf "$GMP_DIR" echo ============================================================================= echo echo "This script should only be used if your distribution does not ship with the" -echo "GMP configuration you need. For example, contrib/get-win-dependencies cross-" -echo "compiles GMP for Windows. You can also use the script if your distribution" -echo "does not ship with static GMP libraries (e.g., Arch Linux) and you want to" -echo "build CVC4 statically." +echo "GMP configuration you need. For example, for cross-compiling GMP for" +echo "Windows or Linux ARM platforms. You can also use the script if your Linux" +echo "distribution does not ship with static GMP libraries (e.g., Arch Linux)" +echo "and you want to build CVC4 statically." echo echo "In most of the cases the GMP version installed on your system is the one you" echo "want and should use." diff --git a/contrib/get-win-dependencies b/contrib/get-win-dependencies deleted file mode 100755 index 47acc7c08..000000000 --- a/contrib/get-win-dependencies +++ /dev/null @@ -1,111 +0,0 @@ -#!/usr/bin/env bash -# -# win32-build script -# Morgan Deters -# Tue, 15 Jan 2013 11:11:24 -0500 -# - -set -e -o pipefail - -export WINDOWS_BUILD=yes -export MAKE_CFLAGS= -export MAKE_CXXFLAGS= -export MAKE_LDFLAGS= -export BUILD_TYPE="--disable-shared --enable-static" -while getopts ":s" opt; do - case ${opt} in - s ) - MAKE_CFLAGS="-static-libgcc -static-libstdc++" - MAKE_CXXFLAGS="-static-libgcc -static-libstdc++" - # CVC4 uses some internal symbols of ANTLR, so all symbols need to be - # exported - MAKE_LDFLAGS="-no-undefined -Wl,--export-all-symbols" - BUILD_TYPE="--enable-shared --disable-static" - ;; - esac -done - -if [ -z "$HOST" ]; then - HOST=x86_64-w64-mingw32 - echo "WARNING:" - echo "WARNING: Using default HOST value: $HOST" - echo "WARNING: You should probably run this script like this:" - echo "WARNING:" - echo "WARNING: HOST=i686-w64-mingw32 win-build" - echo "WARNING:" - echo "WARNING: (replacing the i686-w64-mingw32 with your build host)" - echo "WARNING: to ensure the script builds correctly." - echo "WARNING:" -fi - -GMPVERSION=6.2.0 -BOOSTVERSION=1.55.0 -BOOSTBASE=boost_1_55_0 - -function reporterror { - echo - echo ============================================================================= - echo - echo "There was an error setting up the prerequisites. Look above for details." - echo - exit 1 -} - -function webget { - if [ -x "$(command -v wget)" ]; then - wget -c -O "$2" "$1" - elif [ -x "$(command -v curl)" ]; then - curl -L "$1" >"$2" - else - echo "Can't figure out how to download from web. Please install wget or curl." >&2 - exit 1 - fi -} - -for dir in antlr-3.4 gmp-$GMPVERSION boost-$BOOSTVERSION; do - if [ -e "$dir" ]; then - echo "error: $dir directory exists; please move it out of the way." >&2 - exit 1 - fi -done - -echo ============================================================================= -echo -echo "Setting up ANTLR 3.4..." -echo -MACHINE_TYPE="x86_64" ANTLR_CONFIGURE_ARGS="--host=$HOST" contrib/get-antlr-3.4 | grep -v 'Now configure CVC4 with' | grep -v '\./configure --with-antlr-dir=' -[ ${PIPESTATUS[0]} -eq 0 ] || reporterror -echo - -# Setup GMP -HOST="$HOST" \ -BUILD_TYPE="$BUILD_TYPE" \ -MAKE_CFLAGS="$MAKE_CFLAGS" \ -MAKE_CXXFLAGS="$MAKE_CXXFLAGS" \ -MAKE_LDFLAGS="$MAKE_LDFLAGS" \ -GMPVERSION="$GMPVERSION" \ - contrib/get-gmp-dev || reporterror - -echo -echo ============================================================================= -echo -echo "Setting up Boost..." -echo -( mkdir boost-$BOOSTVERSION && - cd boost-$BOOSTVERSION && - webget https://sourceforge.net/projects/boost/files/boost/$BOOSTVERSION/$BOOSTBASE.tar.gz/download $BOOSTBASE.tar.gz && - tar xfz $BOOSTBASE.tar.gz && - cd $BOOSTBASE && - ./bootstrap.sh --with-toolset=gcc --prefix=`pwd`/.. --with-libraries=thread && - echo "using gcc : mingw32 : $HOST-gcc ;" >> project-config.jam && - cp tools/build/v2/tools/gcc.jam tools/build/v2/tools/gcc.jam.orig && - sed 's,option = -pthread ; libs = rt ;,,' tools/build/v2/tools/gcc.jam.orig > tools/build/v2/tools/gcc.jam && - ./b2 gcc-mingw32 threadapi=win32 link=static install ) || exit 1 -echo -echo ============================================================================= -echo -echo 'Now just run:' -echo " ./configure --enable-static-binary --disable-shared --host=$HOST LDFLAGS=\"-L`pwd`/gmp-$GMPVERSION/lib -L`pwd`/antlr-3.4/lib -L`pwd`/boost-$BOOSTVERSION/lib\" CPPFLAGS=\"-I`pwd`/gmp-$GMPVERSION/include -I`pwd`/antlr-3.4/include -I`pwd`/boost-$BOOSTVERSION/include\" --with-antlr-dir=\"`pwd`/antlr-3.4\" ANTLR=\"`pwd`/antlr-3.4/bin/antlr3\"" -echo ' make' -echo -echo ============================================================================= diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index 2fe92fb45..3fccac37b 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -8,7 +8,6 @@ ## All rights reserved. See the file COPYING in the top-level source ## directory for licensing information. ## -set(ANTLR_HOME ${ANTLR_DIR}) find_package(ANTLR REQUIRED) if(NOT HAVE_ANTLR3_FILE_STREAM_NEW) diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index fb0505bae..1b7355fdf 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -788,7 +788,8 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node { long rr = range.getConst().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; - for( unsigned k=0; kmkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) ); t = Rewriter::rewrite( t ); elements.push_back( t ); -- 2.30.2