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,3 +1,10 @@
+extern int __CPROVER_rounding_mode;
+
+void __asm_fstcw(void *dest)
+{
+  *(unsigned short *)dest = __CPROVER_rounding_mode << 10;
+}
+
 int main()
 {
   unsigned short cw;

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

regression/cbmc/va_list2/main.c

@@ -1,4 +1,4 @@
-#ifdef __GNUC__
+#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
 
 #  include <assert.h>
 

regression/cbmc/va_list4/main.c

@@ -1,4 +1,4 @@
-#ifdef __GNUC__
+#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
 
 struct __va_list_tag;
 typedef struct __va_list_tag __va_list_tag;

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -77,9 +77,13 @@ bool is_ptr_comparison(const exprt &expr)
          (expr.operands()[1].type().id() == ID_pointer);
 }
 
-static bool is_access_expr(const irep_idt &id)
+static bool is_access_expr(const exprt &expr)
 {
-  return id == ID_member || id == ID_index || id == ID_dereference;
+  if(auto tc = expr_try_dynamic_cast<typecast_exprt>(expr))
+    return is_access_expr(tc->op());
+
+  return expr.id() == ID_member || expr.id() == ID_index ||
+         expr.id() == ID_dereference;
 }
 
 static bool is_object_creation(const irep_idt &id)
@@ -107,7 +111,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     return resolve_symbol(simplified_expr, ns);
 
   if(
-    is_access_expr(simplified_id) || is_ptr_diff(simplified_expr) ||
+    is_access_expr(simplified_expr) || is_ptr_diff(simplified_expr) ||
     is_ptr_comparison(simplified_expr))
   {
     auto const operands = eval_operands(simplified_expr, *this, ns);
@@ -168,7 +172,9 @@ bool abstract_environmentt::assign(
   std::stack<exprt> stactions; // I'm not a continuation, honest guv'
   while(s.id() != ID_symbol)
   {
-    if(s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference)
+    if(
+      s.id() == ID_index || s.id() == ID_member || s.id() == ID_dereference ||
+      s.id() == ID_typecast)
     {
       stactions.push(s);
       s = s.operands()[0];
@@ -248,8 +254,8 @@ abstract_object_pointert abstract_environmentt::write(
   const irep_idt &stack_head_id = next_expr.id();
   INVARIANT(
     stack_head_id == ID_index || stack_head_id == ID_member ||
-      stack_head_id == ID_dereference,
-    "Write stack expressions must be index, member, or dereference");
+      stack_head_id == ID_dereference || stack_head_id == ID_typecast,
+    "Write stack expressions must be index, member, dereference, or typecast");
 
   return lhs->write(*this, ns, remaining_stack, next_expr, rhs, merge_write);
 }

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

@@ -544,15 +544,23 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   // is the type, which will need to be fixed and checked.
   // The type is given by the parser as type of the expression.
 
-  typet arg_type=expr.type();
-  typecheck_type(arg_type);
-
-  const code_typet new_type(
-    {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
-
   exprt arg = to_unary_expr(expr).op();
+  auto typedef_id = arg.type().get(ID_C_typedef);
+  if(
+    typedef_id != "__builtin_va_list" && typedef_id != "__builtin_ms_va_list" &&
+    typedef_id != "va_list")
+  {
+    error().source_location = expr.source_location();
+    error() << "argument of type '" << to_string(arg.type())
+            << "' not permitted for va_arg" << eom;
+    throw 0;
+  }
+
+  typet arg_type = expr.type();
+  typecheck_type(arg_type);
 
-  implicit_typecast(arg, pointer_type(void_type()));
+  const code_typet new_type{
+    {code_typet::parametert{arg.type()}}, std::move(arg_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