Implement support for generators

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

@@ -313,9 +313,19 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_size_align {
             ($which: ident) => {{
                 let tp_ty = instance.substs.type_at(0);
-                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)
+                if tp_ty.is_generator() {
+                    let e = self.codegen_unimplemented(
+                        "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)
+                }
             }};
         }
 

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

@@ -136,6 +136,7 @@ fn main() {
         }
     };
 
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(size_of_val(&gen_u8_tiny_niche()), 1);
     assert_eq!(size_of_val(&Some(gen_u8_tiny_niche())), 1); // uses niche
     assert_eq!(size_of_val(&Some(Some(gen_u8_tiny_niche()))), 2); // cannot use niche anymore

tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs

@@ -0,0 +1,35 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs
+
+// Test that niche finding works with captured generator upvars.
+
+// run-pass
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+use std::mem::size_of_val;
+
+fn take<T>(_: T) {}
+
+#[kani::proof]
+fn main() {
+    let x = false;
+    let mut gen1 = || {
+        yield;
+        take(x);
+    };
+
+    // FIXME: for some reason, these asserts are very hard for CBMC to figure out
+    // Kani didn't terminate within 5 minutes.
+    // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(()));
+    // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(()));
+    assert!(false); // to make the test fail without taking forever
+}

tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs → tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs

@@ -24,5 +24,6 @@ fn main() {
         take(x);
     };
 
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(size_of_val(&gen1), size_of_val(&Some(gen1)));
 }

tests/kani/Generator/rustc-generator-tests/overlap-locals.rs

@@ -8,31 +8,35 @@
 
 // run-pass
 
-#![feature(generators)]
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
 
 #[kani::proof]
 fn main() {
-    let a = || {
+    let mut a = || {
         {
             let w: i32 = 4;
             yield;
-            println!("{:?}", w);
         }
         {
             let x: i32 = 5;
             yield;
-            println!("{:?}", x);
         }
         {
             let y: i32 = 6;
             yield;
-            println!("{:?}", y);
         }
         {
             let z: i32 = 7;
             yield;
-            println!("{:?}", z);
         }
     };
-    assert_eq!(8, std::mem::size_of_val(&a));
+
+    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Complete(()));
 }

tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs

@@ -0,0 +1,40 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs
+
+// run-pass
+
+#![feature(generators)]
+
+#[kani::proof]
+fn main() {
+    let a = || {
+        {
+            let w: i32 = 4;
+            yield;
+            println!("{:?}", w);
+        }
+        {
+            let x: i32 = 5;
+            yield;
+            println!("{:?}", x);
+        }
+        {
+            let y: i32 = 6;
+            yield;
+            println!("{:?}", y);
+        }
+        {
+            let z: i32 = 7;
+            yield;
+            println!("{:?}", z);
+        }
+    };
+
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
+    assert_eq!(8, std::mem::size_of_val(&a));
+}

tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs → tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs

@@ -32,6 +32,7 @@ fn main() {
 
     // Neither of these generators have the resume arg live across the `yield`, so they should be
     // 1 Byte in size (only storing the discriminant)
+    // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395)
     assert_eq!(size_of_val(&gen_copy), 1);
     assert_eq!(size_of_val(&gen_move), 1);
 }

tests/kani/Generator/rustc-generator-tests/resume-arg.rs

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+// run-pass
+
+use std::mem::size_of_val;
+
+#[kani::proof]
+fn main() {
+    // Generator taking a `Copy`able resume arg.
+    let mut gen_copy = |mut x: usize| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    // Generator taking a non-`Copy` resume arg.
+    let mut gen_move = |mut x: Box<usize>| {
+        loop {
+            drop(x);
+            x = yield;
+        }
+    };
+
+    assert_eq!(Pin::new(&mut gen_copy).resume(0), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_copy).resume(1), GeneratorState::Yielded(()));
+
+    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(0)), GeneratorState::Yielded(()));
+    assert_eq!(Pin::new(&mut gen_move).resume(Box::new(1)), GeneratorState::Yielded(()));
+}

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

@@ -0,0 +1,136 @@
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Modifications Copyright Kani Contributors
+// See GitHub history for details.
+
+// Copyright rustc Contributors
+// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs
+
+// 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
+// `complex` below.)
+//
+// The exact sizes here can change (we'd like to know when they do). What we
+// 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.
+
+// edition:2018
+// ignore-wasm32 issue #62807
+// ignore-asmjs issue #62807
+
+#![feature(generators, generator_trait)]
+
+use std::ops::{Generator, GeneratorState};
+use std::pin::Pin;
+
+const FOO_SIZE: usize = 1024;
+struct Foo([u8; FOO_SIZE]);
+
+impl Drop for Foo {
+    fn drop(&mut self) {}
+}
+
+fn move_before_yield() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+fn noop() {}
+
+fn move_before_yield_with_noop() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        noop();
+        let _second = first;
+        yield;
+        // _second dropped here
+    }
+}
+
+// Today we don't have NRVO (we allocate space for both `first` and `second`,)
+// but we can overlap `first` with `_third`.
+fn overlap_move_points() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let first = Foo([0; FOO_SIZE]);
+        yield;
+        let second = first;
+        yield;
+        let _third = second;
+        yield;
+    }
+}
+
+fn overlap_x_and_y() -> impl Generator<Yield = (), Return = ()> {
+    static || {
+        let x = Foo([0; FOO_SIZE]);
+        yield;
+        drop(x);
+        let y = Foo([0; FOO_SIZE]);
+        yield;
+        drop(y);
+    }
+}
+
+#[kani::proof]
+fn main() {
+    // FIXME: the following tests are very slow (did not terminate in a couple of minutes)
+    /* let mut generator = move_before_yield();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = move_before_yield_with_noop();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = overlap_move_points();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    );
+
+    let mut generator = overlap_x_and_y();
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Yielded(())
+    );
+    assert_eq!(
+        unsafe { Pin::new_unchecked(&mut generator) }.resume(()),
+        GeneratorState::Complete(())
+    ); */
+    assert!(false); // to make the test fail without taking forever
+}

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

@@ -79,11 +79,12 @@ 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()));
+    assert_eq!(1026, 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()));
 }