Update expectation for projection of slice reference. (rust-lang#1032)

* Fix 1: Slice projection yields a thin pointer

Our expectation did not considered the array decay when creating fat
pointers.

* Added new testcases for size_of and raw slice

* Add test for different representations + fix comment

Author: celinval

src/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs

@@ -78,7 +78,23 @@ impl<'tcx> ProjectedPlace<'tcx> {
             TypeOrVariant::Type(t) => {
                 let expr_ty = expr.typ().clone();
                 let type_from_mir = ctx.codegen_ty(*t);
-                if expr_ty != type_from_mir { Some((expr_ty, type_from_mir)) } else { None }
+                if expr_ty != type_from_mir {
+                    match t.kind() {
+                        // Slice references (`&[T]`) store raw pointers to the element type `T`
+                        // due to pointer decay. They are fat pointers with the following repr:
+                        // SliceRef { data: *T, len: usize }.
+                        // In those cases, the projection will yield a pointer type.
+                        ty::Slice(..) | ty::Str
+                            if expr_ty.is_pointer()
+                                && expr_ty.base_type() == type_from_mir.base_type() =>
+                        {
+                            None
+                        }
+                        _ => Some((expr_ty, type_from_mir)),
+                    }
+                } else {
+                    None
+                }
             }
             // TODO: handle Variant https://github.com/model-checking/kani/issues/448
             TypeOrVariant::Variant(_) => None,
@@ -320,7 +336,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         inner_goto_expr.member("data", &self.symbol_table)
                     }
                     ty::Adt(..) if self.is_unsized(inner_mir_typ) => {
-                        // in cbmc-reg/Strings/os_str_reduced.rs, we see
+                        // in tests/kani/Strings/os_str_reduced.rs, we see
                         // ```
                         //  p.projection = [
                         //     Deref,
@@ -461,9 +477,10 @@ impl<'tcx> GotocCtx<'tcx> {
     /// If it passes through a fat pointer along the way, it stores info about it,
     /// which can be useful in reconstructing fat pointer operations.
     pub fn codegen_place(&mut self, p: &Place<'tcx>) -> ProjectedPlace<'tcx> {
-        debug!("codegen_place: {:?}", p);
+        debug!(place=?p, "codegen_place");
         let initial_expr = self.codegen_local(p.local);
         let initial_typ = TypeOrVariant::Type(self.local_ty(p.local));
+        debug!(?initial_typ, ?initial_expr, "codegen_place");
         let initial_projection = ProjectedPlace::new(initial_expr, initial_typ, None, None, self);
         p.projection
             .iter()

src/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -538,9 +538,12 @@ impl<'tcx> GotocCtx<'tcx> {
             //TODO: Ensure that this is correct
             ty::Dynamic(..) => self.codegen_fat_ptr(ty),
             // As per zulip, a raw slice/str is a variable length array
-            // https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp
+            // https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp/topic/Memory.20layout.20of.20DST
+            // &[T] -> { data: *const T, len: usize }
+            // [T] -> memory location (flexible array)
+            // Note: This is not valid C but CBMC seems to be ok with it.
             ty::Slice(e) => self.codegen_ty(*e).flexible_array_of(),
-            ty::Str => Type::c_char().array_of(0),
+            ty::Str => Type::c_char().flexible_array_of(),
             ty::Ref(_, t, _) | ty::RawPtr(ty::TypeAndMut { ty: t, .. }) => self.codegen_ty_ref(*t),
             ty::FnDef(_, _) => {
                 let sig = self.monomorphize(ty.fn_sig(self.tcx));
@@ -754,7 +757,7 @@ impl<'tcx> GotocCtx<'tcx> {
         if self.use_slice_fat_pointer(mir_type) {
             let pointer_name = match mir_type.kind() {
                 ty::Slice(..) => self.ty_mangled_name(mir_type),
-                ty::Str => "str".intern(),
+                ty::Str => "refstr".intern(),
                 ty::Adt(..) => format!("&{}", self.ty_mangled_name(mir_type)).intern(),
                 kind => unreachable!("Generating a slice fat pointer to {:?}", kind),
             };

tests/expected/raw_slice/expected

@@ -0,0 +1,73 @@
+Checking harness check_non_empty_raw...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(raw) == 4"\
+slice.rs:61:5 in function check_non_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner.len() == 4"\
+slice.rs:62:5 in function check_non_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner[0] == 1"\
+slice.rs:63:5 in function check_non_empty_raw
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_empty_raw...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(raw) == 0"\
+slice.rs:70:5 in function check_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner.len() == 0"\
+slice.rs:71:5 in function check_empty_raw
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_non_empty_slice...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(slice) == 2"\
+slice.rs:78:5 in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others.len() == 1"\
+slice.rs:79:5 in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.first == 1"\
+slice.rs:80:5 in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others[0] == 5"\
+slice.rs:81:5 in function check_non_empty_slice
+
+VERIFICATION:- SUCCESSFUL
+
+
+Checking harness check_naive_iterator_should_fail...
+
+Status: SUCCESS\
+Description: ""Naive new should have the wrong slice len""\
+slice.rs:94:5 in function check_naive_iterator_should_fail
+
+Status: SUCCESS\
+Description: "assertion failed: slice.first == first"\
+slice.rs:95:5 in function check_naive_iterator_should_fail
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others[0] == second"\
+slice.rs:96:5 in function check_naive_iterator_should_fail
+
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+slice.rs:100:32 in function check_naive_iterator_should_fail
+
+VERIFICATION:- FAILED
+
+
+Summary:\
+Verification failed for - check_naive_iterator_should_fail\
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.

tests/expected/raw_slice/slice.rs

@@ -0,0 +1,102 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: --unwind 3
+
+//! This test case has a bunch of checks related to structures using raw slices ([T]).
+use std::mem;
+
+/// Non-sized structure with a sized element and an unsized element.
+struct NonEmptySlice {
+    first: u8,
+    others: [u8],
+}
+
+/// Non-sized structure with only an unsized element.
+struct RawSlice {
+    inner: [u8],
+}
+
+impl NonEmptySlice {
+    /// This creates a NonEmptySlice from a byte slice.
+    ///
+    /// Note that the cast operation keep the the fat pointer structure, so we need to manually
+    /// create the expected pointer with correct len. For the NonEmptySlice, this looks like:
+    /// ```rust
+    /// struct NonEmptySliceRef {
+    ///   ptr: *const u8,
+    ///   unsize_len: usize,
+    /// }
+    /// ```
+    ///
+    /// I.e.: The length is only relative to the unsized part of the structure.
+    /// The total size of the object is the `size_of(sized_members) + (unsize_len * size_of::<u8>())`
+    ///
+    fn new(bytes: &mut [u8]) -> &Self {
+        assert!(bytes.len() > 0, "This requires at least one element");
+        let unsized_len = bytes.len() - 1;
+        unsafe {
+            let ptr = std::ptr::slice_from_raw_parts_mut(bytes.as_mut_ptr(), unsized_len);
+            unsafe { &*(ptr as *mut Self) }
+        }
+    }
+
+    /// This function does a naive transmute in the slice which generates a corrupt structure.
+    /// See the documentation of `NonEmptySliceRef::new()` for more details.
+    fn naive_new(bytes: &mut [u8]) -> &Self {
+        assert!(bytes.len() > 0, "This requires at least one element");
+        unsafe { std::mem::transmute(bytes) }
+    }
+}
+
+impl RawSlice {
+    fn new(bytes: &mut [u8]) -> &Self {
+        unsafe { std::mem::transmute(bytes) }
+    }
+}
+
+#[kani::proof]
+fn check_non_empty_raw() {
+    let mut vector = vec![1u8, 2u8, 3u8, 4u8];
+    let raw = RawSlice::new(vector.as_mut_slice());
+    assert_eq!(mem::size_of_val(raw), 4);
+    assert_eq!(raw.inner.len(), 4);
+    assert_eq!(raw.inner[0], 1);
+}
+
+#[kani::proof]
+fn check_empty_raw() {
+    let mut vector = vec![];
+    let raw = RawSlice::new(vector.as_mut_slice());
+    assert_eq!(mem::size_of_val(raw), 0);
+    assert_eq!(raw.inner.len(), 0);
+}
+
+#[kani::proof]
+fn check_non_empty_slice() {
+    let mut vector = vec![1u8, 5u8];
+    let slice = NonEmptySlice::new(vector.as_mut_slice());
+    assert_eq!(mem::size_of_val(slice), 2);
+    assert_eq!(slice.others.len(), 1);
+    assert_eq!(slice.first, 1);
+    assert_eq!(slice.others[0], 5);
+}
+
+#[kani::proof]
+#[kani::unwind(3)]
+fn check_naive_iterator_should_fail() {
+    let mut bytes = vec![1u8, 5u8];
+    assert_eq!(bytes.len(), 2);
+
+    let first = bytes[0];
+    let second = bytes[1];
+
+    let slice = NonEmptySlice::naive_new(&mut bytes);
+    assert_eq!(slice.others.len(), 2, "Naive new should have the wrong slice len");
+    assert_eq!(slice.first, first);
+    assert_eq!(slice.others[0], second);
+    let mut sum = 0u8;
+    for e in &slice.others {
+        // This should trigger out-of-bounds.
+        sum = sum.wrapping_add(*e);
+    }
+}

tests/expected/raw_slice_c_repr/expected

@@ -0,0 +1,73 @@
+Checking harness check_non_empty_raw...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(raw) == 4"\
+in function check_non_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner.len() == 4"\
+in function check_non_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner[0] == 1"\
+in function check_non_empty_raw
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_empty_raw...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(raw) == 0"\
+in function check_empty_raw
+
+Status: SUCCESS\
+Description: "assertion failed: raw.inner.len() == 0"\
+in function check_empty_raw
+
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_non_empty_slice...
+
+Status: SUCCESS\
+Description: "assertion failed: mem::size_of_val(slice) == 2"\
+in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others.len() == 1"\
+in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.first == 1"\
+in function check_non_empty_slice
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others[0] == 5"\
+in function check_non_empty_slice
+
+VERIFICATION:- SUCCESSFUL
+
+
+Checking harness check_naive_iterator_should_fail...
+
+Status: SUCCESS\
+Description: ""Naive new should have the wrong slice len""\
+in function check_naive_iterator_should_fail
+
+Status: SUCCESS\
+Description: "assertion failed: slice.first == first"\
+in function check_naive_iterator_should_fail
+
+Status: SUCCESS\
+Description: "assertion failed: slice.others[0] == second"\
+in function check_naive_iterator_should_fail
+
+Status: FAILURE\
+Description: "dereference failure: pointer outside object bounds"\
+in function check_naive_iterator_should_fail
+
+VERIFICATION:- FAILED
+
+
+Summary:\
+Verification failed for - check_naive_iterator_should_fail\
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.