Fix generator layout and sizes

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,20 @@
+use std::{
+    future::Future,
+    pin::Pin,
+    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

@@ -79,12 +79,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 passes:
+    // assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop()));
+    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()));
 }