Build and distribute arm64 binaries on/for Apple silicon

[samcowger]

The solvers we currently distribute for macOS are for Intel silicon. It would be nice to distribute binaries suitable for Apple silicon as well.

I spent some time using .github/ci.sh to try to build each of these solvers on my M2 MacBook Pro. I eventually succeeded in building the following solvers:

• abc
• boolector
• cvc4
• cvc5
• yices
• yices-smt2
• yices_sat
• yices_sat_new
• yices_smt
• yices_smt2
• yices_smt2_mt
• yices_smtcomp
• z3-4.8.14
• z3-4.8.8

I believe this is the entire suite of solvers that ci.sh knows how to build. I encountered several hurdles in this process. I'll try to document them here, both for the benefit of whomever might want to do this in the future and in case anyone can shed light on an easier way to accomplish things than what I ended up doing.

Building this required installing several system-level packages. I have no idea whether or not this list is exhaustive, but it probably becomes exhaustive in concert with the CI workflow spec:

• autoconf
• automake
• cmake
• flex
• ninja
• python >=3.6 && <3.11

Additionally, a couple of Python packages were required. I think this list is exhaustive:

• pyparsing
• toml

I believe the Python packages were only required for cvc5, but I can't vouch for that with certainty. I do not know what solvers required what system packages.

A few more findings:

• Setting RUNNER_OS to "macOS" was necessary to run ci.sh locally.

• Off the shelf, the cvc4 build process guesses that, because my machine architecture is not precisely x86_64, it must be 32-bit, and tries to compile ANTLR with -m32. This gives the error .../what4-solvers/repos/CVC4-archived/src/parser/antlr_line_buffered_input.cpp:291:10: error: cast from pointer to smaller type 'ANTLR3_MARKER' (aka 'int') loses information. My fix for this was to change the conditions in the script repos/CVC4-archived/contrib/get-antlr-3.4 to check MACHINE_TYPE against both x86_64 and aarch64:

  
  diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
  index 45dc86583..ea69b4b7f 100755
  --- a/contrib/get-antlr-3.4
  +++ b/contrib/get-antlr-3.4
  @@ -47,7 +47,7 @@ cd "$ANTLR_HOME_DIR/libantlr3c-3.4"
  
  # Make antlr3debughandlers.c empty to avoid unreferenced symbols
  rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c
  -if [ "${MACHINE_TYPE}" == 'x86_64' ]; then
  +if [[ "${MACHINE_TYPE}" == 'x86_64' || "${MACHINE_TYPE}" == 'aarch64' ]]; then
  # 64-bit stuff here
  ./configure --enable-64bit --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
  else
  @@ -67,7 +67,7 @@ fi
  mv "$INSTALL_LIB_DIR/libantlr3c.a" "$INSTALL_LIB_DIR/libantlr3c-static.a"
  make clean

-if [ "${MACHINE_TYPE}" == 'x86_64' ]; then +if [[ "${MACHINE_TYPE}" == 'x86_64' || "${MACHINE_TYPE}" == 'aarch64' ]]; then

64-bit stuff here

./configure --enable-64bit --with-pic --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE else @@ -84,7 +84,7 @@ 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" > "$INSTAL L_LIB_DIR/libantlr3c.la" rm "$INSTALL_LIB_DIR/libantlr3c.la.orig"

-if [ "${MACHINE_TYPE}" == 'x86_64' ]; then +if [[ "${MACHINE_TYPE}" == 'x86_64' || "${MACHINE_TYPE}" == 'aarch64' ]]; then

64-bit stuff here

echo ============== WARNING ==================== echo The script guessed that this machine is 64 bit.

