Use dynamic allocation for non-deterministic slices (rust-lang#1011)

* Use dynamic allocation for non-deterministic slices

* Rename NonDetSlice to AnySlice

Author: zhassan-aws

library/kani/src/slice.rs

@@ -1,7 +1,8 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-use crate::{any, any_raw, assume};
-use core::ops::{Deref, DerefMut};
+use crate::{any, any_raw, assume, Arbitrary};
+use std::alloc::{alloc, dealloc, Layout};
+use std::ops::{Deref, DerefMut};
 
 /// Given an array `arr` of length `LENGTH`, this function returns a **valid**
 /// slice of `arr` with non-deterministic start and end points.  This is useful
@@ -38,50 +39,116 @@ fn any_range<const LENGTH: usize>() -> (usize, usize) {
 /// between `0..=MAX_SLICE_LENGTH` and with non-deterministic content.  This is
 /// useful in situations where one wants to verify that all slices with any
 /// content and with a length up to `MAX_SLICE_LENGTH` satisfy a certain
-/// property. Use `any_slice` to create an instance of this struct.
+/// property. Use `any_slice` or `any_raw_slice` to create an instance of this
+/// struct.
 ///
 /// # Example:
 ///
 /// ```rust
-/// let slice: kani::slice::NonDetSlice<u8, 5> = kani::slice::any_slice();
+/// let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
 /// foo(&slice); // where foo is a function that takes a slice and verifies a property about it
 /// ```
-pub struct NonDetSlice<T, const MAX_SLICE_LENGTH: usize> {
-    arr: [T; MAX_SLICE_LENGTH],
+pub struct AnySlice<T, const MAX_SLICE_LENGTH: usize> {
+    layout: Layout,
+    ptr: *mut T,
     slice_len: usize,
 }
 
-impl<T, const MAX_SLICE_LENGTH: usize> NonDetSlice<T, MAX_SLICE_LENGTH> {
-    fn new() -> Self {
-        let arr: [T; MAX_SLICE_LENGTH] = unsafe { any_raw() };
-        let slice_len: usize = any();
+impl<T, const MAX_SLICE_LENGTH: usize> AnySlice<T, MAX_SLICE_LENGTH> {
+    fn new() -> Self
+    where
+        T: Arbitrary,
+    {
+        let any_slice = AnySlice::<T, MAX_SLICE_LENGTH>::alloc_slice();
+        unsafe {
+            let mut i = 0;
+            // Note: even though the guard `i < MAX_SLICE_LENGTH` is redundant
+            // since the assumption above guarantees that `slice_len` <=
+            // `MAX_SLICE_LENGTH`, without it, CBMC fails to infer the required
+            // unwind value, and requires specifying one, which is inconvenient.
+            // CBMC also fails to infer the unwinding if the loop is simply
+            // written as:
+            //     for i in 0..slice_len {
+            //         *(ptr as *mut T).add(i) = any();
+            //     }
+            while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
+                *any_slice.ptr.add(i) = any();
+                i += 1;
+            }
+        }
+        any_slice
+    }
+
+    fn new_raw() -> Self {
+        let any_slice = AnySlice::<T, MAX_SLICE_LENGTH>::alloc_slice();
+        unsafe {
+            let mut i = 0;
+            // See note on `MAX_SLICE_LENGTH` in `new` method above
+            while i < any_slice.slice_len && i < MAX_SLICE_LENGTH {
+                *any_slice.ptr.add(i) = any_raw();
+                i += 1;
+            }
+        }
+        any_slice
+    }
+
+    fn alloc_slice() -> Self {
+        let slice_len = any();
         assume(slice_len <= MAX_SLICE_LENGTH);
-        Self { arr, slice_len }
+        let layout = Layout::array::<T>(slice_len).unwrap();
+        let ptr = if slice_len == 0 { std::ptr::null() } else { unsafe { alloc(layout) } };
+        Self { layout, ptr: ptr as *mut T, slice_len }
     }
 
     pub fn get_slice(&self) -> &[T] {
-        &self.arr[..self.slice_len]
+        if self.slice_len == 0 {
+            &[]
+        } else {
+            unsafe { std::slice::from_raw_parts(self.ptr, self.slice_len) }
+        }
     }
 
     pub fn get_slice_mut(&mut self) -> &mut [T] {
-        &mut self.arr[..self.slice_len]
+        if self.slice_len == 0 {
+            &mut []
+        } else {
+            unsafe { std::slice::from_raw_parts_mut(self.ptr, self.slice_len) }
+        }
     }
 }
 
-impl<T, const MAX_SLICE_LENGTH: usize> Deref for NonDetSlice<T, MAX_SLICE_LENGTH> {
+impl<T, const MAX_SLICE_LENGTH: usize> Drop for AnySlice<T, MAX_SLICE_LENGTH> {
+    fn drop(&mut self) {
+        if self.slice_len > 0 {
+            assert!(!self.ptr.is_null());
+            unsafe {
+                dealloc(self.ptr as *mut u8, self.layout);
+            }
+        }
+    }
+}
+
+impl<T, const MAX_SLICE_LENGTH: usize> Deref for AnySlice<T, MAX_SLICE_LENGTH> {
     type Target = [T];
 
     fn deref(&self) -> &Self::Target {
         self.get_slice()
     }
 }
 
-impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for NonDetSlice<T, MAX_SLICE_LENGTH> {
+impl<T, const MAX_SLICE_LENGTH: usize> DerefMut for AnySlice<T, MAX_SLICE_LENGTH> {
     fn deref_mut(&mut self) -> &mut Self::Target {
         self.get_slice_mut()
     }
 }
 
-pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> NonDetSlice<T, MAX_SLICE_LENGTH> {
-    NonDetSlice::<T, MAX_SLICE_LENGTH>::new()
+pub fn any_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH>
+where
+    T: Arbitrary,
+{
+    AnySlice::<T, MAX_SLICE_LENGTH>::new()
+}
+
+pub unsafe fn any_raw_slice<T, const MAX_SLICE_LENGTH: usize>() -> AnySlice<T, MAX_SLICE_LENGTH> {
+    AnySlice::<T, MAX_SLICE_LENGTH>::new_raw()
 }

tests/expected/nondet-slice-i32-oob/expected

@@ -0,0 +1,6 @@
+Status: FAILURE\
+dereference failure: pointer outside object bounds\
+in function check_out_of_bounds
+
+Status: FAILURE\
+pointer arithmetic: pointer outside object bounds

tests/expected/nondet-slice-i32-oob/main.rs

@@ -0,0 +1,12 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that Kani reports out-of-bound accesses on a non-det slice
+// created using kani::slice::any_slice
+
+#[kani::proof]
+fn check_out_of_bounds() {
+    let bytes = kani::slice::any_slice::<i32, 8>();
+    let val = unsafe { *bytes.get_slice().as_ptr().offset(1) };
+    assert_eq!(val - val, 0);
+}

tests/expected/nondet-slice-len/expected

@@ -0,0 +1,5 @@
+Failed Checks: assertion failed: s.len() != 0
+Failed Checks: assertion failed: s.len() != 1
+Failed Checks: assertion failed: s.len() != 2
+Failed Checks: assertion failed: s.len() != 3
+Failed Checks: assertion failed: s.len() != 4

tests/expected/nondet-slice-len/main.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that non-det slices created using kani::slice::any_slice can
+// assume any length up the specified maximum
+
+#[kani::proof]
+fn check_possible_slice_lengths() {
+    let s = kani::slice::any_slice::<i32, 4>();
+    assert!(s.len() != 0);
+    assert!(s.len() != 1);
+    assert!(s.len() != 2);
+    assert!(s.len() != 3);
+    assert!(s.len() != 4);
+}

tests/expected/nondet-slice-u8-oob/expected

@@ -0,0 +1,6 @@
+Status: FAILURE\
+dereference failure: pointer outside object bounds\
+in function check_out_of_bounds
+
+Status: FAILURE\
+pointer arithmetic: pointer outside object bounds

tests/expected/nondet-slice-u8-oob/main.rs

@@ -0,0 +1,13 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that Kani reports out-of-bound accesses on a non-det slice
+// created using kani::slice::any_slice
+
+#[kani::proof]
+fn check_out_of_bounds() {
+    let mut bytes = kani::slice::any_slice::<u8, 5>();
+    let val = unsafe { *bytes.get_slice().as_ptr().add(4) };
+    kani::assume(val != 0);
+    assert_ne!(val, 0);
+}

tests/kani/NondetSlices/test2.rs

@@ -10,6 +10,6 @@ fn check(s: &[u8]) {
 #[kani::proof]
 fn main() {
     // returns a slice of length between 0 and 5 with non-det content
-    let slice: kani::slice::NonDetSlice<u8, 5> = kani::slice::any_slice();
+    let slice: kani::slice::AnySlice<u8, 5> = kani::slice::any_slice();
     check(&slice);
 }

tests/kani/NondetSlices/test3.rs

@@ -0,0 +1,15 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test uses kani::slice::any_slice of i32
+
+// kani-flags: --unwind 6
+
+#[kani::proof]
+fn check_any_slice_i32() {
+    let s = kani::slice::any_slice::<i32, 5>();
+    s.iter().for_each(|x| kani::assume(*x < 10 && *x > -20));
+    let sum = s.iter().fold(0, |acc, x| acc + x);
+    assert!(sum <= 45); // 9 * 5
+    assert!(sum >= -95); // 19 * 5
+}

tests/kani/NondetSlices/test4.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that values returned by `kani::slice::any_slice` satisfy the
+// type invariant
+
+// kani-flags: --unwind 4
+
+extern crate kani;
+use kani::slice::{any_slice, AnySlice};
+use kani::Invariant;
+
+#[kani::proof]
+fn check_any_slice_valid() {
+    let s: AnySlice<char, 3> = any_slice();
+    for i in s.get_slice() {
+        assert!(i.is_valid());
+    }
+}

tests/kani/NondetSlices/test5.rs

@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// This test checks that values returned by `kani::slice::any_raw_slice` do
+// *not* necessarily satisfy the type invariant
+
+// kani-flags: --unwind 4
+
+extern crate kani;
+use kani::slice::{any_raw_slice, AnySlice};
+use kani::Invariant;
+
+#[kani::proof]
+fn check_any_raw_slice_invalid() {
+    let s: AnySlice<char, 3> = unsafe { any_raw_slice() };
+    for i in s.get_slice() {
+        kani::expect_fail(i.is_valid(), "any_raw_slice values may not be valid");
+    }
+}