Skip to content

Commit 5cd085b

Browse files
tautschnigtautschnig
authored
Merge pull request #8572 from tautschnig/arm-ci
Add aarch64 (Arm 64-bit) CI job
2 parents 7a6e2f7 + 431f460 commit 5cd085b

File tree

18 files changed

+310
-33
lines changed

18 files changed

+310
-33
lines changed

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

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -451,6 +451,60 @@ jobs:
451451
- name: Run tests
452452
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
453453

454+
# This job takes approximately 17 to 41 minutes
455+
check-ubuntu-24_04-arm-cmake-gcc:
456+
runs-on: ubuntu-24.04-arm
457+
steps:
458+
- uses: actions/checkout@v4
459+
with:
460+
submodules: recursive
461+
- name: Fetch dependencies
462+
env:
463+
# This is needed in addition to -yq to prevent apt-get from asking for
464+
# user input
465+
DEBIAN_FRONTEND: noninteractive
466+
run: |
467+
sudo apt-get update
468+
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
469+
- name: Confirm z3 solver is available and log the version installed
470+
run: z3 --version
471+
- name: Download cvc-5 from the releases page and make sure it can be deployed
472+
run: |
473+
wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip
474+
unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5
475+
rm cvc5-Linux-arm64-static.zip
476+
cvc5 --version
477+
- name: Prepare ccache
478+
uses: actions/cache@v4
479+
with:
480+
save-always: true
481+
path: .ccache
482+
key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-PR
483+
restore-keys: |
484+
${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}
485+
${{ runner.os }}-24.04-Arm-Release
486+
- name: ccache environment
487+
run: |
488+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
489+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
490+
- name: Configure using CMake
491+
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"
492+
- name: Check that doc task works
493+
run: ninja -C build doc
494+
- name: Zero ccache stats and limit in size
495+
run: ccache -z --max-size=500M
496+
- name: Build with Ninja
497+
run: ninja -C build -j${{env.linux-vcpus}}
498+
- name: Print ccache stats
499+
run: ccache -s
500+
- name: Check if package building works
501+
run: |
502+
cd build
503+
ninja package
504+
ls *.deb
505+
- name: Run tests
506+
run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}}
507+
454508
# This job takes approximately 14 to 60 minutes
455509
check-ubuntu-22_04-cmake-gcc-32bit:
456510
runs-on: ubuntu-22.04

‎.github/workflows/release-packages.yaml

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,77 @@ jobs:
7777
SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }}
7878
SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 package built and uploaded successfully' || 'Ubuntu 24.04 package build failed' }}"
7979

80+
ubuntu-24_04-arm-package:
81+
runs-on: ubuntu-24.04-arm
82+
env:
83+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
84+
steps:
85+
- uses: actions/checkout@v4
86+
with:
87+
submodules: recursive
88+
- name: Fetch dependencies
89+
run: |
90+
sudo apt-get update
91+
sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3
92+
- name: Confirm z3 solver is available and log the version installed
93+
run: z3 --version
94+
- name: Download cvc-5 from the releases page and make sure it can be deployed
95+
run: |
96+
wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip
97+
unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5
98+
rm cvc5-Linux-arm64-static.zip
99+
cvc5 --version
100+
- name: Prepare ccache
101+
uses: actions/cache@v4
102+
with:
103+
save-always: true
104+
path: .ccache
105+
key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG
106+
restore-keys:
107+
${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}
108+
${{ runner.os }}-24.04-Arm-Release
109+
- name: ccache environment
110+
run: |
111+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
112+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
113+
- name: Configure CMake
114+
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"
115+
- name: Zero ccache stats and limit in size
116+
run: ccache -z --max-size=500M
117+
- name: Build using Ninja
118+
run: ninja -C build -j4
119+
- name: Print ccache stats
120+
run: ccache -s
121+
- name: Run CTest
122+
run: cd build; ctest . -V -L CORE -C Release -j4
123+
- name: Create packages
124+
id: create_packages
125+
run: |
126+
cd build
127+
ninja package
128+
deb_package_name="$(ls *.deb)"
129+
echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT
130+
echo "deb_package_name=ubuntu-24.04-arm64-$deb_package_name" >> $GITHUB_OUTPUT
131+
- name: Get release info
132+
id: get_release_info
133+
uses: bruceadams/[email protected]
134+
- name: Upload binary packages
135+
uses: actions/upload-release-asset@v1
136+
with:
137+
upload_url: ${{ steps.get_release_info.outputs.upload_url }}
138+
asset_path: ${{ steps.create_packages.outputs.deb_package }}
139+
asset_name: ${{ steps.create_packages.outputs.deb_package_name }}
140+
asset_content_type: application/x-deb
141+
- name: Slack notification of CI status
142+
uses: rtCamp/action-slack-notify@v2
143+
if: success() || failure()
144+
env:
145+
SLACK_CHANNEL: aws-cbmc
146+
SLACK_COLOR: ${{ job.status }}
147+
SLACK_USERNAME: Github Actions CI bot
148+
SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }}
149+
SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 Arm package built and uploaded successfully' || 'Ubuntu 24.04 Arm package build failed' }}"
150+
80151
ubuntu-22_04-package:
81152
runs-on: ubuntu-22.04
82153
env:

