Add aarch64 (Arm 64-bit) CI job

.github/workflows/pull-request-checks.yaml

@@ -451,6 +451,60 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
 
+  # This job takes approximately 17 to 41 minutes
+  check-ubuntu-24_04-arm-cmake-gcc:
+    runs-on: ubuntu-24.04-arm
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5
+          rm cvc5-Linux-arm64-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}
+            ${{ runner.os }}-24.04-Arm-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
+      - name: Check that doc task works
+        run: ninja -C build doc
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j${{env.linux-vcpus}}
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Check if package building works
+        run: |
+          cd build
+          ninja package
+          ls *.deb
+      - name: Run tests
+        run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
+
   # This job takes approximately 14 to 60 minutes
   check-ubuntu-22_04-cmake-gcc-32bit:
     runs-on: ubuntu-22.04

.github/workflows/release-packages.yaml

@@ -77,6 +77,77 @@ jobs:
           SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }}
           SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 package built and uploaded successfully' || 'Ubuntu 24.04 package build failed' }}"
 
+  ubuntu-24_04-arm-package:
+    runs-on: ubuntu-24.04-arm
+    env:
+      GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip
+          unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5
+          rm cvc5-Linux-arm64-static.zip
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v4
+        with:
+          save-always: true
+          path: .ccache
+          key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG
+          restore-keys:
+            ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}
+            ${{ runner.os }}-24.04-Arm-Release
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure CMake
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical"
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build using Ninja
+        run: ninja -C build -j4
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run CTest
+        run: cd build; ctest . -V -L CORE -C Release -j4
+      - name: Create packages
+        id: create_packages
+        run: |
+          cd build
+          ninja package
+          deb_package_name="$(ls *.deb)"
+          echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT
+          echo "deb_package_name=ubuntu-24.04-arm64-$deb_package_name" >> $GITHUB_OUTPUT
+      - name: Get release info
+        id: get_release_info
+        uses: bruceadams/[email protected]
+      - name: Upload binary packages
+        uses: actions/upload-release-asset@v1
+        with:
+          upload_url: ${{ steps.get_release_info.outputs.upload_url }}
+          asset_path: ${{ steps.create_packages.outputs.deb_package }}
+          asset_name: ${{ steps.create_packages.outputs.deb_package_name }}
+          asset_content_type: application/x-deb
+      - name: Slack notification of CI status
+        uses: rtCamp/action-slack-notify@v2
+        if: success() || failure()
+        env:
+          SLACK_CHANNEL: aws-cbmc
+          SLACK_COLOR: ${{ job.status }}
+          SLACK_USERNAME: Github Actions CI bot
+          SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }}
+          SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 Arm package built and uploaded successfully' || 'Ubuntu 24.04 Arm package build failed' }}"
+
   ubuntu-22_04-package:
     runs-on: ubuntu-22.04
     env:

regression/cbmc-concurrency/memory_barrier2/msvc.desc

@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --mm tso --winx64
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-concurrency/memory_barrier2/msvc.c → regression/cbmc-concurrency/memory_barrier2/msvc.i

@@ -1,3 +1,8 @@
+void __asm_mfence(void)
+{
+  __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence");
+}
+
 volatile int turn;
 int x;
 volatile int flag1 = 0, flag2 = 0;

regression/cbmc-library/__asm_fstcw-01/msvc.desc

@@ -1,5 +1,5 @@
 CORE
-msvc.c
+msvc.i
 --pointer-check --bounds-check --winx64
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-library/__asm_fstcw-01/msvc.c → regression/cbmc-library/__asm_fstcw-01/msvc.i

