From a20437a54fdc28203dc4154255848dad3d93ed47 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 29 Sep 2023 13:13:34 -0400 Subject: [PATCH] Avoid mismatch when generating structs that represent scalar data but also include ZSTs (#2794) This change considers another case for the code generation of scalar data. In particular, when the expected type is an ADT, we previously considered two cases: either there is no field or there is one. But in cases where the ADT includes a ZST, the ADT will contain multiple fields: one associated to the scalar data, and other fields associated to the ZSTs. In those cases, we ended up crashing as in #2680: ```rust error: internal compiler error: Kani unexpectedly panicked at panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }]. thread 'rustc' panicked at cprover_bindings/src/goto_program/expr.rs:804:9: assertion failed: `(left == right)` left: `2`, right: `1`: Error in struct_expr; mismatch in number of fields and values. StructTag("tag-_161424092592971241517604180463813633314") [Expr { value: IntConstant(0), typ: Unsignedbv { width: 8 }, location: None, size_of_annotation: None }] ``` With the changes in this PR, that's no longer the case. Resolves #2364 Resolves #2680 --- .../codegen_cprover_gotoc/codegen/operand.rs | 56 ++++++++++--------- .../codegen-scalar-with-phantom/Cargo.toml | 11 ++++ .../check_phantom_data.expected | 4 ++ .../codegen-scalar-with-phantom/src/lib.rs | 21 +++++++ .../codegen-scalar-with-zsts/Cargo.toml | 11 ++++ .../check_zst.expected | 4 ++ .../codegen-scalar-with-zsts/src/lib.rs | 17 ++++++ 7 files changed, 98 insertions(+), 26 deletions(-) create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/check_phantom_data.expected create mode 100644 tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected create mode 100644 tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs 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); +}