From ac34884314d13ab92faae93a5721adeccf012e29 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 14 Jul 2022 18:17:06 -0400 Subject: [PATCH 01/15] Implement support for generators --- .../codegen_cprover_gotoc/codegen/place.rs | 80 +++--- .../codegen/statement.rs | 23 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 249 +++++++++++++----- .../src/codegen_cprover_gotoc/utils/utils.rs | 6 - 4 files changed, 235 insertions(+), 123 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index d35e6e6d8bf3..7d6a41871961 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -15,7 +15,7 @@ use rustc_middle::{ mir::{Field, Local, Place, ProjectionElem}, ty::{self, Ty, TypeAndMut, VariantDef}, }; -use rustc_target::abi::{TagEncoding, Variants}; +use rustc_target::abi::{TagEncoding, VariantIdx, Variants}; use tracing::{debug, trace, warn}; /// A projection in Kani can either be to a type (the normal case), @@ -24,6 +24,7 @@ use tracing::{debug, trace, warn}; pub enum TypeOrVariant<'tcx> { Type(Ty<'tcx>), Variant(&'tcx VariantDef), + GeneratorVariant(VariantIdx), } /// A struct for storing the data for passing to `codegen_unimplemented` @@ -129,7 +130,7 @@ impl<'tcx> ProjectedPlace<'tcx> { } } // TODO: handle Variant https://github.com/model-checking/kani/issues/448 - TypeOrVariant::Variant(_) => None, + TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => None, } } @@ -197,7 +198,7 @@ impl<'tcx> TypeOrVariant<'tcx> { pub fn monomorphize(self, ctx: &GotocCtx<'tcx>) -> Self { match self { TypeOrVariant::Type(t) => TypeOrVariant::Type(ctx.monomorphize(t)), - TypeOrVariant::Variant(_) => self, + TypeOrVariant::Variant(_) | TypeOrVariant::GeneratorVariant(_) => self, } } } @@ -207,6 +208,9 @@ impl<'tcx> TypeOrVariant<'tcx> { match self { TypeOrVariant::Type(t) => *t, TypeOrVariant::Variant(v) => panic!("expect a type but variant is found: {:?}", v), + TypeOrVariant::GeneratorVariant(v) => { + panic!("expect a type but generator variant is found: {:?}", v) + } } } @@ -215,6 +219,9 @@ impl<'tcx> TypeOrVariant<'tcx> { match self { TypeOrVariant::Type(t) => panic!("expect a variant but type is found: {:?}", t), TypeOrVariant::Variant(v) => v, + TypeOrVariant::GeneratorVariant(v) => { + panic!("expect a variant but generator variant found {:?}", v) + } } } } @@ -269,12 +276,9 @@ impl<'tcx> GotocCtx<'tcx> { Ok(res.member(&field.name.to_string(), &self.symbol_table)) } ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)), - ty::Generator(..) => Err(UnimplementedData::new( - "ty::Generator", - "https://github.com/model-checking/kani/issues/416", - Type::code(vec![], Type::empty()), - *res.location(), - )), + ty::Generator(..) => unreachable!( + "field access is only possible for generator variants, not the generator type" + ), _ => unimplemented!(), } } @@ -283,6 +287,10 @@ impl<'tcx> GotocCtx<'tcx> { let field = &v.fields[f.index()]; Ok(res.member(&field.name.to_string(), &self.symbol_table)) } + TypeOrVariant::GeneratorVariant(_) => { + let field_name = self.generator_field_name(f.index().into()); + Ok(res.member(field_name, &self.symbol_table)) + } } } @@ -498,33 +506,37 @@ impl<'tcx> GotocCtx<'tcx> { ProjectionElem::Downcast(_, idx) => { // downcast converts a variable of an enum type to one of its discriminated cases let t = before.mir_typ(); - match t.kind() { + let (case_name, type_or_variant) = match t.kind() { ty::Adt(def, _) => { - let variant = def.variants().get(idx).unwrap(); - let case_name = variant.name.to_string(); - let typ = TypeOrVariant::Variant(variant); - let expr = match &self.layout_of(t).variants { - Variants::Single { .. } => before.goto_expr, - Variants::Multiple { tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => before - .goto_expr - .member("cases", &self.symbol_table) - .member(&case_name, &self.symbol_table), - TagEncoding::Niche { .. } => { - before.goto_expr.member(&case_name, &self.symbol_table) - } - }, - }; - ProjectedPlace::try_new( - expr, - typ, - before.fat_ptr_goto_expr, - before.fat_ptr_mir_typ, - self, - ) + let variant = def.variant(idx); + (variant.name.to_string(), TypeOrVariant::Variant(variant)) } - _ => unreachable!("it's a bug to reach here!"), - } + ty::Generator(..) => ( + self.generator_variant_field_name(idx), + TypeOrVariant::GeneratorVariant(idx), + ), + _ => unreachable!("it's a bug to reach here! {:?}", &t.kind()), + }; + let layout = self.layout_of(t); + let expr = match &layout.variants { + Variants::Single { .. } => before.goto_expr, + Variants::Multiple { tag_encoding, .. } => match tag_encoding { + TagEncoding::Direct => before + .goto_expr + .member("cases", &self.symbol_table) + .member(&case_name, &self.symbol_table), + TagEncoding::Niche { .. } => { + before.goto_expr.member(&case_name, &self.symbol_table) + } + }, + }; + ProjectedPlace::try_new( + expr, + type_or_variant, + before.fat_ptr_goto_expr, + before.fat_ptr_mir_typ, + self, + ) } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 7b04cbad6b45..cf8b6394b7dd 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -360,9 +360,7 @@ impl<'tcx> GotocCtx<'tcx> { args.iter() .filter_map(|o| { let ot = self.operand_ty(o); - if self.ignore_var_ty(ot) { - None - } else if ot.is_bool() { + if ot.is_bool() { Some(self.codegen_operand(o).cast_to(Type::c_bool())) } else { Some(self.codegen_operand(o)) @@ -653,8 +651,6 @@ impl<'tcx> GotocCtx<'tcx> { let layout = self.layout_of(dst_mir_ty); if layout.is_zst() || dst_type.sizeof_in_bits(&self.symbol_table) == 0 { // We ignore assignment for all zero size types - // Ignore generators too for now: - // https://github.com/model-checking/kani/issues/416 Stmt::skip(location) } else { unwrap_or_return_codegen_unimplemented_stmt!(self, self.codegen_place(place)) @@ -665,26 +661,13 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::SetDiscriminant { place, variant_index } => { // this requires place points to an enum type. let pt = self.place_ty(place); - let (def, _) = match pt.kind() { - ty::Adt(def, substs) => (def, substs), - ty::Generator(..) => { - return self - .codegen_unimplemented( - "ty::Generator", - Type::code(vec![], Type::empty()), - location, - "https://github.com/model-checking/kani/issues/416", - ) - .as_stmt(location); - } - _ => unreachable!(), - }; 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 = def.discriminant_for_variant(self.tcx, *variant_index); + 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 diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 768d2958fc73..49bcd95556ba 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -6,6 +6,7 @@ use cbmc::goto_program::{DatatypeComponent, Expr, Location, Parameter, Symbol, S use cbmc::utils::aggr_tag; use cbmc::{InternString, InternedString}; use rustc_ast::ast::Mutability; +use rustc_hir::{LangItem, Unsafety}; use rustc_index::vec::IndexVec; use rustc_middle::mir::{HasLocalDecls, Local, Operand, Place, Rvalue}; use rustc_middle::ty::layout::LayoutOf; @@ -13,10 +14,12 @@ use rustc_middle::ty::print::with_no_trimmed_paths; use rustc_middle::ty::print::FmtPrinter; use rustc_middle::ty::subst::InternalSubsts; use rustc_middle::ty::{ - self, AdtDef, FloatTy, Instance, IntTy, PolyFnSig, Ty, UintTy, VariantDef, VtblEntry, + self, AdtDef, FloatTy, GeneratorSubsts, Instance, IntTy, PolyFnSig, Ty, UintTy, VariantDef, + VtblEntry, }; use rustc_middle::ty::{List, TypeFoldable}; use rustc_span::def_id::DefId; +use rustc_target::abi::TyAndLayout; use rustc_target::abi::{ Abi::Vector, FieldsShape, Integer, Layout, Primitive, TagEncoding, VariantIdx, Variants, }; @@ -197,6 +200,47 @@ impl<'tcx> GotocCtx<'tcx> { self.sig_with_closure_untupled(sig) } + // Adapted from `fn_sig_for_fn_abi` in compiler/rustc_middle/src/ty/layout.rs + // Code duplication tracked here: https://github.com/model-checking/kani/issues/1365 + fn generator_sig( + &self, + ty: Ty<'tcx>, + substs: ty::subst::SubstsRef<'tcx>, + ) -> ty::PolyFnSig<'tcx> { + let sig = substs.as_generator().poly_sig(); + + let bound_vars = self.tcx.mk_bound_variable_kinds( + sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), + ); + let br = ty::BoundRegion { + var: ty::BoundVar::from_usize(bound_vars.len() - 1), + kind: ty::BoundRegionKind::BrEnv, + }; + let env_region = ty::ReLateBound(ty::INNERMOST, br); + let env_ty = self.tcx.mk_mut_ref(self.tcx.mk_region(env_region), ty); + + let pin_did = self.tcx.require_lang_item(LangItem::Pin, None); + let pin_adt_ref = self.tcx.adt_def(pin_did); + let pin_substs = self.tcx.intern_substs(&[env_ty.into()]); + let env_ty = self.tcx.mk_adt(pin_adt_ref, pin_substs); + + let sig = sig.skip_binder(); + let state_did = self.tcx.require_lang_item(LangItem::GeneratorState, None); + let state_adt_ref = self.tcx.adt_def(state_did); + let state_substs = self.tcx.intern_substs(&[sig.yield_ty.into(), sig.return_ty.into()]); + let ret_ty = self.tcx.mk_adt(state_adt_ref, state_substs); + ty::Binder::bind_with_vars( + self.tcx.mk_fn_sig( + [env_ty, sig.resume_ty].iter(), + &ret_ty, + false, + Unsafety::Normal, + rustc_target::spec::abi::Abi::Rust, + ), + bound_vars, + ) + } + pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> Option> { let fntyp = instance.ty(self.tcx, ty::ParamEnv::reveal_all()); self.monomorphize(match fntyp.kind() { @@ -211,13 +255,7 @@ impl<'tcx> GotocCtx<'tcx> { } Some(sig) } - ty::Generator(_def_id, _substs, _movability) => { - let error_msg = GotocCtx::unsupported_msg( - "The `generators` feature", - Some("https://github.com/model-checking/kani/issues/416"), - ); - self.emit_error_and_exit(&error_msg) - } + ty::Generator(_def_id, substs, _movability) => Some(self.generator_sig(fntyp, substs)), _ => unreachable!("Can't get function signature of type: {:?}", fntyp), }) } @@ -620,7 +658,7 @@ impl<'tcx> GotocCtx<'tcx> { } ty::FnPtr(sig) => self.codegen_function_sig(*sig).to_pointer(), ty::Closure(_, subst) => self.codegen_ty_closure(ty, subst), - ty::Generator(_, subst, _) => self.codegen_ty_generator(subst), + ty::Generator(..) => self.codegen_ty_generator(ty), ty::Never => self.ensure_struct(NEVER_TYPE_EMPTY_STRUCT_NAME, "!", |_, _| vec![]), ty::Tuple(ts) => { if ts.is_empty() { @@ -804,13 +842,129 @@ impl<'tcx> GotocCtx<'tcx> { }) } + pub fn generator_variant_field_name(&self, var_idx: VariantIdx) -> String { + format!("generator_variant_{}", GeneratorSubsts::variant_name(var_idx)) + } + /// Preliminary support for the Generator type kind. The core functionality remains /// unimplemented, but this way we fail at verification time only if paths that /// rely on Generator types are used. - fn codegen_ty_generator(&mut self, substs: ty::subst::SubstsRef<'tcx>) -> Type { - let tys = substs.as_generator().upvar_tys().map(|t| self.codegen_ty(t)).collect(); - let output = self.codegen_ty(substs.as_generator().return_ty()); - Type::code_with_unnamed_parameters(tys, output) + /// TODO: there is some duplication with `codegen_enum` + fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type { + let pretty_name = self.ty_pretty_name(ty); + let generator_struct = + self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| { + let type_and_layout = ctx.layout_of(ty); + let variants = match &type_and_layout.variants { + Variants::Multiple { tag_encoding, variants, .. } => { + assert!(matches!(tag_encoding, TagEncoding::Direct)); + variants + } + Variants::Single { .. } => { + unreachable!("generators cannot have a single variant") + } + }; + let discr_t = ctx.codegen_enum_discr_typ(ty); + let int = ctx.codegen_ty(discr_t); + let discr_offset = ctx.layout_of(discr_t).size.bits_usize(); + let initial_offset = ctx.variant_min_offset(&variants).unwrap_or(discr_offset); + let mut fields = vec![DatatypeComponent::field("case", int)]; + if let Some(padding) = ctx.codegen_struct_padding(discr_offset, initial_offset, 0) { + fields.push(padding); + } + fields.push(DatatypeComponent::field( + "cases", + ctx.ensure_union( + &format!("{}::GeneratorUnion", name), + format!("{}::GeneratorUnion", pretty_name), + |ctx, name| { + // TODO: filter out zero-sized variants? + variants + .indices() + .map(|var_idx| { + DatatypeComponent::field( + ctx.generator_variant_field_name(var_idx), + ctx.codegen_generator_variant( + name, + pretty_name, + type_and_layout.for_variant(ctx, var_idx), + var_idx, + initial_offset, + ), + ) + }) + .collect() + }, + ), + )); + fields + }); + generator_struct + } + + pub fn generator_field_name(&self, idx: usize) -> String { + format!("generator_field_{idx}") + } + + fn codegen_generator_variant( + &mut self, + name: InternedString, + pretty_name: InternedString, + type_and_layout: TyAndLayout<'tcx, Ty<'tcx>>, + variant_idx: VariantIdx, + initial_offset: usize, + ) -> Type { + let variant_name = GeneratorSubsts::variant_name(variant_idx); + let layout = type_and_layout.layout; + let case_name = format!("{}::{variant_name}", name); + let pretty_name = format!("{}::{variant_name}", pretty_name); + debug!("handling generator variant {}", variant_idx.index()); + self.ensure_struct(&case_name, pretty_name, |cx, _| { + match &layout.fields() { + FieldsShape::Arbitrary { offsets, memory_index } => { + assert_eq!(offsets.len(), memory_index.len()); + let mut final_fields = Vec::with_capacity(offsets.len()); + let mut offset: u64 = initial_offset.try_into().unwrap(); + for field_idx in layout.fields().index_by_increasing_offset() { + let field_type_and_layout = type_and_layout.field(cx, field_idx); + let field_offset = offsets[field_idx].bits(); + let field_ty = field_type_and_layout.ty; + if let Some(padding) = + cx.codegen_struct_padding(offset, field_offset, final_fields.len()) + { + final_fields.push(padding) + } + // TODO: could create better names by doing something similar as `build_generator_variant_struct_type_di_node` in codegen-llvm + final_fields.push(DatatypeComponent::field( + cx.generator_field_name(field_idx), + cx.codegen_ty(field_ty), + )); + let layout = field_type_and_layout.layout; + // we compute the overall offset of the end of the current struct + offset = field_offset + layout.size().bits(); + } + + // If we don't meet our expected alignment, pad until we do + let align = type_and_layout.layout.align().abi.bits(); + let overhang = offset % align; + if overhang != 0 { + final_fields.push( + cx.codegen_struct_padding( + offset, + offset + align - overhang, + final_fields.len(), + ) + .unwrap(), + ) + } + + final_fields + } + // Primitives, such as NEVER, have no fields + FieldsShape::Primitive => vec![], + _ => unreachable!("{}\n{:?}", cx.current_fn().readable_name(), layout.fields()), + } + }) } /// Codegen "fat pointers" to the given `pointee_type`. These are pointers with metadata. @@ -887,6 +1041,7 @@ impl<'tcx> GotocCtx<'tcx> { | ty::Closure(..) | ty::Float(_) | ty::Foreign(_) + | ty::Generator(..) | ty::Int(_) | ty::RawPtr(_) | ty::Ref(..) @@ -902,15 +1057,6 @@ impl<'tcx> GotocCtx<'tcx> { // https://github.com/model-checking/kani/issues/214 ty::FnPtr(_) => self.codegen_ty(pointee_type).to_pointer(), - // Use the default for a reference to a generator. This is a - // temporary workaround to allow codegen to continue to a point - // where it either: - // 1. codegens unimplemented for the generator OR - // 2. errors out - // Adding full support for generators is tracked by: - // https://github.com/model-checking/kani/issues/416 - ty::Generator(_, _, _) => self.codegen_ty(pointee_type).to_pointer(), - // These types have no regression tests for them. // For soundness, hold off on generating them till we have test-cases. ty::Bound(_, _) => todo!("{:?} {:?}", pointee_type, pointee_type.kind()), @@ -953,9 +1099,6 @@ impl<'tcx> GotocCtx<'tcx> { // Codegen type with thin pointer (E.g.: Box -> Box). Some(self.codegen_trait_receiver(*arg_type)) } - } else if self.ignore_var_ty(*arg_type) { - debug!("Ignoring type {:?} in function signature", arg_type); - None } else { debug!("Using type {:?} in function signature", arg_type); Some(self.codegen_ty(*arg_type)) @@ -974,13 +1117,8 @@ impl<'tcx> GotocCtx<'tcx> { .inputs() .iter() .filter_map(|t| { - if self.ignore_var_ty(*t) { - debug!("Ignoring type {:?} in function signature", t); - None - } else { - debug!("Using type {:?} in function signature", t); - Some(self.codegen_ty(*t)) - } + debug!("Using type {:?} in function signature", t); + Some(self.codegen_ty(*t)) }) .collect(); @@ -1349,28 +1487,24 @@ impl<'tcx> GotocCtx<'tcx> { .iter() .enumerate() .filter_map(|(i, t)| { - if self.ignore_var_ty(*t) { - None - } else { - let lc = Local::from_usize(i + 1); - let mut ident = self.codegen_var_name(&lc); - - // `spread_arg` indicates that the last argument is tupled - // at the LLVM/codegen level, so we need to declare the indivual - // components as parameters with a special naming convention - // so that we can "retuple" them in the function prelude. - // See: compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude - if let Some(spread) = self.current_fn().mir().spread_arg { - if lc.index() >= spread.index() { - let (name, _) = self.codegen_spread_arg_name(&lc); - ident = name; - } + let lc = Local::from_usize(i + 1); + let mut ident = self.codegen_var_name(&lc); + + // `spread_arg` indicates that the last argument is tupled + // at the LLVM/codegen level, so we need to declare the indivual + // components as parameters with a special naming convention + // so that we can "retuple" them in the function prelude. + // See: compiler/rustc_codegen_llvm/src/gotoc/mod.rs:codegen_function_prelude + if let Some(spread) = self.current_fn().mir().spread_arg { + if lc.index() >= spread.index() { + let (name, _) = self.codegen_spread_arg_name(&lc); + ident = name; } - Some( - self.codegen_ty(*t) - .as_parameter(Some(ident.clone().into()), Some(ident.into())), - ) } + Some( + self.codegen_ty(*t) + .as_parameter(Some(ident.clone().into()), Some(ident.into())), + ) }) .collect(); @@ -1393,17 +1527,6 @@ impl<'tcx> GotocCtx<'tcx> { } } - /// Whether a variable of type ty should be ignored as a parameter to a function - pub fn ignore_var_ty(&self, ty: Ty<'tcx>) -> bool { - match ty.kind() { - // Ignore variables of the generator type until we add support for - // them: - // https://github.com/model-checking/kani/issues/416 - ty::Generator(..) => true, - _ => false, - } - } - /// Generate code for a valid object-safe trait receiver type. /// /// Note that all these types only contain the data pointer and ZST fields. Thus, we generate diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs index b0f342d8f697..3e1ad1566711 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/utils/utils.rs @@ -6,7 +6,6 @@ use crate::codegen_cprover_gotoc::codegen::PropertyClass; use crate::codegen_cprover_gotoc::GotocCtx; use cbmc::goto_program::{Expr, ExprValue, Location, Stmt, SymbolTable, Type}; use cbmc::{btree_string_map, InternedString}; -use rustc_errors::FatalError; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::{Instance, Ty}; use tracing::debug; @@ -101,11 +100,6 @@ impl<'tcx> GotocCtx<'tcx> { } s } - - pub fn emit_error_and_exit(&self, error_msg: &str) -> ! { - self.tcx.sess.err(error_msg); - FatalError.raise() - } } /// Members traverse path to get to the raw pointer of a box (b.0.pointer.pointer). From 798af9128492ea33bf397b4a4f5cc9ddf613e44b Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Thu, 14 Jul 2022 19:05:44 -0400 Subject: [PATCH 02/15] Fix tests --- tests/expected/generators/as_parameter/expected | 3 +-- tests/expected/generators/pin/expected | 15 +++++++++++++-- tests/expected/generators/pin/main.rs | 6 +++--- tests/kani/Generator/main.rs | 6 ++---- 4 files changed, 19 insertions(+), 11 deletions(-) diff --git a/tests/expected/generators/as_parameter/expected b/tests/expected/generators/as_parameter/expected index 9207afd95b24..34c886c358cb 100644 --- a/tests/expected/generators/as_parameter/expected +++ b/tests/expected/generators/as_parameter/expected @@ -1,2 +1 @@ -Status: FAILURE\ -Description: "ty::Generator is not currently supported by Kani. Please post your example at https://github.com/model-checking/kani/issues/416" +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/generators/pin/expected b/tests/expected/generators/pin/expected index b37edb7b4b92..f665f880591d 100644 --- a/tests/expected/generators/pin/expected +++ b/tests/expected/generators/pin/expected @@ -1,2 +1,13 @@ -The `generators` feature is not currently supported by Kani -exited with status exit status: 101 +SUCCESS\ +Description: "unexpected return from resume"\ +in function main + +SUCCESS\ +Description: "unexpected yield from resume"\ +in function main + +UNREACHABLE\ +Description: "generator resumed after completion" +in function main::{closure#0} + +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/generators/pin/main.rs b/tests/expected/generators/pin/main.rs index 313f323b1eae..83f8d446b935 100644 --- a/tests/expected/generators/pin/main.rs +++ b/tests/expected/generators/pin/main.rs @@ -13,7 +13,7 @@ use std::pin::Pin; fn main() { let mut generator = || { yield 1; - return "foo"; + return true; }; match Pin::new(&mut generator).resume(()) { @@ -21,7 +21,7 @@ fn main() { _ => panic!("unexpected return from resume"), } match Pin::new(&mut generator).resume(()) { - GeneratorState::Complete("foo") => {} - _ => panic!("unexpected return from resume"), + GeneratorState::Complete(true) => {} + _ => panic!("unexpected yield from resume"), } } diff --git a/tests/kani/Generator/main.rs b/tests/kani/Generator/main.rs index 38df9ebe962b..9a558318421a 100644 --- a/tests/kani/Generator/main.rs +++ b/tests/kani/Generator/main.rs @@ -2,14 +2,12 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Check that we can codegen code that has a Generator type present, -// as long as the path is not dynamically used. Full Generator support -// tracked in: https://github.com/model-checking/kani/issues/416 - +// when the path is not dynamically used. #![feature(generators, generator_trait)] use std::ops::{Generator, GeneratorState}; -// Seperate function to force translation +// Separate function to force translation fn maybe_call(call: bool) { if call { let mut _generator = || { From 9ca62638fb2239a78979bb711d634bb20a363e00 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 18 Jul 2022 18:10:53 -0400 Subject: [PATCH 03/15] Fix generator codegen (different approach than enums) --- .../codegen_cprover_gotoc/codegen/place.rs | 34 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 5 + .../codegen/statement.rs | 20 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 298 +++++++++++------- 4 files changed, 217 insertions(+), 140 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 7d6a41871961..570d6a8b8a4a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -276,9 +276,12 @@ impl<'tcx> GotocCtx<'tcx> { Ok(res.member(&field.name.to_string(), &self.symbol_table)) } ty::Closure(..) => Ok(res.member(&f.index().to_string(), &self.symbol_table)), - ty::Generator(..) => unreachable!( - "field access is only possible for generator variants, not the generator type" - ), + ty::Generator(..) => { + let field_name = self.generator_field_name(f.index().into()); + Ok(res + .member("direct_fields", &self.symbol_table) + .member(field_name, &self.symbol_table)) + } _ => unimplemented!(), } } @@ -287,7 +290,7 @@ impl<'tcx> GotocCtx<'tcx> { let field = &v.fields[f.index()]; Ok(res.member(&field.name.to_string(), &self.symbol_table)) } - TypeOrVariant::GeneratorVariant(_) => { + TypeOrVariant::GeneratorVariant(_var_idx) => { let field_name = self.generator_field_name(f.index().into()); Ok(res.member(field_name, &self.symbol_table)) } @@ -509,24 +512,27 @@ impl<'tcx> GotocCtx<'tcx> { let (case_name, type_or_variant) = match t.kind() { ty::Adt(def, _) => { let variant = def.variant(idx); - (variant.name.to_string(), TypeOrVariant::Variant(variant)) + (variant.name.as_str().into(), TypeOrVariant::Variant(variant)) + } + ty::Generator(..) => { + (self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx)) } - ty::Generator(..) => ( - self.generator_variant_field_name(idx), - TypeOrVariant::GeneratorVariant(idx), - ), _ => unreachable!("it's a bug to reach here! {:?}", &t.kind()), }; let layout = self.layout_of(t); let expr = match &layout.variants { Variants::Single { .. } => before.goto_expr, Variants::Multiple { tag_encoding, .. } => match tag_encoding { - TagEncoding::Direct => before - .goto_expr - .member("cases", &self.symbol_table) - .member(&case_name, &self.symbol_table), + TagEncoding::Direct => { + let cases = if t.is_generator() { + before.goto_expr + } else { + before.goto_expr.member("cases", &self.symbol_table) + }; + cases.member(case_name, &self.symbol_table) + } TagEncoding::Niche { .. } => { - before.goto_expr.member(&case_name, &self.symbol_table) + before.goto_expr.member(case_name, &self.symbol_table) } }, }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 56e9e6e3b409..5e9df490d92e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -510,6 +510,11 @@ impl<'tcx> GotocCtx<'tcx> { } Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { + let e = if ty.is_generator() { + e.member("direct_fields", &&self.symbol_table) + } else { + e + }; e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty)) } TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index cf8b6394b7dd..bb5205e8043d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -358,12 +358,12 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { args.iter() - .filter_map(|o| { + .map(|o| { let ot = self.operand_ty(o); if ot.is_bool() { - Some(self.codegen_operand(o).cast_to(Type::c_bool())) + self.codegen_operand(o).cast_to(Type::c_bool()) } else { - Some(self.codegen_operand(o)) + self.codegen_operand(o) } }) .collect() @@ -682,13 +682,19 @@ impl<'tcx> GotocCtx<'tcx> { // DISCRIMINANT - val:0 ty:i8 // DISCRIMINANT - val:1 ty:i8 let discr = Expr::int_constant(discr.val, self.codegen_ty(discr_t)); - unwrap_or_return_codegen_unimplemented_stmt!( + let place_goto_expr = unwrap_or_return_codegen_unimplemented_stmt!( self, self.codegen_place(place) ) - .goto_expr - .member("case", &self.symbol_table) - .assign(discr, location) + .goto_expr; + let place_goto_expr = if pt.is_generator() { + place_goto_expr.member("direct_fields", &self.symbol_table) + } else { + place_goto_expr + }; + place_goto_expr + .member("case", &self.symbol_table) + .assign(discr, location) } TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { if dataful_variant != variant_index { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 49bcd95556ba..54a9fb822729 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -19,9 +19,9 @@ use rustc_middle::ty::{ }; use rustc_middle::ty::{List, TypeFoldable}; use rustc_span::def_id::DefId; -use rustc_target::abi::TyAndLayout; use rustc_target::abi::{ - Abi::Vector, FieldsShape, Integer, Layout, Primitive, TagEncoding, VariantIdx, Variants, + Abi::Vector, FieldsShape, Integer, Layout, Primitive, Size, TagEncoding, TyAndLayout, + VariantIdx, Variants, }; use rustc_target::spec::abi::Abi; use std::collections::BTreeMap; @@ -719,16 +719,16 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_struct_padding( &self, - current_offset: T, - next_offset: T, + current_offset_in_bits: T, + next_offset_in_bits: T, idx: usize, ) -> Option where T: TryInto, T::Error: Debug, { - let current_offset: u64 = current_offset.try_into().unwrap(); - let next_offset: u64 = next_offset.try_into().unwrap(); + let current_offset: u64 = current_offset_in_bits.try_into().unwrap(); + let next_offset: u64 = next_offset_in_bits.try_into().unwrap(); assert!(current_offset <= next_offset); if current_offset < next_offset { // We need to pad to the next offset @@ -842,131 +842,186 @@ impl<'tcx> GotocCtx<'tcx> { }) } - pub fn generator_variant_field_name(&self, var_idx: VariantIdx) -> String { - format!("generator_variant_{}", GeneratorSubsts::variant_name(var_idx)) - } - - /// Preliminary support for the Generator type kind. The core functionality remains - /// unimplemented, but this way we fail at verification time only if paths that - /// rely on Generator types are used. - /// TODO: there is some duplication with `codegen_enum` + /// Translate a generator type similarly to an enum with a variant for each suspend point. + /// + /// Consider the following generator: + /// ``` + /// || { + /// let a = true; + /// let b = &a; + /// yield; + /// assert_eq!(b as *const _, &a as *const _); + /// yield; + /// }; + /// ``` + /// + /// Rustc compiles this to something similar to the following enum (but there are differences, see below!): + /// + /// ```ignore + /// enum GeneratorEnum { + /// Unresumed, // initial state of the generator + /// Returned, // generator has returned + /// Panicked, // generator has panicked + /// Suspend0 { b: &bool, a: bool }, // state after suspending (`yield`ing) for the first time + /// Suspend1, // state after suspending (`yield`ing) for the second time + /// } + /// ``` + /// + /// However, its layout may differ from normal Rust enums in the following ways: + /// * Contrary to enums, the discriminant may not be at offset 0. + /// * Contrary to enums, there may be other fields than the discriminant "at the top level" (outside the variants). + /// + /// This means that we CANNOT use the enum translation, which would be roughly as follows: + /// + /// ```ignore + /// struct GeneratorEnum { + /// int case; // discriminant + /// union GeneratorEnum-union cases; // variant + /// } + /// + /// union GeneratorEnum-union { + /// struct Unresumed variant0; + /// struct Returned variant1; + /// // ... + /// } + /// ``` + /// + /// Instead, we use the following translation: + /// + /// ```ignore + /// union GeneratorEnum { + /// struct Direct direct; + /// struct Unresumed variant0; + /// struct Returned variant1; + /// // ... + /// } + /// + /// struct Direct { + /// padding; // if necessary + /// int case; + /// padding; //if necessary + /// } + /// + /// struct Unresumed { + /// padding; // if necessary + /// int case; + /// padding; // if necessary + /// } + /// + /// // ... + /// + /// struct Suspend0 { + /// bool *b; + /// int case; + /// bool a; + /// } + /// ``` + /// + /// Of course, if the generator has any other top-level/direct fields, they'd be included in the Direct struct as well. fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type { + let generator_name = self.ty_mangled_name(ty); let pretty_name = self.ty_pretty_name(ty); - let generator_struct = - self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| { - let type_and_layout = ctx.layout_of(ty); - let variants = match &type_and_layout.variants { - Variants::Multiple { tag_encoding, variants, .. } => { - assert!(matches!(tag_encoding, TagEncoding::Direct)); - variants - } - Variants::Single { .. } => { - unreachable!("generators cannot have a single variant") - } - }; - let discr_t = ctx.codegen_enum_discr_typ(ty); - let int = ctx.codegen_ty(discr_t); - let discr_offset = ctx.layout_of(discr_t).size.bits_usize(); - let initial_offset = ctx.variant_min_offset(&variants).unwrap_or(discr_offset); - let mut fields = vec![DatatypeComponent::field("case", int)]; - if let Some(padding) = ctx.codegen_struct_padding(discr_offset, initial_offset, 0) { - fields.push(padding); + let generator_enum = self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| { + let type_and_layout = ctx.layout_of(ty); + let (discriminant_field, variants) = match &type_and_layout.variants { + Variants::Multiple { tag_encoding, tag_field, variants, .. } => { + assert!(matches!(tag_encoding, TagEncoding::Direct)); + (tag_field, variants) } - fields.push(DatatypeComponent::field( - "cases", - ctx.ensure_union( - &format!("{}::GeneratorUnion", name), - format!("{}::GeneratorUnion", pretty_name), - |ctx, name| { - // TODO: filter out zero-sized variants? - variants - .indices() - .map(|var_idx| { - DatatypeComponent::field( - ctx.generator_variant_field_name(var_idx), - ctx.codegen_generator_variant( - name, - pretty_name, - type_and_layout.for_variant(ctx, var_idx), - var_idx, - initial_offset, - ), - ) - }) - .collect() - }, - ), - )); - fields + Variants::Single { .. } => { + unreachable!("generators cannot have a single variant") + } + }; + let mut fields = vec![]; + // generate a struct for the direct fields of the layout (fields that don't occur in the variants) + fields.push(DatatypeComponent::Field { + name: "direct_fields".into(), + typ: ctx.codegen_generator_variant_struct( + generator_name, + pretty_name, + type_and_layout, + "DirectFields".into(), + Some(*discriminant_field), + ), }); - generator_struct - } - - pub fn generator_field_name(&self, idx: usize) -> String { - format!("generator_field_{idx}") + for var_idx in variants.indices() { + let variant_name = GeneratorSubsts::variant_name(var_idx).into(); + fields.push(DatatypeComponent::Field { + name: ctx.generator_variant_name(var_idx), + typ: ctx.codegen_generator_variant_struct( + generator_name, + pretty_name, + type_and_layout.for_variant(ctx, var_idx), + variant_name, + None, + ), + }); + } + fields + }); + generator_enum } - fn codegen_generator_variant( + fn codegen_generator_variant_struct( &mut self, - name: InternedString, - pretty_name: InternedString, + generator_name: InternedString, + pretty_generator_name: InternedString, type_and_layout: TyAndLayout<'tcx, Ty<'tcx>>, - variant_idx: VariantIdx, - initial_offset: usize, + variant_name: InternedString, + discriminant_field: Option, ) -> Type { - let variant_name = GeneratorSubsts::variant_name(variant_idx); - let layout = type_and_layout.layout; - let case_name = format!("{}::{variant_name}", name); - let pretty_name = format!("{}::{variant_name}", pretty_name); - debug!("handling generator variant {}", variant_idx.index()); - self.ensure_struct(&case_name, pretty_name, |cx, _| { - match &layout.fields() { - FieldsShape::Arbitrary { offsets, memory_index } => { - assert_eq!(offsets.len(), memory_index.len()); - let mut final_fields = Vec::with_capacity(offsets.len()); - let mut offset: u64 = initial_offset.try_into().unwrap(); - for field_idx in layout.fields().index_by_increasing_offset() { - let field_type_and_layout = type_and_layout.field(cx, field_idx); - let field_offset = offsets[field_idx].bits(); - let field_ty = field_type_and_layout.ty; - if let Some(padding) = - cx.codegen_struct_padding(offset, field_offset, final_fields.len()) - { - final_fields.push(padding) - } - // TODO: could create better names by doing something similar as `build_generator_variant_struct_type_di_node` in codegen-llvm - final_fields.push(DatatypeComponent::field( - cx.generator_field_name(field_idx), - cx.codegen_ty(field_ty), - )); - let layout = field_type_and_layout.layout; - // we compute the overall offset of the end of the current struct - offset = field_offset + layout.size().bits(); - } - - // If we don't meet our expected alignment, pad until we do - let align = type_and_layout.layout.align().abi.bits(); - let overhang = offset % align; - if overhang != 0 { - final_fields.push( - cx.codegen_struct_padding( - offset, - offset + align - overhang, - final_fields.len(), - ) - .unwrap(), - ) - } - - final_fields + let struct_name = format!("{generator_name}::{variant_name}"); + let pretty_struct_name = format!("{pretty_generator_name}::{variant_name}"); + debug!("codegen generator variant struct {}", pretty_struct_name); + self.ensure_struct(struct_name, pretty_struct_name, |ctx, _| { + let mut offset = Size::ZERO; + let mut fields = vec![]; + for idx in type_and_layout.fields.index_by_increasing_offset() { + let field_name = if Some(idx) == discriminant_field { + "case".into() + } else { + ctx.generator_field_name(idx).into() + }; + let field_ty = type_and_layout.field(ctx, idx).ty; + let field_offset = type_and_layout.fields.offset(idx); + let field_size = type_and_layout.field(ctx, idx).size; + if let Some(padding) = + ctx.codegen_struct_padding(offset.bits(), field_offset.bits(), idx) + { + fields.push(padding); } - // Primitives, such as NEVER, have no fields - FieldsShape::Primitive => vec![], - _ => unreachable!("{}\n{:?}", cx.current_fn().readable_name(), layout.fields()), + fields.push(DatatypeComponent::Field { + name: field_name, + typ: ctx.codegen_ty(field_ty), + }); + offset += field_size; } + // TODO: is this necessary? I don't see how padding at the end matters. But codegen_struct_fields does it too. + // If we don't meet our expected alignment, pad until we do + let align = type_and_layout.layout.align().abi.bits(); + let overhang = offset.bits() % align; + if overhang != 0 { + fields.push( + ctx.codegen_struct_padding( + offset.bits(), + offset.bits() + align - overhang, + type_and_layout.fields.count(), + ) + .unwrap(), + ) + } + fields }) } + pub fn generator_variant_name(&self, var_idx: VariantIdx) -> InternedString { + format!("generator_variant_{}", GeneratorSubsts::variant_name(var_idx)).into() + } + + pub fn generator_field_name(&self, field_idx: usize) -> InternedString { + format!("generator_field_{field_idx}").into() + } + /// Codegen "fat pointers" to the given `pointee_type`. These are pointers with metadata. /// /// There are three kinds of fat pointers: @@ -1237,8 +1292,9 @@ impl<'tcx> GotocCtx<'tcx> { self.ensure_struct(self.ty_mangled_name(ty), pretty_name, |ctx, name| { // variants appearing in source code (in source code order) let source_variants = &adtdef.variants(); + let layout = ctx.layout_of(ty); // variants appearing in mir code - match &ctx.layout_of(ty).variants { + match &layout.variants { Variants::Single { index } => { match source_variants.get(*index) { None => { @@ -1252,7 +1308,11 @@ impl<'tcx> GotocCtx<'tcx> { } } } - Variants::Multiple { tag_encoding, variants, .. } => { + Variants::Multiple { tag_encoding, variants, tag_field, .. } => { + // Contrary to generators, currently enums have only one field (the discriminant), the rest are in the variants: + assert!(layout.fields.count() <= 1); + // Contrary to generators, the discriminant is the first (and only) field for enums: + assert_eq!(*tag_field, 0); match tag_encoding { TagEncoding::Direct => { // For direct encoding of tags, we generate a type with two fields: From f8c06bb678c8559da299697d2ad2b8b4392c6106 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 18 Jul 2022 18:14:48 -0400 Subject: [PATCH 04/15] Add tests (mostly taken from rustc) --- .../expected/generators/as_parameter/main.rs | 2 +- tests/expected/generators/expected | 10 + tests/expected/generators/main.rs | 23 +++ tests/expected/generators/pin/main.rs | 2 +- tests/kani/Generator/main.rs | 1 + .../rustc-generator-tests/conditional-drop.rs | 71 +++++++ .../rustc-generator-tests/control-flow.rs | 63 ++++++ .../rustc-generator-tests/discriminant.rs | 144 ++++++++++++++ .../rustc-generator-tests/env-drop.rs | 72 +++++++ .../rustc-generator-tests/iterator-count.rs | 51 +++++ .../live-upvar-across-yield.rs | 21 ++ .../nested-generators.rs | 27 +++ .../niche-in-generator.rs | 25 +++ .../rustc-generator-tests/overlap-locals.rs | 35 ++++ .../rustc-generator-tests/resume-arg-size.rs | 34 ++++ .../resume-live-across-yield.rs | 52 +++++ .../size-moved-locals.rs | 86 ++++++++ .../smoke-resume-args.rs | 107 ++++++++++ .../Generator/rustc-generator-tests/smoke.rs | 188 ++++++++++++++++++ .../rustc-generator-tests/static-generator.rs | 27 +++ .../rustc-generator-tests/yield-in-box.rs | 32 +++ 21 files changed, 1071 insertions(+), 2 deletions(-) create mode 100644 tests/expected/generators/expected create mode 100644 tests/expected/generators/main.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/conditional-drop.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/control-flow.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/discriminant.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/env-drop.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/iterator-count.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/nested-generators.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/overlap-locals.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/smoke.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/static-generator.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/yield-in-box.rs diff --git a/tests/expected/generators/as_parameter/main.rs b/tests/expected/generators/as_parameter/main.rs index ad5644006c2a..2a3cc9c20ef9 100644 --- a/tests/expected/generators/as_parameter/main.rs +++ b/tests/expected/generators/as_parameter/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Test that includes a generator as a parameter to a function -// Codegen should succeed, but verification should fail (codegen_unimplemented) +// from https://github.com/model-checking/kani/issues/1075 #![feature(generators, generator_trait)] diff --git a/tests/expected/generators/expected b/tests/expected/generators/expected new file mode 100644 index 000000000000..b619dd8c009a --- /dev/null +++ b/tests/expected/generators/expected @@ -0,0 +1,10 @@ +SUCCESS\ +Description: "assertion failed: res == GeneratorState::Yielded(val)" + +SUCCESS\ +Description: "assertion failed: res == GeneratorState::Complete(!val)" + +UNREACHABLE\ +Description: "generator resumed after completion" + +VERIFICATION:- SUCCESSFUL \ No newline at end of file diff --git a/tests/expected/generators/main.rs b/tests/expected/generators/main.rs new file mode 100644 index 000000000000..b6dbce9363c5 --- /dev/null +++ b/tests/expected/generators/main.rs @@ -0,0 +1,23 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 OR MIT + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +#[kani::proof] +#[kani::unwind(2)] +fn main() { + let val: bool = kani::any(); + let mut generator = move || { + let x = val; + yield x; + return !x; + }; + + let res = Pin::new(&mut generator).resume(()); + assert_eq!(res, GeneratorState::Yielded(val)); + let res = Pin::new(&mut generator).resume(()); + assert_eq!(res, GeneratorState::Complete(!val)); +} diff --git a/tests/expected/generators/pin/main.rs b/tests/expected/generators/pin/main.rs index 83f8d446b935..bf7ddf4e4dc5 100644 --- a/tests/expected/generators/pin/main.rs +++ b/tests/expected/generators/pin/main.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Test contains a call to a generator via a Pin -// This is currently not supported, so Kani should error out +// from https://github.com/model-checking/kani/issues/416 #![feature(generators, generator_trait)] diff --git a/tests/kani/Generator/main.rs b/tests/kani/Generator/main.rs index 9a558318421a..3383f8ef8190 100644 --- a/tests/kani/Generator/main.rs +++ b/tests/kani/Generator/main.rs @@ -20,6 +20,7 @@ fn maybe_call(call: bool) { } #[kani::proof] +#[kani::unwind(2)] fn main() { maybe_call(false); } diff --git a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs new file mode 100644 index 000000000000..ef2a0232eb64 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs @@ -0,0 +1,71 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/conditional-drop.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +// revisions: default nomiropt +//[nomiropt]compile-flags: -Z mir-opt-level=0 + +#![feature(generators, generator_trait)] + +use std::ops::Generator; +use std::pin::Pin; +use std::sync::atomic::{AtomicUsize, Ordering}; + +static A: AtomicUsize = AtomicUsize::new(0); + +struct B; + +impl Drop for B { + fn drop(&mut self) { + A.fetch_add(1, Ordering::SeqCst); + } +} + +fn test() -> bool { + true +} +fn test2() -> bool { + false +} + +#[kani::proof] +#[kani::unwind(4)] +fn main() { + t1(); + t2(); +} + +fn t1() { + let mut a = || { + let b = B; + if test() { + drop(b); + } + yield; + }; + + let n = A.load(Ordering::SeqCst); + Pin::new(&mut a).resume(()); + assert_eq!(A.load(Ordering::SeqCst), n + 1); + Pin::new(&mut a).resume(()); + assert_eq!(A.load(Ordering::SeqCst), n + 1); +} + +fn t2() { + let mut a = || { + let b = B; + if test2() { + drop(b); + } + yield; + }; + + let n = A.load(Ordering::SeqCst); + Pin::new(&mut a).resume(()); + assert_eq!(A.load(Ordering::SeqCst), n); + Pin::new(&mut a).resume(()); + assert_eq!(A.load(Ordering::SeqCst), n + 1); +} diff --git a/tests/kani/Generator/rustc-generator-tests/control-flow.rs b/tests/kani/Generator/rustc-generator-tests/control-flow.rs new file mode 100644 index 000000000000..fa804ed730ee --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/control-flow.rs @@ -0,0 +1,63 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/control-flow.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +// revisions: default nomiropt +//[nomiropt]compile-flags: -Z mir-opt-level=0 + +#![feature(generators, generator_trait)] + +use std::marker::Unpin; +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +fn finish(mut amt: usize, mut t: T) -> T::Return +where + T: Generator<(), Yield = ()> + Unpin, +{ + loop { + match Pin::new(&mut t).resume(()) { + GeneratorState::Yielded(()) => amt = amt.checked_sub(1).unwrap(), + GeneratorState::Complete(ret) => { + assert_eq!(amt, 0); + return ret; + } + } + } +} + +#[kani::proof] +#[kani::unwind(16)] +fn main() { + finish(1, || yield); + finish(8, || { + for _ in 0..8 { + yield; + } + }); + finish(1, || { + if true { + yield; + } else { + } + }); + finish(1, || { + if false { + } else { + yield; + } + }); + finish(2, || { + if { + yield; + false + } { + yield; + panic!() + } + yield + }); +} diff --git a/tests/kani/Generator/rustc-generator-tests/discriminant.rs b/tests/kani/Generator/rustc-generator-tests/discriminant.rs new file mode 100644 index 000000000000..8d3f53c235d5 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/discriminant.rs @@ -0,0 +1,144 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/discriminant.rs +// Changes: copyright Kani contributors, Apache or MIT + +//! Tests that generator discriminant sizes and ranges are chosen optimally and that they are +//! reflected in the output of `mem::discriminant`. + +// run-pass + +#![feature(generators, generator_trait, core_intrinsics, discriminant_kind)] + +use std::intrinsics::discriminant_value; +use std::marker::{DiscriminantKind, Unpin}; +use std::mem::size_of_val; +use std::{cmp, ops::*}; + +macro_rules! yield25 { + ($e:expr) => { + yield $e; + yield $e; + yield $e; + yield $e; + yield $e; + + yield $e; + yield $e; + yield $e; + yield $e; + yield $e; + + yield $e; + yield $e; + yield $e; + yield $e; + yield $e; + + yield $e; + yield $e; + yield $e; + yield $e; + yield $e; + + yield $e; + yield $e; + yield $e; + yield $e; + yield $e; + }; +} + +/// Yields 250 times. +macro_rules! yield250 { + () => { + yield250!(()) + }; + + ($e:expr) => { + yield25!($e); + yield25!($e); + yield25!($e); + yield25!($e); + yield25!($e); + + yield25!($e); + yield25!($e); + yield25!($e); + yield25!($e); + yield25!($e); + }; +} + +fn cycle( + gen: impl Generator<()> + Unpin + DiscriminantKind, + expected_max_discr: u32, +) { + let mut gen = Box::pin(gen); + let mut max_discr = 0; + loop { + max_discr = cmp::max(max_discr, discriminant_value(gen.as_mut().get_mut())); + match gen.as_mut().resume(()) { + GeneratorState::Yielded(_) => {} + GeneratorState::Complete(_) => { + assert_eq!(max_discr, expected_max_discr); + return; + } + } + } +} + +#[kani::proof] +#[kani::unwind(260)] +fn main() { + // Has only one invalid discr. value. + let gen_u8_tiny_niche = || { + || { + // 3 reserved variants + + yield250!(); // 253 variants + + yield; // 254 + yield; // 255 + } + }; + + // Uses all values in the u8 discriminant. + let gen_u8_full = || { + || { + // 3 reserved variants + + yield250!(); // 253 variants + + yield; // 254 + yield; // 255 + yield; // 256 + } + }; + + // Barely needs a u16 discriminant. + let gen_u16 = || { + || { + // 3 reserved variants + + yield250!(); // 253 variants + + yield; // 254 + yield; // 255 + yield; // 256 + yield; // 257 + } + }; + + assert_eq!(size_of_val(&gen_u8_tiny_niche()), 1); + assert_eq!(size_of_val(&Some(gen_u8_tiny_niche())), 1); // uses niche + assert_eq!(size_of_val(&Some(Some(gen_u8_tiny_niche()))), 2); // cannot use niche anymore + assert_eq!(size_of_val(&gen_u8_full()), 1); + assert_eq!(size_of_val(&Some(gen_u8_full())), 2); // cannot use niche + assert_eq!(size_of_val(&gen_u16()), 2); + assert_eq!(size_of_val(&Some(gen_u16())), 2); // uses niche + + cycle(gen_u8_tiny_niche(), 254); + cycle(gen_u8_full(), 255); + cycle(gen_u16(), 256); +} diff --git a/tests/kani/Generator/rustc-generator-tests/env-drop.rs b/tests/kani/Generator/rustc-generator-tests/env-drop.rs new file mode 100644 index 000000000000..57f66914d8cc --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/env-drop.rs @@ -0,0 +1,72 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/env-drop.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +// revisions: default nomiropt +//[nomiropt]compile-flags: -Z mir-opt-level=0 + +#![feature(generators, generator_trait)] + +use std::ops::Generator; +use std::pin::Pin; +use std::sync::atomic::{AtomicUsize, Ordering}; + +static A: AtomicUsize = AtomicUsize::new(0); + +struct B; + +impl Drop for B { + fn drop(&mut self) { + A.fetch_add(1, Ordering::SeqCst); + } +} + +#[kani::proof] +fn main() { + t1(); + t2(); + t3(); +} + +fn t1() { + let b = B; + let mut foo = || { + yield; + drop(b); + }; + + let n = A.load(Ordering::SeqCst); + drop(Pin::new(&mut foo).resume(())); + assert_eq!(A.load(Ordering::SeqCst), n); + drop(foo); + assert_eq!(A.load(Ordering::SeqCst), n + 1); +} + +fn t2() { + let b = B; + let mut foo = || { + yield b; + }; + + let n = A.load(Ordering::SeqCst); + drop(Pin::new(&mut foo).resume(())); + assert_eq!(A.load(Ordering::SeqCst), n + 1); + drop(foo); + assert_eq!(A.load(Ordering::SeqCst), n + 1); +} + +fn t3() { + let b = B; + let foo = || { + yield; + drop(b); + }; + + let n = A.load(Ordering::SeqCst); + assert_eq!(A.load(Ordering::SeqCst), n); + drop(foo); + assert_eq!(A.load(Ordering::SeqCst), n + 1); +} diff --git a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs new file mode 100644 index 000000000000..56cc56847943 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs @@ -0,0 +1,51 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/iterator-count.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators, generator_trait)] + +use std::marker::Unpin; +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +struct W(T); + +// This impl isn't safe in general, but the generator used in this test is movable +// so it won't cause problems. +impl + Unpin> Iterator for W { + type Item = T::Yield; + + fn next(&mut self) -> Option { + match Pin::new(&mut self.0).resume(()) { + GeneratorState::Complete(..) => None, + GeneratorState::Yielded(v) => Some(v), + } + } +} + +fn test() -> impl Generator<(), Return = (), Yield = u8> + Unpin { + || { + for i in 1..6 { + yield i + } + } +} + +#[kani::proof] +#[kani::unwind(11)] +fn main() { + let end = 11; + + let closure_test = |start| { + move || { + for i in start..end { + yield i + } + } + }; + + assert!(W(test()).chain(W(closure_test(6))).eq(1..11)); +} diff --git a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs new file mode 100644 index 000000000000..dc65639d14ed --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs @@ -0,0 +1,21 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/live-upvar-across-yield.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators, generator_trait)] + +use std::ops::Generator; +use std::pin::Pin; + +#[kani::proof] +#[kani::unwind(2)] +fn main() { + let b = |_| 3; + let mut a = || { + b(yield); + }; + Pin::new(&mut a).resume(()); +} diff --git a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs new file mode 100644 index 000000000000..50fe88b5ad3e --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs @@ -0,0 +1,27 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/nested-generators.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +#[kani::proof] +fn main() { + let _generator = || { + let mut sub_generator = || { + yield 2; + }; + + match Pin::new(&mut sub_generator).resume(()) { + GeneratorState::Yielded(x) => { + yield x; + } + _ => panic!(), + }; + }; +} diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs new file mode 100644 index 000000000000..03ac8198f906 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs @@ -0,0 +1,25 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/niche-in-generator.rs +// Changes: copyright Kani contributors, Apache or MIT + +// Test that niche finding works with captured generator upvars. + +// run-pass + +#![feature(generators)] + +use std::mem::size_of_val; + +fn take(_: T) {} + +#[kani::proof] +fn main() { + let x = false; + let gen1 = || { + yield; + take(x); + }; + + assert_eq!(size_of_val(&gen1), size_of_val(&Some(gen1))); +} diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs new file mode 100644 index 000000000000..e974cf527d4f --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs @@ -0,0 +1,35 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/overlap-locals.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators)] + +#[kani::proof] +fn main() { + let a = || { + { + let w: i32 = 4; + yield; + println!("{:?}", w); + } + { + let x: i32 = 5; + yield; + println!("{:?}", x); + } + { + let y: i32 = 6; + yield; + println!("{:?}", y); + } + { + let z: i32 = 7; + yield; + println!("{:?}", z); + } + }; + assert_eq!(8, std::mem::size_of_val(&a)); +} diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs new file mode 100644 index 000000000000..309709466788 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs @@ -0,0 +1,34 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/resume-arg-size.rs +// Changes: copyright Kani contributors, Apache or MIT + +#![feature(generators)] + +// run-pass + +use std::mem::size_of_val; + +#[kani::proof] +fn main() { + // Generator taking a `Copy`able resume arg. + let gen_copy = |mut x: usize| { + loop { + drop(x); + x = yield; + } + }; + + // Generator taking a non-`Copy` resume arg. + let gen_move = |mut x: Box| { + loop { + drop(x); + x = yield; + } + }; + + // Neither of these generators have the resume arg live across the `yield`, so they should be + // 1 Byte in size (only storing the discriminant) + assert_eq!(size_of_val(&gen_copy), 1); + assert_eq!(size_of_val(&gen_move), 1); +} diff --git a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs new file mode 100644 index 000000000000..4d91678f28be --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs @@ -0,0 +1,52 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/resume-live-across-yield.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; +use std::sync::atomic::{AtomicUsize, Ordering}; + +static DROP: AtomicUsize = AtomicUsize::new(0); + +#[derive(PartialEq, Eq, Debug)] +struct Dropper(String); + +impl Drop for Dropper { + fn drop(&mut self) { + DROP.fetch_add(1, Ordering::SeqCst); + } +} + +#[kani::proof] +#[kani::unwind(16)] +fn main() { + let mut g = |mut _d| { + _d = yield; + _d + }; + + let mut g = Pin::new(&mut g); + + assert_eq!( + g.as_mut().resume(Dropper(String::from("Hello world!"))), + GeneratorState::Yielded(()) + ); + assert_eq!(DROP.load(Ordering::Acquire), 0); + match g.as_mut().resume(Dropper(String::from("Number Two"))) { + GeneratorState::Complete(dropper) => { + assert_eq!(DROP.load(Ordering::Acquire), 1); + assert_eq!(dropper.0, "Number Two"); + drop(dropper); + assert_eq!(DROP.load(Ordering::Acquire), 2); + } + _ => unreachable!(), + } + + drop(g); + assert_eq!(DROP.load(Ordering::Acquire), 2); +} diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs new file mode 100644 index 000000000000..47c28598b30e --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs @@ -0,0 +1,86 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/size-moved-locals.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass +// Test that we don't duplicate storage for a variable that is moved to another +// binding. This used to happen in the presence of unwind and drop edges (see +// `complex` below.) +// +// The exact sizes here can change (we'd like to know when they do). What we +// don't want to see is the `complex` generator size being upwards of 2048 bytes +// (which would indicate it is reserving space for two copies of Foo.) +// +// See issue #59123 for a full explanation. + +// edition:2018 +// ignore-wasm32 issue #62807 +// ignore-asmjs issue #62807 + +#![feature(generators, generator_trait)] + +use std::ops::Generator; + +const FOO_SIZE: usize = 1024; +struct Foo([u8; FOO_SIZE]); + +impl Drop for Foo { + fn drop(&mut self) {} +} + +fn move_before_yield() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + let _second = first; + yield; + // _second dropped here + } +} + +fn noop() {} + +fn move_before_yield_with_noop() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + noop(); + let _second = first; + yield; + // _second dropped here + } +} + +// Today we don't have NRVO (we allocate space for both `first` and `second`,) +// but we can overlap `first` with `_third`. +fn overlap_move_points() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + yield; + let second = first; + yield; + let _third = second; + yield; + } +} + +fn overlap_x_and_y() -> impl Generator { + static || { + let x = Foo([0; FOO_SIZE]); + yield; + drop(x); + let y = Foo([0; FOO_SIZE]); + yield; + drop(y); + } +} + +#[kani::proof] +fn main() { + assert_eq!(1025, std::mem::size_of_val(&move_before_yield())); + // The following assertion fails for some reason. + // But it also fails for WASM (https://github.com/rust-lang/rust/issues/62807), + // so it is probably not a big problem: + // assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop())); + assert_eq!(2051, std::mem::size_of_val(&overlap_move_points())); + assert_eq!(1026, std::mem::size_of_val(&overlap_x_and_y())); +} diff --git a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs new file mode 100644 index 000000000000..dc355ab4381c --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs @@ -0,0 +1,107 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/smoke-resume-args.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +// revisions: default nomiropt +//[nomiropt]compile-flags: -Z mir-opt-level=0 + +#![feature(generators, generator_trait)] + +use std::fmt::Debug; +use std::marker::Unpin; +use std::ops::{ + Generator, + GeneratorState::{self, *}, +}; +use std::pin::Pin; +use std::sync::atomic::{AtomicUsize, Ordering}; + +fn drain + Unpin, R, Y>( + gen: &mut G, + inout: Vec<(R, GeneratorState)>, +) where + Y: Debug + PartialEq, + G::Return: Debug + PartialEq, +{ + let mut gen = Pin::new(gen); + + for (input, out) in inout { + assert_eq!(gen.as_mut().resume(input), out); + } +} + +static DROPS: AtomicUsize = AtomicUsize::new(0); + +#[derive(Debug, PartialEq)] +struct DropMe; + +impl Drop for DropMe { + fn drop(&mut self) { + DROPS.fetch_add(1, Ordering::SeqCst); + } +} + +fn expect_drops(expected_drops: usize, f: impl FnOnce() -> T) -> T { + DROPS.store(0, Ordering::SeqCst); + + let res = f(); + + let actual_drops = DROPS.load(Ordering::SeqCst); + assert_eq!(actual_drops, expected_drops); + res +} + +#[kani::proof] +#[kani::unwind(8)] +fn main() { + drain( + &mut |mut b| { + while b != 0 { + b = yield (b + 1); + } + -1 + }, + vec![(1, Yielded(2)), (-45, Yielded(-44)), (500, Yielded(501)), (0, Complete(-1))], + ); + + expect_drops(2, || drain(&mut |a| yield a, vec![(DropMe, Yielded(DropMe))])); + + expect_drops(6, || { + drain( + &mut |a| yield yield a, + vec![(DropMe, Yielded(DropMe)), (DropMe, Yielded(DropMe)), (DropMe, Complete(DropMe))], + ) + }); + + #[allow(unreachable_code)] + expect_drops(2, || drain(&mut |a| yield return a, vec![(DropMe, Complete(DropMe))])); + + expect_drops(2, || { + drain( + &mut |a: DropMe| { + if false { yield () } else { a } + }, + vec![(DropMe, Complete(DropMe))], + ) + }); + + expect_drops(4, || { + drain( + #[allow(unused_assignments, unused_variables)] + &mut |mut a: DropMe| { + a = yield; + a = yield; + a = yield; + }, + vec![ + (DropMe, Yielded(())), + (DropMe, Yielded(())), + (DropMe, Yielded(())), + (DropMe, Complete(())), + ], + ) + }); +} diff --git a/tests/kani/Generator/rustc-generator-tests/smoke.rs b/tests/kani/Generator/rustc-generator-tests/smoke.rs new file mode 100644 index 000000000000..894aa68999be --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/smoke.rs @@ -0,0 +1,188 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/smoke.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +// revisions: default nomiropt +//[nomiropt]compile-flags: -Z mir-opt-level=0 + +// ignore-emscripten no threads support +// compile-flags: --test + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; +use std::thread; + +#[kani::proof] +fn simple() { + let mut foo = || { + if false { + yield; + } + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(()) => {} + s => panic!("bad state: {:?}", s), + } +} + +#[kani::proof] +#[kani::unwind(4)] +fn return_capture() { + let a = String::from("foo"); + let mut foo = || { + if false { + yield; + } + a + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(ref s) if *s == "foo" => {} + s => panic!("bad state: {:?}", s), + } +} + +#[kani::proof] +fn simple_yield() { + let mut foo = || { + yield; + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(()) => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(()) => {} + s => panic!("bad state: {:?}", s), + } +} + +#[kani::proof] +#[kani::unwind(4)] +fn yield_capture() { + let b = String::from("foo"); + let mut foo = || { + yield b; + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(ref s) if *s == "foo" => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(()) => {} + s => panic!("bad state: {:?}", s), + } +} + +#[kani::proof] +#[kani::unwind(4)] +fn simple_yield_value() { + let mut foo = || { + yield String::from("bar"); + return String::from("foo"); + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(ref s) if *s == "bar" => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(ref s) if *s == "foo" => {} + s => panic!("bad state: {:?}", s), + } +} + +#[kani::proof] +#[kani::unwind(4)] +fn return_after_yield() { + let a = String::from("foo"); + let mut foo = || { + yield; + return a; + }; + + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(()) => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(ref s) if *s == "foo" => {} + s => panic!("bad state: {:?}", s), + } +} + +// This test is useless for Kani +fn send_and_sync() { + assert_send_sync(|| yield); + assert_send_sync(|| { + yield String::from("foo"); + }); + assert_send_sync(|| { + yield; + return String::from("foo"); + }); + let a = 3; + assert_send_sync(|| { + yield a; + return; + }); + let a = 3; + assert_send_sync(move || { + yield a; + return; + }); + let a = String::from("a"); + assert_send_sync(|| { + yield; + drop(a); + return; + }); + let a = String::from("a"); + assert_send_sync(move || { + yield; + drop(a); + return; + }); + + fn assert_send_sync(_: T) {} +} + +// Kani does not support threads, so we cannot run this test: +fn send_over_threads() { + let mut foo = || yield; + thread::spawn(move || { + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(()) => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(()) => {} + s => panic!("bad state: {:?}", s), + } + }) + .join() + .unwrap(); + + let a = String::from("a"); + let mut foo = || yield a; + thread::spawn(move || { + match Pin::new(&mut foo).resume(()) { + GeneratorState::Yielded(ref s) if *s == "a" => {} + s => panic!("bad state: {:?}", s), + } + match Pin::new(&mut foo).resume(()) { + GeneratorState::Complete(()) => {} + s => panic!("bad state: {:?}", s), + } + }) + .join() + .unwrap(); +} diff --git a/tests/kani/Generator/rustc-generator-tests/static-generator.rs b/tests/kani/Generator/rustc-generator-tests/static-generator.rs new file mode 100644 index 000000000000..25893bfaf739 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/static-generator.rs @@ -0,0 +1,27 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/static-generator.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +#[kani::proof] +#[kani::unwind(2)] +fn main() { + let mut generator = static || { + let a = true; + let b = &a; + yield; + assert_eq!(b as *const _, &a as *const _); + }; + // SAFETY: We shadow the original generator variable so have no safe API to + // move it after this point. + let mut generator = unsafe { Pin::new_unchecked(&mut generator) }; + assert_eq!(generator.as_mut().resume(()), GeneratorState::Yielded(())); + assert_eq!(generator.as_mut().resume(()), GeneratorState::Complete(())); +} diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs new file mode 100644 index 000000000000..b87a562426d4 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs @@ -0,0 +1,32 @@ +// Copyright rustc Contributors +// SPDX-License-Identifier: Apache OR MIT +// Adapted from rustc: src/test/ui/generator/yield-in-box.rs +// Changes: copyright Kani contributors, Apache or MIT + +// run-pass +// Test that box-statements with yields in them work. + +#![feature(generators, box_syntax, generator_trait)] +use std::ops::Generator; +use std::ops::GeneratorState; +use std::pin::Pin; + +#[kani::proof] +#[kani::unwind(2)] +fn main() { + let x = 0i32; + || { + //~ WARN unused generator that must be used + let y = 2u32; + { + let _t = box (&x, yield 0, &y); + } + match box (&x, yield 0, &y) { + _t => {} + } + }; + + let mut g = |_| box yield; + assert_eq!(Pin::new(&mut g).resume(1), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut g).resume(2), GeneratorState::Complete(box 2)); +} From 229cf4dc23970cabe6f11a7d2aa55b153b773ca0 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 18 Jul 2022 18:21:47 -0400 Subject: [PATCH 05/15] Fix copyright headers --- .../Generator/rustc-generator-tests/conditional-drop.rs | 7 +++++-- tests/kani/Generator/rustc-generator-tests/control-flow.rs | 7 +++++-- tests/kani/Generator/rustc-generator-tests/discriminant.rs | 7 +++++-- tests/kani/Generator/rustc-generator-tests/env-drop.rs | 7 +++++-- .../kani/Generator/rustc-generator-tests/iterator-count.rs | 7 +++++-- .../rustc-generator-tests/live-upvar-across-yield.rs | 7 +++++-- .../Generator/rustc-generator-tests/nested-generators.rs | 7 +++++-- .../Generator/rustc-generator-tests/niche-in-generator.rs | 7 +++++-- .../kani/Generator/rustc-generator-tests/overlap-locals.rs | 7 +++++-- .../Generator/rustc-generator-tests/resume-arg-size.rs | 7 +++++-- .../rustc-generator-tests/resume-live-across-yield.rs | 7 +++++-- .../Generator/rustc-generator-tests/size-moved-locals.rs | 7 +++++-- .../Generator/rustc-generator-tests/smoke-resume-args.rs | 7 +++++-- tests/kani/Generator/rustc-generator-tests/smoke.rs | 7 +++++-- .../Generator/rustc-generator-tests/static-generator.rs | 7 +++++-- tests/kani/Generator/rustc-generator-tests/yield-in-box.rs | 7 +++++-- 16 files changed, 80 insertions(+), 32 deletions(-) diff --git a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs index ef2a0232eb64..e80e84cf7ba0 100644 --- a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs +++ b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/conditional-drop.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/control-flow.rs b/tests/kani/Generator/rustc-generator-tests/control-flow.rs index fa804ed730ee..b0496bb3d5ae 100644 --- a/tests/kani/Generator/rustc-generator-tests/control-flow.rs +++ b/tests/kani/Generator/rustc-generator-tests/control-flow.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/control-flow.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/discriminant.rs b/tests/kani/Generator/rustc-generator-tests/discriminant.rs index 8d3f53c235d5..7a00ea9bebc6 100644 --- a/tests/kani/Generator/rustc-generator-tests/discriminant.rs +++ b/tests/kani/Generator/rustc-generator-tests/discriminant.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/discriminant.rs -// Changes: copyright Kani contributors, Apache or MIT //! Tests that generator discriminant sizes and ranges are chosen optimally and that they are //! reflected in the output of `mem::discriminant`. diff --git a/tests/kani/Generator/rustc-generator-tests/env-drop.rs b/tests/kani/Generator/rustc-generator-tests/env-drop.rs index 57f66914d8cc..1779ee0f765c 100644 --- a/tests/kani/Generator/rustc-generator-tests/env-drop.rs +++ b/tests/kani/Generator/rustc-generator-tests/env-drop.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/env-drop.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs index 56cc56847943..f391322c72f5 100644 --- a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs +++ b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/iterator-count.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs index dc65639d14ed..27c0e7a9fee9 100644 --- a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs +++ b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/live-upvar-across-yield.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs index 50fe88b5ad3e..159309309f29 100644 --- a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs +++ b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/nested-generators.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs index 03ac8198f906..a9311f18f5d0 100644 --- a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs +++ b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/niche-in-generator.rs -// Changes: copyright Kani contributors, Apache or MIT // Test that niche finding works with captured generator upvars. diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs index e974cf527d4f..01df445f7276 100644 --- a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/overlap-locals.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs index 309709466788..5ad687e1e6fe 100644 --- a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs +++ b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/resume-arg-size.rs -// Changes: copyright Kani contributors, Apache or MIT #![feature(generators)] diff --git a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs index 4d91678f28be..470a98dbe36d 100644 --- a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs +++ b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/resume-live-across-yield.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs index 47c28598b30e..a4989546a40b 100644 --- a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/size-moved-locals.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass // Test that we don't duplicate storage for a variable that is moved to another diff --git a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs index dc355ab4381c..ee8a6e13ec2f 100644 --- a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs +++ b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/smoke-resume-args.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/smoke.rs b/tests/kani/Generator/rustc-generator-tests/smoke.rs index 894aa68999be..378addcfba59 100644 --- a/tests/kani/Generator/rustc-generator-tests/smoke.rs +++ b/tests/kani/Generator/rustc-generator-tests/smoke.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/smoke.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/static-generator.rs b/tests/kani/Generator/rustc-generator-tests/static-generator.rs index 25893bfaf739..2098f71e9ae9 100644 --- a/tests/kani/Generator/rustc-generator-tests/static-generator.rs +++ b/tests/kani/Generator/rustc-generator-tests/static-generator.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/static-generator.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs index b87a562426d4..39fab9d76d9a 100644 --- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs +++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs @@ -1,7 +1,10 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + // Copyright rustc Contributors -// SPDX-License-Identifier: Apache OR MIT // Adapted from rustc: src/test/ui/generator/yield-in-box.rs -// Changes: copyright Kani contributors, Apache or MIT // run-pass // Test that box-statements with yields in them work. From 1443b5ccf96a54b8c43dcf020894ffdc47148071 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 18 Jul 2022 19:10:22 -0400 Subject: [PATCH 06/15] Small code simplification --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 54a9fb822729..b6b3d67812e8 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1168,14 +1168,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_function_sig(&mut self, sig: PolyFnSig<'tcx>) -> Type { let sig = self.monomorphize(sig); let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); - let params = sig - .inputs() - .iter() - .filter_map(|t| { - debug!("Using type {:?} in function signature", t); - Some(self.codegen_ty(*t)) - }) - .collect(); + let params = sig.inputs().iter().map(|t| self.codegen_ty(*t)).collect(); if sig.c_variadic { Type::variadic_code_with_unnamed_parameters(params, self.codegen_ty(sig.output())) @@ -1546,7 +1539,7 @@ impl<'tcx> GotocCtx<'tcx> { .inputs() .iter() .enumerate() - .filter_map(|(i, t)| { + .map(|(i, t)| { let lc = Local::from_usize(i + 1); let mut ident = self.codegen_var_name(&lc); @@ -1561,10 +1554,7 @@ impl<'tcx> GotocCtx<'tcx> { ident = name; } } - Some( - self.codegen_ty(*t) - .as_parameter(Some(ident.clone().into()), Some(ident.into())), - ) + self.codegen_ty(*t).as_parameter(Some(ident.clone().into()), Some(ident.into())) }) .collect(); From 1cabf67c0fba9dd1ea9044f1ce83e7830f6eb1e6 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Tue, 19 Jul 2022 10:48:36 -0400 Subject: [PATCH 07/15] Refactor: remove unnecessary Option --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 2 +- .../codegen_cprover_gotoc/codegen/statement.rs | 2 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 15 +++++++-------- .../codegen_cprover_gotoc/context/current_fn.rs | 4 ++-- 4 files changed, 11 insertions(+), 12 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index cd0ba6353be3..5c7e42a24f83 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -634,7 +634,7 @@ impl<'tcx> GotocCtx<'tcx> { /// This is tracked in . pub fn codegen_func_symbol(&mut self, instance: Instance<'tcx>) -> (&Symbol, Type) { let func = self.symbol_name(instance); - let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap()); + let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance)); // make sure the functions imported from other modules are in the symbol table let sym = self.ensure(&func, |ctx, _| { Symbol::function( diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index d2f34eac7b5a..f3a17f874861 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -60,7 +60,7 @@ impl<'tcx> GotocCtx<'tcx> { loc, ), TerminatorKind::Return => { - let rty = self.current_fn().sig().unwrap().skip_binder().output(); + let rty = self.current_fn().sig().skip_binder().output(); if rty.is_unit() { self.codegen_ret_unit() } else { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index b6b3d67812e8..cb4db5c6b5b3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -241,21 +241,21 @@ impl<'tcx> GotocCtx<'tcx> { ) } - pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> Option> { + pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> ty::PolyFnSig<'tcx> { let fntyp = instance.ty(self.tcx, ty::ParamEnv::reveal_all()); self.monomorphize(match fntyp.kind() { - ty::Closure(def_id, subst) => Some(self.closure_sig(*def_id, subst)), + ty::Closure(def_id, subst) => self.closure_sig(*def_id, subst), ty::FnPtr(..) | ty::FnDef(..) => { let sig = fntyp.fn_sig(self.tcx); // Some virtual calls through a vtable may actually be closures // or shims that also need the arguments untupled, even though // the kind of the trait type is not a ty::Closure. if self.ty_needs_closure_untupled(fntyp) { - return Some(self.sig_with_closure_untupled(sig)); + return self.sig_with_closure_untupled(sig); } - Some(sig) + sig } - ty::Generator(_def_id, substs, _movability) => Some(self.generator_sig(fntyp, substs)), + ty::Generator(_def_id, substs, _movability) => self.generator_sig(fntyp, substs), _ => unreachable!("Can't get function signature of type: {:?}", fntyp), }) } @@ -337,7 +337,7 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> DatatypeComponent { // Gives a binder with function signature - let sig = self.fn_sig_of_instance(instance).unwrap(); + let sig = self.fn_sig_of_instance(instance); // Gives an Irep Pointer object for the signature let fn_ty = self.codegen_dynamic_function_sig(sig); @@ -1532,8 +1532,7 @@ impl<'tcx> GotocCtx<'tcx> { /// the function type of the current instance pub fn fn_typ(&mut self) -> Type { let sig = self.current_fn().sig(); - let sig = - self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap()); + let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); // we don't call [codegen_function_sig] because we want to get a bit more metainformation. let mut params: Vec = sig .inputs() diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs index 09e04df2bedf..1c503cadd3b3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/context/current_fn.rs @@ -28,7 +28,7 @@ pub struct CurrentFnCtx<'tcx> { /// A human readable pretty name for the current function readable_name: String, /// The signature of the current function - sig: Option>, + sig: PolyFnSig<'tcx>, /// A counter to enable creating temporary variables temp_var_counter: u64, } @@ -105,7 +105,7 @@ impl<'tcx> CurrentFnCtx<'tcx> { } /// The signature of the function we are currently compiling - pub fn sig(&self) -> Option> { + pub fn sig(&self) -> PolyFnSig<'tcx> { self.sig } } From 3005cca01e5e99cc4f0ab177ed5e6b65a4e65558 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Tue, 19 Jul 2022 11:22:41 -0400 Subject: [PATCH 08/15] Update comments --- .../src/codegen_cprover_gotoc/codegen/typ.rs | 53 +++++++++---------- 1 file changed, 25 insertions(+), 28 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index cb4db5c6b5b3..50acee4b0de3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -777,7 +777,7 @@ impl<'tcx> GotocCtx<'tcx> { offset = fld_offset + layout.size.bits(); } - // If we don't meet our expected alignment, pad until we do + // Add padding to ensure that the size of the struct is a multiple of the alignment let align = layout.align().abi.bits(); let overhang = offset % align; if overhang != 0 { @@ -859,11 +859,11 @@ impl<'tcx> GotocCtx<'tcx> { /// /// ```ignore /// enum GeneratorEnum { - /// Unresumed, // initial state of the generator - /// Returned, // generator has returned - /// Panicked, // generator has panicked - /// Suspend0 { b: &bool, a: bool }, // state after suspending (`yield`ing) for the first time - /// Suspend1, // state after suspending (`yield`ing) for the second time + /// Unresumed, // initial state of the generator + /// Returned, // generator has returned + /// Panicked, // generator has panicked + /// Suspend0 { b: &bool, a: bool }, // state after suspending (`yield`ing) for the first time + /// Suspend1, // state after suspending (`yield`ing) for the second time /// } /// ``` /// @@ -875,14 +875,14 @@ impl<'tcx> GotocCtx<'tcx> { /// /// ```ignore /// struct GeneratorEnum { - /// int case; // discriminant - /// union GeneratorEnum-union cases; // variant + /// int case; // discriminant + /// union GeneratorEnum-union cases; // variant /// } /// /// union GeneratorEnum-union { - /// struct Unresumed variant0; - /// struct Returned variant1; - /// // ... + /// struct Unresumed variant0; + /// struct Returned variant1; + /// // ... /// } /// ``` /// @@ -890,34 +890,32 @@ impl<'tcx> GotocCtx<'tcx> { /// /// ```ignore /// union GeneratorEnum { - /// struct Direct direct; - /// struct Unresumed variant0; - /// struct Returned variant1; - /// // ... + /// struct DirectFields direct_fields; + /// struct Unresumed generator_variant_Unresumed; + /// struct Returned generator_variant_Returned; + /// // ... /// } /// - /// struct Direct { - /// padding; // if necessary - /// int case; - /// padding; //if necessary + /// struct DirectFields { + /// // padding (for bool *b in Suspend0 below) + /// char case; + /// // padding (for bool a in Suspend0 below) /// } /// /// struct Unresumed { - /// padding; // if necessary - /// int case; - /// padding; // if necessary + /// // padding (this variant has no fields) /// } /// /// // ... /// /// struct Suspend0 { - /// bool *b; - /// int case; - /// bool a; + /// bool *generator_field_0; // variable b in the generator code above + /// // padding (for char case in DirectFields) + /// bool generator_field_1; // variable a in the generator code above /// } /// ``` /// - /// Of course, if the generator has any other top-level/direct fields, they'd be included in the Direct struct as well. + /// Of course, if the generator has any other top-level/direct fields, they'd be included in the `DirectFields` struct as well. fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type { let generator_name = self.ty_mangled_name(ty); let pretty_name = self.ty_pretty_name(ty); @@ -996,8 +994,7 @@ impl<'tcx> GotocCtx<'tcx> { }); offset += field_size; } - // TODO: is this necessary? I don't see how padding at the end matters. But codegen_struct_fields does it too. - // If we don't meet our expected alignment, pad until we do + // Add padding to ensure that the size of the struct is a multiple of the alignment let align = type_and_layout.layout.align().abi.bits(); let overhang = offset.bits() % align; if overhang != 0 { From e269f4ffe3e45ebbdd02901ed239540c4db5578d Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Tue, 19 Jul 2022 16:23:00 -0400 Subject: [PATCH 09/15] Fix merge issue --- kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs index 592ce652ced4..abd99a0bb454 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs @@ -44,8 +44,7 @@ impl<'tcx> GotocCtx<'tcx> { /// Get the number of parameters that the current function expects. fn get_params_size(&self) -> usize { let sig = self.current_fn().sig(); - let sig = - self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap()); + let sig = self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig); // we don't call [codegen_function_sig] because we want to get a bit more metainformation. sig.inputs().len() } From 1826b5b8fbe70e7fa2d71849e10fb7946d859040 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 20 Jul 2022 12:45:37 -0400 Subject: [PATCH 10/15] Address reviewer comments --- .../codegen_cprover_gotoc/codegen/place.rs | 6 ++++- .../codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- .../codegen/statement.rs | 3 +-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 23 +++++++++++-------- .../expected/generators/as_parameter/main.rs | 4 ++-- .../rustc-generator-tests/conditional-drop.rs | 2 +- .../rustc-generator-tests/control-flow.rs | 2 +- .../rustc-generator-tests/discriminant.rs | 5 +++- .../rustc-generator-tests/env-drop.rs | 2 +- .../rustc-generator-tests/iterator-count.rs | 2 +- .../live-upvar-across-yield.rs | 2 +- .../nested-generators.rs | 2 +- .../niche-in-generator.rs | 2 +- .../rustc-generator-tests/overlap-locals.rs | 2 +- .../rustc-generator-tests/resume-arg-size.rs | 2 +- .../resume-live-across-yield.rs | 2 +- .../size-moved-locals.rs | 4 ++-- .../smoke-resume-args.rs | 2 +- .../Generator/rustc-generator-tests/smoke.rs | 2 +- .../rustc-generator-tests/static-generator.rs | 2 +- .../rustc-generator-tests/yield-in-box.rs | 2 +- 21 files changed, 43 insertions(+), 32 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 570d6a8b8a4a..efed76d8480e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -521,7 +521,10 @@ impl<'tcx> GotocCtx<'tcx> { }; let layout = self.layout_of(t); let expr = match &layout.variants { - Variants::Single { .. } => before.goto_expr, + Variants::Single { .. } => { + assert!(!t.is_generator()); + before.goto_expr + } Variants::Multiple { tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { let cases = if t.is_generator() { @@ -532,6 +535,7 @@ impl<'tcx> GotocCtx<'tcx> { cases.member(case_name, &self.symbol_table) } TagEncoding::Niche { .. } => { + assert!(!t.is_generator()); before.goto_expr.member(case_name, &self.symbol_table) } }, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 5c9bda0d3c6a..4cf6e4b6005a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -511,7 +511,7 @@ impl<'tcx> GotocCtx<'tcx> { Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { let e = if ty.is_generator() { - e.member("direct_fields", &&self.symbol_table) + e.member("direct_fields", &self.symbol_table) } else { e }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index f3a17f874861..da045917532c 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -359,8 +359,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_funcall_args(&mut self, args: &[Operand<'tcx>]) -> Vec { args.iter() .map(|o| { - let ot = self.operand_ty(o); - if ot.is_bool() { + if self.operand_ty(o).is_bool() { self.codegen_operand(o).cast_to(Type::c_bool()) } else { self.codegen_operand(o) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 50acee4b0de3..6dd3afeafb88 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -255,7 +255,7 @@ impl<'tcx> GotocCtx<'tcx> { } sig } - ty::Generator(_def_id, substs, _movability) => self.generator_sig(fntyp, substs), + ty::Generator(_, substs, _) => self.generator_sig(fntyp, substs), _ => unreachable!("Can't get function signature of type: {:?}", fntyp), }) } @@ -855,7 +855,8 @@ impl<'tcx> GotocCtx<'tcx> { /// }; /// ``` /// - /// Rustc compiles this to something similar to the following enum (but there are differences, see below!): + /// Rustc compiles this to something similar to the following enum (but there are differences, see below!), + /// as described at the top of https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/generator.rs: /// /// ```ignore /// enum GeneratorEnum { @@ -919,7 +920,8 @@ impl<'tcx> GotocCtx<'tcx> { fn codegen_ty_generator(&mut self, ty: Ty<'tcx>) -> Type { let generator_name = self.ty_mangled_name(ty); let pretty_name = self.ty_pretty_name(ty); - let generator_enum = self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| { + debug!(?pretty_name, "codeged_ty_generator"); + self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| { let type_and_layout = ctx.layout_of(ty); let (discriminant_field, variants) = match &type_and_layout.variants { Variants::Multiple { tag_encoding, tag_field, variants, .. } => { @@ -930,9 +932,8 @@ impl<'tcx> GotocCtx<'tcx> { unreachable!("generators cannot have a single variant") } }; - let mut fields = vec![]; // generate a struct for the direct fields of the layout (fields that don't occur in the variants) - fields.push(DatatypeComponent::Field { + let direct_fields = DatatypeComponent::Field { name: "direct_fields".into(), typ: ctx.codegen_generator_variant_struct( generator_name, @@ -941,7 +942,8 @@ impl<'tcx> GotocCtx<'tcx> { "DirectFields".into(), Some(*discriminant_field), ), - }); + }; + let mut fields = vec![direct_fields]; for var_idx in variants.indices() { let variant_name = GeneratorSubsts::variant_name(var_idx).into(); fields.push(DatatypeComponent::Field { @@ -956,10 +958,12 @@ impl<'tcx> GotocCtx<'tcx> { }); } fields - }); - generator_enum + }) } + /// Generates a struct for a variant of the generator. + /// + /// The parameter `discriminant_field` may contain the index of a field that is the discriminant. fn codegen_generator_variant_struct( &mut self, generator_name: InternedString, @@ -970,11 +974,12 @@ impl<'tcx> GotocCtx<'tcx> { ) -> Type { let struct_name = format!("{generator_name}::{variant_name}"); let pretty_struct_name = format!("{pretty_generator_name}::{variant_name}"); - debug!("codegen generator variant struct {}", pretty_struct_name); + debug!(?pretty_struct_name, "codeged_generator_variant_struct"); self.ensure_struct(struct_name, pretty_struct_name, |ctx, _| { let mut offset = Size::ZERO; let mut fields = vec![]; for idx in type_and_layout.fields.index_by_increasing_offset() { + // The discriminant field needs to have a special name to work with the rest of the code: let field_name = if Some(idx) == discriminant_field { "case".into() } else { diff --git a/tests/expected/generators/as_parameter/main.rs b/tests/expected/generators/as_parameter/main.rs index 2a3cc9c20ef9..b97032a5c8a4 100644 --- a/tests/expected/generators/as_parameter/main.rs +++ b/tests/expected/generators/as_parameter/main.rs @@ -1,8 +1,8 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Test that includes a generator as a parameter to a function -// from https://github.com/model-checking/kani/issues/1075 +// Test that a generator can be passed as a parameter. +// (from https://github.com/model-checking/kani/issues/1075) #![feature(generators, generator_trait)] diff --git a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs index e80e84cf7ba0..7e22f7940349 100644 --- a/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs +++ b/tests/kani/Generator/rustc-generator-tests/conditional-drop.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/conditional-drop.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/conditional-drop.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/control-flow.rs b/tests/kani/Generator/rustc-generator-tests/control-flow.rs index b0496bb3d5ae..a47a01ca4859 100644 --- a/tests/kani/Generator/rustc-generator-tests/control-flow.rs +++ b/tests/kani/Generator/rustc-generator-tests/control-flow.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/control-flow.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/control-flow.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/discriminant.rs b/tests/kani/Generator/rustc-generator-tests/discriminant.rs index 7a00ea9bebc6..fe2af9534ca9 100644 --- a/tests/kani/Generator/rustc-generator-tests/discriminant.rs +++ b/tests/kani/Generator/rustc-generator-tests/discriminant.rs @@ -4,7 +4,10 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/discriminant.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/discriminant.rs + +// This test creates some large generators with around 256 variants, some of them need a u16 discriminant instead of u8. +// This test ensures that we use the right discriminant type. //! Tests that generator discriminant sizes and ranges are chosen optimally and that they are //! reflected in the output of `mem::discriminant`. diff --git a/tests/kani/Generator/rustc-generator-tests/env-drop.rs b/tests/kani/Generator/rustc-generator-tests/env-drop.rs index 1779ee0f765c..b3f7f82af5c9 100644 --- a/tests/kani/Generator/rustc-generator-tests/env-drop.rs +++ b/tests/kani/Generator/rustc-generator-tests/env-drop.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/env-drop.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/env-drop.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs index f391322c72f5..79984a0763fa 100644 --- a/tests/kani/Generator/rustc-generator-tests/iterator-count.rs +++ b/tests/kani/Generator/rustc-generator-tests/iterator-count.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/iterator-count.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/iterator-count.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs index 27c0e7a9fee9..803e285852ce 100644 --- a/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs +++ b/tests/kani/Generator/rustc-generator-tests/live-upvar-across-yield.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/live-upvar-across-yield.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/live-upvar-across-yield.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs index 159309309f29..443877aab062 100644 --- a/tests/kani/Generator/rustc-generator-tests/nested-generators.rs +++ b/tests/kani/Generator/rustc-generator-tests/nested-generators.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/nested-generators.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/nested-generators.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs index a9311f18f5d0..dfa60b534287 100644 --- a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs +++ b/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/niche-in-generator.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs // Test that niche finding works with captured generator upvars. diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs index 01df445f7276..4d9002c4260d 100644 --- a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/overlap-locals.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs index 5ad687e1e6fe..9cc42e5d04bd 100644 --- a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs +++ b/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/resume-arg-size.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs #![feature(generators)] diff --git a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs index 470a98dbe36d..922140cbbe25 100644 --- a/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs +++ b/tests/kani/Generator/rustc-generator-tests/resume-live-across-yield.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/resume-live-across-yield.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-live-across-yield.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs index a4989546a40b..fefb1ce513b1 100644 --- a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/size-moved-locals.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs // run-pass // Test that we don't duplicate storage for a variable that is moved to another @@ -80,7 +80,7 @@ fn overlap_x_and_y() -> impl Generator { #[kani::proof] fn main() { assert_eq!(1025, std::mem::size_of_val(&move_before_yield())); - // The following assertion fails for some reason. + // The following assertion fails for some reason (tracking issue: https://github.com/model-checking/kani/issues/1395). // But it also fails for WASM (https://github.com/rust-lang/rust/issues/62807), // so it is probably not a big problem: // assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop())); diff --git a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs index ee8a6e13ec2f..0251ac142e89 100644 --- a/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs +++ b/tests/kani/Generator/rustc-generator-tests/smoke-resume-args.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/smoke-resume-args.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke-resume-args.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/smoke.rs b/tests/kani/Generator/rustc-generator-tests/smoke.rs index 378addcfba59..276ebd9dca31 100644 --- a/tests/kani/Generator/rustc-generator-tests/smoke.rs +++ b/tests/kani/Generator/rustc-generator-tests/smoke.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/smoke.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/smoke.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/static-generator.rs b/tests/kani/Generator/rustc-generator-tests/static-generator.rs index 2098f71e9ae9..014684430686 100644 --- a/tests/kani/Generator/rustc-generator-tests/static-generator.rs +++ b/tests/kani/Generator/rustc-generator-tests/static-generator.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/static-generator.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/static-generator.rs // run-pass diff --git a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs index 39fab9d76d9a..039cb05ae899 100644 --- a/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs +++ b/tests/kani/Generator/rustc-generator-tests/yield-in-box.rs @@ -4,7 +4,7 @@ // See GitHub history for details. // Copyright rustc Contributors -// Adapted from rustc: src/test/ui/generator/yield-in-box.rs +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/yield-in-box.rs // run-pass // Test that box-statements with yields in them work. From db2263c386965b1f943623af66164dbdcbf3a710 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 20 Jul 2022 13:45:52 -0400 Subject: [PATCH 11/15] Fix comment test --- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index 6dd3afeafb88..c84da0298eca 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -856,7 +856,7 @@ impl<'tcx> GotocCtx<'tcx> { /// ``` /// /// Rustc compiles this to something similar to the following enum (but there are differences, see below!), - /// as described at the top of https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_transform/src/generator.rs: + /// as described at the top of : /// /// ```ignore /// enum GeneratorEnum { From 72d5d108bebeee1616d04fee85493e68768ab5b1 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 20 Jul 2022 16:19:40 -0400 Subject: [PATCH 12/15] Improve tests --- .../expected/generators/as_parameter/main.rs | 14 +++++---- tests/kani/Generator/main.rs | 29 +++++++++---------- 2 files changed, 22 insertions(+), 21 deletions(-) diff --git a/tests/expected/generators/as_parameter/main.rs b/tests/expected/generators/as_parameter/main.rs index b97032a5c8a4..513204e230ec 100644 --- a/tests/expected/generators/as_parameter/main.rs +++ b/tests/expected/generators/as_parameter/main.rs @@ -2,17 +2,21 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // Test that a generator can be passed as a parameter. -// (from https://github.com/model-checking/kani/issues/1075) +// (adapted from https://github.com/model-checking/kani/issues/1075) #![feature(generators, generator_trait)] -use std::ops::Generator; +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; -fn foo(g: T) +fn foo + Unpin>(mut g: G) where - T: Generator, + ::Return: std::cmp::PartialEq, { - let _ = g; + let res = Pin::new(&mut g).resume(()); + assert_eq!(res, GeneratorState::Yielded(1)); + let res2 = Pin::new(&mut g).resume(()); + assert_eq!(res2, GeneratorState::Complete(2)); } #[kani::proof] diff --git a/tests/kani/Generator/main.rs b/tests/kani/Generator/main.rs index 3383f8ef8190..c9f6e9f51db9 100644 --- a/tests/kani/Generator/main.rs +++ b/tests/kani/Generator/main.rs @@ -1,26 +1,23 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that we can codegen code that has a Generator type present, -// when the path is not dynamically used. +// This tests that generators work, even with a non-() resume type. + #![feature(generators, generator_trait)] use std::ops::{Generator, GeneratorState}; - -// Separate function to force translation -fn maybe_call(call: bool) { - if call { - let mut _generator = || { - yield 1; - return 2; - }; - } else { - assert!(1 + 1 == 2); - } -} +use std::pin::Pin; #[kani::proof] -#[kani::unwind(2)] fn main() { - maybe_call(false); + let mut add_one = |mut resume: u8| { + loop { + resume = yield resume.saturating_add(1); + } + }; + for _ in 0..2 { + let val = kani::any(); + let res = Pin::new(&mut add_one).resume(val); + assert_eq!(res, GeneratorState::Yielded(val.saturating_add(1))); + } } From 64f7af1abd18443d9c1dbde8bf75a637936d8a8e Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Wed, 20 Jul 2022 19:22:00 -0400 Subject: [PATCH 13/15] Address reviewer comments --- .../codegen_cprover_gotoc/codegen/operand.rs | 3 +- .../codegen_cprover_gotoc/codegen/place.rs | 11 ++- .../codegen_cprover_gotoc/codegen/rvalue.rs | 27 +++++-- .../codegen/statement.rs | 9 +-- .../src/codegen_cprover_gotoc/codegen/typ.rs | 72 +++++++++++-------- 5 files changed, 71 insertions(+), 51 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index 8583a590feaa..869a83b2f2ed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -324,8 +324,7 @@ impl<'tcx> GotocCtx<'tcx> { let var = tcx.gen_function_local_variable(2, &func_name, cgt.clone()).to_expr(); let body = vec![ Stmt::decl(var.clone(), None, Location::none()), - var.clone() - .member("case", &tcx.symbol_table) + tcx.codegen_discriminant_field(var.clone(), ty) .assign(param.to_expr(), Location::none()), var.ret(Location::none()), ]; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index efed76d8480e..dc45858cf3b9 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -517,14 +517,14 @@ impl<'tcx> GotocCtx<'tcx> { ty::Generator(..) => { (self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx)) } - _ => unreachable!("it's a bug to reach here! {:?}", &t.kind()), + _ => unreachable!( + "cannot downcast {:?} to a varian (only enums and generators can)", + &t.kind() + ), }; let layout = self.layout_of(t); let expr = match &layout.variants { - Variants::Single { .. } => { - assert!(!t.is_generator()); - before.goto_expr - } + Variants::Single { .. } => before.goto_expr, Variants::Multiple { tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { let cases = if t.is_generator() { @@ -535,7 +535,6 @@ impl<'tcx> GotocCtx<'tcx> { cases.member(case_name, &self.symbol_table) } TagEncoding::Niche { .. } => { - assert!(!t.is_generator()); before.goto_expr.member(case_name, &self.symbol_table) } }, diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 4cf6e4b6005a..a24b932976c5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -496,10 +496,30 @@ impl<'tcx> GotocCtx<'tcx> { } } + pub fn codegen_discriminant_field(&self, place: Expr, ty: Ty<'tcx>) -> Expr { + let layout = self.layout_of(ty); + assert!( + matches!( + &layout.variants, + Variants::Multiple { tag_encoding: TagEncoding::Direct, .. } + ), + "discriminant field (`case`) only exists for multiple variants and direct encoding" + ); + let expr = if ty.is_generator() { + // Generators are translated somewhat differently from enums (see [`GotoCtx::codegen_ty_generator`]). + // As a consequence, the discriminant is accessed as `.direct_fields.case` instead of just `.case`. + place.member("direct_fields", &self.symbol_table) + } else { + place + }; + expr.member("case", &self.symbol_table) + } + /// e: ty /// get the discriminant of e, of type res_ty pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty<'tcx>, res_ty: Ty<'tcx>) -> Expr { let layout = self.layout_of(ty); + self.check_generator_layout_assumptions(ty); match &layout.variants { Variants::Single { index } => { let discr_val = layout @@ -510,12 +530,7 @@ impl<'tcx> GotocCtx<'tcx> { } Variants::Multiple { tag, tag_encoding, .. } => match tag_encoding { TagEncoding::Direct => { - let e = if ty.is_generator() { - e.member("direct_fields", &self.symbol_table) - } else { - e - }; - e.member("case", &self.symbol_table).cast_to(self.codegen_ty(res_ty)) + self.codegen_discriminant_field(e, ty).cast_to(self.codegen_ty(res_ty)) } TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { // This code follows the logic in the cranelift codegen backend: diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index da045917532c..58438bea2435 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -660,6 +660,7 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::SetDiscriminant { place, variant_index } => { // this requires place points to an enum type. let pt = self.place_ty(place); + self.check_generator_layout_assumptions(pt); let layout = self.layout_of(pt); match &layout.variants { Variants::Single { .. } => Stmt::skip(location), @@ -686,13 +687,7 @@ impl<'tcx> GotocCtx<'tcx> { self.codegen_place(place) ) .goto_expr; - let place_goto_expr = if pt.is_generator() { - place_goto_expr.member("direct_fields", &self.symbol_table) - } else { - place_goto_expr - }; - place_goto_expr - .member("case", &self.symbol_table) + self.codegen_discriminant_field(place_goto_expr, pt) .assign(discr, location) } TagEncoding::Niche { dataful_variant, niche_variants, niche_start } => { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index c84da0298eca..0e1febba747e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -740,6 +740,22 @@ impl<'tcx> GotocCtx<'tcx> { } } + /// Adds padding to ensure that the size of the struct is a multiple of the alignment + fn codegen_alignment_padding( + &self, + size: Size, + layout: &Layout, + idx: usize, + ) -> Option { + let align = layout.align().abi.bits(); + let overhang = size.bits() % align; + if overhang != 0 { + self.codegen_struct_padding(size.bits(), size.bits() + align - overhang, idx) + } else { + None + } + } + /// generate a struct based on the layout /// the fields and types are determined by flds while their order is determined by layout. /// @@ -776,21 +792,11 @@ impl<'tcx> GotocCtx<'tcx> { // we compute the overall offset of the end of the current struct offset = fld_offset + layout.size.bits(); } - - // Add padding to ensure that the size of the struct is a multiple of the alignment - let align = layout.align().abi.bits(); - let overhang = offset % align; - if overhang != 0 { - final_fields.push( - self.codegen_struct_padding( - offset, - offset + align - overhang, - final_fields.len(), - ) - .unwrap(), - ) - } - + final_fields.extend(self.codegen_alignment_padding( + Size::from_bits(offset), + &layout, + final_fields.len(), + )); final_fields } // Primitives, such as NEVER, have no fields @@ -922,6 +928,7 @@ impl<'tcx> GotocCtx<'tcx> { let pretty_name = self.ty_pretty_name(ty); debug!(?pretty_name, "codeged_ty_generator"); self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| { + ctx.check_generator_layout_assumptions(ty); let type_and_layout = ctx.layout_of(ty); let (discriminant_field, variants) = match &type_and_layout.variants { Variants::Multiple { tag_encoding, tag_field, variants, .. } => { @@ -961,9 +968,21 @@ impl<'tcx> GotocCtx<'tcx> { }) } + pub fn check_generator_layout_assumptions(&self, ty: Ty<'tcx>) { + if ty.is_generator() { + // generators have more than one variant and use direct encoding + assert!(matches!( + &self.layout_of(ty).variants, + Variants::Multiple { tag_encoding: TagEncoding::Direct, .. } + )) + } + } + /// Generates a struct for a variant of the generator. /// - /// The parameter `discriminant_field` may contain the index of a field that is the discriminant. + /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the generator. + /// Then the field with the index `idx` will be treated as the discriminant and will be given a special name to work with the rest of the code. + /// The field `discriminant_field` should be `None` when generating an actual variant of the generator because those don't contain the discriminant as a field. fn codegen_generator_variant_struct( &mut self, generator_name: InternedString, @@ -979,7 +998,8 @@ impl<'tcx> GotocCtx<'tcx> { let mut offset = Size::ZERO; let mut fields = vec![]; for idx in type_and_layout.fields.index_by_increasing_offset() { - // The discriminant field needs to have a special name to work with the rest of the code: + // The discriminant field needs to have a special name to work with the rest of the code. + // If discriminant_field is None, this variant does not have the discriminant as a field. let field_name = if Some(idx) == discriminant_field { "case".into() } else { @@ -999,19 +1019,11 @@ impl<'tcx> GotocCtx<'tcx> { }); offset += field_size; } - // Add padding to ensure that the size of the struct is a multiple of the alignment - let align = type_and_layout.layout.align().abi.bits(); - let overhang = offset.bits() % align; - if overhang != 0 { - fields.push( - ctx.codegen_struct_padding( - offset.bits(), - offset.bits() + align - overhang, - type_and_layout.fields.count(), - ) - .unwrap(), - ) - } + fields.extend(ctx.codegen_alignment_padding( + offset, + &type_and_layout.layout, + fields.len(), + )); fields }) } From 88eaf1f51ab466e21529c1b39b539d12aebbf7b7 Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 25 Jul 2022 11:40:27 -0400 Subject: [PATCH 14/15] Check generator layout assumption only in one place --- .../codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 1 - .../codegen/statement.rs | 1 - .../src/codegen_cprover_gotoc/codegen/typ.rs | 25 ++++++------------- 4 files changed, 8 insertions(+), 21 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index dc45858cf3b9..4548e06520a6 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -518,7 +518,7 @@ impl<'tcx> GotocCtx<'tcx> { (self.generator_variant_name(idx), TypeOrVariant::GeneratorVariant(idx)) } _ => unreachable!( - "cannot downcast {:?} to a varian (only enums and generators can)", + "cannot downcast {:?} to a variant (only enums and generators can)", &t.kind() ), }; diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index a24b932976c5..8e7d1db1c64a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -519,7 +519,6 @@ impl<'tcx> GotocCtx<'tcx> { /// get the discriminant of e, of type res_ty pub fn codegen_get_discriminant(&mut self, e: Expr, ty: Ty<'tcx>, res_ty: Ty<'tcx>) -> Expr { let layout = self.layout_of(ty); - self.check_generator_layout_assumptions(ty); match &layout.variants { Variants::Single { index } => { let discr_val = layout diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 58438bea2435..8db1b24507e3 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -660,7 +660,6 @@ impl<'tcx> GotocCtx<'tcx> { StatementKind::SetDiscriminant { place, variant_index } => { // this requires place points to an enum type. let pt = self.place_ty(place); - self.check_generator_layout_assumptions(pt); let layout = self.layout_of(pt); match &layout.variants { Variants::Single { .. } => 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 0e1febba747e..4d6794c88756 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -928,16 +928,15 @@ impl<'tcx> GotocCtx<'tcx> { let pretty_name = self.ty_pretty_name(ty); debug!(?pretty_name, "codeged_ty_generator"); self.ensure_union(self.ty_mangled_name(ty), pretty_name, |ctx, _| { - ctx.check_generator_layout_assumptions(ty); let type_and_layout = ctx.layout_of(ty); let (discriminant_field, variants) = match &type_and_layout.variants { - Variants::Multiple { tag_encoding, tag_field, variants, .. } => { - assert!(matches!(tag_encoding, TagEncoding::Direct)); - (tag_field, variants) - } - Variants::Single { .. } => { - unreachable!("generators cannot have a single variant") - } + Variants::Multiple { + tag_encoding: TagEncoding::Direct, + tag_field, + variants, + .. + } => (tag_field, variants), + _ => unreachable!("Generators have more than one variant and use direct encoding"), }; // generate a struct for the direct fields of the layout (fields that don't occur in the variants) let direct_fields = DatatypeComponent::Field { @@ -968,16 +967,6 @@ impl<'tcx> GotocCtx<'tcx> { }) } - pub fn check_generator_layout_assumptions(&self, ty: Ty<'tcx>) { - if ty.is_generator() { - // generators have more than one variant and use direct encoding - assert!(matches!( - &self.layout_of(ty).variants, - Variants::Multiple { tag_encoding: TagEncoding::Direct, .. } - )) - } - } - /// Generates a struct for a variant of the generator. /// /// The field `discriminant_field` should be `Some(idx)` when generating the variant for the direct (top-[evel) fields of the generator. From 5864e9f59033e5d0e9c59c3428b384e4308c562d Mon Sep 17 00:00:00 2001 From: Fabian Zaiser Date: Mon, 25 Jul 2022 15:06:28 -0400 Subject: [PATCH 15/15] Make size_of or align_of fail for generators (because they are currently buggy, see #1395) --- .../codegen/intrinsic.rs | 16 ++- ...{discriminant.rs => discriminant_fixme.rs} | 1 + .../niche-in-generator-slow_fixme.rs | 35 +++++ ...nerator.rs => niche-in-generator_fixme.rs} | 1 + .../rustc-generator-tests/overlap-locals.rs | 18 ++- .../overlap-locals_fixme.rs | 40 ++++++ ...e-arg-size.rs => resume-arg-size_fixme.rs} | 1 + .../rustc-generator-tests/resume-arg.rs | 41 ++++++ .../size-moved-locals-slow_fixme.rs | 136 ++++++++++++++++++ ...d-locals.rs => size-moved-locals_fixme.rs} | 3 +- 10 files changed, 281 insertions(+), 11 deletions(-) rename tests/kani/Generator/rustc-generator-tests/{discriminant.rs => discriminant_fixme.rs} (97%) create mode 100644 tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs rename tests/kani/Generator/rustc-generator-tests/{niche-in-generator.rs => niche-in-generator_fixme.rs} (85%) create mode 100644 tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs rename tests/kani/Generator/rustc-generator-tests/{resume-arg-size.rs => resume-arg-size_fixme.rs} (89%) create mode 100644 tests/kani/Generator/rustc-generator-tests/resume-arg.rs create mode 100644 tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs rename tests/kani/Generator/rustc-generator-tests/{size-moved-locals.rs => size-moved-locals_fixme.rs} (93%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index f12a88c9ed3e..4bc976a6ca76 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -313,9 +313,19 @@ impl<'tcx> GotocCtx<'tcx> { macro_rules! codegen_size_align { ($which: ident) => {{ let tp_ty = instance.substs.type_at(0); - let arg = fargs.remove(0); - let size_align = self.size_and_align_of_dst(tp_ty, arg); - self.codegen_expr_to_place(p, size_align.$which) + if tp_ty.is_generator() { + let e = self.codegen_unimplemented( + "size or alignment of a generator type", + cbmc_ret_ty, + loc, + "https://github.com/model-checking/kani/issues/1395", + ); + self.codegen_expr_to_place(p, e) + } else { + let arg = fargs.remove(0); + let size_align = self.size_and_align_of_dst(tp_ty, arg); + self.codegen_expr_to_place(p, size_align.$which) + } }}; } diff --git a/tests/kani/Generator/rustc-generator-tests/discriminant.rs b/tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs similarity index 97% rename from tests/kani/Generator/rustc-generator-tests/discriminant.rs rename to tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs index fe2af9534ca9..08a12b9139d6 100644 --- a/tests/kani/Generator/rustc-generator-tests/discriminant.rs +++ b/tests/kani/Generator/rustc-generator-tests/discriminant_fixme.rs @@ -136,6 +136,7 @@ fn main() { } }; + // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395) assert_eq!(size_of_val(&gen_u8_tiny_niche()), 1); assert_eq!(size_of_val(&Some(gen_u8_tiny_niche())), 1); // uses niche assert_eq!(size_of_val(&Some(Some(gen_u8_tiny_niche()))), 2); // cannot use niche anymore diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs new file mode 100644 index 000000000000..986ab86884b3 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/niche-in-generator-slow_fixme.rs @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// Copyright rustc Contributors +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/niche-in-generator.rs + +// Test that niche finding works with captured generator upvars. + +// run-pass + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +use std::mem::size_of_val; + +fn take(_: T) {} + +#[kani::proof] +fn main() { + let x = false; + let mut gen1 = || { + yield; + take(x); + }; + + // FIXME: for some reason, these asserts are very hard for CBMC to figure out + // Kani didn't terminate within 5 minutes. + // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Yielded(())); + // assert_eq!(Pin::new(&mut gen1).resume(()), GeneratorState::Complete(())); + assert!(false); // to make the test fail without taking forever +} diff --git a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs b/tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs similarity index 85% rename from tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs rename to tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs index dfa60b534287..6113e89fb75d 100644 --- a/tests/kani/Generator/rustc-generator-tests/niche-in-generator.rs +++ b/tests/kani/Generator/rustc-generator-tests/niche-in-generator_fixme.rs @@ -24,5 +24,6 @@ fn main() { take(x); }; + // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395) assert_eq!(size_of_val(&gen1), size_of_val(&Some(gen1))); } diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs index 4d9002c4260d..d3f5e1d8f882 100644 --- a/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/overlap-locals.rs @@ -8,31 +8,35 @@ // run-pass -#![feature(generators)] +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; #[kani::proof] fn main() { - let a = || { + let mut a = || { { let w: i32 = 4; yield; - println!("{:?}", w); } { let x: i32 = 5; yield; - println!("{:?}", x); } { let y: i32 = 6; yield; - println!("{:?}", y); } { let z: i32 = 7; yield; - println!("{:?}", z); } }; - assert_eq!(8, std::mem::size_of_val(&a)); + + assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut a).resume(()), GeneratorState::Complete(())); } diff --git a/tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs b/tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs new file mode 100644 index 000000000000..fb17beb6e679 --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/overlap-locals_fixme.rs @@ -0,0 +1,40 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// Copyright rustc Contributors +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/overlap-locals.rs + +// run-pass + +#![feature(generators)] + +#[kani::proof] +fn main() { + let a = || { + { + let w: i32 = 4; + yield; + println!("{:?}", w); + } + { + let x: i32 = 5; + yield; + println!("{:?}", x); + } + { + let y: i32 = 6; + yield; + println!("{:?}", y); + } + { + let z: i32 = 7; + yield; + println!("{:?}", z); + } + }; + + // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395) + assert_eq!(8, std::mem::size_of_val(&a)); +} diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs similarity index 89% rename from tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs rename to tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs index 9cc42e5d04bd..841fcd77ab32 100644 --- a/tests/kani/Generator/rustc-generator-tests/resume-arg-size.rs +++ b/tests/kani/Generator/rustc-generator-tests/resume-arg-size_fixme.rs @@ -32,6 +32,7 @@ fn main() { // Neither of these generators have the resume arg live across the `yield`, so they should be // 1 Byte in size (only storing the discriminant) + // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395) assert_eq!(size_of_val(&gen_copy), 1); assert_eq!(size_of_val(&gen_move), 1); } diff --git a/tests/kani/Generator/rustc-generator-tests/resume-arg.rs b/tests/kani/Generator/rustc-generator-tests/resume-arg.rs new file mode 100644 index 000000000000..dec73823797a --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/resume-arg.rs @@ -0,0 +1,41 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// Copyright rustc Contributors +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/resume-arg-size.rs + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +// run-pass + +use std::mem::size_of_val; + +#[kani::proof] +fn main() { + // Generator taking a `Copy`able resume arg. + let mut gen_copy = |mut x: usize| { + loop { + drop(x); + x = yield; + } + }; + + // Generator taking a non-`Copy` resume arg. + let mut gen_move = |mut x: Box| { + loop { + drop(x); + x = yield; + } + }; + + assert_eq!(Pin::new(&mut gen_copy).resume(0), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut gen_copy).resume(1), GeneratorState::Yielded(())); + + assert_eq!(Pin::new(&mut gen_move).resume(Box::new(0)), GeneratorState::Yielded(())); + assert_eq!(Pin::new(&mut gen_move).resume(Box::new(1)), GeneratorState::Yielded(())); +} diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs b/tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs new file mode 100644 index 000000000000..6d7a61441d0a --- /dev/null +++ b/tests/kani/Generator/rustc-generator-tests/size-moved-locals-slow_fixme.rs @@ -0,0 +1,136 @@ +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// Modifications Copyright Kani Contributors +// See GitHub history for details. + +// Copyright rustc Contributors +// Adapted from rustc: https://github.com/rust-lang/rust/tree/5f98537eb7b5f42c246a52c550813c3cff336069/src/test/ui/generator/size-moved-locals.rs + +// run-pass +// Test that we don't duplicate storage for a variable that is moved to another +// binding. This used to happen in the presence of unwind and drop edges (see +// `complex` below.) +// +// The exact sizes here can change (we'd like to know when they do). What we +// don't want to see is the `complex` generator size being upwards of 2048 bytes +// (which would indicate it is reserving space for two copies of Foo.) +// +// See issue #59123 for a full explanation. + +// edition:2018 +// ignore-wasm32 issue #62807 +// ignore-asmjs issue #62807 + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; +use std::pin::Pin; + +const FOO_SIZE: usize = 1024; +struct Foo([u8; FOO_SIZE]); + +impl Drop for Foo { + fn drop(&mut self) {} +} + +fn move_before_yield() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + let _second = first; + yield; + // _second dropped here + } +} + +fn noop() {} + +fn move_before_yield_with_noop() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + noop(); + let _second = first; + yield; + // _second dropped here + } +} + +// Today we don't have NRVO (we allocate space for both `first` and `second`,) +// but we can overlap `first` with `_third`. +fn overlap_move_points() -> impl Generator { + static || { + let first = Foo([0; FOO_SIZE]); + yield; + let second = first; + yield; + let _third = second; + yield; + } +} + +fn overlap_x_and_y() -> impl Generator { + static || { + let x = Foo([0; FOO_SIZE]); + yield; + drop(x); + let y = Foo([0; FOO_SIZE]); + yield; + drop(y); + } +} + +#[kani::proof] +fn main() { + // FIXME: the following tests are very slow (did not terminate in a couple of minutes) + /* let mut generator = move_before_yield(); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Complete(()) + ); + + let mut generator = move_before_yield_with_noop(); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Complete(()) + ); + + let mut generator = overlap_move_points(); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Complete(()) + ); + + let mut generator = overlap_x_and_y(); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Yielded(()) + ); + assert_eq!( + unsafe { Pin::new_unchecked(&mut generator) }.resume(()), + GeneratorState::Complete(()) + ); */ + assert!(false); // to make the test fail without taking forever +} diff --git a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs b/tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs similarity index 93% rename from tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs rename to tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs index fefb1ce513b1..f5d63a393404 100644 --- a/tests/kani/Generator/rustc-generator-tests/size-moved-locals.rs +++ b/tests/kani/Generator/rustc-generator-tests/size-moved-locals_fixme.rs @@ -79,11 +79,12 @@ fn overlap_x_and_y() -> impl Generator { #[kani::proof] fn main() { + // FIXME: size of generators does not work reliably (https://github.com/model-checking/kani/issues/1395) assert_eq!(1025, std::mem::size_of_val(&move_before_yield())); // The following assertion fails for some reason (tracking issue: https://github.com/model-checking/kani/issues/1395). // But it also fails for WASM (https://github.com/rust-lang/rust/issues/62807), // so it is probably not a big problem: - // assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop())); + assert_eq!(1026, std::mem::size_of_val(&move_before_yield_with_noop())); assert_eq!(2051, std::mem::size_of_val(&overlap_move_points())); assert_eq!(1026, std::mem::size_of_val(&overlap_x_and_y())); }