‎regression/cbmc-incr-oneloop/Makefile

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,10 +2,10 @@ default: tests.log
22

33
# Note the `perl -e` serves the purpose of providing timeout
44
test:
5-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
5+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 25 ../../../src/cbmc/cbmc --slice-formula"
66

77
tests.log: ../test.pl
8-
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
8+
@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 25 ../../../src/cbmc/cbmc --slice-formula"
99

1010
clean:
1111
@$(RM) *.log

‎regression/cbmc/Quantifiers-statement-expression2/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ int main()
55

66
// clang-format off
77
// clang-format would rewrite the "==>" as "== >"
8-
__CPROVER_assume( __CPROVER_forall { char i; ({ _Bool flag = (i>=0 && i<2); flag ==> b[i]>=10 && b[i]<=10; }) } );
8+
__CPROVER_assume( __CPROVER_forall { signed char i; ({ _Bool flag = (i>=0 && i<2); flag ==> b[i]>=10 && b[i]<=10; }) } );
99
__CPROVER_assume( __CPROVER_forall { unsigned i; ({ _Bool flag = (i>=0 && i<2); flag ==> c[i]>=10 && c[i]<=10; }) } );
1010
// clang-format on
1111

‎regression/cbmc/Quantifiers-statement-expression2/unsigned-char.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
int main()
2+
{
3+
int b[2];
4+
int c[2];
5+
6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
8+
__CPROVER_assume( __CPROVER_forall { unsigned char i; ({ _Bool flag = (i>=0 && i<2); flag ==> b[i]>=10 && b[i]<=10; }) } );
9+
__CPROVER_assume( __CPROVER_forall { unsigned i; ({ _Bool flag = (i>=0 && i<2); flag ==> c[i]>=10 && c[i]<=10; }) } );
10+
// clang-format on
11+
12+
assert(b[0] == 10 && b[1] == 10);
13+
assert(c[0] == 10 && c[1] == 10);
14+
15+
return 0;
16+
}

‎regression/cbmc/Quantifiers-statement-expression2/unsigned-char.desc

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE broken-cprover-smt-backend no-new-smt
2+
main.c
3+
4+
^\*\* Results:$
5+
^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
6+
^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
7+
^VERIFICATION SUCCESSFUL$
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--
13+
skip_typecast as used in expr_eq of boolbv_quantifier.cpp no longer applies when
14+
using an unsigned char, which makes our quantifier instantiation fail when
15+
triggered from our in-tree SMT solver. We need to audit all uses of
16+
skip_typecast as some of these may even be unsound.

‎regression/cbmc/Quantifiers-type2/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ int main()
55

66
// clang-format off
77
// clang-format would rewrite the "==>" as "== >"
8-
__CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
8+
__CPROVER_assume( __CPROVER_forall { signed char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
99
__CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
1010
// clang-format on
1111

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
int main()
2+
{
3+
int b[2];
4+
int c[2];
5+
6+
// clang-format off
7+
// clang-format would rewrite the "==>" as "== >"
8+
__CPROVER_assume( __CPROVER_forall { unsigned char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } );
9+
__CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } );
10+
// clang-format on
11+
12+
assert(b[0] == 10 && b[1] == 10);
13+
assert(c[0] == 10 && c[1] == 10);
14+
15+
return 0;
16+
}

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

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
CORE broken-cprover-smt-backend no-new-smt
2+
unsigned-char.c
3+
4+
^\*\* Results:$
5+
^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$
6+
^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$
7+
^VERIFICATION SUCCESSFUL$
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--
13+
skip_typecast as used in expr_eq of boolbv_quantifier.cpp no longer applies when
14+
using an unsigned char, which makes our quantifier instantiation fail when
15+
triggered from our in-tree SMT solver. We need to audit all uses of
16+
skip_typecast as some of these may even be unsound.

