Add a few examples of using shadow memory to check initialization of …

…slices (#3237)

A follow-up on #3200: use API to check that slices produced by some
slice operations that internally use `unsafe` are properly initialized.

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Jaisurya Nanduri <91620234+jaisnan@users.noreply.github.com>
Co-authored-by: Artem Agvanian <nartagva@amazon.com>

tests/expected/shadow/slices/slice_of_array/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/shadow/slices/slice_of_array/test.rs

@@ -0,0 +1,34 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This test demonstrates a possible usage of the shadow memory API to check that
+// every element of an arbitrary slice of an array is initialized.
+// Since the instrumentation is done manually in the harness only but not inside
+// the library functions, the test only verifies that the slices point to memory
+// that is within the original array.
+
+const N: usize = 16;
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+#[kani::proof]
+#[kani::unwind(31)]
+fn check_slice_init() {
+    let arr: [char; N] = kani::any();
+    // tag every element of the array as initialized
+    for i in &arr {
+        unsafe {
+            SM.set(i as *const char, true);
+        }
+    }
+    // create an arbitrary slice of the array
+    let end: usize = kani::any_where(|x| *x <= N);
+    let begin: usize = kani::any_where(|x| *x < end);
+    let slice = &arr[begin..end];
+
+    // verify that all elements of the slice are initialized
+    for i in slice {
+        assert!(unsafe { SM.get(i as *const char) });
+    }
+}

tests/expected/shadow/slices/slice_reverse/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/shadow/slices/slice_reverse/test.rs

@@ -0,0 +1,28 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This test demonstrates a possible usage of the shadow memory API to check that
+// every element of a reversed array is initialized.
+// Since the instrumentation is done manually in the harness only but not inside
+// the `reverse` function, the test only verifies that the resulting array
+// occupies the same memory as the original one.
+
+const N: usize = 32;
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+#[kani::proof]
+fn check_reverse() {
+    let mut a: [u16; N] = kani::any();
+    for i in &a {
+        unsafe { SM.set(i as *const u16, true) };
+    }
+    a.reverse();
+
+    for i in &a {
+        unsafe {
+            assert!(SM.get(i as *const u16));
+        }
+    }
+}

tests/expected/shadow/slices/slice_split/expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

tests/expected/shadow/slices/slice_split/test.rs

@@ -0,0 +1,35 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zghost-state
+
+// This test demonstrates a possible usage of the shadow memory API to check that
+// every element of an array split into two slices is initialized.
+// Since the instrumentation is done manually in the harness only but not inside
+// the `split_at_checked` function, the test only verifies that the resulting
+// slices occupy the same memory as the original array.
+
+const N: usize = 16;
+
+static mut SM: kani::shadow::ShadowMem<bool> = kani::shadow::ShadowMem::new(false);
+
+#[kani::proof]
+#[kani::unwind(17)]
+fn check_reverse() {
+    let a: [bool; N] = kani::any();
+    for i in &a {
+        unsafe { SM.set(i as *const bool, true) };
+    }
+    let index: usize = kani::any_where(|x| *x <= N);
+    let (s1, s2) = a.split_at_checked(index).unwrap();
+
+    for i in s1 {
+        unsafe {
+            assert!(SM.get(i as *const bool));
+        }
+    }
+    for i in s2 {
+        unsafe {
+            assert!(SM.get(i as *const bool));
+        }
+    }
+}