From d9a5005f97a37ec80ac4712cabfc546dc2a32fbb Mon Sep 17 00:00:00 2001 From: leynos Date: Sat, 13 Jun 2026 17:07:18 +0200 Subject: [PATCH] Add Kani proofs for MacroStateGuard pointer lifecycle (#313) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `MacroInstance::new` transmutes a `Captured` to `Captured<'static>`, and `MacroStateGuard` stores it as a `NonNull>` while being declared `Send + Sync`. Neither the pointer lifecycle nor the thread-safety markers had formal verification. Extract the raw-pointer dance into payload-agnostic helpers, `heap_leak_non_null` and `reclaim_heap_non_null`, which `MacroStateGuard::new` and its `Drop` now use verbatim. Add a `#[cfg(kani)]` module with four proofs: - `macro_state_guard_ptr_is_non_null` — the leaked pointer is non-null and dereferences to the stored value; - `macro_state_guard_drop_is_safe` — the Box → raw → Box round-trip neither leaks nor double-frees; - `macro_instance_is_send` / `macro_instance_is_sync` — compile-time assertions of the marker traits. `Captured`/`State` are too complex for Kani to construct, so the pointer proofs run the real helpers over a small Kani-constructible stand-in payload (the unsafe operations are independent of payload type beyond non-zero size). Register `cfg(kani)` in `Cargo.toml` so ordinary builds do not flag the gated module, extend the `MacroInstance::new` SAFETY comment to reference the proofs by name, and refresh the formal-verification section of the developers' guide. Verified locally with Kani 0.67.0: 4 harnesses, 0 failures. --- Cargo.toml | 3 + docs/developers-guide.md | 13 ++-- src/manifest/jinja_macros/cache.rs | 109 ++++++++++++++++++++++++++--- 3 files changed, 113 insertions(+), 12 deletions(-) diff --git a/Cargo.toml b/Cargo.toml index 13dbe4be..1805599d 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -134,6 +134,9 @@ result_large_err = "deny" unknown_lints = "deny" renamed_and_removed_lints = "deny" missing_docs = "deny" +# `cfg(kani)` is set only by the Kani model checker (`make kani`/`make +# kani-full`); register it so ordinary builds do not flag the gated proofs. +unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] } [lints.rustdoc] missing_crate_level_docs = "deny" diff --git a/docs/developers-guide.md b/docs/developers-guide.md index 858e5efb..2265f74e 100644 --- a/docs/developers-guide.md +++ b/docs/developers-guide.md @@ -152,11 +152,16 @@ non-zero exit status on failure. Use the Make targets for day-to-day formal-verification checks: -- `make kani-check` runs the fast local version check used by `formal-pr`. - Until roadmap item `4.2.*` adds substantive proof harnesses, this check +- `make kani-check` runs the fast local version check used by `formal-pr`. It verifies the installed `cargo kani` command matches `tools/kani/VERSION`. -- `make kani-full` is reserved for the full Kani proof suite once harnesses - exist. Today it invokes `cargo kani` without additional smoke flags. +- `make kani-full` runs the full Kani proof suite (`cargo kani`). The first + proof harnesses live in a `#[cfg(kani)]` module at the bottom of + `src/manifest/jinja_macros/cache.rs`, verifying the `MacroStateGuard` + pointer lifecycle (`macro_state_guard_ptr_is_non_null`, + `macro_state_guard_drop_is_safe`) and the `Send`/`Sync` soundness of the + cached macro instance (`macro_instance_is_send`, `macro_instance_is_sync`). + The `kani` cfg is registered in `Cargo.toml` under `[lints.rust]` so the + gated proofs do not trip `unexpected_cfgs` in ordinary builds. - `make formal-pr` aliases the pull-request formal-verification smoke path. - `make install-verus` and `make verus` delegate to `rust-prover-tools` for the optional Verus installer and proof runner. These targets are not part of diff --git a/src/manifest/jinja_macros/cache.rs b/src/manifest/jinja_macros/cache.rs index e99ca567..af7f5442 100644 --- a/src/manifest/jinja_macros/cache.rs +++ b/src/manifest/jinja_macros/cache.rs @@ -139,7 +139,15 @@ impl MacroInstance { })?; // SAFETY: `register_macro` requires an `Environment<'static>`, so the template // bytecode and captured output outlive the cached state stored in the macro - // instance. + // instance. The precondition is that the environment — and therefore the + // compiled template instructions backing `captured` — outlives this + // `MacroInstance`; manifest macros remain registered for the whole build, + // so this holds. The pointer lifecycle of the resulting + // `Captured<'static>` (heap leak, NonNull invariant, single reclaim) is + // verified by the Kani proofs `macro_state_guard_ptr_is_non_null` and + // `macro_state_guard_drop_is_safe`; the `Send`/`Sync` soundness of the + // cached instance is verified by `macro_instance_is_send` and + // `macro_instance_is_sync`. let captured_static: Captured<'static> = unsafe { std::mem::transmute(captured) }; Ok(Self { state: MacroStateGuard::new(captured_static), @@ -169,12 +177,9 @@ struct MacroStateGuard { impl MacroStateGuard { fn new(captured: Captured<'static>) -> Self { - let boxed = Box::new(captured); - let ptr = Box::into_raw(boxed); - // SAFETY: Box::into_raw never returns null for non-ZST types. Captured - // is non-zero-sized so the pointer is guaranteed valid. - let ptr_non_null = unsafe { NonNull::new_unchecked(ptr) }; - Self { ptr: ptr_non_null } + Self { + ptr: heap_leak_non_null(captured), + } } fn as_ref(&self) -> &State<'static, 'static> { @@ -184,10 +189,37 @@ impl MacroStateGuard { impl Drop for MacroStateGuard { fn drop(&mut self) { - unsafe { drop(Box::from_raw(self.ptr.as_ptr())) } + // SAFETY: `self.ptr` was produced by `heap_leak_non_null` in `new` + // and is reclaimed exactly once here, so the round-trip neither leaks + // nor double-frees. Verified by `macro_state_guard_drop_is_safe`. + unsafe { reclaim_heap_non_null(self.ptr) } } } +/// Box `value` on the heap and leak it as a non-null pointer. +/// +/// Mirrors the ownership transfer performed by [`MacroStateGuard::new`]: +/// `Box::into_raw` never returns null for a non-zero-sized type, so the +/// `NonNull` invariant holds. The caller becomes responsible for reclaiming +/// the allocation exactly once via [`reclaim_heap_non_null`]. +fn heap_leak_non_null(value: T) -> NonNull { + let ptr = Box::into_raw(Box::new(value)); + // SAFETY: `Box::into_raw` never returns null for a non-ZST allocation. + // Verified by `macro_state_guard_ptr_is_non_null`. + unsafe { NonNull::new_unchecked(ptr) } +} + +/// Reclaim and drop a pointer previously produced by [`heap_leak_non_null`]. +/// +/// # Safety +/// +/// `ptr` must have come from [`heap_leak_non_null`] and must not have been +/// reclaimed already; the allocation is freed here exactly once. +unsafe fn reclaim_heap_non_null(ptr: NonNull) { + // SAFETY: upheld by the caller's contract; `ptr` owns a live `Box`. + unsafe { drop(Box::from_raw(ptr.as_ptr())) } +} + unsafe impl Send for MacroStateGuard {} unsafe impl Sync for MacroStateGuard {} @@ -256,3 +288,64 @@ impl Object for CallerAdapter { self.caller.call(state, args) } } + +/// Formal verification of `MacroStateGuard`'s pointer lifecycle and the +/// `Send`/`Sync` soundness of the cached macro instance. +/// +/// `Captured<'static>` and `State<'static, 'static>` are far too complex for +/// Kani to construct or unwind, so the pointer-mechanics proofs run over the +/// payload-agnostic helpers `heap_leak_non_null` / `reclaim_heap_non_null` +/// (which `MacroStateGuard::new` and its `Drop` use verbatim) with a small, +/// Kani-constructible stand-in payload. The unsafe operations being verified — +/// `Box::into_raw` → `NonNull::new_unchecked` → `Box::from_raw` — are +/// independent of the payload type beyond its being non-zero-sized, so a +/// representative payload proves the pattern. +#[cfg(kani)] +mod kani_proofs { + use super::{MacroInstance, heap_leak_non_null, reclaim_heap_non_null}; + + /// Non-zero-sized stand-in for `Captured<'static>` that Kani can build. + #[derive(Clone, Copy, PartialEq, Eq)] + struct ModelCaptured { + tag: u64, + } + + /// The `NonNull` invariant holds after construction: the leaked pointer is + /// never null and dereferences to the original value. + #[kani::proof] + fn macro_state_guard_ptr_is_non_null() { + let tag: u64 = kani::any(); + let ptr = heap_leak_non_null(ModelCaptured { tag }); + // `NonNull` cannot be null by construction; reading back the value + // confirms the pointer targets the live allocation. + // SAFETY: `ptr` owns a live `Box` produced just above. + let observed = unsafe { ptr.as_ref().tag }; + assert_eq!(observed, tag); + // Reclaim to keep the proof free of leaks. + // SAFETY: `ptr` came from `heap_leak_non_null` and is reclaimed once. + unsafe { reclaim_heap_non_null(ptr) }; + } + + /// The Box → raw pointer → Box round-trip used by `new` and `Drop` neither + /// leaks nor double-frees. Kani's memory model flags either fault. + #[kani::proof] + fn macro_state_guard_drop_is_safe() { + let ptr = heap_leak_non_null(ModelCaptured { tag: kani::any() }); + // SAFETY: single reclaim of a pointer from `heap_leak_non_null`. + unsafe { reclaim_heap_non_null(ptr) }; + } + + /// `MacroInstance` is `Send`, as required for registration with MiniJinja. + #[kani::proof] + fn macro_instance_is_send() { + const fn assert_send() {} + assert_send::(); + } + + /// `MacroInstance` is `Sync`, as required for registration with MiniJinja. + #[kani::proof] + fn macro_instance_is_sync() { + const fn assert_sync() {} + assert_sync::(); + } +}