Fix generator layout and sizes (#1607)

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

@@ -361,19 +361,9 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_size_align {
             ($which: ident) => {{
                 let tp_ty = instance.substs.type_at(0);
-                if tp_ty.is_generator() {
-                    let e = self.codegen_unimplemented_expr(
-                        "size or alignment of a generator type",
-                        cbmc_ret_ty,
-                        loc,
-                        "/~https://github.com/model-checking/kani/issues/1395",
-                    );
-                    self.codegen_expr_to_place(p, e)
-                } else {
-                    let arg = fargs.remove(0);
-                    let size_align = self.size_and_align_of_dst(tp_ty, arg);
-                    self.codegen_expr_to_place(p, size_align.$which)
-                }
+                let arg = fargs.remove(0);
+                let size_align = self.size_and_align_of_dst(tp_ty, arg);
+                self.codegen_expr_to_place(p, size_align.$which)
             }};
         }
 

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

@@ -1130,7 +1130,7 @@ impl<'tcx> GotocCtx<'tcx> {
                     name: field_name,
                     typ: ctx.codegen_ty(field_ty),
                 });
-                offset += field_size;
+                offset = field_offset + field_size;
             }
             fields.extend(ctx.codegen_alignment_padding(
                 offset,

tests/kani/Generator/issue-1593.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// compile-flags: --edition 2018
+
+// Regression test for /~https://github.com/model-checking/kani/issues/1593
+// The problem was that the size of a generator was wrong, which was discovered
+// in the context of vtables.
+
+use std::sync::{
+    atomic::{AtomicI64, Ordering},
+    Arc,
+};
+
+#[kani::proof]
+fn issue_1593() {
+    let x = Arc::new(AtomicI64::new(0));
+    let x2 = x.clone();
+    let gen = async move {
+        async {}.await;
+        x2.fetch_add(1, Ordering::Relaxed);
+    };
+    assert_eq!(std::mem::size_of_val(&gen), 16);
+    let pinbox = Box::pin(gen); // check that vtables work
+}

tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs → tests/kani/Generator/rustc-generator-tests/discriminant.rs

@@ -95,7 +95,6 @@ fn cycle(
 }
 
 #[kani::proof]
-#[kani::unwind(260)]
 fn main() {
     // Has only one invalid discr. value.
     let gen_u8_tiny_niche = || {

tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs → tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs

@@ -6,6 +6,14 @@
 // Modifications Copyright Kani Contributors
 // See GitHub history for details.
 
+//! Tests the size of generators
+//! Note that the size of generators can depend on the panic strategy.
+//! This is the case here (see the bottom of the file).
+//! In particular, running rustc with default options on this file will fail an assertion.
+//! Since Kani uses "panic=abort", you need to run rustc with `-C panic=abort`
+//! to get the same results as Kani.
+//! More information: /~https://github.com/rust-lang/rust/issues/59123
+
 // run-pass
 // Test that we don't duplicate storage for a variable that is moved to another
 // binding. This used to happen in the presence of unwind and drop edges (see
@@ -15,7 +23,7 @@
 // don't want to see is the `complex` generator size being upwards of 2048 bytes
 // (which would indicate it is reserving space for two copies of Foo.)
 //
-// See issue #59123 for a full explanation.
+// See issue /~https://github.com/rust-lang/rust/issues/59123 for a full explanation.
 
 // edition:2018
 // ignore-wasm32 issue #62807
@@ -79,12 +87,10 @@ fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
 
 #[kani::proof]
 fn main() {
-    // FIXME: size of generators does not work reliably (/~https://github.com/model-checking/kani/issues/1395)
     assert_eq!(1025, std::mem::size_of_val(&move_before_yield()));
-    // The following assertion fails for some reason (tracking issue: /~https://github.com/model-checking/kani/issues/1395).
-    // But it also fails for WASM (/~https://github.com/rust-lang/rust/issues/62807),
-    // so it is probably not a big problem:
-    assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop()));
+    // With panic=unwind, the following assertion fails because the size increases to 1026.
+    // More information here: /~https://github.com/rust-lang/rust/issues/59123
+    assert_eq!(1025, std::mem::size_of_val(&move_before_yield_with_noop()));
     assert_eq!(2051, std::mem::size_of_val(&overlap_move_points()));
     assert_eq!(1026, std::mem::size_of_val(&overlap_x_and_y()));
 }