Skip to content

Commit

Permalink
Merge branch 'main' into cbmc-5.93.0
Browse files Browse the repository at this point in the history
  • Loading branch information
zhassan-aws authored Sep 29, 2023
2 parents 5933c9f + a20437a commit 61885df
Show file tree
Hide file tree
Showing 7 changed files with 98 additions and 26 deletions.
56 changes: 30 additions & 26 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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<Ty<'_>> =
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<Expr> = 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,
Expand Down Expand Up @@ -398,6 +399,9 @@ impl<'tcx> GotocCtx<'tcx> {
}
},
}
} else {
// if it's a union
unimplemented!()
}
}
(Scalar::Int(int), ty::Tuple(_)) => {
Expand Down
11 changes: 11 additions & 0 deletions tests/cargo-kani/codegen-scalar-with-phantom/Cargo.toml
Original file line number Diff line number Diff line change
@@ -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]
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Status: SUCCESS\
Description: "assertion failed: C.x == 0"

VERIFICATION:- SUCCESSFUL
21 changes: 21 additions & 0 deletions tests/cargo-kani/codegen-scalar-with-phantom/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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<R> {
x: u8,
_t: PhantomData<R>,
}

#[kani::proof]
fn check_phantom_data() {
const C: Foo<usize> = Foo { x: 0, _t: PhantomData };
assert_eq!(C.x, 0);
}
11 changes: 11 additions & 0 deletions tests/cargo-kani/codegen-scalar-with-zsts/Cargo.toml
Original file line number Diff line number Diff line change
@@ -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]
4 changes: 4 additions & 0 deletions tests/cargo-kani/codegen-scalar-with-zsts/check_zst.expected
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
Status: SUCCESS\
Description: "assertion failed: C.x == 0"

VERIFICATION:- SUCCESSFUL
17 changes: 17 additions & 0 deletions tests/cargo-kani/codegen-scalar-with-zsts/src/lib.rs
Original file line number Diff line number Diff line change
@@ -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);
}

0 comments on commit 61885df

Please sign in to comment.