CI: Formal verification and test coverage

.devcontainer/Dockerfile

@@ -49,6 +49,8 @@ RUN dnf update -y && \
 	make \
 	clang \
 	libusb1-devel \
+	openssl-devel \
+	lcov \
 	'dnf-command(copr)' && \
 	dnf copr enable -y rleh/arm-none-eabi-gdb && \
 	dnf install -y --setopt=keepcache=0 arm-none-eabi-gdb && \
@@ -69,11 +71,12 @@ ENV LD_LIBRARY_PATH=/usr/local/lib:/usr/local/lib64
 # Set Rust environment variables
 ENV RUSTUP_HOME=/usr/local/rustup
 ENV CARGO_HOME=/usr/local/cargo
+ENV KANI_HOME=/usr/local/kani
 ENV PATH="/usr/local/cargo/bin:${PATH}"
 
 # Create directories with world-writable permissions before switching to non-root user
-RUN mkdir -p ${RUSTUP_HOME} ${CARGO_HOME} && \
-	chmod 1777 ${RUSTUP_HOME} ${CARGO_HOME}
+RUN mkdir -p ${RUSTUP_HOME} ${CARGO_HOME} ${KANI_HOME} && \
+	chmod 1777 ${RUSTUP_HOME} ${CARGO_HOME} ${KANI_HOME}
 
 # The container now runs with a non-root user to avoid file permission issues
 ARG USERNAME=vscode
@@ -91,6 +94,11 @@ RUN umask 0002 && \
 	cargo install cargo-binutils && \
 	rustup target add thumbv7em-none-eabihf thumbv7em-none-eabi
 
+RUN cargo install --locked kani-verifier && \
+	cargo kani setup
+RUN cargo install --locked cargo-tarpaulin
+RUN cargo install --locked cargo-watch
+
 COPY --from=qemu-builder /usr/local/ /usr/local/
 
 ENTRYPOINT ["/bin/bash"]

.devcontainer/devcontainer.json

@@ -3,22 +3,35 @@
 	"name": "Osiris Dev Container",
 	"build": {
 		"dockerfile": "Dockerfile",
-		"context": ".."
+		"context": "..",
+		"cacheFrom": "ghcr.io/osirisrtos/osiris/devcontainer:main-cache"
 	},
 	"remoteUser": "vscode",
 	"privileged": false,
 	"capAdd": [
 		// Permissions for accessing host USB devices
-		"SYS_RAWIO", "CAP_MKNOD"
+		"SYS_RAWIO", "CAP_MKNOD",
+		// Allow debugging
+		"SYS_PTRACE"
 	],
 	"customizations": {
 		"vscode": {
 			"extensions": [
 				"rust-lang.rust-analyzer",
 				"vadimcn.vscode-lldb",
 				"ms-vscode.cmake-tools",
-				"llvm-vs-code-extensions.vscode-clangd"
-			]
+				"llvm-vs-code-extensions.vscode-clangd",
+				"ryanluker.vscode-coverage-gutters"
+			],
+			"settings": {
+				"rust-analyzer.cargo.cfgs": [
+					"kani"
+				],
+				"coverage-gutters.coverageBaseDir": "${workspaceFolder}",
+				"coverage-gutters.coverageFileNames": [
+					"lcov.info"
+				]
+			}
 		}
 	},
 	"runArgs": [

.devcontainer/pre-commit.sh

@@ -0,0 +1,4 @@
+#!/bin/bash
+set -eoux pipefail
+
+make check-format

.github/workflows/ci.yml

@@ -42,6 +42,7 @@ jobs:
           REPO=$(echo "${GITHUB_REPOSITORY}" | tr '[:upper:]' '[:lower:]')
           CONTAINER_NAME="ghcr.io/${REPO}/devcontainer:${BRANCH//\//-}"
           echo "container_name=$CONTAINER_NAME" >> $GITHUB_OUTPUT
+          echo "container_without_tag=ghcr.io/${REPO}/devcontainer" >> $GITHUB_OUTPUT
 
       - name: Build and push Docker image
         uses: docker/build-push-action@v2
@@ -50,9 +51,39 @@ jobs:
           file: .devcontainer/Dockerfile
           push: true
           tags: ${{ steps.set_output.outputs.container_name }}
-          cache-from: type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache
+          cache-from: |
+            type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache
+            type=registry,ref=${{ steps.set_output.outputs.container_without_tag }}:main-cache
           cache-to: type=registry,ref=${{ steps.set_output.outputs.container_name }}-cache,mode=max
 
+  test:
+    name: Testing
+    needs: [container]
+    runs-on: ubuntu-latest
+    container:
+      image: ${{ needs.container.outputs.container_name }}
+      options: --user root --privileged
+    permissions:
+      contents: read
+      issues: write
+      pull-requests: write
+      packages: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Run tests
+        run: make test
+
+      - name: Report code coverage
+        uses: zgosalvez/github-actions-report-lcov@v4
+        with:
+          coverage-files: lcov.info
+          github-token: ${{ secrets.GITHUB_TOKEN }}
+          update-comment: true
+
   fmt:
     name: Check formatting
     needs: [container]
@@ -66,26 +97,11 @@ jobs:
         with:
           submodules: recursive
 
-      # This step is required to generate some Cargo.toml files
-      - name: Run CMake
-        run: cmake -B build
-
       - name: Check formatting for all Cargo manifests
-        run: |
-          manifests=$(find . \( -path './build*' -o -path '*dep*' -o -path '*verus*' -o -path './target' \) -prune -false -o -name Cargo.toml)
-          failed=0
-          for manifest in $manifests; do
-            echo "::group::Checking formatting for $manifest"
-            cargo fmt --manifest-path="$manifest" -- --check || failed=1
-            echo "::endgroup::"
-          done
-          if [ $failed -ne 0 ]; then
-            echo "Formatting check failed for one or more manifests"
-            exit 1
-          fi
-
-  build-stm32l4r5zi:
-    name: Build for the STM32L4R5ZI
+        run: make check-format
+
+  kani:
+    name: Kani verification
     needs: [container]
     runs-on: ubuntu-latest
     container:
@@ -97,8 +113,21 @@ jobs:
         with:
           submodules: recursive
 
-      - name: Run CMake
-        run: cmake -DBOARD=stm32-nucleo-l4r5zi -DCPU=cortex-m4 -B build
+      - name: Run Kani
+        run: make verify
+
+  build-stm32-nucleo-l4r5zi:
+    name: Build for the STM32 Nucleo L4R5ZI
+    needs: [container]
+    runs-on: ubuntu-latest
+    container:
+      image: ${{ needs.container.outputs.container_name }}
+      options: --user root
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
 
       - name: Build
-        run: cmake --build build --parallel $(nproc)
+        run: make osiris

.gitignore

@@ -3,3 +3,5 @@ build*/
 qemu/
 .venv/
 *.gen.*
+target
+**.info