From 7df8cbd89ae432c8c30dfa27fcb10f65b7763cf2 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 12 Nov 2024 07:18:20 -0500 Subject: [PATCH] CVC4: Add patches to ease building on AArch64 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. --- .github/ci.sh | 3 ++ patches/cvc4-antlr-check-aarch64.patch | 46 +++++++++++++++++-- .../cvc4-antlr-pointer-to-integer-cast.patch | 22 +++++++++ 3 files changed, 67 insertions(+), 4 deletions(-) create mode 100644 patches/cvc4-antlr-pointer-to-integer-cast.patch diff --git a/.github/ci.sh b/.github/ci.sh index 83498cb..5f71155 100755 --- a/.github/ci.sh +++ b/.github/ci.sh @@ -83,7 +83,10 @@ build_boolector() { build_cvc4() { pushd repos/CVC4-archived + # Make the get-antlr script work on both x86-64 and AArch64 patch -p1 -i $PATCHES/cvc4-antlr-check-aarch64.patch + # Fix a pointer-to-integer cast in ANTLR + patch -p1 -i $PATCHES/cvc4-antlr-pointer-to-integer-cast.patch # Add missing #include statements that macos-14's version of Clang++ requires. patch -p1 -i $PATCHES/cvc4-fix-missing-includes.patch ./contrib/get-antlr-3.4 diff --git a/patches/cvc4-antlr-check-aarch64.patch b/patches/cvc4-antlr-check-aarch64.patch index 82151a8..6c60a18 100644 --- a/patches/cvc4-antlr-check-aarch64.patch +++ b/patches/cvc4-antlr-check-aarch64.patch @@ -1,9 +1,47 @@ diff --git a/contrib/get-antlr-3.4 b/contrib/get-antlr-3.4 -index 45dc86583..ea69b4b7f 100755 +index 45dc86583..685623f19 100755 --- a/contrib/get-antlr-3.4 +++ b/contrib/get-antlr-3.4 -@@ -47,7 +47,7 @@ cd "$ANTLR_HOME_DIR/libantlr3c-3.4" +@@ -26,6 +26,22 @@ if [ -z "${MACHINE_TYPE}" ]; then + MACHINE_TYPE=$(${CONFIG_GUESS_SCRIPT} | sed 's,-.*,,') + fi ++# In addition to config.guess, we also download a more recent version of ++# config.sub. We aren't going to use it directly in this script, but we will ++# copy it into our ANTLR checkout later. ++CONFIG_SUB_SCRIPT="$ANTLR_HOME_DIR/config.sub" ++if ! [ -e "${CONFIG_SUB_SCRIPT}" ]; then ++ mkdir -p "$ANTLR_HOME_DIR" ++ # Attempt to download once ++ webget 'http://git.savannah.gnu.org/gitweb/?p=config.git;a=blob_plain;f=config.sub;hb=HEAD' $CONFIG_SUB_SCRIPT ++ if [ -e "$CONFIG_SUB_SCRIPT" ]; then ++ chmod +x "$CONFIG_SUB_SCRIPT" ++ else ++ echo "$(basename $0): I need an up-to-date version of config/config.sub." >&2 ++ exit 1 ++ fi ++fi ++ + mkdir -p "$INSTALL_DIR/share/java" + webget \ + "https://www.antlr3.org/download/antlr-3.4-complete.jar" \ +@@ -43,11 +59,22 @@ 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" ++# Use more up-to-date config.guess and config.sub scripts that are aware of ++# AArch64 Linux and Darwin. ++cp "${CONFIG_GUESS_SCRIPT}" "$ANTLR_HOME_DIR/libantlr3c-3.4/config.guess" ++cp "${CONFIG_SUB_SCRIPT}" "$ANTLR_HOME_DIR/libantlr3c-3.4/config.sub" + cd "$ANTLR_HOME_DIR/libantlr3c-3.4" + ++# By default, ANTLR's configure script will attempt to pass x86-specific flags ++# such as -m64, which do not exist on other architectures (e.g., ARM). We can ++# override this default by passing --disable-abiflags to the configure script. ++if [[ "${MACHINE_TYPE}" != 'x86_64' ]]; then ++ ANTLR_CONFIGURE_ARGS="--disable-abiflags ${ANTLR_CONFIGURE_ARGS}" ++fi ++ # Make antlr3debughandlers.c empty to avoid unreferenced symbols rm -rf src/antlr3debughandlers.c && touch src/antlr3debughandlers.c -if [ "${MACHINE_TYPE}" == 'x86_64' ]; then @@ -11,7 +49,7 @@ index 45dc86583..ea69b4b7f 100755 # 64-bit stuff here ./configure --enable-64bit --disable-antlrdebug --prefix="$INSTALL_DIR" $ANTLR_CONFIGURE_ARGS $BUILD_TYPE else -@@ -67,7 +67,7 @@ fi +@@ -67,7 +94,7 @@ fi mv "$INSTALL_LIB_DIR/libantlr3c.a" "$INSTALL_LIB_DIR/libantlr3c-static.a" make clean @@ -20,7 +58,7 @@ index 45dc86583..ea69b4b7f 100755 # 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" +@@ -84,7 +111,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" diff --git a/patches/cvc4-antlr-pointer-to-integer-cast.patch b/patches/cvc4-antlr-pointer-to-integer-cast.patch new file mode 100644 index 0000000..6ddd59e --- /dev/null +++ b/patches/cvc4-antlr-pointer-to-integer-cast.patch @@ -0,0 +1,22 @@ +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 ++#include + #include + #include + #include +@@ -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); + } + } +