From e6bc33f40167d53860c24898b6415c5027b1016b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 15 May 2024 18:16:59 -0700 Subject: [PATCH] Create first version of ghost state RFC --- rfc/src/SUMMARY.md | 1 + rfc/src/rfcs/0010-ghost-state.md | 166 +++++++++++++++++++++++++++++++ 2 files changed, 167 insertions(+) create mode 100644 rfc/src/rfcs/0010-ghost-state.md diff --git a/rfc/src/SUMMARY.md b/rfc/src/SUMMARY.md index f8d5dc5639f5..207d8dfa4964 100644 --- a/rfc/src/SUMMARY.md +++ b/rfc/src/SUMMARY.md @@ -15,3 +15,4 @@ - [0007-global-conditions](rfcs/0007-global-conditions.md) - [0008-line-coverage](rfcs/0008-line-coverage.md) - [0009-function-contracts](rfcs/0009-function-contracts.md) +- [0010-ghost-state](rfcs/0010-ghost-state.md) diff --git a/rfc/src/rfcs/0010-ghost-state.md b/rfc/src/rfcs/0010-ghost-state.md new file mode 100644 index 000000000000..fefead6d5a4d --- /dev/null +++ b/rfc/src/rfcs/0010-ghost-state.md @@ -0,0 +1,166 @@ +- **Feature Name:** Ghost State (`ghost-state`) +- **Feature Request Issue:** [#3184](https://github.com/model-checking/kani/issues/3184) +- **RFC PR:** +- **Status:** Unstable +- **Version:** 0 +- **Proof-of-concept:** N/A + +------------------- + +## Summary + +Add support to ghost state to allow users to track metadata useful for verification purpose without extra +runtime overhead. + +## User Impact + +TODO + +## User Experience + +We propose that ghost state to be implemented using a trait which is extended by Kani. + +```rust +/// Trait that indicates a type has an associated ghost code of type `S`. +/// +/// A type can have many multiple implementations, each will be mapped to a different ghost state. +pub trait GhostState: Sized + GhostStateExt {} + +/// Trait that specifies types that are safe to be used as a ghost value. +/// +/// A ghost value has to conform to the following existing restrictions: +/// - Type size is 8 bits. +/// - The byte `0` is a valid representation of this type. +/// - A ghost state is always initialized with the byte `0`. +pub unsafe trait GhostValue: Sized {} + +/// These functions are automatically implemented +pub trait GhostStateExt { + /// Set the value of a ghost state. + fn set_ghost_state(&self, value: S); + + /// Get the value of the ghost state. + fn ghost_state(&self) -> S; + + /// Add a dummy function with a private structure so this trait cannot be overwritten. + #[doc(hidden)] + fn private(&self, _: Internal); +} +``` + +For example, let's say a user wants to check their union have been initialized, together with +which variant. + +```rust +union Size { + unsigned: usize, + signed: isize, +} + +/// Declare ghost state to track initialization. +impl kani::GhostState for Size {} + +/// Declare ghost state to track which variant is used. +impl kani::GhostState for Size {} + +/// Declare the shadow memory type and declare that it can be used as `GhostValue` +struct IsInit(bool); + +unsafe impl kani::GhostValue for IsInit {} + +struct IsSigned(bool); + +unsafe impl kani::GhostValue for IsSigned {} + +impl Size { + /// Specify safety contract. + #[kani::requires(self.ghost_state::< IsInit > () && ! self.ghost_state::< IsSigned > ())] + pub unsafe fn unsigned(&self) -> usize { + unsafe { self.unsigned } + } + + /// Show how ghost_state can also be used outside of contracts. + pub fn set_unsigned(&self, val: usize) { + self.unsigned = val; + self.set_ghost_state::(true); + self.set_ghost_state::(false); + } +} +``` + +One limitation today is that ghost state cannot be implemented for ZST types. +Kani compiler will generate an unsupported feature for any reachable occurrence. + +## Software Design + +The trait `GhostStateExt` will contain an automatic implementation for any type `T` that implements `GhostState` +that cannot be overridden. +For that, we added the `private` function, and we will include the following implementation: + +```rust +impl GhostStateExt for T { + #[rustc_diagnostic_item = "KaniSetGhost"] + fn set_ghost_state(&self, value: S) { + kani_intrinsic() + } + + #[rustc_diagnostic_item = "KaniGetGhost"] + fn ghost_state(&self) -> S { + kani_intrinsic() + } + + fn private(&self, _: Internal) {} +} +``` + +Since CBMC shadow memory supports multiple maps which are indexed by a name, we are planning to instantiate one +map per reachable GhostState implementation. +This would avoid value collision. +We could eventually simplify CBMC to avoid using the "OR" logic over the members of a structure. + +## Rationale and alternatives + +The main motivation to implement this in Kani today is to allow more sophisticated safety contracts. +Not doing this will likely limit the expressiveness of UB detection to things that only Kani implements. + +The trait based implementation will also allow us to implement ghost state for things like reference and pointers. + +Another approach we explored was to use a ZST structure, that kani-compiler is aware of. +The compiler would encode dereference and assignments to object of this type by mapping to the shadow memory. + +Something like: + +```rust +struct GhostState(PhantomData) where T: Default + GhostValue; + +impl GhostState { + fn new(val: T) -> Self { /* ... */ } + fn set(&self, val: T) { /* ... */ } + fn get(&self) -> T { /* ... */ } +} + +struct Dummy { + field1: u8, + field2: u8, + ghost_state: GhostState, +} + +impl Dummy { + fn new() -> Dummy { + Dummy { field1: 0, field2: 0, ghost: GhostState::new(false) } + } +} +``` + +One problem with this approach is that CBMC ghost code cannot be mapped to ZST address. + +## Open questions + +- This is a highly experimental feature, and it might be worth revisiting the solution once we get some user + perspective. +- What should be the implementation of ghost state for concrete playback? One possible approach is to implement + memory with a global hash map. + For initial implementations, I would prefer keeping it simple and maybe just add print statements. + +## Out of scope / Future Improvements +