From a576aa49a9f356b99933dff705fc072a9d2de9a8 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 11 Apr 2023 19:43:37 -0700 Subject: [PATCH] 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 | 314 +++++------------- .../codegen/statement.rs | 154 ++++----- .../src/codegen_cprover_gotoc/codegen/typ.rs | 27 +- tests/kani/Enum/multiple_never.rs | 39 +++ 5 files changed, 200 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..9440560baf4b 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,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, + }; + + 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| { + 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( @@ -595,9 +442,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 +545,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(); +}