diff --git a/source/rust_verify/src/fn_call_to_vir.rs b/source/rust_verify/src/fn_call_to_vir.rs index 70e100606..b3e8d498d 100644 --- a/source/rust_verify/src/fn_call_to_vir.rs +++ b/source/rust_verify/src/fn_call_to_vir.rs @@ -214,7 +214,8 @@ pub(crate) fn fn_call_to_vir<'tcx>( is_trait_default = true; remove_self_trait_bound = Some((trait_id, &mut self_trait_impl_path)); } - let impl_paths = get_impl_paths(bctx, did, &inst.args, remove_self_trait_bound); + let impl_paths = + get_impl_paths(bctx, did, &inst.args, remove_self_trait_bound, expr.span)?; if tcx.trait_of_item(did).is_some() { if let Some(vir::ast::ImplPath::TraitImplPath(impl_path)) = self_trait_impl_path { @@ -242,7 +243,7 @@ pub(crate) fn fn_call_to_vir<'tcx>( let vir_args = mk_vir_args(bctx, node_substs, f, &args)?; let typ_args = mk_typ_args(bctx, node_substs, f, expr.span)?; - let impl_paths = get_impl_paths(bctx, f, node_substs, None); + let impl_paths = get_impl_paths(bctx, f, node_substs, None, expr.span)?; let target = CallTarget::Fun(target_kind, name, typ_args, impl_paths, autospec_usage); Ok(bctx.spanned_typed_new(expr.span, &expr_typ()?, ExprX::Call(target, Arc::new(vir_args)))) } @@ -1426,7 +1427,7 @@ fn verus_item_to_vir<'tcx, 'a>( typ_args.swap(0, 1); let typ_args = Arc::new(typ_args); - let impl_paths = get_impl_paths(bctx, f, node_substs, None); + let impl_paths = get_impl_paths(bctx, f, node_substs, None, expr.span)?; return mk_expr(ExprX::Call( CallTarget::BuiltinSpecFun(bsf, typ_args, impl_paths), @@ -1446,7 +1447,8 @@ fn get_impl_paths<'tcx>( f: DefId, node_substs: &'tcx rustc_middle::ty::List>, remove_self_trait_bound: Option<(DefId, &mut Option)>, -) -> vir::ast::ImplPaths { + span: Span, +) -> Result { if let rustc_middle::ty::FnDef(fid, _fsubsts) = bctx.ctxt.tcx.type_of(f).skip_binder().kind() { crate::rust_to_vir_base::get_impl_paths( bctx.ctxt.tcx, @@ -1455,6 +1457,7 @@ fn get_impl_paths<'tcx>( *fid, node_substs, remove_self_trait_bound, + span, ) } else { panic!("unexpected function {:?}", f) diff --git a/source/rust_verify/src/rust_to_vir_base.rs b/source/rust_verify/src/rust_to_vir_base.rs index 25b372291..3b444d947 100644 --- a/source/rust_verify/src/rust_to_vir_base.rs +++ b/source/rust_verify/src/rust_to_vir_base.rs @@ -413,9 +413,17 @@ pub(crate) fn get_impl_paths<'tcx>( target_id: DefId, node_substs: &'tcx rustc_middle::ty::List>, remove_self_trait_bound: Option<(DefId, &mut Option)>, -) -> vir::ast::ImplPaths { + span: Span, +) -> Result { let clauses = instantiate_pred_clauses(tcx, target_id, node_substs); - get_impl_paths_for_clauses(tcx, verus_items, param_env_src, clauses, remove_self_trait_bound) + get_impl_paths_for_clauses( + tcx, + verus_items, + param_env_src, + clauses, + remove_self_trait_bound, + span, + ) } pub(crate) fn get_impl_paths_for_clauses<'tcx>( @@ -424,7 +432,8 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( param_env_src: DefId, clauses: Vec<(Option>, Clause<'tcx>)>, mut remove_self_trait_bound: Option<(DefId, &mut Option)>, -) -> vir::ast::ImplPaths { + span: Span, +) -> Result { let mut impl_paths = Vec::new(); let param_env = tcx.param_env(param_env_src); @@ -465,8 +474,8 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( let trait_refs = tcx.normalize_erasing_regions(param_env, trait_refs); tcx.codegen_select_candidate((param_env, trait_refs)) }); - if let Ok(impl_source) = candidate { - if let rustc_middle::traits::ImplSource::UserDefined(u) = impl_source { + match candidate { + Ok(rustc_middle::traits::ImplSource::UserDefined(u)) => { let impl_path = def_id_to_vir_path(tcx, verus_items, u.impl_def_id); let impl_path = ImplPath::TraitImplPath(impl_path); match (&mut remove_self_trait_bound, inst_bound) { @@ -487,19 +496,9 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( predicate_worklist.push(p); } } - } else if let rustc_middle::traits::ImplSource::Builtin( - rustc_middle::traits::BuiltinImplSource::Misc, - _, - ) = impl_source - { - // When the needed trait bound is `FnDef(f) : FnOnce(...)` - // The `impl_source` doesn't have the information we need, - // so we have to special case this here. - - // REVIEW: need to see if there are other problematic cases here; - // I think codegen_select_candidate lacks some information because - // it's used for codegen - + } + Ok(rustc_middle::traits::ImplSource::Param(_)) => {} + Ok(rustc_middle::traits::ImplSource::Builtin(_, _)) => { match inst_pred_kind { ClauseKind::Trait(TraitPredicate { trait_ref: @@ -514,6 +513,7 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( || Some(trait_def_id) == tcx.lang_items().fn_mut_trait() || Some(trait_def_id) == tcx.lang_items().fn_once_trait() { + // Handle the trait bound is `FnDef(f) : FnOnce(...)` match trait_args.into_type_list(tcx)[0].kind() { TyKind::FnDef(fn_def_id, fn_node_substs) => { let fn_path = @@ -534,15 +534,36 @@ pub(crate) fn get_impl_paths_for_clauses<'tcx>( } _ => {} } + } else if Some(trait_def_id) == tcx.lang_items().sized_trait() + || Some(trait_def_id) == tcx.lang_items().tuple_trait() + || Some(trait_def_id) == tcx.lang_items().pointee_trait() + || Some(trait_def_id) == tcx.lang_items().sync_trait() + || matches!( + verus_items::get_rust_item(tcx, trait_def_id), + Some(RustItem::Send | RustItem::Thin) + ) + { + // Sized, Tuple, Pointee, Thin are all ok to do nothing. + // There can't be user impls of these traits, they can only be built-in. + + // TODO: Send and Sync needs handling, or a rigorous argument why it's ok to skip; + // See https://github.com/verus-lang/verus/issues/1335 + } else { + unsupported_err!(span, "this trait bound: {:?}", trait_refs) } } - _ => {} + _ => { + unsupported_err!(span, "this trait bound: {:?}", trait_refs) + } } } + Err(_) => { + // TODO this happens sometimes - why? + } } } } - Arc::new(impl_paths) + Ok(Arc::new(impl_paths)) } pub(crate) fn mk_visibility<'tcx>(ctxt: &Context<'tcx>, def_id: DefId) -> vir::ast::Visibility { @@ -975,7 +996,8 @@ pub(crate) fn mid_ty_to_vir_ghost<'tcx>( return Ok((Arc::new(TypX::SpecFn(param_typs, ret_typ)), false)); } let typ_args = typ_args.into_iter().map(|(t, _)| t).collect(); - let impl_paths = get_impl_paths(tcx, verus_items, param_env_src, did, args, None); + let impl_paths = + get_impl_paths(tcx, verus_items, param_env_src, did, args, None, span)?; let datatypex = def_id_to_datatype(tcx, verus_items, did, Arc::new(typ_args), impl_paths); (Arc::new(datatypex), false) diff --git a/source/rust_verify/src/rust_to_vir_expr.rs b/source/rust_verify/src/rust_to_vir_expr.rs index 992d7e6c0..a3e5c2d69 100644 --- a/source/rust_verify/src/rust_to_vir_expr.rs +++ b/source/rust_verify/src/rust_to_vir_expr.rs @@ -1551,7 +1551,8 @@ pub(crate) fn expr_to_vir_innermost<'tcx>( bctx.fun_id, vec![(None, clause)], None, - ); + expr.span, + )?; let typ_args = Arc::new(vec![tup_typ, ret_typ, fun_typ]); ( diff --git a/source/rust_verify/src/rust_to_vir_impl.rs b/source/rust_verify/src/rust_to_vir_impl.rs index 8dd136755..59027d485 100644 --- a/source/rust_verify/src/rust_to_vir_impl.rs +++ b/source/rust_verify/src/rust_to_vir_impl.rs @@ -83,7 +83,8 @@ fn trait_impl_to_vir<'tcx>( trait_did, trait_ref.skip_binder().args, None, - ); + span, + )?; // If we have `impl X for Z` then the list of types is [X, A, B, C]. // We keep this full list, with the first element being the Self type X diff --git a/source/rust_verify/src/verus_items.rs b/source/rust_verify/src/verus_items.rs index b4ae97d41..9917951d2 100644 --- a/source/rust_verify/src/verus_items.rs +++ b/source/rust_verify/src/verus_items.rs @@ -598,6 +598,8 @@ pub(crate) enum RustItem { ManuallyDrop, PhantomData, Destruct, + Send, + Thin, } pub(crate) fn get_rust_item<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> Option { @@ -698,6 +700,12 @@ pub(crate) fn get_rust_item_str(rust_path: Option<&str>) -> Option { if rust_path == Some("core::alloc::Allocator") { return Some(RustItem::Allocator); } + if rust_path == Some("core::marker::Send") { + return Some(RustItem::Send); + } + if rust_path == Some("core::ptr::metadata::Thin") { + return Some(RustItem::Thin); + } if let Some(rust_path) = rust_path { static NUM_RE: std::sync::OnceLock = std::sync::OnceLock::new();