From 2b636d64cf740c24218c5701a6b2c9c53ecccc92 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Apr 2023 10:18:13 +0000 Subject: [PATCH 1/4] Factor out niche value computation There will be future re-use of this code, so move it to a public function. --- .../codegen/statement.rs | 31 ++++++++----------- .../src/codegen_cprover_gotoc/codegen/typ.rs | 27 +++++++++++++++- 2 files changed, 39 insertions(+), 19 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 60e817f77670..b237e5679249 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -16,7 +16,7 @@ use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{Instance, InstanceDef, Ty}; use rustc_span::Span; -use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; +use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -88,28 +88,23 @@ impl<'tcx> GotocCtx<'tcx> { } TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { if untagged_variant != variant_index { - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0], - _ => unreachable!("niche encoding must have arbitrary fields"), - }; - let discr_ty = self.codegen_enum_discr_typ(pt); - let discr_ty = self.codegen_ty(discr_ty); - let niche_value = - variant_index.as_u32() - niche_variants.start().as_u32(); - let niche_value = (niche_value as u128).wrapping_add(*niche_start); - let value = if niche_value == 0 - && matches!(tag.primitive(), Primitive::Pointer(_)) - { - discr_ty.null() - } else { - Expr::int_constant(niche_value, discr_ty.clone()) - }; + let value = self.compute_enum_niche_value( + pt, + variant_index, + tag, + niche_variants, + niche_start, + ); let place = unwrap_or_return_codegen_unimplemented_stmt!( self, self.codegen_place(place) ) .goto_expr; - self.codegen_get_niche(place, offset, discr_ty) + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => offsets[0], + _ => unreachable!("niche encoding must have arbitrary fields"), + }; + self.codegen_get_niche(place, offset, value.typ().clone()) .assign(value, location) } else { Stmt::skip(location) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 8508febbeb22..97bd3c6b38cf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -20,11 +20,12 @@ use rustc_middle::ty::{ use rustc_middle::ty::{List, TypeFoldable}; use rustc_span::def_id::DefId; use rustc_target::abi::{ - Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, TyAndLayout, + Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Scalar, Size, TagEncoding, TyAndLayout, VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; use std::iter; +use std::ops::RangeInclusive; use tracing::{debug, trace, warn}; use ty::layout::HasParamEnv; @@ -1571,6 +1572,30 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Compute the discriminant expression for an enum that uses niche optimization. + /// + /// We follow the logic of the SSA and Cranelift back-ends in doing the computation: + /// + /// + pub fn compute_enum_niche_value( + &mut self, + enum_ty: Ty<'tcx>, + variant_index: &VariantIdx, + tag: &Scalar, + niche_variants: &RangeInclusive, + niche_start: &u128, + ) -> Expr { + let discr_ty = self.codegen_enum_discr_typ(enum_ty); + let discr_ty = self.codegen_ty(discr_ty); + let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); + let niche_value = (niche_value as u128).wrapping_add(*niche_start); + if niche_value == 0 && matches!(tag.primitive(), Primitive::Pointer(_)) { + discr_ty.null() + } else { + Expr::int_constant(niche_value, discr_ty) + } + } + pub(crate) fn variant_min_offset( &self, variants: &IndexVec>, From 46936d4c2f61ac7d8a61813360cdca0b84b152c3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 13 Apr 2023 10:11:47 +0000 Subject: [PATCH 2/4] Implement AggregateKind::{Adt,Closure,Generator} --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 305 +++++++++++++++++- .../codegen/statement.rs | 31 +- tests/kani/Enum/one_two.rs | 23 ++ 3 files changed, 349 insertions(+), 10 deletions(-) create mode 100644 tests/kani/Enum/one_two.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index fc6d87bf440a..422fa458413a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -13,11 +13,12 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; +use rustc_index::vec::IndexVec; use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp}; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; -use rustc_target::abi::{FieldsShape, Size, TagEncoding, Variants}; +use rustc_middle::ty::{self, AdtDef, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; +use rustc_target::abi::{FieldsShape, LayoutS, Size, TagEncoding, VariantIdx, Variants}; use std::collections::BTreeMap; use tracing::{debug, warn}; @@ -279,6 +280,262 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Create a struct expression for an enum using `Variants::Single` as layout (an enum where + /// only one variant has data). + fn codegen_rvalue_enum_single( + &mut self, + variant_index: &VariantIdx, + operands: &[Operand<'tcx>], + overall_t: Type, + adt: &AdtDef<'_>, + ) -> Expr { + let variant = &adt.variants()[*variant_index]; + let components = overall_t.lookup_components(&self.symbol_table).unwrap().clone(); + Expr::struct_expr_with_nondet_fields( + overall_t, + variant + .fields + .iter() + .zip(operands.iter().zip(components.iter())) + .filter_map(|(f, (o, c))| { + let op_expr = self.codegen_operand(o); + let op_width = op_expr.typ().sizeof_in_bits(&self.symbol_table); + if op_width == 0 { + None + } else { + Some(( + InternedString::from(f.name.to_string()), + op_expr.transmute_to(c.typ(), &self.symbol_table), + )) + } + }) + .collect(), + &self.symbol_table, + ) + } + + /// Create a struct expression for an enum using `Variants::Multiple` with direct encoding as + /// layout (a tagged enum). + fn codegen_rvalue_enum_direct( + &mut self, + variant_index: &VariantIdx, + operands: &[Operand<'tcx>], + overall_t: Type, + adt: &AdtDef<'_>, + variants: &IndexVec>, + ) -> Expr { + let fields = overall_t.lookup_components(&self.symbol_table).unwrap().clone(); + assert_eq!(fields.len(), 2, "TagEncoding::Direct encountered for enum with empty variants"); + assert_eq!( + fields[0].name().to_string(), + "case", + "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465" + ); + let case_value = Expr::int_constant(variant_index.index(), fields[0].typ()); + assert_eq!( + fields[1].name().to_string(), + "cases", + "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465" + ); + assert!(matches!(variants[*variant_index].variants, Variants::Single { .. })); + let variant = &adt.variants()[*variant_index]; + if variant.fields.is_empty() { + Expr::struct_expr_with_nondet_fields( + overall_t, + btree_string_map![("case", case_value)], + &self.symbol_table, + ) + } else { + let target_component = fields[1] + .typ() + .lookup_field(variant.name.to_string(), &self.symbol_table) + .unwrap() + .clone(); + let cases_value = Expr::union_expr( + fields[1].typ(), + target_component.name(), + Expr::struct_expr_from_values( + target_component.typ(), + variants[*variant_index] + .fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx])) + .collect(), + &self.symbol_table, + ), + &self.symbol_table, + ); + Expr::struct_expr_from_values( + overall_t, + vec![case_value, cases_value], + &self.symbol_table, + ) + } + } + + /// Create an initializer for an enum using niche encoding. This is done while having access to + /// the lvalue so that it can be selectively updated when a variant is being used that is + /// smaller than the maximum (also known as untagged) variant. + pub fn codegen_enum_assignment( + &mut self, + lvalue: Expr, + variant_index: &VariantIdx, + operands: &[Operand<'tcx>], + ty: Ty<'tcx>, + location: Location, + ) -> Stmt { + let overall_t = self.codegen_ty(ty); + let layout = self.layout_of(ty); + let adt = match &ty.kind() { + ty::Adt(adt, _) => adt, + _ => unreachable!(), + }; + match &layout.variants { + Variants::Single { .. } => lvalue.assign( + self.codegen_rvalue_enum_single(variant_index, operands, overall_t, adt), + location, + ), + Variants::Multiple { tag_encoding: TagEncoding::Direct, variants, .. } => lvalue + .assign( + self.codegen_rvalue_enum_direct( + variant_index, + operands, + overall_t, + adt, + variants, + ), + location, + ), + Variants::Multiple { + tag, + tag_encoding: + TagEncoding::Niche { untagged_variant, ref niche_variants, niche_start }, + variants, + tag_field, + .. + } => { + let variant_layout = &variants[*variant_index]; + let target_and_member = { + let variant = &adt.variants()[*variant_index]; + if variant_layout.size.bytes() == 0 { + None + } else { + let target_component = overall_t + .lookup_field(variant.name.to_string(), &self.symbol_table) + .unwrap() + .clone(); + let member_expr = Expr::struct_expr_from_values( + target_component.typ(), + variant_layout + .fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx])) + .collect(), + &self.symbol_table, + ); + Some((target_component, member_expr)) + } + }; + if variant_index == untagged_variant { + // from codegen_enum_niche + let non_zst_count = + variants.iter().filter(|layout| layout.size.bytes() > 0).count(); + let (target_component, member_expr) = match target_and_member { + Some((target_component, member_expr)) => (target_component, member_expr), + _ => unreachable!(), + }; + if non_zst_count > 1 { + lvalue.assign( + Expr::union_expr( + overall_t, + target_component.name(), + member_expr, + &self.symbol_table, + ), + location, + ) + } else { + lvalue.assign( + Expr::struct_expr_with_nondet_fields( + overall_t, + btree_string_map![(target_component.name(), member_expr)], + &self.symbol_table, + ), + location, + ) + } + } else { + let niche_value = self.compute_enum_niche_value( + ty, + variant_index, + tag, + niche_variants, + niche_start, + ); + let niche_offset = layout.fields.offset(*tag_field); + let lvalue_niche = self.codegen_get_niche( + lvalue.clone(), + niche_offset, + niche_value.typ().clone(), + ); + if variant_layout.size.bytes() > 0 { + let (target_component, member_expr) = match target_and_member { + Some((target_component, member_expr)) => { + (target_component, member_expr) + } + _ => unreachable!(), + }; + let lvalue_data = lvalue.reinterpret_cast(target_component.typ()); + // Assign the tag (niche) _after_ the data as the latter may include + // non-deterministic padding values at the address where the nice is. The + // subsequent niche assignment will then set those to a fixed value. + Stmt::block( + vec![ + lvalue_data.assign(member_expr, location), + lvalue_niche.assign(niche_value, location), + ], + location, + ) + } else { + lvalue_niche.assign(niche_value, location) + } + } + } + } + } + + /// Create an initializer for a generator struct. + fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr { + let layout = self.layout_of(ty); + let discriminant_field = match &layout.variants { + Variants::Multiple { tag_encoding: TagEncoding::Direct, tag_field, .. } => tag_field, + _ => unreachable!( + "Expected generators to have multiple variants and direct encoding, but found: {layout:?}" + ), + }; + let overall_t = self.codegen_ty(ty); + let direct_fields = overall_t.lookup_field("direct_fields", &self.symbol_table).unwrap(); + let mut operands_iter = operands.iter(); + let direct_fields_expr = Expr::struct_expr_from_values( + direct_fields.typ(), + layout + .fields + .index_by_increasing_offset() + .map(|idx| { + let field_ty = layout.field(self, idx).ty; + if idx == *discriminant_field { + Expr::int_constant(0, self.codegen_ty(field_ty)) + } else { + self.codegen_operand(operands_iter.next().unwrap()) + } + }) + .collect(), + &self.symbol_table, + ); + assert!(operands_iter.next().is_none()); + Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table) + } + fn codegen_rvalue_aggregate( &mut self, k: &AggregateKind<'tcx>, @@ -304,7 +561,45 @@ impl<'tcx> GotocCtx<'tcx> { ) } } - AggregateKind::Tuple => { + AggregateKind::Adt(_, _, _, _, Some(active_field_index)) => { + assert!(res_ty.is_union()); + assert_eq!(operands.len(), 1); + let typ = self.codegen_ty(res_ty); + let components = typ.lookup_components(&self.symbol_table).unwrap(); + Expr::union_expr( + typ, + components[active_field_index].name(), + self.codegen_operand(&operands[0]), + &self.symbol_table, + ) + } + AggregateKind::Adt(_, _, _, _, _) if res_ty.is_simd() => { + let typ = self.codegen_ty(res_ty); + let layout = self.layout_of(res_ty); + let vector_element_type = typ.base_type().unwrap().clone(); + Expr::vector_expr( + typ, + layout + .fields + .index_by_increasing_offset() + .map(|idx| { + let cgo = self.codegen_operand(&operands[idx]); + // The input operand might actually be a one-element array, as seen + // when running assess on firecracker. + if *cgo.typ() == vector_element_type { + cgo + } else { + cgo.transmute_to(vector_element_type.clone(), &self.symbol_table) + } + }) + .collect(), + ) + } + AggregateKind::Adt(..) if res_ty.is_enum() => { + // codegen_statement handles this case so that we have access to the lvalue + unreachable!() + } + AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => { let typ = self.codegen_ty(res_ty); let layout = self.layout_of(res_ty); Expr::struct_expr_from_values( @@ -317,9 +612,7 @@ impl<'tcx> GotocCtx<'tcx> { &self.symbol_table, ) } - AggregateKind::Adt(_, _, _, _, _) => unimplemented!(), - AggregateKind::Closure(_, _) => unimplemented!(), - AggregateKind::Generator(_, _, _) => unimplemented!(), + AggregateKind::Generator(_, _, _) => self.codegen_rvalue_generator(&operands, res_ty), } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index b237e5679249..e2d999e9fc0d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -9,8 +9,8 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ - AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, - SwitchTargets, Terminator, TerminatorKind, + AggregateKind, AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Rvalue, + Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, }; use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; @@ -48,9 +48,32 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) } else { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) + match r { + Rvalue::Aggregate(ref k, operands) if rty.is_enum() => { + if let AggregateKind::Adt(_, variant_index, _, _, _) = **k { + let lvalue_expr = unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place(l) + ) + .goto_expr; + self.codegen_enum_assignment( + lvalue_expr, + &variant_index, + &operands, + rty, + location, + ) + } else { + unreachable!() + } + } + _ => unwrap_or_return_codegen_unimplemented_stmt!( + self, + self.codegen_place(l) + ) .goto_expr - .assign(self.codegen_rvalue(r, location), location) + .assign(self.codegen_rvalue(r, location), location), + } } } StatementKind::Deinit(place) => self.codegen_deinit(place, location), diff --git a/tests/kani/Enum/one_two.rs b/tests/kani/Enum/one_two.rs new file mode 100644 index 000000000000..54b2dc8bbc0b --- /dev/null +++ b/tests/kani/Enum/one_two.rs @@ -0,0 +1,23 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +enum Niche_Enum { + One(bool), + Two(bool, bool), +} + +enum Enum { + One(u32), + Two(u32, u32), +} + +#[kani::proof] +fn check() { + // This will have one operand. + let _var = Niche_Enum::One(false); + // This will have two operands -- true and false + let _var = Niche_Enum::Two(true, false); + // This will have one operand. + let _var = Enum::One(1); + // This will have two operands -- 2 and 3 + let _var = Enum::Two(2, 3); +} From 8d0c26b756d2dbb3c74b78a51fa98833aca9591e Mon Sep 17 00:00:00 2001 From: tautschnig Date: Tue, 28 Mar 2023 20:44:05 +0000 Subject: [PATCH 3/4] Upgrade Rust toolchain to nightly-2023-02-05 --- rust-toolchain.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 7844043def0b..4747ffef5d2d 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-02-04" +channel = "nightly-2023-02-05" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"] From 80afe842aa31669c4f62e584521119a7baba6001 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Apr 2023 19:43:37 -0700 Subject: [PATCH 4/4] Adjust enum aggregation Simplify the code by reusing some of the existing logic --- .../codegen_cprover_gotoc/codegen/place.rs | 11 + .../codegen_cprover_gotoc/codegen/rvalue.rs | 310 +++++------------- .../codegen/statement.rs | 154 ++++----- .../src/codegen_cprover_gotoc/codegen/typ.rs | 27 +- tests/kani/Enum/multiple_never.rs | 39 +++ 5 files changed, 196 insertions(+), 345 deletions(-) create mode 100644 tests/kani/Enum/multiple_never.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 67801f747acc..72440401275a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -624,6 +624,17 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Given a projection, generate an lvalue that represents the given variant index. + pub fn codegen_variant_lvalue( + &mut self, + initial_projection: ProjectedPlace<'tcx>, + variant_idx: VariantIdx, + ) -> ProjectedPlace<'tcx> { + debug!(?initial_projection, ?variant_idx, "codegen_variant_lvalue"); + let downcast = ProjectionElem::Downcast(None, variant_idx); + self.codegen_projection(Ok(initial_projection), downcast).unwrap() + } + // https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.ProjectionElem.html // ConstantIndex // [−] diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 422fa458413a..e17cd7f3031a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -2,6 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT use super::typ::pointee_type; +use crate::codegen_cprover_gotoc::codegen::place::{ProjectedPlace, TypeOrVariant}; use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; @@ -13,14 +14,13 @@ use cbmc::goto_program::{Expr, Location, Stmt, Symbol, Type}; use cbmc::MachineModel; use cbmc::{btree_string_map, InternString, InternedString}; use num::bigint::BigInt; -use rustc_index::vec::IndexVec; use rustc_middle::mir::{AggregateKind, BinOp, CastKind, NullOp, Operand, Place, Rvalue, UnOp}; use rustc_middle::ty::adjustment::PointerCast; use rustc_middle::ty::layout::LayoutOf; -use rustc_middle::ty::{self, AdtDef, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; -use rustc_target::abi::{FieldsShape, LayoutS, Size, TagEncoding, VariantIdx, Variants}; +use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy, VtblEntry}; +use rustc_target::abi::{FieldsShape, Size, TagEncoding, VariantIdx, Variants}; use std::collections::BTreeMap; -use tracing::{debug, warn}; +use tracing::{debug, trace, warn}; impl<'tcx> GotocCtx<'tcx> { fn codegen_comparison(&mut self, op: &BinOp, e1: &Operand<'tcx>, e2: &Operand<'tcx>) -> Expr { @@ -280,230 +280,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Create a struct expression for an enum using `Variants::Single` as layout (an enum where - /// only one variant has data). - fn codegen_rvalue_enum_single( - &mut self, - variant_index: &VariantIdx, - operands: &[Operand<'tcx>], - overall_t: Type, - adt: &AdtDef<'_>, - ) -> Expr { - let variant = &adt.variants()[*variant_index]; - let components = overall_t.lookup_components(&self.symbol_table).unwrap().clone(); - Expr::struct_expr_with_nondet_fields( - overall_t, - variant - .fields - .iter() - .zip(operands.iter().zip(components.iter())) - .filter_map(|(f, (o, c))| { - let op_expr = self.codegen_operand(o); - let op_width = op_expr.typ().sizeof_in_bits(&self.symbol_table); - if op_width == 0 { - None - } else { - Some(( - InternedString::from(f.name.to_string()), - op_expr.transmute_to(c.typ(), &self.symbol_table), - )) - } - }) - .collect(), - &self.symbol_table, - ) - } - - /// Create a struct expression for an enum using `Variants::Multiple` with direct encoding as - /// layout (a tagged enum). - fn codegen_rvalue_enum_direct( - &mut self, - variant_index: &VariantIdx, - operands: &[Operand<'tcx>], - overall_t: Type, - adt: &AdtDef<'_>, - variants: &IndexVec>, - ) -> Expr { - let fields = overall_t.lookup_components(&self.symbol_table).unwrap().clone(); - assert_eq!(fields.len(), 2, "TagEncoding::Direct encountered for enum with empty variants"); - assert_eq!( - fields[0].name().to_string(), - "case", - "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465" - ); - let case_value = Expr::int_constant(variant_index.index(), fields[0].typ()); - assert_eq!( - fields[1].name().to_string(), - "cases", - "Unexpected field in enum/generator. Please report your failing case at https://github.com/model-checking/kani/issues/1465" - ); - assert!(matches!(variants[*variant_index].variants, Variants::Single { .. })); - let variant = &adt.variants()[*variant_index]; - if variant.fields.is_empty() { - Expr::struct_expr_with_nondet_fields( - overall_t, - btree_string_map![("case", case_value)], - &self.symbol_table, - ) - } else { - let target_component = fields[1] - .typ() - .lookup_field(variant.name.to_string(), &self.symbol_table) - .unwrap() - .clone(); - let cases_value = Expr::union_expr( - fields[1].typ(), - target_component.name(), - Expr::struct_expr_from_values( - target_component.typ(), - variants[*variant_index] - .fields - .index_by_increasing_offset() - .map(|idx| self.codegen_operand(&operands[idx])) - .collect(), - &self.symbol_table, - ), - &self.symbol_table, - ); - Expr::struct_expr_from_values( - overall_t, - vec![case_value, cases_value], - &self.symbol_table, - ) - } - } - - /// Create an initializer for an enum using niche encoding. This is done while having access to - /// the lvalue so that it can be selectively updated when a variant is being used that is - /// smaller than the maximum (also known as untagged) variant. - pub fn codegen_enum_assignment( - &mut self, - lvalue: Expr, - variant_index: &VariantIdx, - operands: &[Operand<'tcx>], - ty: Ty<'tcx>, - location: Location, - ) -> Stmt { - let overall_t = self.codegen_ty(ty); - let layout = self.layout_of(ty); - let adt = match &ty.kind() { - ty::Adt(adt, _) => adt, - _ => unreachable!(), - }; - match &layout.variants { - Variants::Single { .. } => lvalue.assign( - self.codegen_rvalue_enum_single(variant_index, operands, overall_t, adt), - location, - ), - Variants::Multiple { tag_encoding: TagEncoding::Direct, variants, .. } => lvalue - .assign( - self.codegen_rvalue_enum_direct( - variant_index, - operands, - overall_t, - adt, - variants, - ), - location, - ), - Variants::Multiple { - tag, - tag_encoding: - TagEncoding::Niche { untagged_variant, ref niche_variants, niche_start }, - variants, - tag_field, - .. - } => { - let variant_layout = &variants[*variant_index]; - let target_and_member = { - let variant = &adt.variants()[*variant_index]; - if variant_layout.size.bytes() == 0 { - None - } else { - let target_component = overall_t - .lookup_field(variant.name.to_string(), &self.symbol_table) - .unwrap() - .clone(); - let member_expr = Expr::struct_expr_from_values( - target_component.typ(), - variant_layout - .fields - .index_by_increasing_offset() - .map(|idx| self.codegen_operand(&operands[idx])) - .collect(), - &self.symbol_table, - ); - Some((target_component, member_expr)) - } - }; - if variant_index == untagged_variant { - // from codegen_enum_niche - let non_zst_count = - variants.iter().filter(|layout| layout.size.bytes() > 0).count(); - let (target_component, member_expr) = match target_and_member { - Some((target_component, member_expr)) => (target_component, member_expr), - _ => unreachable!(), - }; - if non_zst_count > 1 { - lvalue.assign( - Expr::union_expr( - overall_t, - target_component.name(), - member_expr, - &self.symbol_table, - ), - location, - ) - } else { - lvalue.assign( - Expr::struct_expr_with_nondet_fields( - overall_t, - btree_string_map![(target_component.name(), member_expr)], - &self.symbol_table, - ), - location, - ) - } - } else { - let niche_value = self.compute_enum_niche_value( - ty, - variant_index, - tag, - niche_variants, - niche_start, - ); - let niche_offset = layout.fields.offset(*tag_field); - let lvalue_niche = self.codegen_get_niche( - lvalue.clone(), - niche_offset, - niche_value.typ().clone(), - ); - if variant_layout.size.bytes() > 0 { - let (target_component, member_expr) = match target_and_member { - Some((target_component, member_expr)) => { - (target_component, member_expr) - } - _ => unreachable!(), - }; - let lvalue_data = lvalue.reinterpret_cast(target_component.typ()); - // Assign the tag (niche) _after_ the data as the latter may include - // non-deterministic padding values at the address where the nice is. The - // subsequent niche assignment will then set those to a fixed value. - Stmt::block( - vec![ - lvalue_data.assign(member_expr, location), - lvalue_niche.assign(niche_value, location), - ], - location, - ) - } else { - lvalue_niche.assign(niche_value, location) - } - } - } - } - } - /// Create an initializer for a generator struct. fn codegen_rvalue_generator(&mut self, operands: &[Operand<'tcx>], ty: Ty<'tcx>) -> Expr { let layout = self.layout_of(ty); @@ -536,13 +312,80 @@ impl<'tcx> GotocCtx<'tcx> { Expr::union_expr(overall_t, "direct_fields", direct_fields_expr, &self.symbol_table) } + /// This code will generate an expression that initializes an enumeration. + /// + /// It will first create a temporary variant with the same enum type. + /// Initialize the case structure and set its discriminant. + /// Finally, it will return the temporary value. + fn codegen_rvalue_enum_aggregate( + &mut self, + variant_index: VariantIdx, + operands: &[Operand<'tcx>], + res_ty: Ty<'tcx>, + loc: Location, + ) -> Expr { + let mut stmts = vec![]; + let typ = self.codegen_ty(res_ty); + // 1- Create a temporary value of the enum type. + tracing::debug!(?typ, ?res_ty, "aggregate_enum"); + let (temp_var, decl) = self.decl_temp_variable(typ.clone(), None, loc); + stmts.push(decl); + if !operands.is_empty() { + // 2- Initialize the members of the temporary variant. + let initial_projection = ProjectedPlace::try_new( + temp_var.clone(), + TypeOrVariant::Type(res_ty), + None, + None, + self, + ) + .unwrap(); + let variant_proj = self.codegen_variant_lvalue(initial_projection, variant_index); + let variant_expr = variant_proj.goto_expr.clone(); + let layout = self.layout_of(res_ty); + let fields = match &layout.variants { + Variants::Single { index } => { + if *index != variant_index { + // This may occur if all variants except for the one pointed by + // index can never be constructed. Generic code might still try + // to initialize the non-existing invariant. + trace!(?res_ty, ?variant_index, "Unreachable invariant"); + return Expr::nondet(typ); + } + &layout.fields + } + Variants::Multiple { variants, .. } => &variants[variant_index].fields, + }; + + trace!(?variant_expr, ?fields, ?operands, "codegen_aggregate enum"); + let init_struct = Expr::struct_expr_from_values( + variant_expr.typ().clone(), + fields + .index_by_increasing_offset() + .map(|idx| self.codegen_operand(&operands[idx])) + .collect(), + &self.symbol_table, + ); + let assign_case = variant_proj.goto_expr.assign(init_struct, loc); + stmts.push(assign_case); + } + // 3- Set discriminant. + let set_discriminant = + self.codegen_set_discriminant(res_ty, temp_var.clone(), variant_index, loc); + stmts.push(set_discriminant); + // 4- Return temporary variable. + stmts.push(temp_var.as_stmt(loc)); + Expr::statement_expression(stmts, typ) + } + fn codegen_rvalue_aggregate( &mut self, - k: &AggregateKind<'tcx>, + aggregate: &AggregateKind<'tcx>, operands: &[Operand<'tcx>], res_ty: Ty<'tcx>, + loc: Location, ) -> Expr { - match *k { + match *aggregate { AggregateKind::Array(et) => { if et.is_unit() { Expr::struct_expr_from_values( @@ -595,9 +438,8 @@ impl<'tcx> GotocCtx<'tcx> { .collect(), ) } - AggregateKind::Adt(..) if res_ty.is_enum() => { - // codegen_statement handles this case so that we have access to the lvalue - unreachable!() + AggregateKind::Adt(_, variant_index, ..) if res_ty.is_enum() => { + self.codegen_rvalue_enum_aggregate(variant_index, operands, res_ty, loc) } AggregateKind::Adt(..) | AggregateKind::Closure(..) | AggregateKind::Tuple => { let typ = self.codegen_ty(res_ty); @@ -699,7 +541,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_get_discriminant(place, pt, res_ty) } Rvalue::Aggregate(ref k, operands) => { - self.codegen_rvalue_aggregate(k, operands, res_ty) + self.codegen_rvalue_aggregate(k, operands, res_ty, loc) } Rvalue::ThreadLocalRef(def_id) => { // Since Kani is single-threaded, we treat a thread local like a static variable: diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index e2d999e9fc0d..4892ed988e39 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -9,14 +9,15 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type}; use rustc_hir::def_id::DefId; use rustc_middle::mir; use rustc_middle::mir::{ - AggregateKind, AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Rvalue, - Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind, + AssertKind, BasicBlock, NonDivergingIntrinsic, Operand, Place, Statement, StatementKind, + SwitchTargets, Terminator, TerminatorKind, }; use rustc_middle::ty; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{Instance, InstanceDef, Ty}; use rustc_span::Span; -use rustc_target::abi::{FieldsShape, TagEncoding, Variants}; +use rustc_target::abi::VariantIdx; +use rustc_target::abi::{FieldsShape, Primitive, TagEncoding, Variants}; use tracing::{debug, debug_span, trace}; impl<'tcx> GotocCtx<'tcx> { @@ -48,93 +49,18 @@ impl<'tcx> GotocCtx<'tcx> { .goto_expr .assign(self.codegen_rvalue(r, location).cast_to(Type::c_bool()), location) } else { - match r { - Rvalue::Aggregate(ref k, operands) if rty.is_enum() => { - if let AggregateKind::Adt(_, variant_index, _, _, _) = **k { - let lvalue_expr = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(l) - ) - .goto_expr; - self.codegen_enum_assignment( - lvalue_expr, - &variant_index, - &operands, - rty, - location, - ) - } else { - unreachable!() - } - } - _ => unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(l) - ) + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) .goto_expr - .assign(self.codegen_rvalue(r, location), location), - } + .assign(self.codegen_rvalue(r, location), location) } } StatementKind::Deinit(place) => self.codegen_deinit(place, location), StatementKind::SetDiscriminant { place, variant_index } => { - // this requires place points to an enum type. - let pt = self.place_ty(place); - let layout = self.layout_of(pt); - match &layout.variants { - Variants::Single { .. } => Stmt::skip(location), - Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => { - let discr = - pt.discriminant_for_variant(self.tcx, *variant_index).unwrap(); - let discr_t = self.codegen_enum_discr_typ(pt); - // The constant created below may not fit into the type. - // https://github.com/model-checking/kani/issues/996 - // - // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` - // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` - // because when it tries to codegen `std::cmp::Ordering` (which should produce - // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: - // - // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); - // DISCRIMINANT - val:255 ty:i8 - // DISCRIMINANT - val:0 ty:i8 - // DISCRIMINANT - val:1 ty:i8 - let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); - let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - self.codegen_discriminant_field(place_goto_expr, pt) - .assign(discr, location) - } - TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { - if untagged_variant != variant_index { - let value = self.compute_enum_niche_value( - pt, - variant_index, - tag, - niche_variants, - niche_start, - ); - let place = unwrap_or_return_codegen_unimplemented_stmt!( - self, - self.codegen_place(place) - ) - .goto_expr; - let offset = match &layout.fields { - FieldsShape::Arbitrary { offsets, .. } => offsets[0], - _ => unreachable!("niche encoding must have arbitrary fields"), - }; - self.codegen_get_niche(place, offset, value.typ().clone()) - .assign(value, location) - } else { - Stmt::skip(location) - } - } - }, - } + let dest_ty = self.place_ty(place); + let dest_expr = + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) + .goto_expr; + self.codegen_set_discriminant(dest_ty, dest_expr, *variant_index, location) } StatementKind::StorageLive(_) => Stmt::skip(location), // TODO: fix me StatementKind::StorageDead(_) => Stmt::skip(location), // TODO: fix me @@ -277,6 +203,64 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Create a statement that sets the variable discriminant to the value that corresponds to the + /// variant index. + pub fn codegen_set_discriminant( + &mut self, + dest_ty: Ty<'tcx>, + dest_expr: Expr, + variant_index: VariantIdx, + location: Location, + ) -> Stmt { + // this requires place points to an enum type. + let layout = self.layout_of(dest_ty); + match &layout.variants { + Variants::Single { .. } => Stmt::skip(location), + Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { + TagEncoding::Direct => { + let discr = dest_ty.discriminant_for_variant(self.tcx, variant_index).unwrap(); + let discr_t = self.codegen_enum_discr_typ(dest_ty); + // The constant created below may not fit into the type. + // https://github.com/model-checking/kani/issues/996 + // + // It doesn't matter if the type comes from `self.codegen_enum_discr_typ(pt)` + // or `discr.ty`. It looks like something is wrong with `discriminat_for_variant` + // because when it tries to codegen `std::cmp::Ordering` (which should produce + // discriminant values -1, 0 and 1) it produces values 255, 0 and 1 with i8 types: + // + // debug!("DISCRIMINANT - val:{:?} ty:{:?}", discr.val, discr.ty); + // DISCRIMINANT - val:255 ty:i8 + // DISCRIMINANT - val:0 ty:i8 + // DISCRIMINANT - val:1 ty:i8 + let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); + self.codegen_discriminant_field(dest_expr, dest_ty).assign(discr, location) + } + TagEncoding::Niche { untagged_variant, niche_variants, niche_start } => { + if *untagged_variant != variant_index { + let offset = match &layout.fields { + FieldsShape::Arbitrary { offsets, .. } => offsets[0], + _ => unreachable!("niche encoding must have arbitrary fields"), + }; + let discr_ty = self.codegen_enum_discr_typ(dest_ty); + let discr_ty = self.codegen_ty(discr_ty); + let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); + let niche_value = (niche_value as u128).wrapping_add(*niche_start); + let value = if niche_value == 0 + && matches!(tag.primitive(), Primitive::Pointer(_)) + { + discr_ty.null() + } else { + Expr::int_constant(niche_value, discr_ty.clone()) + }; + self.codegen_get_niche(dest_expr, offset, discr_ty).assign(value, location) + } else { + Stmt::skip(location) + } + } + }, + } + } + /// From rustc doc: "This writes `uninit` bytes to the entire place." /// Our model of GotoC has a similar statement, which is later lowered /// to assigning a Nondet in CBMC, with a comment specifying that it diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 97bd3c6b38cf..8508febbeb22 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -20,12 +20,11 @@ use rustc_middle::ty::{ use rustc_middle::ty::{List, TypeFoldable}; use rustc_span::def_id::DefId; use rustc_target::abi::{ - Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Scalar, Size, TagEncoding, TyAndLayout, + Abi::Vector, FieldsShape, Integer, LayoutS, Primitive, Size, TagEncoding, TyAndLayout, VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; use std::iter; -use std::ops::RangeInclusive; use tracing::{debug, trace, warn}; use ty::layout::HasParamEnv; @@ -1572,30 +1571,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Compute the discriminant expression for an enum that uses niche optimization. - /// - /// We follow the logic of the SSA and Cranelift back-ends in doing the computation: - /// - /// - pub fn compute_enum_niche_value( - &mut self, - enum_ty: Ty<'tcx>, - variant_index: &VariantIdx, - tag: &Scalar, - niche_variants: &RangeInclusive, - niche_start: &u128, - ) -> Expr { - let discr_ty = self.codegen_enum_discr_typ(enum_ty); - let discr_ty = self.codegen_ty(discr_ty); - let niche_value = variant_index.as_u32() - niche_variants.start().as_u32(); - let niche_value = (niche_value as u128).wrapping_add(*niche_start); - if niche_value == 0 && matches!(tag.primitive(), Primitive::Pointer(_)) { - discr_ty.null() - } else { - Expr::int_constant(niche_value, discr_ty) - } - } - pub(crate) fn variant_min_offset( &self, variants: &IndexVec>, diff --git a/tests/kani/Enum/multiple_never.rs b/tests/kani/Enum/multiple_never.rs new file mode 100644 index 000000000000..4dc3f54d1b44 --- /dev/null +++ b/tests/kani/Enum/multiple_never.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test is to check how Kani handle enums where only one variant is valid. +#![feature(never_type)] + +enum MyResult { + Yes(Y), + No(N), + Maybe(M), +} + +fn change_maybe(orig: MyResult, val: O) -> MyResult { + match orig { + MyResult::Yes(y) => MyResult::Yes(y), + MyResult::No(n) => MyResult::No(n), + MyResult::Maybe(m) => MyResult::Maybe(val), + } +} + +fn check() -> Result { + let val = Result::::Ok(10)?; + Ok(val) +} + +fn checkErr() -> Result { + let val = Result::::Err(10)?; +} + +fn checkMaybe() -> MyResult { + change_maybe(MyResult::::Maybe(10), 0) +} + +#[kani::proof] +pub fn harness_residual() { + let _ = checkMaybe(); + let _ = checkErr(); + let _ = check(); +}