diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 5138c365fc5f..37cbee6d2782 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/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) }}; } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 45f766e40f22..b56bd703b255 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/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, diff --git a/tests/kani/Generator/issue-1593.rs b/tests/kani/Generator/issue-1593.rs new file mode 100644 index 000000000000..c1ee4a8ddf31 --- /dev/null +++ b/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 +} diff --git a/tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs b/tests/kani/Generator/rustc-generator-tests/discriminant.rs similarity index 99% rename from tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs rename to tests/kani/Generator/rustc-generator-tests/discriminant.rs index e47d2e241617..f2c2a6a15b33 100644 --- a/tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs +++ b/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 = || { diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs b/tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs similarity index 75% rename from tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs rename to tests/kani/Generator/rustc-generator-tests/moved-locals-size.rs index 8d7254a18c6e..77cdd6ada955 100644 --- a/tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs +++ b/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 { #[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())); } diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs b/tests/kani/Generator/rustc-generator-tests/moved-locals.rs similarity index 100% rename from tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs rename to tests/kani/Generator/rustc-generator-tests/moved-locals.rs diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator-size.rs similarity index 100% rename from tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs rename to tests/kani/Generator/rustc-generator-tests/niche-in-generator-size.rs diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals-size.rs similarity index 100% rename from tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs rename to tests/kani/Generator/rustc-generator-tests/overlap-locals-size.rs diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs similarity index 100% rename from tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs rename to tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs