Fix codegen of constant byte slices (#2663)

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

@@ -196,17 +196,11 @@ impl<'tcx> GotocCtx<'tcx> {
                 }
                 ty::Slice(slice_ty) => {
                     if let Uint(UintTy::U8) = slice_ty.kind() {
-                        // The case where we have a slice of u8 is easy enough: make an array of u8
+                        let mem_var = self.codegen_const_allocation(data, None);
                         let slice =
                             data.inspect_with_uninit_and_ptr_outside_interpreter(start..end);
-                        let vec_of_bytes: Vec<Expr> = slice
-                            .iter()
-                            .map(|b| Expr::int_constant(*b, Type::unsigned_int(8)))
-                            .collect();
-                        let len = vec_of_bytes.len();
-                        let array_expr =
-                            Expr::array_expr(Type::unsigned_int(8).array_of(len), vec_of_bytes);
-                        let data_expr = array_expr.array_to_ptr();
+                        let len = slice.len();
+                        let data_expr = mem_var.cast_to(Type::unsigned_int(8).to_pointer());
                         let len_expr = Expr::int_constant(len, Type::size_t());
                         return slice_fat_ptr(
                             self.codegen_ty(lit_ty),

tests/cargo-kani/itoa_dep/check_unsigned.expected

@@ -1,7 +1,4 @@
 Status: SUCCESS\
 Description: "assertion failed: result == &output"
 
-Status: FAILURE\
-Description: "memcpy source region readable"
-
-VERIFICATION:- FAILED
+VERIFICATION:- SUCCESSFUL

tests/cargo-kani/itoa_dep/src/main.rs

@@ -2,8 +2,6 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! This test checks Kani's support for the `itoa` crate
-//! Currently fails with a spurious failure:
-//! https://github.com/model-checking/kani/issues/2066
 
 use itoa::{Buffer, Integer};
 use std::fmt::Write;

tests/kani/Slice/const_bytes.rs

@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This test checks that byte slices are codegen correctly. This used to fail
+//! in the past (see https://github.com/model-checking/kani/issues/2656).
+
+#[kani::proof]
+fn main() {
+    const MY_CONSTANT: &[u8] = &[147, 211];
+    let x: u8 = MY_CONSTANT[0];
+    let y: u8 = MY_CONSTANT[1];
+    assert_eq!(x, 147);
+    assert_eq!(y, 211);
+}

tests/kani/Vectors/vector_extend_bytes.rs

@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Check that we propertly handle `Vec::extend` with a constant byte slice.
+//! This used to fail previously (see
+//! https://github.com/model-checking/kani/issues/2656).
+
+#[kani::proof]
+fn check_extend_const_byte_slice() {
+    const MY_CONSTANT: &[u8] = b"Hi";
+
+    let mut my_vec: Vec<u8> = Vec::new();
+    my_vec.extend(MY_CONSTANT);
+    assert_eq!(my_vec, [72, 105]);
+}