‎regression/cbmc/va_list2/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#ifdef __GNUC__
1+
#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
22

33
# include <assert.h>
44

‎regression/cbmc/va_list4/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
#ifdef __GNUC__
1+
#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
22

33
struct __va_list_tag;
44
typedef struct __va_list_tag __va_list_tag;

‎src/ansi-c/ansi_c_internal_additions.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -286,6 +286,23 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
286286
code+="typedef signed __int128 __int128_t;\n"
287287
"typedef unsigned __int128 __uint128_t;\n";
288288
}
289+
290+
if(
291+
config.ansi_c.arch == "arm64" &&
292+
config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS)
293+
{
294+
code += "typedef struct __va_list {";
295+
code += "void *__stack;";
296+
code += "void *__gr_top;";
297+
code += "void *__vr_top;";
298+
code += "int __gr_offs;";
299+
code += "int __vr_offs;";
300+
code += " } __builtin_va_list;\n";
301+
}
302+
else
303+
{
304+
code += "typedef void ** __builtin_va_list;\n";
305+
}
289306
}
290307

291308
// this is Visual C/C++ only

‎src/ansi-c/c_typecheck_expr.cpp

Lines changed: 23 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -543,16 +543,32 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
543543
// The first parameter is the va_list, and the second
544544
// is the type, which will need to be fixed and checked.
545545
// The type is given by the parser as type of the expression.
546-
547-
typet arg_type=expr.type();
548-
typecheck_type(arg_type);
549-
550-
const code_typet new_type(
551-
{code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
546+
auto type_not_permitted = [this](const exprt &expr)
547+
{
548+
const exprt &arg = to_unary_expr(expr).op();
549+
error().source_location = expr.source_location();
550+
error() << "argument of type '" << to_string(arg.type())
551+
<< "' not permitted for va_arg" << eom;
552+
throw 0;
553+
};
552554

553555
exprt arg = to_unary_expr(expr).op();
556+
if(auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(arg.type()))
557+
{
558+
// aarch64 ABI mandates that va_list has struct type with member names as
559+
// specified
560+
const auto &components = follow_tag(*struct_tag_type).components();
561+
if(components.size() != 5)
562+
type_not_permitted(expr);
563+
}
564+
else if(arg.type().id() != ID_pointer && arg.type().id() != ID_array)
565+
type_not_permitted(expr);
566+
567+
typet arg_type = expr.type();
568+
typecheck_type(arg_type);
554569

555-
implicit_typecast(arg, pointer_type(void_type()));
570+
const code_typet new_type{
571+
{code_typet::parametert{arg.type()}}, std::move(arg_type)};
556572

557573
symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
558574
function.add_source_location() = expr.source_location();

‎src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@
22
// stdarg
33
void* __builtin_apply_args();
44
void* __builtin_apply(void (*)(), void*, __CPROVER_size_t);
5-
void __builtin_ms_va_end(void *ap);
6-
void __builtin_ms_va_start(void *ap, ...);
5+
void __builtin_ms_va_end(__builtin_ms_va_list ap);
6+
void __builtin_ms_va_start(__builtin_ms_va_list ap, ...);
77
void* __builtin_next_arg();
88
int __builtin_va_arg_pack();
99
int __builtin_va_arg_pack_len();
1010
void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src);
11-
void __builtin_va_end(void *ap);
12-
void __builtin_va_start(void *ap, ...);
11+
void __builtin_va_end(__builtin_va_list ap);
12+
void __builtin_va_start(__builtin_va_list ap, ...);
1313

1414
// stdlib
1515
void __builtin__Exit(int);

‎src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
// clang-format off
2-
typedef void ** __builtin_va_list;
32
typedef void ** __builtin_ms_va_list;
43

54
typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__));
@@ -45,4 +44,13 @@ enum __gcc_atomic_memmodels {
4544
};
4645

4746
typedef unsigned char __tile __attribute__ ((__vector_size__ (1024)));
47+
48+
// GCC and Clang use the following on ARM:
49+
typedef float __Float32x4_t __attribute__ ((__vector_size__ (16)));
50+
typedef double __Float64x2_t __attribute__ ((__vector_size__ (16)));
51+
// The following ARM (scalable vector) extensions define vectors the size of
52+
// which is not known at compile time.
53+
typedef float *__SVFloat32_t;
54+
typedef double *__SVFloat64_t;
55+
typedef __CPROVER_bool *__SVBool_t;
4856
// clang-format on

0 commit comments

Comments
 (0)