diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 687761e134a77..45ce90880fd68 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -303,38 +303,39 @@ impl<'tcx> GotocCtx<'tcx> { } } (Scalar::Int(_), ty::Adt(adt, subst)) => { - if adt.is_struct() || adt.is_union() { - // in this case, we must have a one variant ADT. there are two cases - let variant = &adt.variants().raw[0]; - // if there is no field, then it's just a ZST - if variant.fields.is_empty() { - if adt.is_struct() { - let overall_t = self.codegen_ty(ty); - Expr::struct_expr_from_values(overall_t, vec![], &self.symbol_table) - } else { - unimplemented!() - } - } else { - // otherwise, there is just one field, which is stored as the scalar data - let field = &variant.fields[0usize.into()]; - let fty = field.ty(self.tcx, subst); - - let overall_t = self.codegen_ty(ty); - if adt.is_struct() { - self.codegen_single_variant_single_field(s, span, overall_t, fty) - } else { - unimplemented!() - } - } - } else { - // if it's an enum + if adt.is_struct() { + // In this case, we must have a one variant ADT. + let variant = adt.non_enum_variant(); + let overall_type = self.codegen_ty(ty); + // There must be at least one field associated with the scalar data. + // Any additional fields correspond to ZSTs. + let field_types: Vec> = + variant.fields.iter().map(|f| f.ty(self.tcx, subst)).collect(); + // Check that there is a single non-ZST field. + let non_zst_types: Vec<_> = + field_types.iter().filter(|t| !self.is_zst(**t)).collect(); + assert!( + non_zst_types.len() == 1, + "error: expected exactly one field whose type is not a ZST" + ); + let field_values: Vec = field_types + .iter() + .map(|t| { + if self.is_zst(*t) { + Expr::init_unit(self.codegen_ty(*t), &self.symbol_table) + } else { + self.codegen_scalar(s, *t, span) + } + }) + .collect(); + Expr::struct_expr_from_values(overall_type, field_values, &self.symbol_table) + } else if adt.is_enum() { let layout = self.layout_of(ty); let overall_t = self.codegen_ty(ty); match &layout.variants { Variants::Single { index } => { // here we must have one variant let variant = &adt.variants()[*index]; - match variant.fields.len() { 0 => Expr::struct_expr_from_values( overall_t, @@ -398,6 +399,9 @@ impl<'tcx> GotocCtx<'tcx> { } }, } + } else { + // if it's a union + unimplemented!() } } (Scalar::Int(int), ty::Tuple(_)) => { diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml b/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml new file mode 100644 index 0000000000000..541ac718603f3 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "codegen-scalar-with-phantom" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected new file mode 100644 index 0000000000000..97d4b6c54c095 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected @@ -0,0 +1,4 @@ +Status: SUCCESS\ +Description: "assertion failed: C.x == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs b/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs new file mode 100644 index 0000000000000..9b17a8207e287 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs @@ -0,0 +1,21 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can codegen structs with scalar and phantom data. +//! +//! Note: Phantom data is represented with ZSTs, which are already covered by +//! the test `codegen-scalar-with-zsts`, but we include this one as well for +//! completeness. + +use std::marker::PhantomData; + +pub struct Foo { + x: u8, + _t: PhantomData, +} + +#[kani::proof] +fn check_phantom_data() { + const C: Foo = Foo { x: 0, _t: PhantomData }; + assert_eq!(C.x, 0); +} diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml b/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml new file mode 100644 index 0000000000000..86bf3dff0ecb9 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml @@ -0,0 +1,11 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT + +[package] +name = "codegen-scalar-with-zsts" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html + +[dependencies] diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected new file mode 100644 index 0000000000000..97d4b6c54c095 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected @@ -0,0 +1,4 @@ +Status: SUCCESS\ +Description: "assertion failed: C.x == 0" + +VERIFICATION:- SUCCESSFUL diff --git a/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs b/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs new file mode 100644 index 0000000000000..e50e64f185806 --- /dev/null +++ b/tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Check that we can codegen structs with scalar and ZSTs. + +struct Empty {} + +pub struct Foo { + x: u8, + _t: Empty, +} + +#[kani::proof] +fn check_zst() { + const C: Foo = Foo { x: 0, _t: Empty {} }; + assert_eq!(C.x, 0); +}