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

0 commit comments

Comments
 (0)