Skip to content

Commit ca31133

Browse files
xarantolusthomasw04
xarantolus
and
thomasw04
authored
CI: Formal verification and test coverage (#8)
* Add tarpaulin * Also cache from main branch * Verification in CI * fix cargo-tarpaulin. * Add test coverage configuration * Report code coverage in CI * Use container for tests * Fix CI * Fix makefile * Fix * Fix indent * Add coverage report dependencies * Allow commenting * Fix permission * Exclude top-level Cargo.toml * Permissions * Add group for build dir * Rename job * Add pre-commit hook for formatting * Kernel formatting * Small improvements * fix: update kernel submodule. * small fix --------- Co-authored-by: thomasw04 <[email protected]>
1 parent 9e9518a commit ca31133

File tree

12 files changed

+1031
-33
lines changed

12 files changed

+1031
-33
lines changed

‎.devcontainer/Dockerfile‎

Lines changed: 10 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -49,6 +49,8 @@ RUN dnf update -y && \
4949
make \
5050
clang \
5151
libusb1-devel \
52+
openssl-devel \
53+
lcov \
5254
'dnf-command(copr)' && \
5355
dnf copr enable -y rleh/arm-none-eabi-gdb && \
5456
dnf install -y --setopt=keepcache=0 arm-none-eabi-gdb && \
@@ -69,11 +71,12 @@ ENV LD_LIBRARY_PATH=/usr/local/lib:/usr/local/lib64
6971
# Set Rust environment variables
7072
ENV RUSTUP_HOME=/usr/local/rustup
7173
ENV CARGO_HOME=/usr/local/cargo
74+
ENV KANI_HOME=/usr/local/kani
7275
ENV PATH="/usr/local/cargo/bin:${PATH}"
7376

7477
# Create directories with world-writable permissions before switching to non-root user
75-
RUN mkdir -p ${RUSTUP_HOME} ${CARGO_HOME} && \
76-
chmod 1777 ${RUSTUP_HOME} ${CARGO_HOME}
78+
RUN mkdir -p ${RUSTUP_HOME} ${CARGO_HOME} ${KANI_HOME} && \
79+
chmod 1777 ${RUSTUP_HOME} ${CARGO_HOME} ${KANI_HOME}
7780

7881
# The container now runs with a non-root user to avoid file permission issues
7982
ARG USERNAME=vscode
@@ -91,6 +94,11 @@ RUN umask 0002 && \
9194
cargo install cargo-binutils && \
9295
rustup target add thumbv7em-none-eabihf thumbv7em-none-eabi
9396

97+
RUN cargo install --locked kani-verifier && \
98+
cargo kani setup
99+
RUN cargo install --locked cargo-tarpaulin
100+
RUN cargo install --locked cargo-watch
101+
94102
COPY --from=qemu-builder /usr/local/ /usr/local/
95103

96104
ENTRYPOINT ["/bin/bash"]

‎.devcontainer/devcontainer.json‎

Lines changed: 17 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,22 +3,35 @@
33
"name": "Osiris Dev Container",
44
"build": {
55
"dockerfile": "Dockerfile",
6-
"context": ".."
6+
"context": "..",
7+
"cacheFrom": "ghcr.io/osirisrtos/osiris/devcontainer:main-cache"
78
},
89
"remoteUser": "vscode",
910
"privileged": false,
1011
"capAdd": [
1112
// Permissions for accessing host USB devices
12-
"SYS_RAWIO", "CAP_MKNOD"
13+
"SYS_RAWIO", "CAP_MKNOD",
14+
// Allow debugging
15+
"SYS_PTRACE"
1316
],
1417
"customizations": {
1518
"vscode": {
1619
"extensions": [
1720
"rust-lang.rust-analyzer",
1821
"vadimcn.vscode-lldb",
1922
"ms-vscode.cmake-tools",
20-
"llvm-vs-code-extensions.vscode-clangd"
21-
]
23+
"llvm-vs-code-extensions.vscode-clangd",
24+
"ryanluker.vscode-coverage-gutters"
25+
],
26+
"settings": {
27+
"rust-analyzer.cargo.cfgs": [
28+
"kani"
29+
],
30+
"coverage-gutters.coverageBaseDir": "${workspaceFolder}",
31+
"coverage-gutters.coverageFileNames": [
32+
"lcov.info"
33+
]
34+
}
2235
}
2336
},
2437
"runArgs": [

‎.devcontainer/pre-commit.sh‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,4 @@
1+
#!/bin/bash
2+
set -eoux pipefail
3+
4+
make check-format

‎.github/workflows/ci.yml‎

Lines changed: 52 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -42,6 +42,7 @@ jobs:
4242
REPO=$(echo "${GITHUB_REPOSITORY}" | tr '[:upper:]' '[:lower:]')
4343
CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:${BRANCH//\//-}"
4444
echo "container_name=$CONTAINER_NAME" >> $GITHUB_OUTPUT
45+
echo "container_without_tag=ghcr.io/${REPO}/devcontainer" >> $GITHUB_OUTPUT
4546
4647
- name: Build and push Docker image
4748
uses: docker/build-push-action@v2
@@ -50,9 +51,39 @@ jobs:
5051
file: .devcontainer/Dockerfile
5152
push: true
5253
tags: ${{ steps.set_output.outputs.container_name }}
53-
cache-from: type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache
54+
cache-from: |
55+
type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache
56+
type=registry,ref=${{ steps.set_output.outputs.container_without_tag }}:main-cache
5457
cache-to: type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache,mode=max
5558

59+
test:
60+
name: Testing
61+
needs: [container]
62+
runs-on: ubuntu-latest
63+
container:
64+
image: ${{ needs.container.outputs.container_name }}
65+
options: --user root --privileged
66+
permissions:
67+
contents: read
68+
issues: write
69+
pull-requests: write
70+
packages: read
71+
steps:
72+
- name: Checkout
73+
uses: actions/checkout@v4
74+
with:
75+
submodules: recursive
76+
77+
- name: Run tests
78+
run: make test
79+
80+
- name: Report code coverage
81+
uses: zgosalvez/github-actions-report-lcov@v4
82+
with:
83+
coverage-files: lcov.info
84+
github-token: ${{ secrets.GITHUB_TOKEN }}
85+
update-comment: true
86+
5687
fmt:
5788
name: Check formatting
5889
needs: [container]
@@ -66,26 +97,11 @@ jobs:
6697
with:
6798
submodules: recursive
6899

69-
# This step is required to generate some Cargo.toml files
70-
- name: Run CMake
71-
run: cmake -B build
72-
73100
- name: Check formatting for all Cargo manifests
74-
run: |
75-
manifests=$(find . \( -path './build*' -o -path '*dep*' -o -path '*verus*' -o -path './target' \) -prune -false -o -name Cargo.toml)
76-
failed=0
77-
for manifest in $manifests; do
78-
echo "::group::Checking formatting for $manifest"
79-
cargo fmt --manifest-path="$manifest" -- --check || failed=1
80-
echo "::endgroup::"
81-
done
82-
if [ $failed -ne 0 ]; then
83-
echo "Formatting check failed for one or more manifests"
84-
exit 1
85-
fi
86-
87-
build-stm32l4r5zi:
88-
name: Build for the STM32L4R5ZI
101+
run: make check-format
102+
103+
kani:
104+
name: Kani verification
89105
needs: [container]
90106
runs-on: ubuntu-latest
91107
container:
@@ -97,8 +113,21 @@ jobs:
97113
with:
98114
submodules: recursive
99115

100-
- name: Run CMake
101-
run: cmake -DBOARD=stm32-nucleo-l4r5zi -DCPU=cortex-m4 -B build
116+
- name: Run Kani
117+
run: make verify
118+
119+
build-stm32-nucleo-l4r5zi:
120+
name: Build for the STM32 Nucleo L4R5ZI
121+
needs: [container]
122+
runs-on: ubuntu-latest
123+
container:
124+
image: ${{ needs.container.outputs.container_name }}
125+
options: --user root
126+
steps:
127+
- name: Checkout
128+
uses: actions/checkout@v4
129+
with:
130+
submodules: recursive
102131

103132
- name: Build
104-
run: cmake --build build --parallel $(nproc)
133+
run: make osiris

‎.gitignore‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,3 +3,5 @@ build*/
33
qemu/
44
.venv/
55
*.gen.*
6+
target
7+
**.info

0 commit comments

Comments
 (0)