From 980517ef256740f7893c05feed14c9b2d29f4006 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 14 Sep 2021 18:24:28 +0000 Subject: [PATCH 1/2] Partial support for Generator --- .../src/gotoc/cbmc/goto_program/expr.rs | 19 ++++++---- .../src/gotoc/cbmc/goto_program/symbol.rs | 2 +- .../src/gotoc/mir_to_goto/codegen/function.rs | 6 +++- .../gotoc/mir_to_goto/codegen/intrinsic.rs | 14 +++----- .../src/gotoc/mir_to_goto/codegen/operand.rs | 2 +- .../src/gotoc/mir_to_goto/codegen/place.rs | 10 +++++- .../gotoc/mir_to_goto/codegen/statement.rs | 20 +++++++++-- .../src/gotoc/mir_to_goto/codegen/typ.rs | 33 +++++++++-------- .../gotoc/mir_to_goto/context/current_fn.rs | 4 +-- .../src/gotoc/mir_to_goto/overrides/hooks.rs | 36 +++++++++++++++---- .../src/gotoc/mir_to_goto/utils/names.rs | 10 +----- 11 files changed, 99 insertions(+), 57 deletions(-) diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs index a9e91ec98d65..9feb01e91b4e 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs @@ -351,7 +351,7 @@ macro_rules! expr { impl Expr { /// `&self` pub fn address_of(self) -> Self { - assert!(self.can_take_address_of()); + assert!(self.can_take_address_of(), "Can't take address of {:?}", self); expr!(AddressOf(self), self.typ.clone().to_pointer()) } @@ -566,9 +566,11 @@ impl Expr { self, field, ); - - let typ = symbol_table.lookup_field_type_in_type(self.typ(), field).unwrap().clone(); - expr!(Member { lhs: self, field: field.to_string() }, typ) + if let Some(ty) = symbol_table.lookup_field_type_in_type(self.typ(), field) { + expr!(Member { lhs: self, field: field.to_string() }, ty.clone()) + } else { + unreachable!("unable to find field {:?} for type {:?}", field, self.typ()) + } } /// `__nondet_typ()` @@ -603,8 +605,9 @@ impl Expr { // Check that each formal field has an value assert!( fields.iter().zip(values.iter()).all(|(f, v)| f.typ() == *v.typ()), - "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}", + "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}", typ, + fields, values ); expr!(Struct { values }, typ) @@ -709,8 +712,9 @@ impl Expr { .iter() .zip(non_padding_values.iter()) .all(|(f, v)| f.field_typ().unwrap() == v.typ()), - "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}", + "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}", typ, + non_padding_fields, non_padding_values ); @@ -748,8 +752,9 @@ impl Expr { ); assert!( fields.iter().zip(values.iter()).all(|(f, v)| &f.typ() == v.typ()), - "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}", + "Error in struct_expr; value type does not match field type.\n\t{:?}\n\t{:?}\n\t{:?}", typ, + fields, values ); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs index 4864f7a41787..75fa4b230357 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/symbol.rs @@ -209,7 +209,7 @@ impl Symbol { /// Setters impl Symbol { pub fn update_fn_declaration_with_definition(&mut self, body: Stmt) { - assert!(self.is_function_declaration()); + assert!(self.is_function_declaration(), "Expected function declaration, got {:?}", self); self.value = SymbolValues::Stmt(body); } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/function.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/function.rs index 0d938580509b..693aff61276c 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/function.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/function.rs @@ -25,6 +25,10 @@ impl<'tcx> GotocCtx<'tcx> { name if name.starts_with("bridge::client") => true, // https://github.com/model-checking/rmc/issues/282 "bridge::closure::Closure::<'a, A, R>::call" => true, + // Generators + name if name.starts_with("") => true, + name if name.contains("reusable_box::ReusableBoxFuture") => true, + "tokio::sync::Semaphore::acquire_owned::{closure#0}" => true, _ => false, } } @@ -64,7 +68,6 @@ impl<'tcx> GotocCtx<'tcx> { self.set_current_fn(instance); let name = self.current_fn().name(); let old_sym = self.symbol_table.lookup(&name).unwrap(); - assert!(old_sym.is_function()); if old_sym.is_function_definition() { warn!("Double codegen of {:?}", old_sym); } else if self.should_skip_current_fn() { @@ -79,6 +82,7 @@ impl<'tcx> GotocCtx<'tcx> { ); self.symbol_table.update_fn_declaration_with_definition(&name, body); } else { + assert!(old_sym.is_function()); let mir = self.current_fn().mir(); self.print_instance(instance, mir); let labels = self diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs index bbdeabb717fc..76e2a8dec05b 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/intrinsic.rs @@ -60,7 +60,9 @@ impl<'tcx> GotocCtx<'tcx> { let dst = fargs.remove(0).cast_to(Type::void_pointer()); let count = fargs.remove(0); let sz = { - match self.fn_sig_of_instance(instance).skip_binder().inputs()[0].kind() { + match self.fn_sig_of_instance(instance).unwrap().skip_binder().inputs()[0] + .kind() + { ty::RawPtr(t) => { let layout = self.layout_of(t.ty); Expr::int_constant(layout.size.bytes(), Type::size_t()) @@ -259,17 +261,9 @@ impl<'tcx> GotocCtx<'tcx> { "atomic_and_acqrel" => codegen_atomic_binop!(bitand), "atomic_and_rel" => codegen_atomic_binop!(bitand), "atomic_and_relaxed" => codegen_atomic_binop!(bitand), - "atomic_cxchg" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_acq" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_acq_failrelaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_acqrel" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_acqrel_failrelaxed" => { + name if name.starts_with("atomic_cxchg") => { self.codegen_atomic_cxchg(intrinsic, fargs, p, loc) } - "atomic_cxchg_failacq" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_failrelaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_rel" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), - "atomic_cxchg_relaxed" => self.codegen_atomic_cxchg(intrinsic, fargs, p, loc), "atomic_fence" => self.codegen_atomic_noop(intrinsic, loc), "atomic_fence_acq" => self.codegen_atomic_noop(intrinsic, loc), "atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc), diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/operand.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/operand.rs index e596c0518d31..b8c2ea8ac339 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/operand.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/operand.rs @@ -573,7 +573,7 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_func_expr(&mut self, instance: Instance<'tcx>, span: Option<&Span>) -> Expr { let func = self.symbol_name(instance); - let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance)); + let funct = self.codegen_function_sig(self.fn_sig_of_instance(instance).unwrap()); // make sure the functions imported from other modules are in the symbol table self.ensure(&func, |ctx, _| { Symbol::function( diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs index 045f3b0ccd6f..40238f0e8c40 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/place.rs @@ -207,6 +207,12 @@ impl<'tcx> GotocCtx<'tcx> { res.member(&field.ident.name.to_string(), &self.symbol_table) } ty::Closure(..) => res.member(&f.index().to_string(), &self.symbol_table), + ty::Generator(..) => self.codegen_unimplemented( + "ty::Generator", + Type::code(vec![], Type::empty()), + res.location().clone(), + "https://github.com/model-checking/rmc/issues/416", + ), _ => unimplemented!(), } } @@ -235,7 +241,9 @@ impl<'tcx> GotocCtx<'tcx> { // A local that is itself a FnDef, like Fn::call_once ty::FnDef(defid, substs) => Some(self.codegen_fndef(*defid, substs, None)), // A local can be pointer to a FnDef, like Fn::call and Fn::call_mut - ty::RawPtr(inner) => self.codegen_local_fndef(inner.ty).map(|f| f.address_of()), + ty::RawPtr(inner) => self + .codegen_local_fndef(inner.ty) + .map(|f| if f.can_take_address_of() { f.address_of() } else { f }), // A local can be a boxed function pointer ty::Adt(def, _) if def.is_box() => { let boxed_ty = self.codegen_ty(ty); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs index e56db5b9fbc3..3645bb9bac9f 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/statement.rs @@ -42,7 +42,7 @@ impl<'tcx> GotocCtx<'tcx> { TerminatorKind::Resume => Stmt::assert_false("resume instruction", loc), TerminatorKind::Abort => Stmt::assert_false("abort instruction", loc), TerminatorKind::Return => { - let rty = self.current_fn().sig().skip_binder().output(); + let rty = self.current_fn().sig().unwrap().skip_binder().output(); if rty.is_unit() { self.codegen_ret_unit() } else { @@ -358,8 +358,12 @@ impl<'tcx> GotocCtx<'tcx> { // should be a fat pointer for the trait let trait_fat_ptr = fargs[0].to_owned(); - // Check the Gotoc-level fat pointer type - assert!(trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table)); + //Check the Gotoc-level fat pointer type + assert!( + trait_fat_ptr.typ().is_rust_trait_fat_ptr(&self.symbol_table), + "Expected fat pointer, got:\n{:?}", + trait_fat_ptr, + ); self.codegen_virtual_funcall( trait_fat_ptr, @@ -537,6 +541,16 @@ impl<'tcx> GotocCtx<'tcx> { 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::none(), + "https://github.com/model-checking/rmc/issues/416", + ) + .as_stmt(Location::none()); + } _ => unreachable!(), }; let layout = self.layout_of(pt); diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs index b38f200e99f2..13ca61a9566e 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/codegen/typ.rs @@ -148,20 +148,21 @@ impl<'tcx> GotocCtx<'tcx> { self.sig_with_closure_untupled(sig) } - pub fn fn_sig_of_instance(&self, instance: Instance<'tcx>) -> ty::PolyFnSig<'tcx> { + 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() { - ty::Closure(def_id, subst) => self.closure_sig(*def_id, subst), + ty::Closure(def_id, subst) => Some(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 self.sig_with_closure_untupled(sig); + return Some(self.sig_with_closure_untupled(sig)); } - sig + Some(sig) } + ty::Generator(_def_id, _substs, _movability) => None, _ => unreachable!("Can't get function signature of type: {:?}", fntyp), }) } @@ -243,7 +244,7 @@ impl<'tcx> GotocCtx<'tcx> { idx: usize, ) -> DatatypeComponent { // Gives a binder with function signature - let sig = self.fn_sig_of_instance(instance); + let sig = self.fn_sig_of_instance(instance).unwrap(); // Gives an Irep Pointer object for the signature let fn_ty = self.codegen_dynamic_function_sig(sig); @@ -367,14 +368,6 @@ impl<'tcx> GotocCtx<'tcx> { // StructTag("tag-std::boxed::Box") } let t = self.monomorphize(t); with_no_trimmed_paths(|| printer.print_type(t).unwrap()); - // TODO: The following line is a temporary measure to remove the static lifetime - // appearing as \'static in mangled type names. This should be done using regular - // expressions to handle more or less whitespace around the lifetime, but this - // requires adding the regex module to the dependencies in Cargo.toml. This should - // probably be done modifying the rustc pretty printer, but that is deep in the rustc - // code. See the implementation of pretty_print_region on line 1720 in - // compiler/rustc_middle/src/ty/print/pretty.rs. - let name = name.replace(" + \'static", "").replace("\'static ", ""); // Crate resolution: mangled names need to be distinct across different versions // of the same crate that could be pulled in by dependencies. However, RMC's @@ -493,7 +486,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(_, _, _) => unimplemented!(), + ty::Generator(_, subst, _) => self.codegen_ty_generator(subst), ty::Never => // unfortunately, there is no bottom in C. We must pick a type { @@ -681,6 +674,15 @@ impl<'tcx> GotocCtx<'tcx> { }) } + /// 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) + } + pub fn codegen_fat_ptr(&mut self, mir_type: Ty<'tcx>) -> Type { assert!( !self.use_thin_pointer(mir_type), @@ -1125,7 +1127,8 @@ 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); + let sig = + self.tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig.unwrap()); // 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/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/current_fn.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/current_fn.rs index 4528c25945a8..9327c7e1ae10 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/current_fn.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/context/current_fn.rs @@ -25,7 +25,7 @@ pub struct CurrentFnCtx<'tcx> { /// A human readable pretty name for the current function readable_name: String, /// The signature of the current function - sig: PolyFnSig<'tcx>, + sig: Option>, /// A counter to enable creating temporary variables temp_var_counter: u64, } @@ -111,7 +111,7 @@ impl CurrentFnCtx<'tcx> { } /// The signature of the function we are currently compiling - pub fn sig(&self) -> PolyFnSig<'tcx> { + pub fn sig(&self) -> Option> { self.sig } } diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/overrides/hooks.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/overrides/hooks.rs index da78c049f6ec..a8b0a1d885e3 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/overrides/hooks.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/overrides/hooks.rs @@ -10,15 +10,13 @@ use super::stubs::{HashMapStub, VecStub}; use crate::gotoc::cbmc::goto_program::{BuiltinFn, Expr, Location, Stmt, Symbol, Type}; -use crate::gotoc::mir_to_goto::utils::{ - instance_name_is, instance_name_starts_with, sig_of_instance, -}; +use crate::gotoc::mir_to_goto::utils::{instance_name_is, instance_name_starts_with}; use crate::gotoc::mir_to_goto::GotocCtx; use rustc_hir::definitions::DefPathDataName; use rustc_middle::mir::{BasicBlock, Place}; use rustc_middle::ty::layout::LayoutOf; use rustc_middle::ty::print::with_no_trimmed_paths; -use rustc_middle::ty::{Instance, InstanceDef, Ty, TyCtxt}; +use rustc_middle::ty::{self, Instance, InstanceDef, Ty, TyCtxt}; use rustc_span::Span; use std::rc::Rc; @@ -42,6 +40,31 @@ pub trait GotocHook<'tcx> { ) -> Stmt; } +fn output_of_instance_is_never<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { + let ty = instance.ty(tcx, ty::ParamEnv::reveal_all()); + match ty.kind() { + ty::Closure(_, substs) => tcx + .normalize_erasing_late_bound_regions( + ty::ParamEnv::reveal_all(), + substs.as_closure().sig(), + ) + .output() + .is_never(), + ty::FnDef(..) | ty::FnPtr(..) => tcx + .normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), ty.fn_sig(tcx)) + .output() + .is_never(), + ty::Generator(_, substs, _) => substs.as_generator().return_ty().is_never(), + _ => { + unreachable!( + "Can't take get ouput type of instance:\n{:?}\nType kind:\n{:?}", + ty, + ty.kind() + ) + } + } +} + struct ExpectFail; impl<'tcx> GotocHook<'tcx> for ExpectFail { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { @@ -166,7 +189,7 @@ struct Panic; impl<'tcx> GotocHook<'tcx> for Panic { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - sig_of_instance(tcx, instance).output().is_never() + output_of_instance_is_never(tcx, instance) && (instance_name_is(tcx, instance, "begin_panic") || instance_name_is(tcx, instance, "panic")) } @@ -188,8 +211,7 @@ struct Nevers; impl<'tcx> GotocHook<'tcx> for Nevers { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let sig = sig_of_instance(tcx, instance); - sig.output().is_never() + output_of_instance_is_never(tcx, instance) } fn handle( diff --git a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/names.rs b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/names.rs index 51ed925f3c50..900a50eeccaf 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/names.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/mir_to_goto/utils/names.rs @@ -10,7 +10,7 @@ use rustc_hir::definitions::DefPathDataName; use rustc_middle::mir::mono::CodegenUnitNameBuilder; use rustc_middle::mir::Local; use rustc_middle::ty::print::with_no_trimmed_paths; -use rustc_middle::ty::{self, Instance, TyCtxt}; +use rustc_middle::ty::{Instance, TyCtxt}; use tracing::debug; impl<'tcx> GotocCtx<'tcx> { @@ -126,14 +126,6 @@ pub fn full_crate_name(tcx: TyCtxt<'tcx>) -> String { } //TODO: These were moved from hooks.rs, where they didn't have a goto context. Normalize them. -pub fn sig_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> ty::FnSig<'tcx> { - let ty = instance.ty(tcx, ty::ParamEnv::reveal_all()); - let sig = match ty.kind() { - ty::Closure(_, substs) => substs.as_closure().sig(), - _ => ty.fn_sig(tcx), - }; - tcx.normalize_erasing_late_bound_regions(ty::ParamEnv::reveal_all(), sig) -} /// Helper function to determine if the function name starts with `expected` // TODO: rationalize how we match the hooks https://github.com/model-checking/rmc/issues/130 From 60f9d0d7c34351fabddad8908d4b34cc7c1b5fe5 Mon Sep 17 00:00:00 2001 From: Alexa VanHattum Date: Tue, 14 Sep 2021 18:42:21 +0000 Subject: [PATCH 2/2] Add test --- src/test/cbmc/Generator/main.rs | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) create mode 100644 src/test/cbmc/Generator/main.rs diff --git a/src/test/cbmc/Generator/main.rs b/src/test/cbmc/Generator/main.rs new file mode 100644 index 000000000000..7bfc80113ab7 --- /dev/null +++ b/src/test/cbmc/Generator/main.rs @@ -0,0 +1,26 @@ +// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +// 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/rmc/issues/416 + +#![feature(generators, generator_trait)] + +use std::ops::{Generator, GeneratorState}; + +// Seperate function to force translation +fn maybe_call(call: bool) { + if call { + let mut _generator = || { + yield 1; + return 2; + }; + } else { + assert!(1 + 1 == 2); + } +} + +fn main() { + maybe_call(false); +}