- Setting `FLEX_INCLUDE_DIRS` was necessary for `cvc5` (for me, the appropriate value was `/opt/homebrew/opt/flex/include`).
- Setting `pythonLocation` was necessary for `cvc5`. It must be the directory in which `python` exists, and not the path of the executable itself.
- Building `yices` entails compiling `libpoly`, which has `Werror` set. Naturally, compiling `libpoly` produces warnings. I needed to go into `repos/libpoly/src/CMakeLists.txt` and delete `Werror` from its flag settings. (I thought I might be able to override this with a `*FLAGS` environment variable, but `CMakeLists` puts `Werror` after the flags it sources from the environment, so `Werror` takes precedence.)
```diff
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6205689..1da534f 100755
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -63,7 +63,7 @@ set(polyxx_SOURCES
 )

 # Add warnings as errors for good practice
-set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Werror -Wextra -std=gnu99")
+set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -Wextra -std=gnu99")
 set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Werror -Wextra -std=c++11")

 include_directories(${GMP_INCLUDE_DIR})

• Failed cvc4 builds leave build artifacts in the CVC4 repo (a folder named deps) that prevent subsequent build attempts. If we want to let users run ci.sh to build things for themselves, it might be nice to delete deps automatically.

• yices builds create a directory tree rooted at install-root, the presence of which causes ci.sh to fail on subsequent yices builds. We might consider using mkdir -p in ci.sh:

  
  @@ -131,9 +135,8 @@ build_yices() {
   export CONFIGURE_FLAGS="--prefix=$TOP/install-root"
  fi

• mkdir install-root

• mkdir install-root/include

• mkdir install-root/lib

• mkdir -p install-root/include

• mkdir -p install-root/lib

[RyanGlScott]

Thanks for looking into this, @samcowger!

My fix for this was to change the conditions in the script repos/CVC4-archived/contrib/get-antlr-3.4 to check MACHINE_TYPE against both x86_64 and aarch64:

This sounds like a reasonable fix. CVC4 is no longer actively maintained, so if there is a patch that needs to be applied, we will have to apply it ourselves. We already have a list of such patches here.

Setting FLEX_INCLUDE_DIRS was necessary for cvc5 (for me, the appropriate value was /opt/homebrew/opt/flex/include).

I'm surprised that this step is necessary, given that CVC5 claims to support Apple Silicon. (See this commit.) It might be worth opening an issue upstream with CVC5 about this.

Building yices entails compiling libpoly, which has Werror set. Naturally, compiling libpoly produces warnings. I needed to go into repos/libpoly/src/CMakeLists.txt and delete Werror from its flag settings.

What sort of warnings did you see? Admittedly, it's been a while since we've updated the yices submodule, so I wonder if this issue persists with the latest version.

Failed cvc4 builds leave build artifacts in the CVC4 repo (a folder named deps) that prevent subsequent build attempts. If we want to let users run ci.sh to build things for themselves, it might be nice to delete deps automatically.

That is indeed a bit unfortunate. I'm not sure off the top of my head when the best time to do this deps deletion step would be, however.

We might consider using mkdir -p in ci.sh

Yes, this seems like a much more reasonable approach. Would you like to submit a patch to improve this?

More generally, it would be nicer to have a user-oriented script that sets all of the necessary environment variables for you (RUNNER_OS, pythonLocation, etc.). I haven't gotten around to doing this yet, as this repo has been CI-driven for nearly all of its existence.

[RyanGlScott]

Related to this discussion, the next step to making it possible to actually distribute M1 macOS binaries is to change our naming conventions a bit. Currently, we have things like macos-12-bin, but this gives no indication of whether this is for x86_64 or aarch64 Macs. We should probably name these macos-12-$(uname -m)-bin instead. I'll submit a patch for this.

[samcowger]

My fix for this was to change the conditions in the script repos/CVC4-archived/contrib/get-antlr-3.4 to check MACHINE_TYPE against both x86_64 and aarch64:

This sounds like a reasonable fix. CVC4 is no longer actively maintained, so if there is a patch that needs to be applied, we will have to apply it ourselves. We already have a list of such patches here.

Ah, neat - I think I can manage to contribute a patch like this.

Setting FLEX_INCLUDE_DIRS was necessary for cvc5 (for me, the appropriate value was /opt/homebrew/opt/flex/include).

I'm surprised that this step is necessary, given that CVC5 claims to support Apple Silicon. (See this commit.) It might be worth opening an issue upstream with CVC5 about this.

I will double-check that I haven't done anything screwy here - it's possible that I changed several things at once (some subset of brew installing flex, updating {LD,CPP}FLAGS, and/or setting that variable).

Building yices entails compiling libpoly, which has Werror set. Naturally, compiling libpoly produces warnings. I needed to go into repos/libpoly/src/CMakeLists.txt and delete Werror from its flag settings.

What sort of warnings did you see? Admittedly, it's been a while since we've updated the yices submodule, so I wonder if this issue persists with the latest version.

+ ninja -j4 static_poly
[23/37] Building C object src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o
FAILED: src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o 
/Library/Developer/CommandLineTools/usr/bin/cc -DHAVE_OPEN_MEMSTREAM -I/opt/homebrew/include -I/Users/sam/projects/do1/what4-solvers/install-root/include -I/Users/sam/projects/do1/what4-solvers/repos/libpoly/src -I/Users/sam/projects/do1/what4-solvers/repos/libpoly/include -Wall -Werror -Wextra -std=gnu99 -O3 -DNDEBUG -arch arm64 -isysroot /Library/Developer/CommandLineTools/SDKs/MacOSX13.3.sdk -MD -MT src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o -MF src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o.d -o src/CMakeFiles/static_poly.dir/upolynomial/factorization.c.o -c /Users/sam/projects/do1/what4-solvers/repos/libpoly/src/upolynomial/factorization.c
/Users/sam/projects/do1/what4-solvers/repos/libpoly/src/upolynomial/factorization.c:1269:7: error: variable 'enabled_count' set but not used [-Werror,-Wunused-but-set-variable]
  int enabled_count = 0;
      ^
1 error generated.
[26/37] Building C object src/CMakeFiles/static_poly.dir/polynomial/coefficient.c.o
ninja: build stopped: subcommand failed.

Failed cvc4 builds leave build artifacts in the CVC4 repo (a folder named deps) that prevent subsequent build attempts. If we want to let users run ci.sh to build things for themselves, it might be nice to delete deps automatically.

That is indeed a bit unfortunate. I'm not sure off the top of my head when the best time to do this deps deletion step would be, however.

I guess I'm not sure either - some kind of wholesale try-except block seems most appropriate, but I don't know the bash idioms for that. Seems like the sort of thing to address in a user-facing script, as you mention below.

We might consider using mkdir -p in ci.sh

Yes, this seems like a much more reasonable approach. Would you like to submit a patch to improve this?

Gladly.

More generally, it would be nicer to have a user-oriented script that sets all of the necessary environment variables for you (RUNNER_OS, pythonLocation, etc.). I haven't gotten around to doing this yet, as this repo has been CI-driven for nearly all of its existence.

Yeah, I agree. I would think two scripts in this paradigm could coexist/codepend nicely.

[RyanGlScott]

Regarding the libpoly warning, it turns out that this was noticed separately in cvc5 (which also depends on libpoly) in https://github.com/cvc5/cvc5/issues/9265. They worked around the issue by applying a patch on top of libpoly—see https://github.com/cvc5/cvc5/pull/9266. While this fix arguably should go into libpoly itself, we could also apply this workaround for the yices build if need be.

[RyanGlScott]

Some updates:

• @samcowger has locally built AArch64 versions of all the SMT solvers that we use, which is available for download here. Until we start building these via the CI, this will do.

  Speaking of which...

• GitHub Actions now offers M1 macOS runners (which use AArch64), but they are only available as larger runners, which are more expensive. See this blog post. Personally, I'm not in a huge hurry to build these via CI, so perhaps it is worth waiting until GitHub Actions inevitably offers an ordinary tier of AArch64 macOS runners.