Mark APIs as unstable

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -310,8 +310,6 @@ impl GotocHook for PointerOffset {
     }
 }
 
-
-
 struct RustAlloc;
 // Removing this hook causes regression failures.
 // https://github.com/model-checking/kani/issues/1170

kani_metadata/src/unstable.rs

@@ -87,6 +87,8 @@ pub enum UnstableFeature {
     /// Automatically check that no invalid value is produced which is considered UB in Rust.
     /// Note that this does not include checking uninitialized value.
     ValidValueChecks,
+    /// Ghost state and shadow memory APIs
+    GhostState,
 }
 
 impl UnstableFeature {

library/kani/src/shadow.rs

@@ -13,11 +13,22 @@ pub struct ShadowMem<T: Copy> {
 }
 
 impl<T: Copy> ShadowMem<T> {
+    /// Create a new shadow memory instance initialized with the given value
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
     pub const fn new(val: T) -> Self {
         Self { mem: [[val; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS] }
     }
 
     /// Get the shadow memory value of the given pointer
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
     pub fn get<U>(&self, ptr: *const U) -> T {
         let obj = crate::mem::pointer_object(ptr);
         let offset = crate::mem::pointer_offset(ptr);
@@ -27,6 +38,11 @@ impl<T: Copy> ShadowMem<T> {
     }
 
     /// Set the shadow memory value of the given pointer
+    #[crate::unstable(
+        feature = "ghost-state",
+        issue = 3184,
+        reason = "experimental ghost state/shadow memory API"
+    )]
     pub fn set<U>(&mut self, ptr: *const U, val: T) {
         let obj = crate::mem::pointer_object(ptr);
         let offset = crate::mem::pointer_offset(ptr);

tests/expected/shadow/uninit_array/test.rs

@@ -1,13 +1,14 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
 
 // This is a basic test for the shadow memory implementation.
 // It checks that shadow memory can be used to track whether a memory location
 // is initialized.
 
 use std::alloc::{alloc, dealloc, Layout};
 
-static mut SM: kani::shadow::ShadowMem::<bool> = kani::shadow::ShadowMem::new(false);
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
 fn write(ptr: *mut i8, offset: usize, x: i8) {
     unsafe {

tests/expected/shadow/unsupported_num_objects/test.rs

@@ -1,10 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
 
 // This test checks the maximum number of objects supported by Kani's shadow
 // memory model (currently 1024)
 
-static mut SM: kani::shadow::ShadowMem::<bool> = kani::shadow::ShadowMem::new(false);
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
 fn check_max_objects<const N: usize>() {
     let mut i = 0;
@@ -15,19 +16,13 @@ fn check_max_objects<const N: usize>() {
     // - the object ID for `i`
     while i < N {
         let x = i;
-        assert_eq!(
-            kani::mem::pointer_object(&x as *const usize),
-            i + 2
-        );
+        assert_eq!(kani::mem::pointer_object(&x as *const usize), i + 2);
         i += 1;
     }
 
     // create a new object whose ID is `N` + 2
     let x = 42;
-    assert_eq!(
-        kani::mem::pointer_object(&x as *const i32),
-        N + 2
-    );
+    assert_eq!(kani::mem::pointer_object(&x as *const i32), N + 2);
     // the following call to `set` would fail if the object ID for `x` exceeds
     // the maximum allowed by Kani's shadow memory model
     unsafe {

tests/expected/shadow/unsupported_object_size/test.rs

@@ -1,10 +1,11 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
 
 // This test checks the maximum object size supported by Kani's shadow
 // memory model (currently 64)
 
-static mut SM: kani::shadow::ShadowMem::<bool> = kani::shadow::ShadowMem::new(false);
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
 
 fn check_max_objects<const N: usize>() {
     let arr: [u8; N] = [0; N];