Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

ARM64 Linux builds #50

Open
RyanGlScott opened this issue Sep 3, 2024 · 2 comments
Open

ARM64 Linux builds #50

RyanGlScott opened this issue Sep 3, 2024 · 2 comments
Labels
enhancement New feature or request Linux Issues relating to Linux support

Comments

@RyanGlScott
Copy link
Contributor

Currently, we offer X64 Linux builds of the solvers, but not ARM64 builds. This is primarily limited by the fact that GitHub Actions only offers X64 Ubuntu small runners at the time of writing this. There is a possibility that this may expand to ARM64 in the future, as GitHub now offers ARM64 Ubuntu large runners (which are more expensive than the default, small runners).
@RyanGlScott RyanGlScott added the enhancement New feature or request label Sep 3, 2024
@RyanGlScott RyanGlScott added the Linux Issues relating to Linux support label Nov 8, 2024
@RyanGlScott RyanGlScott mentioned this issue Nov 11, 2024
Closed
@RyanGlScott
Copy link
Contributor Author

In the meantime, I have built the solvers locally on AArch64 Linux (or rather, on an linux/arm64 ubuntu:22.04 Docker image) to see what issues surfaced. Happily, most of the solvers built without issue, with the notable of exception of CVC4. I had to patch CVC4 in the following ways in order to make it compile:

config.guess

I needed to use a more up-to-date config.guess script that is aware of aarch64-linux, which requires this patch: #53 (comment).

--disable-abiflags

I also needed to teach the get-antlr-3.4 script not to pass -m64 to gcc, as this flag does not work on AArch64. I hacked around this issue by changing the patches/cvc4-antlr-check-aarch64.patch file to pass --disable-abiflags to configure:

diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4
index 45dc86583..0018474e7 100755
--- a/contrib/get-antlr-3.4
+++ b/contrib/get-antlr-3.4
@@ -47,12 +47,12 @@ 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
+  ./configure --enable-64bit --disable-abiflags --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 else
   # 32-bit stuff here
-  ./configure --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
+  ./configure --disable-abiflags --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 fi
 
 cp Makefile Makefile.orig
@@ -67,12 +67,12 @@ 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
+  ./configure --enable-64bit --with-pic --disable-abiflags --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
+  ./configure --with-pic --disable-abiflags --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE
 fi
 
 cp Makefile Makefile.orig
@@ -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" > "$INSTALL_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.

This patch is still not quite right, as we should only pass --disable-abiflags on non-x86-64 architectures. But it's a start.

Pointer-to-integer casts

There is part of the CVC4 source code that implicitly casts a pointer to an integer. While gcc simply warns about this on x86-64, this turns into an outright error on AArch64. I worked around the issue by first casting the pointer to an intptr_t:

diff --git a/src/parser/antlr_line_buffered_input.cpp b/src/parser/antlr_line_buffered_input.cpp
index cdf553880..ba0214dd4 100644
--- a/src/parser/antlr_line_buffered_input.cpp
+++ b/src/parser/antlr_line_buffered_input.cpp
@@ -31,6 +31,7 @@
 #include "parser/antlr_line_buffered_input.h"
 
 #include <antlr3.h>
+#include <stdint.h>
 #include <iostream>
 #include <string>
 #include <cassert>
@@ -288,7 +289,7 @@ static void bufferedInputSeek(pANTLR3_INT_STREAM is, ANTLR3_MARKER seekPoint) {
               ->line_buffer->isPtrBefore(
                   (uint8_t*)seekPoint, input->line, input->charPositionInLine));
 
-  while ((ANTLR3_MARKER)(input->nextChar) != seekPoint) {
+  while ((ANTLR3_MARKER)((intptr_t)input->nextChar) != seekPoint) {
     is->consume(is);
   }
 }

@sauclovian-g
Copy link

LGTM; might as well go ahead and push the patches...

RyanGlScott added a commit that referenced this issue Nov 12, 2024
@RyanGlScott
CVC4: Add patches to ease building on AArch64
6929941 
This adds three patches from #50, which will make it easier to build CVC4 on
AArch64 (and especially AArch64 Linux) in the future:

* `cvc4-antlr-update-config-guess.patch`: This updates the very old
  `config.guess` script that ANTLR uses (dating back to 2009) to a more recent
  one that is aware of AArch64 Linux and Darwin. Doing so fixes a spurious
  warning about building for 32-bit on AArch64 Darwin (thereby fixing #53) and
  unbreaks the AArch64 Linux build when combined with the next patch...

* `cvc4-antlr-check-aarch64.patch`: By default, ANTLR's `configure` script will
  pass x86-specific flags such as `-m64`, which aren't supported by `gcc` on
  other architectures (e.g., AArch64). We can prevent this by passing
  `--disable-abiflags` to `configure` on these architectures.

* `cvc4-antlr-pointer-to-integer-cast.patch`: Fix an implicit
  pointer-to-integer cast that causes x86-64 `gcc` to warn, but causes AArch64
  `gcc` to fail with a full-blown error.
@RyanGlScott RyanGlScott mentioned this issue Nov 12, 2024
Merged
RyanGlScott added a commit that referenced this issue Nov 12, 2024
@RyanGlScott
CVC4: Add patches to ease building on AArch64
7df8cbd 
This adds the patches from #50, which will make it easier to build CVC4 on
AArch64 (and especially AArch64 Linux) in the future:

* `cvc4-antlr-check-aarch64.patch` This updates the very old
  `config.guess` and `config.sub` scripts that ANTLR uses (dating back to 2009)
  to more recent ones that are aware of AArch64 Linux and Darwin. Doing so
  fixes a spurious warning about building for 32-bit on AArch64 Darwin (thereby
  fixing #53) and unbreaks the AArch64 Linux build.

  Also, ANTLR's `configure` script will pass x86-specific flags such as `-m64`
  by default, which aren't supported by `gcc` on other architectures (e.g.,
  AArch64). We can prevent this by passing `--disable-abiflags` to `configure`
  on these architectures.

* `cvc4-antlr-pointer-to-integer-cast.patch`: Fix an implicit
  pointer-to-integer cast that causes x86-64 `gcc` to warn, but causes AArch64
  `gcc` to fail with a full-blown error.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request Linux Issues relating to Linux support
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@RyanGlScott @sauclovian-g