@@ -1,9 +1,15 @@
+extern int __CPROVER_rounding_mode;
+
+void __asm_fstcw(void *dest)
+{
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
+}
+
 int main()
 {
   unsigned short cw;
   __asm { fstcw cw; }
   __CPROVER_assert((cw & 0xc00) == 0, "default rounding mode");
-  // fesetround(FE_UPWARD);
   __CPROVER_rounding_mode = 2;
   __asm { fstcw cw; }
   __CPROVER_assert((cw & 0xc00) == 0x800, "round upwards");

regression/cbmc/Quantifiers-type2/main.c

@@ -5,7 +5,7 @@ int main()
 
   // clang-format off
   // clang-format would rewrite the "==>" as "== >"
-  __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { signed char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
   __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
   // clang-format on
 

regression/cbmc/Quantifiers-type2/unsigned-char.c

@@ -0,0 +1,16 @@
+int main()
+{
+  int b[2];
+  int c[2];
+
+  // clang-format off
+  // clang-format would rewrite the "==>" as "== >"
+  __CPROVER_assume( __CPROVER_forall { unsigned char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
+  __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
+  // clang-format on
+
+  assert(b[0] == 10 && b[1] == 10);
+  assert(c[0] == 10 && c[1] == 10);
+
+  return 0;
+}

regression/cbmc/Quantifiers-type2/unsigned-char.desc

@@ -0,0 +1,11 @@
+CORE no-new-smt
+unsigned-char.c
+
+^\*\* Results:$
+^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
+^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/ansi-c/ansi_c_internal_additions.cpp

@@ -286,6 +286,23 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       code+="typedef signed __int128 __int128_t;\n"
             "typedef unsigned __int128 __uint128_t;\n";
     }
+
+    if(
+      config.ansi_c.arch == "arm64" &&
+      config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS)
+    {
+      code += "typedef struct __va_list {";
+      code += "void *__stack;";
+      code += "void *__gr_top;";
+      code += "void *__vr_top;";
+      code += "int   __gr_offs;";
+      code += "int   __vr_offs;";
+      code += " } __builtin_va_list;\n";
+    }
+    else
+    {
+      code += "typedef void ** __builtin_va_list;\n";
+    }
   }
 
   // this is Visual C/C++ only

src/ansi-c/c_typecheck_expr.cpp

@@ -547,12 +547,20 @@
   typet arg_type=expr.type();
   typecheck_type(arg_type);
 
+  const symbolt *symbol_ptr;
+  if(lookup("__builtin_va_list", symbol_ptr))
+  {
+    error().source_location = expr.source_location();
+    error() << "failed to find typedef name __builtin_va_list" << eom;
+    throw 0;
+  }
+
   const code_typet new_type(
-    {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
+    {code_typet::parametert(symbol_ptr->type)}, std::move(arg_type));
 
   exprt arg = to_unary_expr(expr).op();
 
-  implicit_typecast(arg, pointer_type(void_type()));
+  implicit_typecast(arg, new_type.parameters().front().type());
 
   symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
   function.add_source_location() = expr.source_location();

src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h

@@ -2,14 +2,14 @@
 // stdarg
 void* __builtin_apply_args();
 void* __builtin_apply(void (*)(), void*, __CPROVER_size_t);
-void __builtin_ms_va_end(void *ap);
-void __builtin_ms_va_start(void *ap, ...);
+void __builtin_ms_va_end(__builtin_ms_va_list ap);
+void __builtin_ms_va_start(__builtin_ms_va_list ap, ...);
 void* __builtin_next_arg();
 int __builtin_va_arg_pack();
 int __builtin_va_arg_pack_len();
 void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src);
-void __builtin_va_end(void *ap);
-void __builtin_va_start(void *ap, ...);
+void __builtin_va_end(__builtin_va_list ap);
+void __builtin_va_start(__builtin_va_list ap, ...);
 
 // stdlib
 void __builtin__Exit(int);

src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

@@ -1,5 +1,4 @@
 // clang-format off
-typedef void ** __builtin_va_list;
 typedef void ** __builtin_ms_va_list;
 
 typedef int    __gcc_m64   __attribute__ ((__vector_size__ (8), __may_alias__));
@@ -45,4 +44,13 @@ enum __gcc_atomic_memmodels {
 };
 
 typedef unsigned char __tile __attribute__ ((__vector_size__ (1024)));
+
+// GCC and Clang use the following on ARM:
+typedef float __Float32x4_t __attribute__ ((__vector_size__ (16)));
+typedef double __Float64x2_t __attribute__ ((__vector_size__ (16)));
+// The following ARM (scalable vector) extensions define vectors the size of
+// which is not known at compile time.
+typedef float *__SVFloat32_t;
+typedef double *__SVFloat64_t;
+typedef __CPROVER_bool *__SVBool_t;
 // clang-format on

src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -593,8 +593,20 @@
   copy(array_op_statement, OTHER, dest);
 }
 
-exprt make_va_list(const exprt &expr)
+static exprt make_va_list(const exprt &expr, const namespacet &ns)
 {
+  if(
+    auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(expr.type()))
+  {
+    // aarch64 ABI mandates that va_list has struct type with member names as
+    // specified
+    const auto &components = ns.follow_tag(*struct_tag_type).components();
+    DATA_INVARIANT(
+      components.size() == 5,
+      "va_list struct type expected to have 5 components");
+    return member_exprt{expr, components.front()};
+  }
+
   exprt result = skip_typecast(expr);
 
   // if it's an address of an lvalue, we take that
@@ -1296,14 +1308,15 @@
       throw 0;
     }
 
-    exprt list_arg = make_va_list(arguments[0]);
+    exprt list_arg = make_va_list(arguments[0], ns);
+    const bool va_list_is_void_ptr =
+      list_arg.type().id() == ID_pointer &&
+      to_pointer_type(list_arg.type()).base_type().id() == ID_empty;
 
     if(lhs.is_not_nil())
     {
       exprt list_arg_cast = list_arg;
-      if(
-        list_arg.type().id() == ID_pointer &&
-        to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
+      if(va_list_is_void_ptr)
       {
         list_arg_cast =
           typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))};
@@ -1317,8 +1330,14 @@
         goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
-    code_assignt assign{
-      list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
+    exprt list_arg_ptr_arithmetic = typecast_exprt::conditional_cast(
+      plus_exprt{
+        (va_list_is_void_ptr
+           ? typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))}
+           : list_arg),
+        from_integer(1, pointer_diff_type())},
+      list_arg.type());
+    code_assignt assign{list_arg, std::move(list_arg_ptr_arithmetic)};
     assign.rhs().set(
       ID_C_va_arg_type, to_code_type(function.type()).return_type());
     dest.add(goto_programt::make_assignment(
@@ -1333,7 +1352,7 @@
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
     const typecast_exprt src_expr(arguments[1], dest_expr.type());
 
     if(!is_assignable(dest_expr))
@@ -1357,7 +1376,7 @@
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
 
     if(!is_assignable(dest_expr))
     {
@@ -1392,7 +1411,7 @@
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
 
     if(!is_assignable(dest_expr))
     {