Add tests that check the limits of the shadow memory model

library/kani/src/shadow.rs

@@ -33,24 +33,32 @@ impl ShadowMem {
     }
 }
 
+const MAX_NUM_OBJECTS_ASSERT_MSG: &str = "The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)";
+const MAX_OBJECT_SIZE_ASSERT_MSG: &str =
+    "The object size exceeds the maximum size supported by Kani's shadow memory model (64)";
+
 /// # Safety
 ///
 /// `ptr` must be valid
 pub unsafe fn read(sm: &[[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8) -> bool {
     let obj = unsafe { __KANI_pointer_object(ptr) };
     let offset = unsafe { __KANI_pointer_offset(ptr) };
-    assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model ({MAX_NUM_OBJECTS})");
-    assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model ({MAX_OBJECT_SIZE})");
+    crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+    crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
     sm[obj][offset]
 }
 
 /// # Safety
 ///
 /// `ptr` must be valid
-pub unsafe fn write(sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS], ptr: *const u8, val: bool) {
+pub unsafe fn write(
+    sm: &mut [[bool; MAX_OBJECT_SIZE]; MAX_NUM_OBJECTS],
+    ptr: *const u8,
+    val: bool,
+) {
     let obj = unsafe { __KANI_pointer_object(ptr) };
     let offset = unsafe { __KANI_pointer_offset(ptr) };
-    assert!(obj < MAX_NUM_OBJECTS, "Object index exceeds the maximum number of objects supported by Kani's shadow memory model (1024)");
-    assert!(offset < MAX_OBJECT_SIZE, "Offset into object exceeds the maximum object size supported by Kani's shadow memory model (64)");
+    crate::assert(obj < MAX_NUM_OBJECTS, MAX_NUM_OBJECTS_ASSERT_MSG);
+    crate::assert(offset < MAX_OBJECT_SIZE, MAX_OBJECT_SIZE_ASSERT_MSG);
     sm[obj][offset] = val;
 }

tests/expected/shadow/unsupported_num_objects/expected

@@ -0,0 +1,3 @@
+Failed Checks: The number of objects exceeds the maximum number supported by Kani's shadow memory model (1024)
+Verification failed for - check_max_objects_fail
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/shadow/unsupported_num_objects/test.rs

@@ -0,0 +1,46 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks the maximum number of objects supported by Kani's shadow
+// memory model (currently 1024)
+
+static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new();
+
+fn check_max_objects<const N: usize>() {
+    let mut i = 0;
+    // A dummy loop that creates `N`` objects.
+    // After the loop, CBMC's object ID counter should be at `N` + 2:
+    // - `N` created in the loop +
+    // - the NULL pointer whose object ID is 0, and
+    // - the object ID for `i`
+    while i < N {
+        let x = i;
+        assert_eq!(
+            unsafe { kani::shadow::__KANI_pointer_object(&x as *const usize as *const u8) },
+            i + 2
+        );
+        i += 1;
+    }
+
+    // create a new object whose ID is `N` + 2
+    let x = 42;
+    assert_eq!(
+        unsafe { kani::shadow::__KANI_pointer_object(&x as *const i32 as *const u8) },
+        N + 2
+    );
+    // the following call to `set_init` would fail if the object ID for `x`
+    // exceeds the maximum allowed by Kani's shadow memory model
+    unsafe {
+        SM.set_init(&x as *const i32 as *const u8, true);
+    }
+}
+
+#[kani::proof]
+fn check_max_objects_pass() {
+    check_max_objects::<1021>();
+}
+
+#[kani::proof]
+fn check_max_objects_fail() {
+    check_max_objects::<1022>();
+}

tests/expected/shadow/unsupported_object_size/expected

@@ -0,0 +1,3 @@
+Failed Checks: The object size exceeds the maximum size supported by Kani's shadow memory model (64)
+Verification failed for - check_max_object_size_fail
+Complete - 1 successfully verified harnesses, 1 failures, 2 total.

tests/expected/shadow/unsupported_object_size/test.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks the maximum object size supported by Kani's shadow
+// memory model (currently 64)
+
+static mut SM: kani::shadow::ShadowMem = kani::shadow::ShadowMem::new();
+
+fn check_max_objects<const N: usize>() {
+    let arr: [u8; N] = [0; N];
+    let last = &arr[N - 1];
+    assert_eq!(unsafe { kani::shadow::__KANI_pointer_offset(last as *const u8) }, N - 1);
+    // the following call to `set_init` would fail if the object offset for
+    // `last` exceeds the maximum allowed by Kani's shadow memory model
+    unsafe {
+        SM.set_init(last as *const u8, true);
+    }
+}
+
+#[kani::proof]
+fn check_max_object_size_pass() {
+    check_max_objects::<64>();
+}
+
+#[kani::proof]
+fn check_max_object_size_fail() {
+    check_max_objects::<65>();
+}