Fix ICE due to mishandling of Aggregate rvalue for raw pointers to str

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

@@ -694,6 +694,14 @@ impl<'tcx> GotocCtx<'tcx> {
                         let meta = self.codegen_operand_stable(&operands[1]);
                         slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                     }
+                    TyKind::RigidTy(RigidTy::Str) => {
+                        let pointee_goto_typ = Type::unsigned_int(8);
+                        // cast data to pointer with specified type
+                        let data_cast =
+                            data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
+                        let meta = self.codegen_operand_stable(&operands[1]);
+                        slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                    }
                     TyKind::RigidTy(RigidTy::Adt(..)) => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         let data_cast =

tests/kani/Str/raw_ptr.rs

@@ -0,0 +1,20 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that Kani can handle creating pointers for slices from raw parts.
+//! This used to trigger an ICE reported in <https://github.com/model-checking/kani/issues/3312>.
+#![feature(ptr_metadata)]
+
+#[derive(kani::Arbitrary)]
+struct AscII {
+    #[safety_constraint(*inner < 128)]
+    inner: u8,
+}
+
+#[kani::proof]
+fn check_from_raw() {
+    let ascii: [AscII; 5] = kani::any();
+    let slice_ptr: *const [AscII] = &ascii;
+    let (ptr, metadata) = slice_ptr.to_raw_parts();
+    let str_ptr: *const str = std::ptr::from_raw_parts(ptr, metadata);
+    assert!(unsafe { (&*str_ptr).is_ascii() });
+}

tests/perf/smol_str/Cargo.toml

@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "check_smol_str"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]
+# Make dependency fixed to ensure the test stays the same.
+smol_str = "=0.2.2"

tests/perf/smol_str/expected

@@ -0,0 +1,4 @@
+Checking harness check_new...
+VERIFICATION:- SUCCESSFUL
+
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/perf/smol_str/src/lib.rs

@@ -0,0 +1,13 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Test that Kani can correctly verify the cedar implementation of `SmolStr`
+//! An ICE was initially reported for this case in:
+//! <https://github.com/model-checking/kani/issues/3312>
+
+#[kani::proof]
+#[kani::unwind(4)]
+fn check_new() {
+    let data: [char; 3] = kani::any();
+    let input: String = data.iter().collect();
+    smol_str::SmolStr::new(&input);
+}