diff --git a/.github/workflows/renode-tests.yml b/.github/workflows/renode-tests.yml index 8bffeea..476c455 100644 --- a/.github/workflows/renode-tests.yml +++ b/.github/workflows/renode-tests.yml @@ -1,10 +1,13 @@ -# Multi-architecture build verification +# Renode emulation tests for Gale on M4F and M33 architectures # -# Builds Zephyr+Gale semaphore test for M4F, M33, and R5 targets. -# Proves the Rust FFI cross-compiles correctly for each architecture. -# Renode emulation tests will be added once renode-bazel-rules is wired in. +# Builds Zephyr+Gale semaphore test for each board with west, then runs +# the Renode Robot Framework tests to verify correct execution on the +# emulated hardware. Complements zephyr-tests.yml (which uses QEMU M3) +# by covering hardware-accurate M4F (STM32F4) and M33 (STM32L552/nucleo_l552ze_q) emulation. +# +# Renode portable handles its own .NET runtime — no system deps needed. -name: Multi-Arch Build +name: Renode Emulation Tests on: push: @@ -17,9 +20,10 @@ env: DOCKER_CONFIG: /tmp/.docker jobs: - build: + renode-test: name: "${{ matrix.arch }} (${{ matrix.board }})" runs-on: ubuntu-22.04 + timeout-minutes: 30 container: image: ghcr.io/zephyrproject-rtos/ci:v0.29.0 options: --user root @@ -27,18 +31,17 @@ jobs: fail-fast: false matrix: include: - - board: mps2/an385 - arch: cortex-m3 - rust_target: thumbv7m-none-eabi - test_path: tests/kernel/semaphore/semaphore - - board: mps2/an386 - arch: cortex-m4 + - board: stm32f4_disco + arch: cortex-m4f rust_target: thumbv7em-none-eabihf test_path: tests/kernel/semaphore/semaphore - - board: mps2/an521/cpu0 + robot_file: stm32f4_sem.robot + + - board: nucleo_l552ze_q arch: cortex-m33 rust_target: thumbv8m.main-none-eabihf test_path: tests/kernel/semaphore/semaphore + robot_file: stm32l552_sem.robot steps: - name: Checkout Gale @@ -54,7 +57,7 @@ jobs: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain stable . /root/.cargo/env rustup target add "${RUST_TARGET}" - # Also install non-hf variant in case FPU is disabled + # Install non-hf variant in case the board uses soft-float ABI NON_HF=$(echo "${RUST_TARGET}" | sed 's/eabihf$/eabi/') if [ "${NON_HF}" != "${RUST_TARGET}" ]; then rustup target add "${NON_HF}" || true @@ -68,7 +71,7 @@ jobs: west update --narrow -o=--depth=1 west sdk install - - name: Build semaphore test + - name: Build Zephyr+Gale ELF env: BOARD: ${{ matrix.board }} TEST_PATH: ${{ matrix.test_path }} @@ -83,6 +86,30 @@ jobs: -DZEPHYR_EXTRA_MODULES="${GALE_ROOT}" \ -DOVERLAY_CONFIG="${GALE_ROOT}/zephyr/gale_overlay.conf" + - name: Install Robot Framework + run: | + # The Zephyr CI Docker image (ci:v0.29.0) includes Renode pre-installed + # at /opt/renode (already in PATH). Just install Robot Framework. + pip3 install robotframework + + - name: Run Renode test + env: + ROBOT_FILE: ${{ matrix.robot_file }} + ELF: ${{ github.workspace }}/zephyr-workspace/build/zephyr/zephyr.elf + run: | + GALE_ROOT="${GITHUB_WORKSPACE}/gale" + mkdir -p "${GITHUB_WORKSPACE}/renode-results" + cd "${GITHUB_WORKSPACE}/renode-results" + renode-test "${GALE_ROOT}/renode/${ROBOT_FILE}" + + - name: Upload Renode results + if: always() + uses: actions/upload-artifact@v4 + with: + name: "renode-results-${{ matrix.arch }}" + path: renode-results/ + retention-days: 7 + - name: Upload ELF if: success() uses: actions/upload-artifact@v4 diff --git a/Cargo.toml b/Cargo.toml index 7282483..183098d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -46,7 +46,7 @@ overflow-checks = true # Core safety lints unsafe_code = "deny" # TODO: enable missing_docs = "warn" once all items are documented -unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)', 'cfg(verus_keep_ghost)'] } [lints.clippy] # === DENY: Correctness & safety-critical === diff --git a/README.md b/README.md index 19a7338..b6f8279 100644 --- a/README.md +++ b/README.md @@ -116,8 +116,8 @@ Triple-track formal verification: | Workflow | Scope | Status | |----------|-------|--------| | Rust CI | cargo test, clippy, verus-strip gate | 995 tests | -| Zephyr Kernel Tests | 13 upstream test suites on qemu_cortex_m3 | 13/13 pass | -| Multi-Arch Build | M3, M4F, M33 cross-compilation | 3 boards | +| Zephyr Kernel Tests | 20 upstream test suites on qemu_cortex_m3 | 20/20 pass | +| Renode Emulation Tests | Cortex-M4F (STM32F4) + Cortex-M33 (STM32L552) | 2 boards | ## Traceability diff --git a/artifacts/design.yaml b/artifacts/design.yaml index 89e4ee5..956e2f8 100644 --- a/artifacts/design.yaml +++ b/artifacts/design.yaml @@ -3604,3 +3604,89 @@ artifacts: target: SWREQ-SM-SM02 - type: function-maps-to target: PROV-SM-001 + + # ── Integration test targets (SWE.5 / SWE.6) ───────────────────────── + # + # These architecture decisions capture the hardware/emulation platforms + # used for Zephyr integration and Renode emulation testing. + # Kiln and Synth can reference these IDs to declare compatibility or + # to specify which targets their code generation must pass on. + + - id: SWARCH-TGT-001 + type: sw-arch-component + title: Integration test target — QEMU Cortex-M3 (qemu_cortex_m3) + status: approved + description: > + Primary Zephyr integration test target for Gale kernel primitives. + 20 upstream Zephyr test suites (semaphore, mutex, condvar, msgq, + stack, pipe, timer, event, sched, thread, and more) run on the + qemu_cortex_m3 board under west + QEMU. All 20/20 suites pass + with Gale replacing the corresponding C kernel modules. + Chosen for QEMU Cortex-M3 availability in Zephyr CI Docker image + without hardware setup — the canonical CI board for Zephyr kernel tests. + tags: [test-target, qemu, cortex-m3, integration] + fields: + platform: qemu_cortex_m3 + emulator: QEMU (via west build -t run) + architecture: ARMv7-M (Cortex-M3, no FPU) + rust-target: thumbv7m-none-eabi + ci-workflow: .github/workflows/zephyr-tests.yml + test-suites: 20 + links: + - type: allocated-from + target: SYSREQ-SEM-001 + + - id: SWARCH-TGT-002 + type: sw-arch-component + title: Renode emulation target — STM32F4 Discovery (Cortex-M4F) + status: approved + description: > + Hardware-accurate Renode emulation target for Cortex-M4F (ARMv7E-M + with FPU) validation. The stm32f4_disco board with stm32f4_discovery.repl + platform runs Gale semaphore tests under Renode 1.16.0 (pre-installed + in Zephyr CI Docker image). Confirms Gale functions correctly on + hardware with hardware floating-point and higher clock rates than M3. + Chosen because stm32f4_discovery.repl is fully emulated in Renode 1.16.0 + with working USART2 for Zephyr console output. + tags: [test-target, renode, cortex-m4f, stm32f4] + fields: + platform: stm32f4_disco + emulator: Renode 1.16.0 (renode-test via Robot Framework) + renode-platform: platforms/boards/stm32f4_discovery.repl + architecture: ARMv7E-M (Cortex-M4F, with FPU) + rust-target: thumbv7em-none-eabihf + ci-workflow: .github/workflows/renode-tests.yml + uart: sysbus.usart2 + links: + - type: allocated-from + target: SYSREQ-SEM-001 + - type: enables + target: SWREQ-KILN-003 + + - id: SWARCH-TGT-003 + type: sw-arch-component + title: Renode emulation target — STM32L552 Nucleo (Cortex-M33) + status: approved + description: > + Hardware-accurate Renode emulation target for Cortex-M33 (ARMv8-M + Mainline with TrustZone) validation. The nucleo_l552ze_q board with + the Renode nucleo_l552ze_q_ns platform runs Gale semaphore tests + under Renode 1.16.0. Confirms Gale functions on ARMv8-M which + introduces security extension changes to the exception model. + Chosen because Renode 1.16.0 ships a dedicated test platform + (tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl) with + complete STM32L552 peripheral support including LPUART1. + tags: [test-target, renode, cortex-m33, stm32l552] + fields: + platform: nucleo_l552ze_q + emulator: Renode 1.16.0 (renode-test via Robot Framework) + renode-platform: tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl + architecture: ARMv8-M Mainline (Cortex-M33, with FPU + TrustZone) + rust-target: thumbv8m.main-none-eabihf + ci-workflow: .github/workflows/renode-tests.yml + uart: sysbus.lpuart1 + links: + - type: allocated-from + target: SYSREQ-SEM-001 + - type: enables + target: SWREQ-KILN-003 diff --git a/artifacts/phase2_kiln_integration.yaml b/artifacts/phase2_kiln_integration.yaml index 044dd2d..bf8e84d 100644 --- a/artifacts/phase2_kiln_integration.yaml +++ b/artifacts/phase2_kiln_integration.yaml @@ -147,6 +147,10 @@ artifacts: links: - type: derives-from target: SYSREQ-KILN-002 + - type: verified-on + target: SWARCH-TGT-002 + - type: verified-on + target: SWARCH-TGT-003 - id: SWREQ-KILN-004 type: sw-req diff --git a/plain/src/event.rs b/plain/src/event.rs index 330b53e..a6106e4 100644 --- a/plain/src/event.rs +++ b/plain/src/event.rs @@ -58,7 +58,9 @@ impl Event { /// /// Returns the resulting event bitmask. pub fn post(&mut self, new_events: u32) -> u32 { + let old_events = self.events; self.events = self.events | new_events; + let new_val = self.events; self.events } /// Set the event bitmask to an exact value, replacing all bits. diff --git a/plain/src/fatal.rs b/plain/src/fatal.rs index e66df62..1f3c981 100644 --- a/plain/src/fatal.rs +++ b/plain/src/fatal.rs @@ -76,7 +76,11 @@ pub struct FatalError { } impl FatalError { /// Create a fatal error event. - pub fn new(reason: FatalReason, context: FatalContext, test_mode: bool) -> FatalError { + pub fn new( + reason: FatalReason, + context: FatalContext, + test_mode: bool, + ) -> FatalError { FatalError { reason, context, @@ -93,29 +97,37 @@ impl FatalError { if !self.test_mode { match self.reason { FatalReason::KernelPanic => RecoveryAction::Halt, - FatalReason::CpuException => match self.context { - FatalContext::Isr => RecoveryAction::Halt, - FatalContext::Thread => RecoveryAction::AbortThread, - }, - FatalReason::SpuriousIrq => match self.context { - FatalContext::Isr => RecoveryAction::Halt, - FatalContext::Thread => RecoveryAction::AbortThread, - }, + FatalReason::CpuException => { + match self.context { + FatalContext::Isr => RecoveryAction::Halt, + FatalContext::Thread => RecoveryAction::AbortThread, + } + } + FatalReason::SpuriousIrq => { + match self.context { + FatalContext::Isr => RecoveryAction::Halt, + FatalContext::Thread => RecoveryAction::AbortThread, + } + } FatalReason::StackCheckFail => RecoveryAction::AbortThread, - FatalReason::KernelOops => match self.context { - FatalContext::Isr => RecoveryAction::Halt, - FatalContext::Thread => RecoveryAction::AbortThread, - }, + FatalReason::KernelOops => { + match self.context { + FatalContext::Isr => RecoveryAction::Halt, + FatalContext::Thread => RecoveryAction::AbortThread, + } + } } } else { match self.context { - FatalContext::Isr => match self.reason { - FatalReason::SpuriousIrq => RecoveryAction::Ignore, - FatalReason::StackCheckFail => RecoveryAction::AbortThread, - FatalReason::CpuException => RecoveryAction::Ignore, - FatalReason::KernelOops => RecoveryAction::Ignore, - FatalReason::KernelPanic => RecoveryAction::Ignore, - }, + FatalContext::Isr => { + match self.reason { + FatalReason::SpuriousIrq => RecoveryAction::Ignore, + FatalReason::StackCheckFail => RecoveryAction::AbortThread, + FatalReason::CpuException => RecoveryAction::Ignore, + FatalReason::KernelOops => RecoveryAction::Ignore, + FatalReason::KernelPanic => RecoveryAction::Ignore, + } + } FatalContext::Thread => RecoveryAction::AbortThread, } } diff --git a/plain/src/fault_decode.rs b/plain/src/fault_decode.rs index 0f17349..c6b178d 100644 --- a/plain/src/fault_decode.rs +++ b/plain/src/fault_decode.rs @@ -31,94 +31,93 @@ //! //! Extends the existing fatal.rs module with hardware-specific fault //! register decoding for ARM Cortex-M targets. - -#[doc = " IACCVIOL: instruction access violation."] +/// IACCVIOL: instruction access violation. pub const MMFSR_IACCVIOL: u32 = 1u32 << 0u32; -#[doc = " DACCVIOL: data access violation."] +/// DACCVIOL: data access violation. pub const MMFSR_DACCVIOL: u32 = 1u32 << 1u32; -#[doc = " MUNSTKERR: MemManage fault on unstacking (exception return)."] +/// MUNSTKERR: MemManage fault on unstacking (exception return). pub const MMFSR_MUNSTKERR: u32 = 1u32 << 3u32; -#[doc = " MSTKERR: MemManage fault on stacking (exception entry)."] +/// MSTKERR: MemManage fault on stacking (exception entry). pub const MMFSR_MSTKERR: u32 = 1u32 << 4u32; -#[doc = " MLSPERR: MemManage fault during lazy FP state preservation."] +/// MLSPERR: MemManage fault during lazy FP state preservation. pub const MMFSR_MLSPERR: u32 = 1u32 << 5u32; -#[doc = " MMARVALID: MMFAR holds a valid fault address."] +/// MMARVALID: MMFAR holds a valid fault address. pub const MMFSR_MMARVALID: u32 = 1u32 << 7u32; -#[doc = " IBUSERR: instruction bus error."] +/// IBUSERR: instruction bus error. pub const BFSR_IBUSERR: u32 = 1u32 << 8u32; -#[doc = " PRECISERR: precise data bus error."] +/// PRECISERR: precise data bus error. pub const BFSR_PRECISERR: u32 = 1u32 << 9u32; -#[doc = " IMPRECISERR: imprecise data bus error."] +/// IMPRECISERR: imprecise data bus error. pub const BFSR_IMPRECISERR: u32 = 1u32 << 10u32; -#[doc = " UNSTKERR: bus fault on unstacking."] +/// UNSTKERR: bus fault on unstacking. pub const BFSR_UNSTKERR: u32 = 1u32 << 11u32; -#[doc = " STKERR: bus fault on stacking."] +/// STKERR: bus fault on stacking. pub const BFSR_STKERR: u32 = 1u32 << 12u32; -#[doc = " LSPERR: bus fault during lazy FP state preservation."] +/// LSPERR: bus fault during lazy FP state preservation. pub const BFSR_LSPERR: u32 = 1u32 << 13u32; -#[doc = " BFARVALID: BFAR holds a valid fault address."] +/// BFARVALID: BFAR holds a valid fault address. pub const BFSR_BFARVALID: u32 = 1u32 << 15u32; -#[doc = " UNDEFINSTR: undefined instruction."] +/// UNDEFINSTR: undefined instruction. pub const UFSR_UNDEFINSTR: u32 = 1u32 << 16u32; -#[doc = " INVSTATE: invalid state (e.g., ARM mode on Thumb-only core)."] +/// INVSTATE: invalid state (e.g., ARM mode on Thumb-only core). pub const UFSR_INVSTATE: u32 = 1u32 << 17u32; -#[doc = " INVPC: invalid PC load via EXC_RETURN."] +/// INVPC: invalid PC load via EXC_RETURN. pub const UFSR_INVPC: u32 = 1u32 << 18u32; -#[doc = " NOCP: no coprocessor (attempted access to unavailable CP)."] +/// NOCP: no coprocessor (attempted access to unavailable CP). pub const UFSR_NOCP: u32 = 1u32 << 19u32; -#[doc = " STKOF: stack overflow (ARMv8-M only, bit 20)."] +/// STKOF: stack overflow (ARMv8-M only, bit 20). pub const UFSR_STKOF: u32 = 1u32 << 20u32; -#[doc = " UNALIGNED: unaligned memory access."] +/// UNALIGNED: unaligned memory access. pub const UFSR_UNALIGNED: u32 = 1u32 << 24u32; -#[doc = " DIVBYZERO: integer divide by zero."] +/// DIVBYZERO: integer divide by zero. pub const UFSR_DIVBYZERO: u32 = 1u32 << 25u32; -#[doc = " VECTTBL: bus fault on vector table read."] +/// VECTTBL: bus fault on vector table read. pub const HFSR_VECTTBL: u32 = 1u32 << 1u32; -#[doc = " FORCED: forced HardFault (escalated from configurable fault)."] +/// FORCED: forced HardFault (escalated from configurable fault). pub const HFSR_FORCED: u32 = 1u32 << 30u32; -#[doc = " DEBUGEVT: debug event caused HardFault."] +/// DEBUGEVT: debug event caused HardFault. pub const HFSR_DEBUGEVT: u32 = 1u32 << 31u32; -#[doc = " Mask for MemManage bits (CFSR bits 0-7)."] +/// Mask for MemManage bits (CFSR bits 0-7). pub const MMFSR_MASK: u32 = 0x0000_00FFu32; -#[doc = " Mask for BusFault bits (CFSR bits 8-15)."] +/// Mask for BusFault bits (CFSR bits 8-15). pub const BFSR_MASK: u32 = 0x0000_FF00u32; -#[doc = " Mask for UsageFault bits (CFSR bits 16-31)."] +/// Mask for UsageFault bits (CFSR bits 16-31). pub const UFSR_MASK: u32 = 0xFFFF_0000u32; -#[doc = " High-level fault category decoded from CFSR/HFSR."] +/// High-level fault category decoded from CFSR/HFSR. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub enum FaultCategory { - #[doc = " MemManage fault (MPU violation, stack guard hit)."] + /// MemManage fault (MPU violation, stack guard hit). MemManage, - #[doc = " Bus fault (invalid memory access on bus)."] + /// Bus fault (invalid memory access on bus). BusFault, - #[doc = " Usage fault (illegal instruction, alignment, etc.)."] + /// Usage fault (illegal instruction, alignment, etc.). UsageFault, - #[doc = " Hard fault (escalated or vector table fault)."] + /// Hard fault (escalated or vector table fault). HardFault, - #[doc = " No fault detected (all status bits clear)."] + /// No fault detected (all status bits clear). None, } -#[doc = " ARM Cortex-M fault register snapshot."] -#[doc = ""] -#[doc = " Captures the four fault-related SCB registers at the time of a"] -#[doc = " fault exception. These are read by the fault handler and used to"] -#[doc = " classify and report the fault."] +/// ARM Cortex-M fault register snapshot. +/// +/// Captures the four fault-related SCB registers at the time of a +/// fault exception. These are read by the fault handler and used to +/// classify and report the fault. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct CortexMFault { - #[doc = " Configurable Fault Status Register (SCB->CFSR)."] - #[doc = " Contains MMFSR (bits 0-7), BFSR (bits 8-15), UFSR (bits 16-31)."] + /// Configurable Fault Status Register (SCB->CFSR). + /// Contains MMFSR (bits 0-7), BFSR (bits 8-15), UFSR (bits 16-31). pub cfsr: u32, - #[doc = " HardFault Status Register (SCB->HFSR)."] + /// HardFault Status Register (SCB->HFSR). pub hfsr: u32, - #[doc = " MemManage Fault Address Register (SCB->MMFAR)."] - #[doc = " Valid only when MMFSR.MMARVALID is set."] + /// MemManage Fault Address Register (SCB->MMFAR). + /// Valid only when MMFSR.MMARVALID is set. pub mmfar: u32, - #[doc = " BusFault Address Register (SCB->BFAR)."] - #[doc = " Valid only when BFSR.BFARVALID is set."] + /// BusFault Address Register (SCB->BFAR). + /// Valid only when BFSR.BFARVALID is set. pub bfar: u32, } impl CortexMFault { - #[doc = " Create a fault snapshot from raw register values."] + /// Create a fault snapshot from raw register values. pub fn new(cfsr: u32, hfsr: u32, mmfar: u32, bfar: u32) -> CortexMFault { CortexMFault { cfsr, @@ -127,75 +126,67 @@ impl CortexMFault { bfar, } } - #[doc = " Extract the MemManage fault status (CFSR bits 0-7)."] + /// Extract the MemManage fault status (CFSR bits 0-7). pub fn mmfsr(&self) -> u32 { self.cfsr & 0x0000_00FFu32 } - #[doc = " Extract the BusFault status (CFSR bits 8-15)."] + /// Extract the BusFault status (CFSR bits 8-15). pub fn bfsr(&self) -> u32 { self.cfsr & 0x0000_FF00u32 } - #[doc = " Extract the UsageFault status (CFSR bits 16-31)."] + /// Extract the UsageFault status (CFSR bits 16-31). pub fn ufsr(&self) -> u32 { self.cfsr & 0xFFFF_0000u32 } - #[doc = " FH2: Check if MMFAR holds a valid fault address."] - #[doc = ""] - #[doc = " The MMFAR register is only valid when the MMARVALID bit (bit 7)"] - #[doc = " is set in the MMFSR portion of CFSR."] + /// FH2: Check if MMFAR holds a valid fault address. + /// + /// The MMFAR register is only valid when the MMARVALID bit (bit 7) + /// is set in the MMFSR portion of CFSR. pub fn is_mmfar_valid(&self) -> bool { (self.cfsr & MMFSR_MMARVALID) != 0 } - #[doc = " FH2: Check if BFAR holds a valid fault address."] - #[doc = ""] - #[doc = " The BFAR register is only valid when the BFARVALID bit (bit 15)"] - #[doc = " is set in the BFSR portion of CFSR."] + /// FH2: Check if BFAR holds a valid fault address. + /// + /// The BFAR register is only valid when the BFARVALID bit (bit 15) + /// is set in the BFSR portion of CFSR. pub fn is_bfar_valid(&self) -> bool { (self.cfsr & BFSR_BFARVALID) != 0 } - #[doc = " Get MMFAR value, returning None if not valid."] - #[doc = ""] - #[doc = " FH2: Only returns Some when MMARVALID is set."] + /// Get MMFAR value, returning None if not valid. + /// + /// FH2: Only returns Some when MMARVALID is set. pub fn mmfar_checked(&self) -> Option { - if (self.cfsr & MMFSR_MMARVALID) != 0 { - Some(self.mmfar) - } else { - None - } + if (self.cfsr & MMFSR_MMARVALID) != 0 { Some(self.mmfar) } else { None } } - #[doc = " Get BFAR value, returning None if not valid."] - #[doc = ""] - #[doc = " FH2: Only returns Some when BFARVALID is set."] + /// Get BFAR value, returning None if not valid. + /// + /// FH2: Only returns Some when BFARVALID is set. pub fn bfar_checked(&self) -> Option { - if (self.cfsr & BFSR_BFARVALID) != 0 { - Some(self.bfar) - } else { - None - } - } - #[doc = " FH3: Check if HardFault was escalated from a configurable fault."] - #[doc = ""] - #[doc = " The FORCED bit (HFSR bit 30) indicates that a configurable fault"] - #[doc = " (MemManage, BusFault, or UsageFault) was escalated to HardFault"] - #[doc = " because the configurable fault was disabled or another fault"] - #[doc = " occurred during fault processing."] + if (self.cfsr & BFSR_BFARVALID) != 0 { Some(self.bfar) } else { None } + } + /// FH3: Check if HardFault was escalated from a configurable fault. + /// + /// The FORCED bit (HFSR bit 30) indicates that a configurable fault + /// (MemManage, BusFault, or UsageFault) was escalated to HardFault + /// because the configurable fault was disabled or another fault + /// occurred during fault processing. pub fn is_escalated(&self) -> bool { (self.hfsr & HFSR_FORCED) != 0 } - #[doc = " Check if a vector table read caused the HardFault."] + /// Check if a vector table read caused the HardFault. pub fn is_vecttbl_fault(&self) -> bool { (self.hfsr & HFSR_VECTTBL) != 0 } - #[doc = " FH1: Classify the primary fault category."] - #[doc = ""] - #[doc = " Determines the highest-priority fault category from the"] - #[doc = " CFSR and HFSR registers. Priority order (from ARM architecture):"] - #[doc = " 1. HardFault (checked via HFSR)"] - #[doc = " 2. MemManage (CFSR bits 0-7)"] - #[doc = " 3. BusFault (CFSR bits 8-15)"] - #[doc = " 4. UsageFault (CFSR bits 16-31)"] - #[doc = ""] - #[doc = " Returns None if no fault bits are set."] + /// FH1: Classify the primary fault category. + /// + /// Determines the highest-priority fault category from the + /// CFSR and HFSR registers. Priority order (from ARM architecture): + /// 1. HardFault (checked via HFSR) + /// 2. MemManage (CFSR bits 0-7) + /// 3. BusFault (CFSR bits 8-15) + /// 4. UsageFault (CFSR bits 16-31) + /// + /// Returns None if no fault bits are set. pub fn classify(&self) -> FaultCategory { let hfsr = self.hfsr; let cfsr = self.cfsr; @@ -211,43 +202,43 @@ impl CortexMFault { FaultCategory::None } } - #[doc = " Check for instruction access violation (MPU)."] + /// Check for instruction access violation (MPU). pub fn has_iaccviol(&self) -> bool { (self.cfsr & MMFSR_IACCVIOL) != 0 } - #[doc = " Check for data access violation (MPU)."] + /// Check for data access violation (MPU). pub fn has_daccviol(&self) -> bool { (self.cfsr & MMFSR_DACCVIOL) != 0 } - #[doc = " Check for instruction bus error."] + /// Check for instruction bus error. pub fn has_ibuserr(&self) -> bool { (self.cfsr & BFSR_IBUSERR) != 0 } - #[doc = " Check for precise data bus error."] + /// Check for precise data bus error. pub fn has_preciserr(&self) -> bool { (self.cfsr & BFSR_PRECISERR) != 0 } - #[doc = " Check for imprecise data bus error."] + /// Check for imprecise data bus error. pub fn has_impreciserr(&self) -> bool { (self.cfsr & BFSR_IMPRECISERR) != 0 } - #[doc = " Check for undefined instruction."] + /// Check for undefined instruction. pub fn has_undefinstr(&self) -> bool { (self.cfsr & UFSR_UNDEFINSTR) != 0 } - #[doc = " Check for invalid state (e.g., ARM mode on Thumb-only)."] + /// Check for invalid state (e.g., ARM mode on Thumb-only). pub fn has_invstate(&self) -> bool { (self.cfsr & UFSR_INVSTATE) != 0 } - #[doc = " Check for divide by zero."] + /// Check for divide by zero. pub fn has_divbyzero(&self) -> bool { (self.cfsr & UFSR_DIVBYZERO) != 0 } - #[doc = " Check for unaligned memory access."] + /// Check for unaligned memory access. pub fn has_unaligned(&self) -> bool { (self.cfsr & UFSR_UNALIGNED) != 0 } - #[doc = " Check for stack overflow (ARMv8-M)."] + /// Check for stack overflow (ARMv8-M). pub fn has_stkof(&self) -> bool { (self.cfsr & UFSR_STKOF) != 0 } diff --git a/plain/src/futex.rs b/plain/src/futex.rs index d060dda..dc7de69 100644 --- a/plain/src/futex.rs +++ b/plain/src/futex.rs @@ -133,11 +133,70 @@ impl Futex { pub fn wake(&mut self, wake_all: bool) -> WakeResult { let mut woken: u32 = 0; let mut threads: [Option; 64] = [ - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, ]; if !wake_all { let thread = self.wait_q.unpend_first(OK); diff --git a/plain/src/heap.rs b/plain/src/heap.rs index 7400721..16af61a 100644 --- a/plain/src/heap.rs +++ b/plain/src/heap.rs @@ -241,7 +241,12 @@ impl Heap { /// `bytes` = size of chunk being freed. /// `merge_left` = whether left neighbor is free. /// `merge_right` = whether right neighbor is free. - pub fn coalesce_free(&mut self, bytes: u32, merge_left: bool, merge_right: bool) -> i32 { + pub fn coalesce_free( + &mut self, + bytes: u32, + merge_left: bool, + merge_right: bool, + ) -> i32 { #[allow(clippy::arithmetic_side_effects)] { self.allocated_bytes = self.allocated_bytes - bytes; diff --git a/plain/src/kheap.rs b/plain/src/kheap.rs index 3800203..34d7ebb 100644 --- a/plain/src/kheap.rs +++ b/plain/src/kheap.rs @@ -32,32 +32,30 @@ //! KH4: free(n): allocated_bytes -= n (with underflow protection) //! KH5: conservation: free_bytes + allocated_bytes == capacity //! KH6: no arithmetic overflow in any operation - use crate::error::*; - -#[doc = " Kernel heap allocation tracker — byte count model."] -#[doc = ""] -#[doc = " Corresponds to Zephyr's struct k_heap {"] -#[doc = " struct sys_heap heap; // actual allocator (not modeled)"] -#[doc = " _wait_q_t wait_q; // blocking waiters (not modeled)"] -#[doc = " struct k_spinlock lock; // synchronization (not modeled)"] -#[doc = " };"] -#[doc = ""] -#[doc = " We model the byte-level accounting: allocated_bytes tracks total"] -#[doc = " bytes currently allocated. The C sys_heap manages the actual"] -#[doc = " free-list, coalescing, and alignment."] +/// Kernel heap allocation tracker — byte count model. +/// +/// Corresponds to Zephyr's struct k_heap { +/// struct sys_heap heap; // actual allocator (not modeled) +/// _wait_q_t wait_q; // blocking waiters (not modeled) +/// struct k_spinlock lock; // synchronization (not modeled) +/// }; +/// +/// We model the byte-level accounting: allocated_bytes tracks total +/// bytes currently allocated. The C sys_heap manages the actual +/// free-list, coalescing, and alignment. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct KHeap { - #[doc = " Maximum heap size in bytes (immutable after init)."] + /// Maximum heap size in bytes (immutable after init). pub capacity: u32, - #[doc = " Total bytes currently allocated."] + /// Total bytes currently allocated. pub allocated_bytes: u32, } impl KHeap { - #[doc = " Initialize a kernel heap with the given capacity in bytes."] - #[doc = ""] - #[doc = " Corresponds to k_heap_init() (kheap.c:26-33)."] - #[doc = " Returns EINVAL if capacity is 0."] + /// Initialize a kernel heap with the given capacity in bytes. + /// + /// Corresponds to k_heap_init() (kheap.c:26-33). + /// Returns EINVAL if capacity is 0. pub fn init(capacity: u32) -> Result { if capacity == 0 { Err(EINVAL) @@ -68,12 +66,12 @@ impl KHeap { }) } } - #[doc = " Allocate `bytes` from the heap."] - #[doc = ""] - #[doc = " Corresponds to k_heap_alloc() (kheap.c:119-129)."] - #[doc = " KH2: success when space available, allocated_bytes += bytes."] - #[doc = " KH3: returns ENOMEM when would exceed capacity."] - #[doc = " KH6: no overflow — checked addition."] + /// Allocate `bytes` from the heap. + /// + /// Corresponds to k_heap_alloc() (kheap.c:119-129). + /// KH2: success when space available, allocated_bytes += bytes. + /// KH3: returns ENOMEM when would exceed capacity. + /// KH6: no overflow — checked addition. pub fn alloc(&mut self, bytes: u32) -> i32 { if bytes <= self.capacity - self.allocated_bytes { #[allow(clippy::arithmetic_side_effects)] @@ -85,10 +83,10 @@ impl KHeap { ENOMEM } } - #[doc = " Free `bytes` back to the heap."] - #[doc = ""] - #[doc = " Corresponds to k_heap_free() (kheap.c:206-218)."] - #[doc = " KH4: allocated_bytes -= bytes, with underflow protection."] + /// Free `bytes` back to the heap. + /// + /// Corresponds to k_heap_free() (kheap.c:206-218). + /// KH4: allocated_bytes -= bytes, with underflow protection. pub fn free(&mut self, bytes: u32) -> i32 { if bytes <= self.allocated_bytes { #[allow(clippy::arithmetic_side_effects)] @@ -100,21 +98,21 @@ impl KHeap { EINVAL } } - #[doc = " Allocate with alignment requirement."] - #[doc = ""] - #[doc = " Corresponds to k_heap_aligned_alloc() (kheap.c:131-155)."] - #[doc = " Models the byte accounting; actual alignment is handled by C's sys_heap."] - #[doc = " The `align` parameter must be a power of 2 (or 0 for no alignment)."] - #[doc = ""] - #[doc = " For the model, alignment doesn't affect byte accounting — the"] - #[doc = " underlying sys_heap handles alignment padding internally."] + /// Allocate with alignment requirement. + /// + /// Corresponds to k_heap_aligned_alloc() (kheap.c:131-155). + /// Models the byte accounting; actual alignment is handled by C's sys_heap. + /// The `align` parameter must be a power of 2 (or 0 for no alignment). + /// + /// For the model, alignment doesn't affect byte accounting — the + /// underlying sys_heap handles alignment padding internally. pub fn aligned_alloc(&mut self, bytes: u32, align: u32) -> i32 { self.alloc(bytes) } - #[doc = " Allocate and zero-initialize memory for `num * size` bytes."] - #[doc = ""] - #[doc = " Corresponds to k_heap_calloc() (kheap.c:157-174)."] - #[doc = " KH6: overflow check on num * size multiplication."] + /// Allocate and zero-initialize memory for `num * size` bytes. + /// + /// Corresponds to k_heap_calloc() (kheap.c:157-174). + /// KH6: overflow check on num * size multiplication. pub fn calloc(&mut self, num: u32, size: u32) -> i32 { let num64: u64 = num as u64; let size64: u64 = size as u64; @@ -126,26 +124,26 @@ impl KHeap { let total_u32: u32 = total as u32; self.alloc(total_u32) } - #[doc = " Number of bytes currently allocated."] + /// Number of bytes currently allocated. pub fn allocated_get(&self) -> u32 { self.allocated_bytes } - #[doc = " Number of free (available) bytes."] - #[doc = " KH5: free_bytes + allocated_bytes == capacity."] + /// Number of free (available) bytes. + /// KH5: free_bytes + allocated_bytes == capacity. pub fn free_get(&self) -> u32 { #[allow(clippy::arithmetic_side_effects)] let r = self.capacity - self.allocated_bytes; r } - #[doc = " Total heap capacity in bytes."] + /// Total heap capacity in bytes. pub fn capacity_get(&self) -> u32 { self.capacity } - #[doc = " Check if the heap is full (all bytes allocated)."] + /// Check if the heap is full (all bytes allocated). pub fn is_full(&self) -> bool { self.allocated_bytes == self.capacity } - #[doc = " Check if the heap is empty (no bytes allocated)."] + /// Check if the heap is empty (no bytes allocated). pub fn is_empty(&self) -> bool { self.allocated_bytes == 0 } diff --git a/plain/src/lib.rs b/plain/src/lib.rs index bca0c03..c552c5c 100644 --- a/plain/src/lib.rs +++ b/plain/src/lib.rs @@ -19,10 +19,7 @@ //! - [`mutex`] — Reentrant mutex (port of kernel/mutex.c) //! - [`condvar`] — Condition variable (port of kernel/condvar.c) #![no_std] -#![allow(unused_imports, unused_variables)] -// Verus-stripped code: the stripping process produces patterns that trigger -// clippy lints (e.g., `x = x | y` instead of `x |= y`, `x as u64` casts). -// These are suppressed since this is generated output, not hand-written code. +#![allow(unused_imports)] #![allow( clippy::arithmetic_side_effects, clippy::indexing_slicing, @@ -31,67 +28,47 @@ clippy::self_assignment, clippy::absurd_extreme_comparisons, clippy::wildcard_enum_match_arm, - clippy::checked_conversions, - clippy::assign_op_pattern, - clippy::cast_lossless, - clippy::wildcard_imports, - clippy::match_same_arms, - clippy::option_if_let_else, - clippy::if_not_else, - clippy::new_without_default, - clippy::must_use_candidate, - clippy::unused_self, - clippy::needless_bool, - clippy::useless_asref, - clippy::redundant_field_names, - clippy::manual_map, - clippy::single_match, - clippy::return_self_not_must_use, - clippy::len_without_is_empty, - clippy::match_like_matches_macro, - clippy::manual_is_power_of_two, - clippy::manual_div_ceil, - clippy::too_long_first_doc_paragraph, - clippy::len_zero, - clippy::single_match_else + clippy::checked_conversions )] #[cfg(kani)] extern crate kani; -pub mod atomic; -pub mod condvar; -pub mod device_init; -pub mod dynamic; pub mod error; -pub mod event; -pub mod fatal; -pub mod fault_decode; +pub mod priority; +pub mod thread; +pub mod wait_queue; +pub mod sem; +pub mod mutex; +pub mod condvar; +pub mod msgq; +pub mod pipe; +pub mod stack; pub mod fifo; -pub mod futex; -pub mod heap; -pub mod kheap; pub mod lifo; -pub mod mbox; -pub mod mem_domain; +pub mod timer; +pub mod event; pub mod mem_slab; -pub mod mempool; -pub mod msgq; -pub mod mutex; -pub mod pipe; -pub mod poll; -pub mod priority; pub mod queue; -pub mod ring_buf; +pub mod futex; +pub mod mbox; +pub mod timeout; +#[cfg(not(verus_keep_ghost))] +pub mod poll; +#[cfg(not(verus_keep_ghost))] pub mod sched; -pub mod sem; -pub mod smp_state; -pub mod spinlock; -pub mod stack; -pub mod stack_config; -pub mod thread; pub mod thread_lifecycle; -pub mod timeout; -pub mod timer; pub mod timeslice; -pub mod userspace; -pub mod wait_queue; +pub mod heap; +pub mod kheap; pub mod work; +pub mod fatal; +pub mod fault_decode; +pub mod mempool; +pub mod dynamic; +pub mod smp_state; +pub mod stack_config; +pub mod device_init; +pub mod mem_domain; +pub mod spinlock; +pub mod atomic; +pub mod userspace; +pub mod ring_buf; diff --git a/plain/src/mbox.rs b/plain/src/mbox.rs index b16b426..1434bfb 100644 --- a/plain/src/mbox.rs +++ b/plain/src/mbox.rs @@ -119,11 +119,15 @@ impl Mbox { /// - MB4: thread ID filtering — K_ANY matches any, else exact match /// - MB5: data exchange size = min(tx_size, rx_buf_size) /// - MB6: no overflow in size min computation - pub fn message_match(&self, tx_msg: &MboxMsg, rx_msg: &MboxMsg) -> Result<(u32, u32), i32> { - let tx_target_ok = - tx_msg.tx_target_thread == K_ANY || tx_msg.tx_target_thread == rx_msg.tx_target_thread; - let rx_source_ok = - rx_msg.rx_source_thread == K_ANY || rx_msg.rx_source_thread == tx_msg.rx_source_thread; + pub fn message_match( + &self, + tx_msg: &MboxMsg, + rx_msg: &MboxMsg, + ) -> Result<(u32, u32), i32> { + let tx_target_ok = tx_msg.tx_target_thread == K_ANY + || tx_msg.tx_target_thread == rx_msg.tx_target_thread; + let rx_source_ok = rx_msg.rx_source_thread == K_ANY + || rx_msg.rx_source_thread == tx_msg.rx_source_thread; if tx_target_ok && rx_source_ok { let actual_size = if rx_msg.size > tx_msg.size { tx_msg.size @@ -160,11 +164,7 @@ impl Mbox { /// - MB5: actual size = min(tx_data_size, rx_buffer_size) /// - MB6: no overflow — result <= both inputs pub fn validate_data_exchange(tx_data_size: u32, rx_buffer_size: u32) -> u32 { - if rx_buffer_size > tx_data_size { - tx_data_size - } else { - rx_buffer_size - } + if rx_buffer_size > tx_data_size { tx_data_size } else { rx_buffer_size } } /// Check if a send/receive pair's thread IDs are compatible. /// diff --git a/plain/src/mem_domain.rs b/plain/src/mem_domain.rs index ac8d920..9476906 100644 --- a/plain/src/mem_domain.rs +++ b/plain/src/mem_domain.rs @@ -98,8 +98,10 @@ impl MemDomain { } let mut i: u32 = 0; while i < MAX_PARTITIONS { - if self.partitions[i as usize].size > 0 && part.overlaps(&self.partitions[i as usize]) { - return false; + if self.partitions[i as usize].size > 0 { + if part.overlaps(&self.partitions[i as usize]) { + return false; + } } i = i + 1; } diff --git a/plain/src/mempool.rs b/plain/src/mempool.rs index 0de7934..0cd4814 100644 --- a/plain/src/mempool.rs +++ b/plain/src/mempool.rs @@ -25,26 +25,24 @@ //! MP4: free when allocated > 0: allocated -= 1 //! MP5: conservation: free_blocks + allocated == capacity //! MP6: no arithmetic overflow in any operation - use crate::error::*; - -#[doc = " Fixed-block memory pool model."] -#[doc = ""] -#[doc = " Models a pool of equal-sized blocks. Each block is either"] -#[doc = " allocated or free. We track the count, not individual blocks."] +/// Fixed-block memory pool model. +/// +/// Models a pool of equal-sized blocks. Each block is either +/// allocated or free. We track the count, not individual blocks. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct MemPool { - #[doc = " Total number of blocks in the pool (immutable after init)."] + /// Total number of blocks in the pool (immutable after init). pub capacity: u32, - #[doc = " Number of blocks currently allocated."] + /// Number of blocks currently allocated. pub allocated: u32, - #[doc = " Size of each block in bytes (immutable after init)."] + /// Size of each block in bytes (immutable after init). pub block_size: u32, } impl MemPool { - #[doc = " Initialize a memory pool."] - #[doc = ""] - #[doc = " Returns EINVAL if capacity or block_size is 0."] + /// Initialize a memory pool. + /// + /// Returns EINVAL if capacity or block_size is 0. pub fn init(capacity: u32, block_size: u32) -> Result { if capacity == 0 || block_size == 0 { Err(EINVAL) @@ -56,11 +54,11 @@ impl MemPool { }) } } - #[doc = " Allocate one block from the pool."] - #[doc = ""] - #[doc = " MP2: success when allocated < capacity."] - #[doc = " MP3: returns ENOMEM when full."] - #[doc = " MP6: no overflow."] + /// Allocate one block from the pool. + /// + /// MP2: success when allocated < capacity. + /// MP3: returns ENOMEM when full. + /// MP6: no overflow. pub fn alloc(&mut self) -> i32 { if self.allocated < self.capacity { #[allow(clippy::arithmetic_side_effects)] @@ -72,10 +70,10 @@ impl MemPool { ENOMEM } } - #[doc = " Allocate `count` blocks from the pool."] - #[doc = ""] - #[doc = " Returns OK if enough blocks are available, ENOMEM otherwise."] - #[doc = " MP6: no overflow — checked addition."] + /// Allocate `count` blocks from the pool. + /// + /// Returns OK if enough blocks are available, ENOMEM otherwise. + /// MP6: no overflow — checked addition. pub fn alloc_many(&mut self, count: u32) -> i32 { if count <= self.capacity - self.allocated { #[allow(clippy::arithmetic_side_effects)] @@ -87,9 +85,9 @@ impl MemPool { ENOMEM } } - #[doc = " Free one block back to the pool."] - #[doc = ""] - #[doc = " MP4: success when allocated > 0."] + /// Free one block back to the pool. + /// + /// MP4: success when allocated > 0. pub fn free(&mut self) -> i32 { if self.allocated > 0 { #[allow(clippy::arithmetic_side_effects)] @@ -101,7 +99,7 @@ impl MemPool { EINVAL } } - #[doc = " Free `count` blocks back to the pool."] + /// Free `count` blocks back to the pool. pub fn free_many(&mut self, count: u32) -> i32 { if count <= self.allocated { #[allow(clippy::arithmetic_side_effects)] @@ -113,43 +111,41 @@ impl MemPool { EINVAL } } - #[doc = " Number of blocks currently allocated."] + /// Number of blocks currently allocated. pub fn allocated_get(&self) -> u32 { self.allocated } - #[doc = " Number of free (available) blocks."] - #[doc = " MP5: free_blocks + allocated == capacity."] + /// Number of free (available) blocks. + /// MP5: free_blocks + allocated == capacity. pub fn free_get(&self) -> u32 { #[allow(clippy::arithmetic_side_effects)] let r = self.capacity - self.allocated; r } - #[doc = " Total pool capacity in blocks."] + /// Total pool capacity in blocks. pub fn capacity_get(&self) -> u32 { self.capacity } - #[doc = " Block size in bytes."] + /// Block size in bytes. pub fn block_size_get(&self) -> u32 { self.block_size } - #[doc = " Total pool size in bytes (capacity * block_size)."] - #[doc = " MP6: overflow check."] + /// Total pool size in bytes (capacity * block_size). + /// MP6: overflow check. pub fn total_size(&self) -> Option { let cap64: u64 = self.capacity as u64; let bs64: u64 = self.block_size as u64; - #[allow(clippy::arithmetic_side_effects)] - let total: u64 = cap64 * bs64; - if total > u32::MAX as u64 { - None - } else { - Some(total as u32) - } + let total: u64 = match cap64.checked_mul(bs64) { + Some(v) => v, + None => return None, + }; + if total > u32::MAX as u64 { None } else { Some(total as u32) } } - #[doc = " Check if the pool is full."] + /// Check if the pool is full. pub fn is_full(&self) -> bool { self.allocated == self.capacity } - #[doc = " Check if the pool is empty (no blocks allocated)."] + /// Check if the pool is empty (no blocks allocated). pub fn is_empty(&self) -> bool { self.allocated == 0 } diff --git a/plain/src/msgq.rs b/plain/src/msgq.rs index 857198e..db6510a 100644 --- a/plain/src/msgq.rs +++ b/plain/src/msgq.rs @@ -233,11 +233,7 @@ impl MsgQ { } let sum: u64 = self.read_idx as u64 + idx as u64; let max: u64 = self.max_msgs as u64; - if sum < max { - Ok(sum as u32) - } else { - Ok((sum - max) as u32) - } + if sum < max { Ok(sum as u32) } else { Ok((sum - max) as u32) } } /// Purge the queue (reset indices). /// diff --git a/plain/src/pipe.rs b/plain/src/pipe.rs index 2f8f299..039975c 100644 --- a/plain/src/pipe.rs +++ b/plain/src/pipe.rs @@ -83,7 +83,7 @@ impl Pipe { /// Err(ENOMSG) — zero-length write request pub fn write_check(&mut self, request_len: u32) -> Result { if (self.flags & FLAG_RESET) != 0 { - let _ = self.flags; // cleared by verus-strip + self.flags = self.flags; return Err(ECANCELED); } if (self.flags & FLAG_OPEN) == 0 { @@ -97,11 +97,7 @@ impl Pipe { if free == 0 { return Err(EAGAIN); } - let n = if request_len <= free { - request_len - } else { - free - }; + let n = if request_len <= free { request_len } else { free }; #[allow(clippy::arithmetic_side_effects)] { self.used = self.used + n; @@ -131,11 +127,7 @@ impl Pipe { } return Err(EAGAIN); } - let n = if request_len <= self.used { - request_len - } else { - self.used - }; + let n = if request_len <= self.used { request_len } else { self.used }; #[allow(clippy::arithmetic_side_effects)] { self.used = self.used - n; diff --git a/plain/src/priority.rs b/plain/src/priority.rs index 02bc994..24db011 100644 --- a/plain/src/priority.rs +++ b/plain/src/priority.rs @@ -17,11 +17,7 @@ pub struct Priority { impl Priority { /// Create a new priority. Fails if out of range. pub fn new(value: u32) -> Option { - if value < MAX_PRIORITY { - Some(Priority { value }) - } else { - None - } + if value < MAX_PRIORITY { Some(Priority { value }) } else { None } } /// Get the raw priority value. pub fn get(&self) -> u32 { diff --git a/plain/src/ring_buf.rs b/plain/src/ring_buf.rs index fade9fe..c0e8e7a 100644 --- a/plain/src/ring_buf.rs +++ b/plain/src/ring_buf.rs @@ -177,11 +177,7 @@ impl RingBuf { } let sum: u64 = self.head as u64 + idx as u64; let cap: u64 = self.capacity as u64; - if sum < cap { - Ok(sum as u32) - } else { - Ok((sum - cap) as u32) - } + if sum < cap { Ok(sum as u32) } else { Ok((sum - cap) as u32) } } /// Reset the ring buffer (discard all data). /// diff --git a/plain/src/sched.rs b/plain/src/sched.rs index 850ebf4..6e94ad9 100644 --- a/plain/src/sched.rs +++ b/plain/src/sched.rs @@ -32,8 +32,8 @@ //! SC10: current stays if higher priority than candidate (SMP) //! SC11: ties only switch if swap_ok / yield (SMP) //! SC12: current re-queued only if active + not queued + not idle + not MetaIRQ preempted -use crate::error::*; use crate::thread::{Thread, ThreadId, ThreadState}; +use crate::error::*; /// Maximum threads in the run queue. pub const MAX_RUNQ_SIZE: u32 = 64; /// Priority-ordered run queue for the scheduler. @@ -54,11 +54,70 @@ impl RunQueue { pub fn new() -> Self { RunQueue { entries: [ - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, ], len: 0, } @@ -271,11 +330,8 @@ pub fn next_up_smp( Some(mirqp) => current.id == mirqp.id, None => false, }; - let requeue_current = is_switching - && current_is_active - && !current_is_queued - && !is_current_idle - && !is_current_mirq_preempted; + let requeue_current = is_switching && current_is_active && !current_is_queued + && !is_current_idle && !is_current_mirq_preempted; if is_switching { update_metairq_preempt( &chosen, @@ -440,7 +496,10 @@ pub fn sched_resume(state: SchedThreadState) -> Result { /// SC16: abort always succeeds from any non-Dead/non-Aborting state. /// /// The `smp_remote` flag indicates the thread is running on another CPU. -pub fn sched_abort(state: SchedThreadState, smp_remote: bool) -> Result { +pub fn sched_abort( + state: SchedThreadState, + smp_remote: bool, +) -> Result { match state { SchedThreadState::Dead => Err(EINVAL), SchedThreadState::Aborting => Err(EINVAL), diff --git a/plain/src/stack.rs b/plain/src/stack.rs index 77a6695..2b64e3e 100644 --- a/plain/src/stack.rs +++ b/plain/src/stack.rs @@ -54,11 +54,7 @@ impl Stack { /// stack->base = buffer; stack->next = buffer; /// stack->top = buffer + num_entries; pub fn init(capacity: u32) -> Result { - if capacity == 0 { - Err(EINVAL) - } else { - Ok(Stack { capacity, count: 0 }) - } + if capacity == 0 { Err(EINVAL) } else { Ok(Stack { capacity, count: 0 }) } } /// Push an entry onto the stack. /// diff --git a/plain/src/thread_lifecycle.rs b/plain/src/thread_lifecycle.rs index a1303ce..b76ca42 100644 --- a/plain/src/thread_lifecycle.rs +++ b/plain/src/thread_lifecycle.rs @@ -33,7 +33,7 @@ //! TH5: thread count >= 0 (no underflow on exit) //! TH6: no overflow on thread count use crate::error::*; -use crate::priority::{MAX_PRIORITY, Priority}; +use crate::priority::{Priority, MAX_PRIORITY}; /// Maximum number of threads tracked by the system. /// Models CONFIG_MAX_THREAD_BYTES * 8 in Zephyr. pub const MAX_THREADS: u32 = 256; @@ -66,15 +66,7 @@ impl StackInfo { /// new_thread->stack_info.start = (uintptr_t)stack_buf_start; /// new_thread->stack_info.size = stack_buf_size; pub fn init(base: u32, size: u32) -> Result { - if size == 0 { - Err(EINVAL) - } else { - Ok(StackInfo { - base, - size, - usage: 0, - }) - } + if size == 0 { Err(EINVAL) } else { Ok(StackInfo { base, size, usage: 0 }) } } /// Record observed stack usage (watermark update). /// diff --git a/plain/src/timeout.rs b/plain/src/timeout.rs index 90c5040..6a3e7e3 100644 --- a/plain/src/timeout.rs +++ b/plain/src/timeout.rs @@ -175,7 +175,9 @@ impl Timeout { #[allow(clippy::arithmetic_side_effects)] let new_tick = self.current_tick + ticks; self.current_tick = new_tick; - if self.active && self.deadline != K_FOREVER_TICKS && self.deadline <= self.current_tick { + if self.active && self.deadline != K_FOREVER_TICKS + && self.deadline <= self.current_tick + { self.active = false; Ok(true) } else { @@ -206,11 +208,7 @@ impl Timeout { /// timeout.c z_timeout_expires: /// ticks = curr_tick + timeout_rem(timeout); pub fn expires(&self) -> u64 { - if self.active { - self.deadline - } else { - self.current_tick - } + if self.active { self.deadline } else { self.current_tick } } /// Check if the timeout is active. pub fn is_active(&self) -> bool { diff --git a/plain/src/userspace.rs b/plain/src/userspace.rs index 3e3e98a..96d88a2 100644 --- a/plain/src/userspace.rs +++ b/plain/src/userspace.rs @@ -234,7 +234,6 @@ impl KernelObject { is_supervisor: bool, init_check: InitCheck, ) -> Result<(), i32> { - // US4: type validation — use match to avoid PartialEq on enums let type_ok = match expected_type { ObjType::Any => true, ObjType::Thread => matches!(self.obj_type, ObjType::Thread), diff --git a/plain/src/wait_queue.rs b/plain/src/wait_queue.rs index 11cbf15..059c0b4 100644 --- a/plain/src/wait_queue.rs +++ b/plain/src/wait_queue.rs @@ -13,8 +13,8 @@ //! - unpend_first returns the highest priority thread //! - No thread appears twice in the queue //! - pend/unpend maintain sorted invariant -use crate::priority::MAX_PRIORITY; use crate::thread::{Thread, ThreadId, ThreadState}; +use crate::priority::MAX_PRIORITY; /// Maximum threads that can be waiting on a single kernel object. /// Bounded for verification tractability. pub const MAX_WAITERS: u32 = 64; @@ -39,11 +39,70 @@ impl WaitQueue { pub fn new() -> Self { WaitQueue { entries: [ - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, None, None, None, None, None, None, - None, None, None, None, None, None, None, None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, + None, ], len: 0, } diff --git a/plain/src/work.rs b/plain/src/work.rs index 5ef2ffa..b622d65 100644 --- a/plain/src/work.rs +++ b/plain/src/work.rs @@ -67,7 +67,8 @@ impl WorkItem { /// Corresponds to k_work_init() (work.c:153-161). /// WK1: produces IDLE state. pub fn init() -> WorkItem { - WorkItem { flags: 0 } + let w = WorkItem { flags: 0 }; + w } /// Get the busy status flags. /// @@ -115,6 +116,7 @@ impl WorkItem { return 0; } let was_running = (self.flags & FLAG_RUNNING) != 0; + let old_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = self.flags | FLAG_QUEUED; @@ -126,6 +128,7 @@ impl WorkItem { /// Dequeues the item and marks it as running. /// Precondition: item must be queued. pub fn start_running(&mut self) { + let old_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = (self.flags & !FLAG_QUEUED) | FLAG_RUNNING; @@ -136,6 +139,7 @@ impl WorkItem { /// Clears the RUNNING flag. /// Precondition: item must be running. pub fn finish_running(&mut self) { + let old_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = self.flags & !FLAG_RUNNING; @@ -150,12 +154,14 @@ impl WorkItem { /// /// Returns the busy flags after cancellation attempt. pub fn cancel(&mut self) -> u8 { + let old_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = self.flags & !FLAG_QUEUED; } let busy = self.flags & BUSY_MASK; if busy != 0 { + let mid_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = self.flags | FLAG_CANCELING; @@ -168,6 +174,7 @@ impl WorkItem { /// Models finalize_cancel_locked() (work.c:128-151). /// Clears the CANCELING flag. Called when the running handler completes. pub fn finish_cancel(&mut self) { + let old_flags = self.flags; #[allow(clippy::arithmetic_side_effects)] { self.flags = self.flags & !FLAG_CANCELING; diff --git a/renode/mps2_an521_sem.robot b/renode/mps2_an521_sem.robot new file mode 100644 index 0000000..3e5d85f --- /dev/null +++ b/renode/mps2_an521_sem.robot @@ -0,0 +1,15 @@ +*** Variables *** +# MPS2/AN521 Cortex-M33 uses UART0 for Zephyr console +${UART} sysbus.uart0 + +*** Keywords *** +Create Machine + Execute Command mach create + Execute Command machine LoadPlatformDescription @platforms/boards/mps2-an521.repl + Execute Command sysbus LoadELF @%{ELF} + +*** Test Cases *** +Should Pass Gale Semaphore Tests On Cortex-M33 + Create Machine + Create Terminal Tester ${UART} defaultPauseEmulation=true + Wait For Line On Uart PROJECT EXECUTION SUCCESSFUL timeout=120 diff --git a/renode/stm32f4_sem.robot b/renode/stm32f4_sem.robot index e27f018..c7af7d0 100644 --- a/renode/stm32f4_sem.robot +++ b/renode/stm32f4_sem.robot @@ -6,7 +6,7 @@ ${UART} sysbus.usart2 Create Machine Execute Command mach create Execute Command machine LoadPlatformDescription @platforms/boards/stm32f4_discovery.repl - Execute Command sysbus LoadELF ${ELF} + Execute Command sysbus LoadELF @%{ELF} *** Test Cases *** Should Pass Gale Semaphore Tests On Cortex-M4F diff --git a/renode/stm32l552_sem.robot b/renode/stm32l552_sem.robot index ab18f4f..f744b78 100644 --- a/renode/stm32l552_sem.robot +++ b/renode/stm32l552_sem.robot @@ -5,8 +5,8 @@ ${UART} sysbus.lpuart1 *** Keywords *** Create Machine Execute Command mach create - Execute Command machine LoadPlatformDescription @platforms/cpus/stm32l552.repl - Execute Command sysbus LoadELF ${ELF} + Execute Command machine LoadPlatformDescription @tests/platforms/nucleo_l552ze_q/nucleo_l552ze_q_ns.repl + Execute Command sysbus LoadELF @%{ELF} *** Test Cases *** Should Pass Gale Semaphore Tests On Cortex-M33 diff --git a/renode/zynqmp_r5_sem.robot b/renode/zynqmp_r5_sem.robot index fff5e82..a5715f2 100644 --- a/renode/zynqmp_r5_sem.robot +++ b/renode/zynqmp_r5_sem.robot @@ -9,7 +9,7 @@ Create Machine # - Halts all A53 cores # - Enables RPU core 0 # - Loads the ELF onto rpu0 - Execute Command set bin ${ELF} + Execute Command set bin @%{ELF} Execute Command include @scripts/single-node/zynqmp_zephyr.resc Execute Command machine SetSerialExecution True diff --git a/tools/verus-strip/src/lib.rs b/tools/verus-strip/src/lib.rs index 4971d70..0b73a0c 100644 --- a/tools/verus-strip/src/lib.rs +++ b/tools/verus-strip/src/lib.rs @@ -189,11 +189,6 @@ fn strip_body(body: &str) -> String { // Check for verus clause keywords: requires, ensures, invariant, decreases if is_verus_clause_at(&trees, i) { - let keyword = if let TokenTree::Ident(id) = &trees[i] { - id.to_string() - } else { - String::new() - }; let skip_to = skip_clause(&trees, i); trim_trailing_whitespace(&mut out); i = skip_to; @@ -214,6 +209,47 @@ fn strip_body(body: &str) -> String { continue; } + // Check for inline `proof { ... }` blocks inside exec function bodies. + // These appear as `Ident("proof")` followed directly by a brace group. + // Distinct from `proof fn` (which is handled by try_skip_verus_item). + if let TokenTree::Ident(id) = &trees[i] { + if id.to_string() == "proof" { + if let Some(TokenTree::Group(g)) = trees.get(i + 1) { + if g.delimiter() == Delimiter::Brace { + // Inline proof block — drop both the keyword and the body + trim_trailing_whitespace(&mut out); + i += 2; + continue; + } + } + } + } + + // Check for `let ghost x = ...;` — ghost variable declarations. + // Strip the entire statement (up to and including the semicolon). + if let TokenTree::Ident(id) = &trees[i] { + if id.to_string() == "let" { + if let Some(TokenTree::Ident(next)) = trees.get(i + 1) { + if next.to_string() == "ghost" { + // Skip: let ghost ... ; + let mut j = i + 2; + while j < trees.len() { + if let TokenTree::Punct(p) = &trees[j] { + if p.as_char() == ';' { + j += 1; + break; + } + } + j += 1; + } + trim_trailing_whitespace(&mut out); + i = j; + continue; + } + } + } + } + // Check for named return type: -> (name: Type) if is_arrow_at(&trees, i) { if let Some((replacement, skip_to)) = try_strip_named_return(&trees, i) { @@ -313,38 +349,6 @@ fn collect_idents(trees: &[TokenTree], pos: usize) -> Vec { } /// Check if the Brace group at `pos` is an impl or mod body -/// (as opposed to a function body, match arm, loop body, etc.). -/// We check by looking backwards for `impl` or `mod` keywords. -fn is_impl_or_mod_body(trees: &[TokenTree], pos: usize) -> bool { - // Walk backwards to find the nearest ident before this brace group. - // Skip over type parameters, where clauses, etc. - let mut j = pos; - while j > 0 { - j -= 1; - match &trees[j] { - TokenTree::Ident(id) => { - let s = id.to_string(); - if s == "impl" || s == "mod" { - return true; - } - // If we hit fn, struct, enum, etc. — not an impl body - if is_item_keyword(&s) { - return false; - } - // Other idents (type names, where clause) — keep looking - } - TokenTree::Group(_) => { - // Skip over generic params, where clauses - } - TokenTree::Punct(_) => { - // Skip punctuation - } - _ => {} - } - } - false -} - fn is_item_keyword(s: &str) -> bool { matches!(s, "pub" | "fn" | "struct" | "enum" | "impl" | "use" | "const" | "type" | "trait" | "mod" | "static" | "unsafe" | "extern") @@ -379,20 +383,6 @@ fn is_verus_clause_at(trees: &[TokenTree], pos: usize) -> bool { } } -/// Skip a loop invariant/decreases clause. Returns the index of the -/// loop body brace group. Takes the FIRST Brace group after the keyword. -fn skip_clause_simple(trees: &[TokenTree], pos: usize) -> usize { - let mut j = pos + 1; - while j < trees.len() { - if let TokenTree::Group(g) = &trees[j] { - if g.delimiter() == Delimiter::Brace { - return j; - } - } - j += 1; - } - j -} /// Skip a requires/ensures/invariant/decreases clause. Returns the index /// of the body brace group (function body or loop body) which should be emitted. @@ -1122,4 +1112,46 @@ impl Foo { assert!(!result.contains("#[cfg(not(verus_keep_ghost))]"), "cfg not removed"); assert!(result.contains("pub fn foo"), "missing foo fn"); } + + #[test] + fn test_strip_inline_proof_block() { + let body = r#" +pub fn classify(hfsr: u32, cfsr: u32) -> u32 { + if hfsr != 0 { + proof { + assert(hfsr > 0u32) by (bit_vector) requires hfsr != 0u32; + } + 1u32 + } else { + proof { + assert(cfsr == 0u32) by (bit_vector); + } + 0u32 + } +} +"#; + let result = strip_body(body); + assert!(!result.contains("proof {"), "proof block not stripped: {result}"); + assert!(!result.contains("assert("), "assert not stripped: {result}"); + assert!(result.contains("fn classify"), "missing classify fn: {result}"); + assert!(result.contains("1u32"), "missing 1u32: {result}"); + assert!(result.contains("0u32"), "missing 0u32: {result}"); + } + + #[test] + fn test_strip_let_ghost() { + let body = r#" +pub fn add_partition(&mut self, part: u32) -> i32 { + let ghost orig = self.count; + let real_orig = self.count; + self.count = self.count + part; + 0i32 +} +"#; + let result = strip_body(body); + assert!(!result.contains("let ghost"), "let ghost not stripped: {result}"); + assert!(!result.contains("ghost orig"), "ghost var not stripped: {result}"); + assert!(result.contains("real_orig"), "real var wrongly stripped: {result}"); + assert!(result.contains("fn add_partition"), "missing fn: {result}"); + } } diff --git a/tools/verus-strip/tests/gate.rs b/tools/verus-strip/tests/gate.rs index 1def21a..c15391c 100644 --- a/tools/verus-strip/tests/gate.rs +++ b/tools/verus-strip/tests/gate.rs @@ -75,3 +75,52 @@ fn plain_matches_stripped_src() { ); } } + +/// Gate for standalone Rocq files (plain/*.rs) — generated with --standalone mode. +/// These are used directly by rocq_of_rust for theorem proving. +const STANDALONE_FILES: &[&str] = &[ + "sem", "mutex", "condvar", "msgq", "stack", "pipe", "timer", "event", "mem_slab", +]; + +#[test] +fn plain_standalone_matches_stripped_standalone() { + let root = find_gale_root(); + let mut failures = Vec::new(); + + for name in STANDALONE_FILES { + let src_path = root.join(format!("src/{name}.rs")); + let plain_path = root.join(format!("plain/{name}.rs")); + + let src_content = fs::read_to_string(&src_path) + .unwrap_or_else(|e| panic!("Cannot read {}: {e}", src_path.display())); + let plain_content = fs::read_to_string(&plain_path) + .unwrap_or_else(|e| panic!("Cannot read {}: {e}", plain_path.display())); + + let stripped = verus_strip::strip_file(&src_content); + let standalone = verus_strip::make_standalone(&stripped.output); + + if standalone != plain_content { + let s_lines: Vec<&str> = standalone.lines().collect(); + let p_lines: Vec<&str> = plain_content.lines().collect(); + let first_diff = s_lines.iter().zip(p_lines.iter()) + .enumerate() + .find(|(_, (a, b))| a != b) + .map(|(i, (a, b))| format!(" line {}: stripped={:?} vs plain={:?}", i + 1, a, b)) + .unwrap_or_else(|| { + format!(" length: stripped={} vs plain={} lines", + s_lines.len(), p_lines.len()) + }); + failures.push(format!("{name}.rs:\n{first_diff}")); + } + } + + if !failures.is_empty() { + panic!( + "plain/ standalone files are out of sync. Regenerate with:\n\ + for f in {}; do verus-strip --standalone src/$f.rs -o plain/$f.rs; done\n\n\ + Divergences:\n{}", + STANDALONE_FILES.join(" "), + failures.join("\n"), + ); + } +}