diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs index 5fa9ede910ee..4d4c1db17912 100644 --- a/cprover_bindings/src/goto_program/expr.rs +++ b/cprover_bindings/src/goto_program/expr.rs @@ -131,7 +131,7 @@ pub enum ExprValue { StringConstant { s: InternedString, }, - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, field2, ... } <<<` Struct { values: Vec, @@ -142,7 +142,7 @@ pub enum ExprValue { }, /// `(typ) self`. Target type is in the outer `Expr` struct. Typecast(Expr), - /// Union initializer + /// Union initializer /// `union foo the_foo = >>> {.field = value } <<<` Union { value: Expr, @@ -681,7 +681,7 @@ impl Expr { expr!(StatementExpression { statements: ops }, typ) } - /// Internal helper function for Struct initalizer + /// Internal helper function for Struct initalizer /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<` /// ALL fields must be given, including padding fn struct_expr_with_explicit_padding( @@ -698,7 +698,7 @@ impl Expr { expr!(Struct { values }, typ) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {.field1 = val1, .field2 = val2, ... } <<<` /// Note that only the NON padding fields should be explicitly given. /// Padding fields are automatically inserted using the type from the `SymbolTable` @@ -719,7 +719,7 @@ impl Expr { "Error in struct_expr; mismatch in number of fields and components.\n\t{typ:?}\n\t{components:?}" ); - // Check that each formal field has an value + // Check that each formal field has a value for field in non_padding_fields { let field_typ = field.field_typ().unwrap(); let value = components.get(&field.name()).unwrap(); @@ -764,7 +764,7 @@ impl Expr { Expr::struct_expr_from_values(typ, values, symbol_table) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, field2, ... } <<<` /// Note that only the NON padding fields should be explicitly given. /// Padding fields are automatically inserted using the type from the `SymbolTable` @@ -800,7 +800,7 @@ impl Expr { Expr::struct_expr_with_explicit_padding(typ, fields, values) } - /// Struct initializer + /// Struct initializer /// `struct foo the_foo = >>> {field1, padding2, field3, ... } <<<` /// Note that padding fields should be explicitly given. /// This would be used when the values and padding have already been combined, @@ -859,7 +859,7 @@ impl Expr { self.transmute_to(t, st) } - /// Union initializer + /// Union initializer /// `union foo the_foo = >>> {.field = value } <<<` pub fn union_expr>( typ: Type, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 67801f747acc..00b215a64007 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -231,6 +231,17 @@ impl<'tcx> TypeOrVariant<'tcx> { } } } + + #[allow(dead_code)] + pub fn expect_gen_variant(&self) -> VariantIdx { + match self { + TypeOrVariant::Type(t) => panic!("expect a generator but found type: {t:?}"), + TypeOrVariant::Variant(v) => { + panic!("expect a generator but found variant: {v:?}") + } + TypeOrVariant::GeneratorVariant(v) => *v, + } + } } impl<'tcx> GotocCtx<'tcx> { @@ -624,6 +635,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 7dccc7c8810d..a8b78975a04f 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); @@ -540,13 +316,84 @@ 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, + }; + + debug!(?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| { + let op = self.codegen_operand(&operands[idx]); + debug!(?op, ?idx, "codegen_aggregate enum op"); + op + }) + .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( @@ -597,9 +444,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); @@ -701,7 +547,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..7e881909ef79 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> { @@ -30,111 +31,39 @@ impl<'tcx> GotocCtx<'tcx> { debug!(?stmt, kind=?stmt.kind, "handling_statement"); let location = self.codegen_span(&stmt.source_info.span); match &stmt.kind { - StatementKind::Assign(box (l, r)) => { - let lty = self.place_ty(l); - let rty = self.rvalue_ty(r); + StatementKind::Assign(box (lhs, rhs)) => { + let lty = self.place_ty(lhs); + let rty = self.rvalue_ty(rhs); // we ignore assignment for all zero size types if self.is_zst(lty) { Stmt::skip(location) - } else if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { - // implicit address of a function pointer, e.g. - // let fp: fn() -> i32 = foo; - // where the reference is implicit. - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .goto_expr - .assign(self.codegen_rvalue(r, location).address_of(), location) - } else if rty.is_bool() { - unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(l)) - .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) - ) - .goto_expr - .assign(self.codegen_rvalue(r, location), location), + let rvalue = self.codegen_rvalue(rhs, location); + if lty.is_fn_ptr() && rty.is_fn() && !rty.is_fn_ptr() { + // implicit address of a function pointer, e.g. + // let fp: fn() -> i32 = foo; + // where the reference is implicit. + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs)) + .goto_expr + .assign(rvalue.address_of(), location) + } else if rty.is_bool() { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs)) + .goto_expr + .assign(rvalue.cast_to(Type::c_bool()), location) + } else { + unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(lhs)) + .goto_expr + .assign(rvalue, 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 +206,62 @@ impl<'tcx> GotocCtx<'tcx> { } } + 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..9bea3de6d720 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; @@ -1102,7 +1101,12 @@ impl<'tcx> GotocCtx<'tcx> { variants, .. } => (tag_field, variants), - _ => unreachable!("Generators have more than one variant and use direct encoding"), + Variants::Multiple { .. } => unreachable!( + "Expected generator with direct encoding, got: {type_and_layout:?}" + ), + Variants::Single { .. } => unreachable!( + "Expected generator with multiple variants, got: {type_and_layout:?}" + ), }; // generate a struct for the direct fields of the layout (fields that don't occur in the variants) let direct_fields = DatatypeComponent::Field { @@ -1572,30 +1576,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(); +}