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.

8 files changed, 102 insertions, 163 deletions

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 <configure options...>
 
   cd <build_dir>   # 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;;
 
@@ -358,6 +361,20 @@ do
 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
   export CFLAGS=-Werror
@@ -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" <<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"
@@ -43,63 +47,58 @@ install_bin "$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 =====================
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 <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 =============================================================================
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<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 );