Skip to content

Commit 8e2c440

Browse files
tautschnigtautschnig
committed
Split test execution with coverage into JBMC and non-JBMC tasks
This should reduce the overall runtime by parallelising across runners. Do the build once as a separate step and then just rely on ccache to speed up re-builds in the actual test-execution jobs.
1 parent 5cd6a26 commit 8e2c440

File tree

2 files changed

+112
-5
lines changed

2 files changed

+112
-5
lines changed

‎.github/workflows/coverage.yaml

Lines changed: 111 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,52 @@ env:
1111

1212
jobs:
1313
# This job takes approximately 40 to 75 minutes
14-
Linux:
14+
Linux-cache-build:
15+
runs-on: ubuntu-20.04
16+
steps:
17+
- name: Clone repository
18+
uses: actions/checkout@v4
19+
with:
20+
submodules: recursive
21+
- name: Remove unnecessary software to free up disk space
22+
run: |
23+
# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
24+
df -h
25+
sudo rm -rf /usr/share/dotnet /usr/local/lib/* /opt/*
26+
df -h
27+
- name: Download testing and coverage dependencies
28+
env:
29+
# This is needed in addition to -yq to prevent apt-get from asking for
30+
# user input
31+
DEBIAN_FRONTEND: noninteractive
32+
run: |
33+
sudo apt-get update
34+
sudo apt-get install --no-install-recommends -y g++ gcc gdb binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3
35+
- name: Prepare ccache
36+
uses: actions/cache@v4
37+
with:
38+
save-always: true
39+
path: .ccache
40+
key: ${{ runner.os }}-20.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR
41+
restore-keys: |
42+
${{ runner.os }}-20.04-Coverage-${{ github.ref }}
43+
${{ runner.os }}-20.04-Coverage
44+
- name: ccache environment
45+
run: |
46+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
47+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
48+
- name: Configure CMake CBMC build with coverage instrumentation parameters
49+
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++
50+
- name: Zero ccache stats and limit in size
51+
run: ccache -z --max-size=7G
52+
- name: Execute CMake CBMC build
53+
run: cmake --build build -- -j${{env.linux-vcpus}}
54+
- name: Print ccache stats
55+
run: ccache -s
56+
57+
# This job takes approximately 40 to 75 minutes
58+
Linux-non-JBMC:
59+
needs: Linux-cache-build
1560
runs-on: ubuntu-20.04
1661
steps:
1762
- name: Clone repository
@@ -41,9 +86,8 @@ jobs:
4186
mv cvc5 /usr/local/bin
4287
cvc5 --version
4388
- name: Prepare ccache
44-
uses: actions/cache@v4
89+
uses: actions/cache/restore@v4
4590
with:
46-
save-always: true
4791
path: .ccache
4892
key: ${{ runner.os }}-20.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR
4993
restore-keys: |
@@ -54,7 +98,70 @@ jobs:
5498
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
5599
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
56100
- name: Configure CMake CBMC build with coverage instrumentation parameters
57-
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++
101+
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-E;^jbmc"
102+
- name: Zero ccache stats and limit in size
103+
run: ccache -z --max-size=7G
104+
- name: Execute CMake CBMC build
105+
run: cmake --build build -- -j${{env.linux-vcpus}}
106+
- name: Print ccache stats
107+
run: ccache -s
108+
- name: Run CTest and collect coverage statistics
109+
run: |
110+
echo "lcov_excl_line = UNREACHABLE" > ~/.lcovrc
111+
cmake --build build --target coverage -- -j${{env.linux-vcpus}}
112+
- name: Upload coverage statistics to Codecov
113+
uses: codecov/codecov-action@v4
114+
with:
115+
token: ${{ secrets.CODECOV_TOKEN }}
116+
files: build/html/coverage.info
117+
fail_ci_if_error: true
118+
verbose: true
119+
120+
# This job takes approximately 40 to 75 minutes
121+
Linux-JBMC:
122+
needs: Linux-cache-build
123+
runs-on: ubuntu-20.04
124+
steps:
125+
- name: Clone repository
126+
uses: actions/checkout@v4
127+
with:
128+
submodules: recursive
129+
- name: Remove unnecessary software to free up disk space
130+
run: |
131+
# inspired by https://github.com/easimon/maximize-build-space/blob/master/action.yml
132+
df -h
133+
sudo rm -rf /usr/share/dotnet /usr/local/lib/* /opt/*
134+
df -h
135+
- name: Download testing and coverage dependencies
136+
env:
137+
# This is needed in addition to -yq to prevent apt-get from asking for
138+
# user input
139+
DEBIAN_FRONTEND: noninteractive
140+
run: |
141+
sudo apt-get update
142+
sudo apt-get install --no-install-recommends -y g++ gcc gdb binutils flex bison cmake maven jq libxml2-utils openjdk-11-jdk-headless lcov ccache z3
143+
- name: Confirm z3 solver is available and log the version installed
144+
run: z3 --version
145+
- name: Download cvc-5 from the releases page and make sure it can be deployed
146+
run: |
147+
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
148+
chmod u+x cvc5
149+
mv cvc5 /usr/local/bin
150+
cvc5 --version
151+
- name: Prepare ccache
152+
uses: actions/cache/restore@v4
153+
with:
154+
path: .ccache
155+
key: ${{ runner.os }}-20.04-Coverage-${{ github.ref }}-${{ github.sha }}-PR
156+
restore-keys: |
157+
${{ runner.os }}-20.04-Coverage-${{ github.ref }}
158+
${{ runner.os }}-20.04-Coverage
159+
- name: ccache environment
160+
run: |
161+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
162+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
163+
- name: Configure CMake CBMC build with coverage instrumentation parameters
164+
run: cmake -S . -Bbuild -Denable_coverage=1 -Dparallel_tests=2 -DCMAKE_CXX_COMPILER=/usr/bin/g++ -DCOVERAGE_CTEST_EXTRA_FLAGS="-R;^jbmc"
58165
- name: Zero ccache stats and limit in size
59166
run: ccache -z --max-size=7G
60167
- name: Execute CMake CBMC build

‎CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
155155
find_program(CODE_COVERAGE_GENHTML genhtml)
156156
add_custom_target(coverage
157157
COMMAND ${CMAKE_COMMAND} -E make_directory ${CODE_COVERAGE_OUTPUT_DIR}
158-
COMMAND ctest -V -L CORE -j${parallel_tests}
158+
COMMAND ctest -V -L CORE -j${parallel_tests} ${COVERAGE_CTEST_EXTRA_FLAGS}
159159
COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --capture --directory ${CMAKE_BINARY_DIR} --output-file ${CODE_COVERAGE_INFO_FILE}
160160
COMMAND ${CODE_COVERAGE_LCOV} ${LCOV_FLAGS} --remove ${CODE_COVERAGE_INFO_FILE} '/usr/*' --output-file ${CODE_COVERAGE_INFO_FILE}
161161
COMMAND ${CODE_COVERAGE_GENHTML} ${CODE_COVERAGE_INFO_FILE} --output-directory ${CODE_COVERAGE_OUTPUT_DIR}

0 commit comments

Comments
 (0)