From 313d22decc8c61cddcb5337595f03fee3d47be8b Mon Sep 17 00:00:00 2001 From: xarantolus Date: Fri, 24 Oct 2025 12:33:57 +0200 Subject: [PATCH 1/4] Use CMD instead of entrypoint Enables the use of podman run command --- .devcontainer/Dockerfile | 2 +- hal/cortex-m | 1 + hal/stm32l4 | 1 + verus | 1 + 4 files changed, 4 insertions(+), 1 deletion(-) create mode 160000 hal/cortex-m create mode 160000 hal/stm32l4 create mode 160000 verus diff --git a/.devcontainer/Dockerfile b/.devcontainer/Dockerfile index e119307..42408ab 100644 --- a/.devcontainer/Dockerfile +++ b/.devcontainer/Dockerfile @@ -110,4 +110,4 @@ RUN --mount=type=cache,target=/usr/local/cargo/registry \ COPY --from=qemu-builder /usr/local/ /usr/local/ -ENTRYPOINT ["/bin/bash"] +CMD ["/bin/bash"] diff --git a/hal/cortex-m b/hal/cortex-m new file mode 160000 index 0000000..ab2662d --- /dev/null +++ b/hal/cortex-m @@ -0,0 +1 @@ +Subproject commit ab2662dee48d4cd578904fdea3445499b8880e90 diff --git a/hal/stm32l4 b/hal/stm32l4 new file mode 160000 index 0000000..9dd2aea --- /dev/null +++ b/hal/stm32l4 @@ -0,0 +1 @@ +Subproject commit 9dd2aeaacb6891c1e141b0e399a02320f86d9fb5 diff --git a/verus b/verus new file mode 160000 index 0000000..716aaa5 --- /dev/null +++ b/verus @@ -0,0 +1 @@ +Subproject commit 716aaa5f13b2ccbd3520af2b5380f35558c6b6c1 From d330710a97a1fbedb9f3698f1ec34a99569a1d5b Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Oct 2025 12:47:33 +0000 Subject: [PATCH 2/4] Initial plan From e601a3d93ef350f39fce2609217ed8023ec48829 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Oct 2025 12:51:33 +0000 Subject: [PATCH 3/4] Improve README with badges, devcontainer info, tests, coverage, and CI details Co-authored-by: xarantolus <32465636+xarantolus@users.noreply.github.com> --- README.md | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) diff --git a/README.md b/README.md index ebf3150..90c07c0 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,10 @@ # Osiris + +[![CI](https://github.com/OsirisRTOS/osiris/actions/workflows/ci.yml/badge.svg)](https://github.com/OsirisRTOS/osiris/actions/workflows/ci.yml) +[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) +[![License: Apache 2.0](https://img.shields.io/badge/License-Apache%202.0-blue.svg)](https://opensource.org/licenses/Apache-2.0) + An RTOS designed and verified to enable reliable software updates and operation for embedded systems. @@ -9,6 +14,13 @@ An RTOS designed and verified to enable reliable software updates and operation |-----------|-------------| | [kernel/](kernel/) | This is the actual kernel of osiris. It is a hardware independent layer providing scheduling, memory management, etc. | | [machine/](machine/) | This contains all the HALs and hardware specific code in general. It exports a hardware independent interface to the kernel. | +| [hal/](hal/) | Hardware Abstraction Layer implementations (cortex-m, stm32l4). | +| [tools/](tools/) | Development tools including configuration utilities and ELF injector. | +| [xtask/](xtask/) | Custom cargo xtask implementations for build automation. | +| [presets/](presets/) | Pre-configured build presets for different target boards (e.g., STM32L4R5ZI). | +| [verus/](verus/) | Verification-related files and components. | +| [.devcontainer/](.devcontainer/) | Docker-based development environment configuration. | +| [.github/](.github/) | CI/CD pipeline configurations and GitHub workflows. | ## Build @@ -30,6 +42,28 @@ These tools are used for flashing, debugging, and other development tasks. ### Quick Start +#### **Development Environment** + +##### Using DevContainer (Recommended) +The easiest way to get started is using the provided DevContainer, which includes all necessary dependencies: + +1. Install [Docker](https://www.docker.com/) and [Visual Studio Code](https://code.visualstudio.com/) +2. Install the [Dev Containers extension](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.remote-containers) +3. Open the repository in VS Code +4. When prompted, click "Reopen in Container" (or use Command Palette: "Dev Containers: Reopen in Container") + +The DevContainer includes: +- Rust toolchain with embedded targets +- ARM GCC toolchain +- Kani verifier for formal verification +- All build tools (just, cmake, clang) +- Debugging tools (gdb, stlink) +- Coverage tools (tarpaulin) +- QEMU for emulation + +##### Manual Setup +If you prefer not to use DevContainer, ensure you have all the dependencies listed in the [Build Dependencies](#build-dependencies) section installed on your system. + #### **Configure the build.** Configure all build components. The configuration is stored in `.cargo/config.toml` as environment variables with the `OSIRIS_` prefix. @@ -64,6 +98,51 @@ After the build a binary named ```Kernel.bin``` will be created at the source ro $ just hooks ``` +## Testing + +### Running Tests +Run the test suite using: + +```sh +$ just test +``` + +### Code Coverage +Generate test coverage reports using [cargo-tarpaulin](https://github.com/xd009642/tarpaulin): + +```sh +$ just cov +``` + +This generates an `lcov.info` file that can be viewed with coverage visualization tools. The DevContainer includes the Coverage Gutters VS Code extension for inline coverage display. + +### Formal Verification with Kani +Osiris uses [Kani](https://github.com/model-checking/kani) for formal verification of critical code paths: + +```sh +$ just verify +``` + +Kani performs bounded model checking to mathematically prove the absence of certain classes of bugs, including: +- Arithmetic overflows/underflows +- Array out-of-bounds access +- Undefined behavior +- Assertion violations + +The verification runs are also part of the CI pipeline to ensure all proofs pass on every commit. + +## Continuous Integration + +The project uses GitHub Actions for continuous integration. The CI pipeline includes: + +- **Container Build**: Builds and caches the development container +- **Testing**: Runs the complete test suite with coverage reporting +- **Formatting**: Checks code formatting with `rustfmt` +- **Kani Verification**: Runs formal verification proofs +- **Target Builds**: Builds for specific hardware targets (e.g., STM32 Nucleo L4R5ZI) + +You can view the current build status and detailed results in the [Actions tab](https://github.com/OsirisRTOS/osiris/actions). + ## License Osiris is distributed under the terms of both the MIT license and the Apache License (Version 2.0). From 35fad9c9a359c1ac31139044af855e688e888cdd Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 24 Oct 2025 14:09:13 +0000 Subject: [PATCH 4/4] Remove submodules (hal/cortex-m, hal/stm32l4, verus) Co-authored-by: xarantolus <32465636+xarantolus@users.noreply.github.com> --- hal/cortex-m | 1 - hal/stm32l4 | 1 - verus | 1 - 3 files changed, 3 deletions(-) delete mode 160000 hal/cortex-m delete mode 160000 hal/stm32l4 delete mode 160000 verus diff --git a/hal/cortex-m b/hal/cortex-m deleted file mode 160000 index ab2662d..0000000 --- a/hal/cortex-m +++ /dev/null @@ -1 +0,0 @@ -Subproject commit ab2662dee48d4cd578904fdea3445499b8880e90 diff --git a/hal/stm32l4 b/hal/stm32l4 deleted file mode 160000 index 9dd2aea..0000000 --- a/hal/stm32l4 +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 9dd2aeaacb6891c1e141b0e399a02320f86d9fb5 diff --git a/verus b/verus deleted file mode 160000 index 716aaa5..0000000 --- a/verus +++ /dev/null @@ -1 +0,0 @@ -Subproject commit 716aaa5f13b2ccbd3520af2b5380f35558c6b6c1