Add cross-compilation for arm64 on macOS (#8758)

Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 91832be57b12ae75f44a27aa2bd9e6fdb20301e7..ba2e2f6020f77ffea5363907b5d65110636fc1de 100644 (file)
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -29,6 +29,14 @@ jobs:
             exclude_regress: 3-4
             run_regression_args: --tester base --tester model --tester synth --tester abduct --tester dump
 
+          - name: macos:production-arm64
+            os: macos-11
+            config: production --auto-download --python-bindings --editline --arm64
+            cache-key: production-arm64
+            strip-bin: strip
+            python-bindings: true
+            binary-name: cvc5-macOS-arm64
+
           - name: win64:production
             os: ubuntu-latest
             config: production --auto-download --win64

diff --git a/NEWS.md b/NEWS.md
index f2910e9e1004b32e91b1464cbab5a7a946ec5950..fd4ae1b7fd361097e466735c709a95c90d480c1c 100644 (file)
--- a/NEWS.md
+++ b/NEWS.md
@@ -3,6 +3,10 @@ This file contains a summary of important user-visible changes.
 cvc5 1.0.1
 ==========
 
+**New Features**
+
+- Support for cross-compiling an ARM binary of cvc5 on x86 macOS.
+
 **Changes**
 
 - Removed support for non-standard `declare-funs`, `declare-consts`, and

diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake
index f91286a694e56fec9ae35545c53847c3047bb4e7..a357ca90966ee83378ec492695fbfa4d7147b740 100644 (file)
--- a/cmake/FindANTLR3.cmake
+++ b/cmake/FindANTLR3.cmake
@@ -103,6 +103,15 @@ if(NOT ANTLR3_FOUND_SYSTEM)
         unset(64bit)
     endif()
 
+  set(compilers "")
+  if (CMAKE_CROSSCOMPILING_MACOS)
+    # We set the CC and CXX flags as suggested in
+    # https://github.com/antlr/antlr3/blob/5c2a916a10139cdb5c7c8851ee592ed9c3b3d4ff/runtime/C/INSTALL#L133-L135.
+    set(compilers
+      "CC=${CMAKE_C_COMPILER} -arch ${CMAKE_OSX_ARCHITECTURES}"
+      "CXX=${CMAKE_CXX_COMPILER} -arch ${CMAKE_OSX_ARCHITECTURES}")
+  endif()
+
     # Download, build and install antlr3 runtime
     ExternalProject_Add(
         ANTLR3-EP-runtime
@@ -117,7 +126,9 @@ if(NOT ANTLR3_FOUND_SYSTEM)
         COMMAND ${CMAKE_COMMAND} -E copy
           <INSTALL_DIR>/share/config.sub
           <SOURCE_DIR>/config.sub
-        CONFIGURE_COMMAND <SOURCE_DIR>/configure
+        CONFIGURE_COMMAND
+          <SOURCE_DIR>/configure
+            ${compilers}
             --with-pic
             --disable-antlrdebug
             --disable-abiflags

diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake
index 5e94a7ee08bd64aeaab7db7bde00083c40d81124..09523eb39047a6803f14ed6d0d212a00727913f4 100644 (file)
--- a/cmake/FindCaDiCaL.cmake
+++ b/cmake/FindCaDiCaL.cmake
@@ -53,6 +53,10 @@ if(NOT CaDiCaL_FOUND_SYSTEM)
   # scripts unnecessarily fails for cross compilation thus we do the bare
   # minimum from the configure script here
   set(CXXFLAGS "-fPIC -O3 -DNDEBUG -DQUIET -std=c++11")
+  if(CMAKE_CROSSCOMPILING_MACOS)
+    set(CXXFLAGS "${CXXFLAGS} -arch ${CMAKE_OSX_ARCHITECTURES}")
+  endif()
+
   # check for getc_unlocked
   check_symbol_exists("getc_unlocked" "cstdio" HAVE_UNLOCKED_IO)
   if(NOT HAVE_UNLOCKED_IO)

diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake
index 481bd973a176d6eb76c9c04a16234eab6e0d9d00..f63cf7c2658e4626d89dc18be65b62a6ac9cb881 100644 (file)
--- a/cmake/FindGMP.cmake
+++ b/cmake/FindGMP.cmake
@@ -40,6 +40,16 @@ if(GMP_INCLUDE_DIR AND GMP_LIBRARIES)
   )
 
   check_system_version("GMP")
+
+  TRY_COMPILE(DOES_WORK "${DEPS_BASE}/try_compile/GMP-EP"
+    "${CMAKE_CURRENT_LIST_DIR}/deps-utils/gmp-test.cpp"
+    CMAKE_FLAGS -DCMAKE_TOOLCHAIN_FILE=${CMAKE_TOOLCHAIN_FILE}
+    LINK_LIBRARIES gmpxx gmp
+  )
+  if(NOT ${DOES_WORK})
+    message(VERBOSE "System version for ${name} does not work in the selected configuration. Maybe we are cross-compiling?")
+    set(GMP_FOUND_SYSTEM FALSE)
+  endif()
 endif()
 
 if(NOT GMP_FOUND_SYSTEM)
@@ -66,8 +76,16 @@ if(NOT GMP_FOUND_SYSTEM)
   endif()
 
   set(CONFIGURE_OPTS "")
-  if(CMAKE_CROSSCOMPILING)
-    set(CONFIGURE_OPTS --host=${TOOLCHAIN_PREFIX} --build=${CMAKE_HOST_SYSTEM_PROCESSOR})
+  set(CONFIGURE_ENV "")
+  if(CMAKE_CROSSCOMPILING OR CMAKE_CROSSCOMPILING_MACOS)
+    set(CONFIGURE_OPTS
+      --host=${TOOLCHAIN_PREFIX}
+      --build=${CMAKE_HOST_SYSTEM_PROCESSOR})
+  endif()
+  if (CMAKE_CROSSCOMPILING_MACOS)
+    set(CONFIGURE_ENV ${CMAKE_COMMAND} -E
+      env "CFLAGS=--target=${TOOLCHAIN_PREFIX}"
+      env "LDFLAGS=-arch ${CMAKE_OSX_ARCHITECTURES}")
   endif()
 
   # `CC_FOR_BUILD`, `--host`, and `--build` are passed to `configure` to ensure
@@ -80,7 +98,7 @@ if(NOT GMP_FOUND_SYSTEM)
     URL https://gmplib.org/download/gmp/gmp-${GMP_VERSION}.tar.bz2
     URL_HASH SHA1=2dcf34d4a432dbe6cce1475a835d20fe44f75822
     CONFIGURE_COMMAND
-      ${CMAKE_COMMAND} -E env CC_FOR_BUILD=cc
+      ${CONFIGURE_ENV}
         <SOURCE_DIR>/configure
           ${LINK_OPTS}
           --prefix=<INSTALL_DIR>

diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake
index cec586246d1af76bb9662bb38243c60d5e7b72c1..9e8423691221f34f1337dca23dae910b8ea5f18f 100644 (file)
--- a/cmake/Toolchain-aarch64.cmake
+++ b/cmake/Toolchain-aarch64.cmake
@@ -15,20 +15,34 @@
 # Use: cmake .. -DCMAKE_TOOLCHAIN_FILE=../cmake/Toolchain-aarch64.cmake
 ##
 
-SET(CMAKE_SYSTEM_NAME Linux)
-SET(CMAKE_SYSTEM_PROCESSOR aarch64)
+if(CMAKE_SYSTEM_NAME STREQUAL "Linux")
 
-set(TOOLCHAIN_PREFIX aarch64-linux-gnu)
+  set(CMAKE_SYSTEM_NAME Linux)
+  set(CMAKE_SYSTEM_PROCESSOR aarch64)
 
-SET(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc)
-SET(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++)
+  set(TOOLCHAIN_PREFIX aarch64-linux-gnu)
 
-# Set target environment path
-SET(CMAKE_FIND_ROOT_PATH /usr/${TOOLCHAIN_PREFIX})
+  set(CMAKE_C_COMPILER ${TOOLCHAIN_PREFIX}-gcc)
+  set(CMAKE_CXX_COMPILER ${TOOLCHAIN_PREFIX}-g++)
 
-# 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 ONLY)
-set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
+  # 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 ONLY)
+  set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY)
+
+elseif(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+
+  set(CMAKE_SYSTEM_NAME Darwin)
+  set(CMAKE_SYSTEM_PROCESSOR arm64)
+
+  set(TOOLCHAIN_PREFIX arm64-apple-darwin)
+
+  set(CMAKE_CROSSCOMPILING_MACOS TRUE)
+  set(CMAKE_OSX_ARCHITECTURES arm64 CACHE INTERNAL "")
+
+endif()

diff --git a/cmake/deps-utils/gmp-test.cpp b/cmake/deps-utils/gmp-test.cpp
new file mode 100644 (file)
index 0000000..88d1ca6
--- /dev/null
+++ b/cmake/deps-utils/gmp-test.cpp
@@ -0,0 +1,7 @@
+#include <gmpxx.h>
+
+int main()
+{
+  mpz_class i = 0;
+  return 0;
+}