make slice the unconditional else case

carolynzech · Nov 11, 2024 · 857e32d · 857e32d
1 parent e1e8468
commit 857e32d
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 15 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -709,7 +709,7 @@ impl GotocCtx<'_> {
                         let meta = self.codegen_operand_stable(&operands[1]);
                         slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                     }
-                    TyKind::RigidTy(RigidTy::Adt(_, generic_args)) => {
+                    TyKind::RigidTy(RigidTy::Adt(..)) => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         let data_cast =
                             data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
@@ -719,21 +719,10 @@ impl GotocCtx<'_> {
                             data_cast
                         // This is a wide raw pointer; `pointee_ty` is a DST and has non-zero-sized metadata.
                         // An ADT can be a DST if it is a struct and its last field is a DST.
+                        // The only way to construct such a DST is by making the type generic and having the last field be a slice,
                         // c.f. https://doc.rust-lang.org/nomicon/exotic-sizes.html#dynamically-sized-types-dsts
-                        // Case 1: Last field is a slice
-                        } else if !generic_args.0.is_empty()
-                            && generic_args.0.first().unwrap().expect_ty().kind().is_slice()
-                        {
-                            slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
-                        // Case 2: Last field is a trait object
                         } else {
-                            let vtable_expr = meta
-                                .member("_vtable_ptr", &self.symbol_table)
-                                .member("pointer", &self.symbol_table)
-                                .cast_to(
-                                    typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
-                                );
-                            dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                            slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                         }
                     }
                     TyKind::RigidTy(RigidTy::Dynamic(..)) => {

diff --git a/tests/kani/CodegenRawPtrADTSliceTail/main.rs b/tests/kani/CodegenRawPtrADTSliceTail/main.rs
@@ -16,13 +16,22 @@ mod issue_3615 {
     }
 
     #[kani::proof]
-    pub fn check_size_of_overflows() {
+    pub fn from_raw_parts_for_slices() {
         let var: Wrapper<[u64; 4]> = kani::any();
         let fat_ptr: *const Wrapper<[u64]> = &var as *const _;
         let (thin_ptr, _) = fat_ptr.to_raw_parts();
         let new_size: usize = kani::any();
         let _new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size);
     }
+
+    #[kani::proof]
+    pub fn from_raw_parts_for_slices_nested() {
+        let var: Wrapper<Wrapper<[u8; 4]>> = kani::any();
+        let fat_ptr: *const Wrapper<Wrapper<[u8]>> = &var as *const _;
+        let (thin_ptr, _) = fat_ptr.to_raw_parts();
+        let new_size: usize = kani::any();
+        let _new_ptr: *const Wrapper<Wrapper<[u8]>> = ptr::from_raw_parts(thin_ptr, new_size);
+    }
 }
 
 // https://github.com/model-checking/kani/issues/3638