diff --git a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs index f99b6ef165eb..947210fdfaab 100644 --- a/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs +++ b/compiler/rustc_codegen_llvm/src/gotoc/hooks.rs @@ -48,10 +48,35 @@ fn sig_of_instance<'tcx>(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> ty::FnS 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 +fn name_starts_with(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>, expected: &str) -> bool { + let def_path = tcx.def_path(instance.def.def_id()); + if let Some(data) = def_path.data.last() { + match data.data.name() { + DefPathDataName::Named(name) => return name.to_string().starts_with(expected), + DefPathDataName::Anon { .. } => (), + } + } + false +} + +/// Helper function to determine if the function is exactly `expected` +// TODO: rationalize how we match the hooks https://github.com/model-checking/rmc/issues/130 +fn name_is(tcx: TyCtxt<'tcx>, instance: Instance<'tcx>, expected: &str) -> bool { + let def_path = tcx.def_path(instance.def.def_id()); + if let Some(data) = def_path.data.last() { + match data.data.name() { + DefPathDataName::Named(name) => return name.to_string() == expected, + DefPathDataName::Anon { .. } => (), + } + } + false +} + struct Assume; impl<'tcx> GotocHook<'tcx> for Assume { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let sig = sig_of_instance(tcx, instance); let def_path = tcx.def_path(instance.def.def_id()); if let Some(data) = def_path.data.last() { match data.data.name() { @@ -86,51 +111,36 @@ struct Nondet; impl<'tcx> GotocHook<'tcx> for Nondet { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let sig = sig_of_instance(tcx, instance); - let def_path = tcx.def_path(instance.def.def_id()); - if let Some(data) = def_path.data.last() { - match data.data.name() { - DefPathDataName::Named(name) => { - return name.to_string().starts_with("__nondet") - && sig.inputs().is_empty() - && !sig.output().is_never(); - } - DefPathDataName::Anon { .. } => (), - } - } - false + name_starts_with(tcx, instance, "__nondet") } fn handle( &self, tcx: &mut GotocCtx<'tcx>, _instance: Instance<'tcx>, - _fargs: Vec, + fargs: Vec, assign_to: Option>, target: Option, - _span: Option, + span: Option, ) -> Stmt { - match (assign_to, target) { - (Some(p), Some(target)) => { - let pt = tcx.place_ty(&p); - if pt.is_unit() { - Stmt::goto(tcx.find_label(&target), Location::none()) - } else { - let pe = tcx.codegen_place(&p).goto_expr; - Stmt::block(vec![ - pe.clone().assign(tcx.codegen_ty(pt).nondet()), - // we should potentially generate an assumption - match tcx.codegen_assumption(pt) { - None => Stmt::skip(Location::none()), - Some(f) => { - Stmt::assume(f.call(vec![pe.address_of()]), Location::none()) - } - }, - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - } - _ => unreachable!(), + assert!(fargs.is_empty()); + let loc = tcx.codegen_span_option2(span); + let p = assign_to.unwrap(); + let target = target.unwrap(); + let pt = tcx.place_ty(&p); + if pt.is_unit() { + Stmt::goto(tcx.find_label(&target), loc) + } else { + let pe = tcx.codegen_place(&p).goto_expr; + Stmt::block(vec![ + pe.clone().assign(tcx.codegen_ty(pt).nondet()), + // we should potentially generate an assumption + match tcx.codegen_assumption(pt) { + None => Stmt::skip(loc.clone()), + Some(f) => Stmt::assume(f.call(vec![pe.address_of()]), loc.clone()), + }, + Stmt::goto(tcx.find_label(&target), loc.clone()), + ]) } } } @@ -139,18 +149,8 @@ struct Panic; impl<'tcx> GotocHook<'tcx> for Panic { fn hook_applies(&self, tcx: TyCtxt<'tcx>, instance: Instance<'tcx>) -> bool { - let sig = sig_of_instance(tcx, instance); - let def_path = tcx.def_path(instance.def.def_id()); - if let Some(data) = def_path.data.last() { - match data.data.name() { - DefPathDataName::Named(name) => { - return (name.to_string() == "begin_panic" || name.to_string() == "panic") - && sig.output().is_never(); - } - DefPathDataName::Anon { .. } => (), - } - } - false + sig_of_instance(tcx, instance).output().is_never() + && (name_is(tcx, instance, "begin_panic") || name_is(tcx, instance, "panic")) } fn handle( @@ -214,13 +214,13 @@ impl<'tcx> GotocHook<'tcx> for Intrinsic { target: Option, span: Option, ) -> Stmt { - match (assign_to, target) { - (Some(p), Some(target)) => Stmt::block(vec![ - tcx.codegen_intrinsic(instance, fargs, &p, span), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]), - _ => unreachable!(), - } + let loc = tcx.codegen_span_option2(span); + let p = assign_to.unwrap(); + let target = target.unwrap(); + Stmt::block(vec![ + tcx.codegen_intrinsic(instance, fargs, &p, span), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -239,28 +239,28 @@ impl<'tcx> GotocHook<'tcx> for MemReplace { mut fargs: Vec, assign_to: Option>, target: Option, - _span: Option, + span: Option, ) -> Stmt { - match (assign_to, target) { - (Some(p), Some(target)) => { - // Skip an assignment to a destination that has a zero-sized type - // (For a ZST, Rust optimizes away the source and fargs.len() == 1) - let place_type = tcx.place_ty(&p); - let place_layout = tcx.layout_of(place_type); - let place_is_zst = place_layout.is_zst(); - if place_is_zst { - Stmt::block(vec![Stmt::goto(tcx.find_label(&target), Location::none())]) - } else { - let dest = fargs.remove(0); - let src = fargs.remove(0); - Stmt::block(vec![ - tcx.codegen_place(&p).goto_expr.assign(dest.clone().dereference()), - dest.dereference().assign(src), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - } - _ => unreachable!(), + let loc = tcx.codegen_span_option2(span); + let p = assign_to.unwrap(); + let target = target.unwrap(); + // Skip an assignment to a destination that has a zero-sized type + // (For a ZST, Rust optimizes away the source and fargs.len() == 1) + let place_type = tcx.place_ty(&p); + let place_layout = tcx.layout_of(place_type); + let place_is_zst = place_layout.is_zst(); + if place_is_zst { + Stmt::block(vec![Stmt::goto(tcx.find_label(&target), loc)]) + } else { + let dest = fargs.remove(0); + let src = fargs.remove(0); + Stmt::block(vec![ + tcx.codegen_place(&p) + .goto_expr + .assign(dest.clone().dereference().with_location(loc.clone())), + dest.dereference().assign(src).with_location(loc.clone()), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } } @@ -281,54 +281,49 @@ impl<'tcx> GotocHook<'tcx> for MemSwap { tcx: &mut GotocCtx<'tcx>, instance: Instance<'tcx>, mut fargs: Vec, - assign_to: Option>, + _assign_to: Option>, target: Option, - _span: Option, + span: Option, ) -> Stmt { let ty = tcx.monomorphize(instance.substs.type_at(0)); - match (assign_to, target) { - (Some(_), Some(target)) => { - let x = fargs.remove(0); - let y = fargs.remove(0); - - let func_name = format!("gen-swap<{}>", tcx.ty_mangled_name(ty)); - tcx.ensure(&func_name, |tcx, _| { - let ty = tcx.codegen_ty(ty); - let x_param = - tcx.gen_function_local_variable(1, &func_name, ty.clone().to_pointer()); - let y_param = - tcx.gen_function_local_variable(2, &func_name, ty.clone().to_pointer()); - let var = tcx.gen_function_local_variable(3, &func_name, ty); - let mut block = Vec::new(); - let xe = x_param.to_expr(); - block.push(Stmt::decl( - var.to_expr(), - Some(xe.clone().dereference()), - Location::none(), - )); - let ye = y_param.to_expr(); - let var = var.to_expr(); - block.push(xe.dereference().assign(ye.clone().dereference())); - block.push(ye.dereference().assign(var)); - - Symbol::function( - &func_name, - Type::code( - vec![x_param.to_function_parameter(), y_param.to_function_parameter()], - Type::empty(), - ), - Some(Stmt::block(block)), - Location::none(), - ) - }); - - Stmt::block(vec![ - tcx.find_function(&func_name).unwrap().call(vec![x, y]).as_stmt(), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - _ => unreachable!(), - } + let loc = tcx.codegen_span_option2(span); + let target = target.unwrap(); + let x = fargs.remove(0); + let y = fargs.remove(0); + + let func_name = format!("gen-swap<{}>", tcx.ty_mangled_name(ty)); + tcx.ensure(&func_name, |tcx, _| { + let ty = tcx.codegen_ty(ty); + let x_param = tcx.gen_function_local_variable(1, &func_name, ty.clone().to_pointer()); + let y_param = tcx.gen_function_local_variable(2, &func_name, ty.clone().to_pointer()); + let var = tcx.gen_function_local_variable(3, &func_name, ty); + let mut block = Vec::new(); + let xe = x_param.to_expr(); + block.push(Stmt::decl(var.to_expr(), Some(xe.clone().dereference()), Location::none())); + let ye = y_param.to_expr(); + let var = var.to_expr(); + block.push(xe.dereference().assign(ye.clone().dereference())); + block.push(ye.dereference().assign(var)); + + Symbol::function( + &func_name, + Type::code( + vec![x_param.to_function_parameter(), y_param.to_function_parameter()], + Type::empty(), + ), + Some(Stmt::block(block)), + Location::none(), + ) + }); + + Stmt::block(vec![ + tcx.find_function(&func_name) + .unwrap() + .call(vec![x, y]) + .as_stmt() + .with_location(loc.clone()), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -352,18 +347,16 @@ impl<'tcx> GotocHook<'tcx> for PtrRead { mut fargs: Vec, assign_to: Option>, target: Option, - _span: Option, + span: Option, ) -> Stmt { - match (assign_to, target) { - (Some(p), Some(target)) => { - let src = fargs.remove(0); - Stmt::block(vec![ - tcx.codegen_place(&p).goto_expr.assign(src.dereference()), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - _ => unreachable!(), - } + let loc = tcx.codegen_span_option2(span); + let p = assign_to.unwrap(); + let target = target.unwrap(); + let src = fargs.remove(0); + Stmt::block(vec![ + tcx.codegen_place(&p).goto_expr.assign(src.dereference().with_location(loc.clone())), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -387,19 +380,16 @@ impl<'tcx> GotocHook<'tcx> for PtrWrite { mut fargs: Vec, _assign_to: Option>, target: Option, - _span: Option, + span: Option, ) -> Stmt { - match target { - Some(target) => { - let dst = fargs.remove(0); - let src = fargs.remove(0); - Stmt::block(vec![ - dst.dereference().assign(src), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - _ => unreachable!(), - } + let loc = tcx.codegen_span_option2(span); + let target = target.unwrap(); + let dst = fargs.remove(0); + let src = fargs.remove(0); + Stmt::block(vec![ + dst.dereference().assign(src).with_location(loc.clone()), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -487,23 +477,20 @@ impl<'tcx> GotocHook<'tcx> for RustRealloc { span: Option, ) -> Stmt { let loc = tcx.codegen_span_option2(span); - match (assign_to, target) { - (Some(p), Some(target)) => { - let ptr = fargs.remove(0).cast_to(Type::void_pointer()); - fargs.remove(0); // old_size - fargs.remove(0); // align - let size = fargs.remove(0); - Stmt::block(vec![ - tcx.codegen_place(&p).goto_expr.assign( - BuiltinFn::Realloc - .call(vec![ptr, size], loc) - .cast_to(Type::unsigned_int(8).to_pointer()), - ), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - _ => unreachable!(), - } + let p = assign_to.unwrap(); + let target = target.unwrap(); + let ptr = fargs.remove(0).cast_to(Type::void_pointer()); + fargs.remove(0); // old_size + fargs.remove(0); // align + let size = fargs.remove(0); + Stmt::block(vec![ + tcx.codegen_place(&p).goto_expr.assign( + BuiltinFn::Realloc + .call(vec![ptr, size], loc.clone()) + .cast_to(Type::unsigned_int(8).to_pointer()), + ), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -525,20 +512,17 @@ impl<'tcx> GotocHook<'tcx> for RustAllocZeroed { span: Option, ) -> Stmt { let loc = tcx.codegen_span_option2(span); - match (assign_to, target) { - (Some(p), Some(target)) => { - let size = fargs.remove(0); - Stmt::block(vec![ - tcx.codegen_place(&p).goto_expr.assign( - BuiltinFn::Calloc - .call(vec![Type::size_t().one(), size], loc) - .cast_to(Type::unsigned_int(8).to_pointer()), - ), - Stmt::goto(tcx.find_label(&target), Location::none()), - ]) - } - _ => unreachable!(), - } + let p = assign_to.unwrap(); + let target = target.unwrap(); + let size = fargs.remove(0); + Stmt::block(vec![ + tcx.codegen_place(&p).goto_expr.assign( + BuiltinFn::Calloc + .call(vec![Type::size_t().one(), size], loc.clone()) + .cast_to(Type::unsigned_int(8).to_pointer()), + ), + Stmt::goto(tcx.find_label(&target), loc), + ]) } } @@ -562,20 +546,18 @@ impl<'tcx> GotocHook<'tcx> for SliceFromRawPart { target: Option, span: Option, ) -> Stmt { - match (assign_to, target) { - (Some(p), Some(target)) => { - let pt = tcx.codegen_ty(tcx.place_ty(&p)); - let data = fargs.remove(0); - let len = fargs.remove(0); - let code = tcx - .codegen_place(&p) - .goto_expr - .assign(Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table)) - .with_location(tcx.codegen_span_option2(span)); - Stmt::block(vec![code, Stmt::goto(tcx.find_label(&target), Location::none())]) - } - _ => unreachable!(), - } + let loc = tcx.codegen_span_option2(span); + let p = assign_to.unwrap(); + let target = target.unwrap(); + let pt = tcx.codegen_ty(tcx.place_ty(&p)); + let data = fargs.remove(0); + let len = fargs.remove(0); + let code = tcx + .codegen_place(&p) + .goto_expr + .assign(Expr::struct_expr_from_values(pt, vec![data, len], &tcx.symbol_table)) + .with_location(loc.clone()); + Stmt::block(vec![code, Stmt::goto(tcx.find_label(&target), loc)]) } } @@ -586,19 +568,19 @@ pub fn type_and_fn_hooks<'tcx>() -> (GotocTypeHooks<'tcx>, GotocHooks<'tcx>) { let fhks = GotocHooks { hooks: vec![ Rc::new(Panic), //Must go first, so it overrides Nevers - Rc::new(Nevers), Rc::new(Assume), - Rc::new(Nondet), + Rc::new(Intrinsic), Rc::new(MemReplace), Rc::new(MemSwap), + Rc::new(Nevers), + Rc::new(Nondet), Rc::new(PtrRead), Rc::new(PtrWrite), Rc::new(RustAlloc), + Rc::new(RustAllocZeroed), Rc::new(RustDealloc), Rc::new(RustRealloc), - Rc::new(RustAllocZeroed), Rc::new(SliceFromRawPart), - Rc::new(Intrinsic), hash_map_stub.clone(), vec_stub.clone(), ],