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.
Cross-compiling CVC4 with Mingw-w64 can be done as follows:
```
- HOST=x86_64-w64-mingw32 ./contrib/get-win-dependencies
./configure.sh --win64 --static <configure options...>
cd <build_dir> # default is ./build
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.
--- /dev/null
+#####################
+## 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)
--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
unit_testing=default
valgrind=default
win64=default
+arm64=default
werror=default
abc_dir=default
--no-kissat) kissat=OFF;;
--win64) win64=ON;;
- --no-win64) win64=OFF;;
+
+ --arm64) arm64=ON;;
--ninja) ninja=ON;;
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
&& 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"
# 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"
#
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
mkdir -p "$ANTLR_HOME_DIR/bin"
tee "$ANTLR_HOME_DIR/bin/antlr3" <<EOF
#!/usr/bin/env bash
-JAR_FILE="\$(find "\$(dirname "\$0")/../" -name antlr-3.4-complete.jar)"
+JAR_FILE="$INSTALL_DIR/share/java/antlr-3.4-complete.jar"
exec java -cp "\$JAR_FILE" org.antlr.Tool "\$@"
EOF
chmod a+x "$ANTLR_HOME_DIR/bin/antlr3"
setup_dep \
"https://www.antlr3.org/download/C/libantlr3c-3.4.tar.gz" \
"$ANTLR_HOME_DIR/libantlr3c-3.4"
-cd "$ANTLR_HOME_DIR/libantlr3c-3.4"
+cd "$ANTLR_HOME_DIR/libantlr3c-3.4" || exit 1
+
+# Add aarch64 architecture
+sed 's/avr32 \\$/avr32 | aarch64 \\/' config.sub > 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 =====================
#!/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
[ -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."
+++ /dev/null
-#!/usr/bin/env bash
-#
-# win32-build script
-# Morgan Deters <mdeters@cs.nyu.edu>
-# 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 =============================================================================
## 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)
{
long rr = range.getConst<Rational>().getNumerator().getLong()+1;
Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl;
- for( unsigned k=0; k<rr; k++ ){
+ for (long k = 0; k < rr; k++)
+ {
Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
t = Rewriter::rewrite( t );
elements.push_back( t );
projects / cvc5.git / commitdiff