From 0b8ce0840e10a819e86629251b57575899daf684 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Mon, 11 Dec 2023 20:34:43 -0800 Subject: [PATCH 1/2] In lifetime_generate, only select from all_impls(trait_id) on demand --- source/rust_verify/src/lifetime_generate.rs | 203 ++++++++++++------ .../tests/assoc_type_impls.rs | 7 + 2 files changed, 146 insertions(+), 64 deletions(-) diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 8e578edb36..8b7947b125 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -88,6 +88,13 @@ pub(crate) struct State { pub(crate) datatype_decls: Vec, pub(crate) assoc_type_impls: HashMap>, pub(crate) fun_decls: Vec, + // For an impl "bounds ==> trait T(...t...)", point some or all of t to impl: + // (We add each impl for T to this when we process T) + // (To avoid importing unnecessary impls, we delay processing impl until all t are used) + // t1 -> impl, ..., tn -> impl + typ_to_trait_impls: HashMap>, + // impl -> (t1, ..., tn) and process impl when t1...tn is empty + impl_to_remaining_typs: HashMap)>, enclosing_fun_id: Option, } @@ -110,6 +117,8 @@ impl State { datatype_decls: Vec::new(), assoc_type_impls: HashMap::new(), fun_decls: Vec::new(), + typ_to_trait_impls: HashMap::new(), + impl_to_remaining_typs: HashMap::new(), enclosing_fun_id: None, } } @@ -205,6 +214,16 @@ impl State { self.reached.insert((None, id)); self.datatype_worklist.push(id); } + if let Some(impl_ids) = self.typ_to_trait_impls.remove(&id) { + // Wake up any impls waiting for our type to be reached + for impl_id in impl_ids { + if let Some((_, ref mut ts)) = self.impl_to_remaining_typs.get_mut(&impl_id) { + // Remove ourself from what impl_id is waiting on + ts.retain(|t| *t != id); + } + erase_impl_assocs(ctxt, self, impl_id); + } + } } } @@ -316,6 +335,56 @@ fn erase_generic_const<'tcx>(ctxt: &Context<'tcx>, state: &mut State, cnst: &Con } } +fn adt_args<'a, 'tcx>( + rust_item: Option, + args: &'a [rustc_middle::ty::GenericArg<'tcx>], +) -> (bool, &'a [rustc_middle::ty::GenericArg<'tcx>]) { + if rust_item == Some(RustItem::Box) + || rust_item == Some(RustItem::Rc) + || rust_item == Some(RustItem::Arc) + { + // For Box, Rc, Arc, skip the second argument (the Allocator) + // which is currently restricted to always be `Global`. + assert!(args.len() == 2); + (false, &args[0..1]) + } else { + (true, args) + } +} + +// Collect some or all as-yet unreached types mentioned directly by ty +// (It's ok to miss some, but the more we capture, the less extraneous code +// we have to import.) +fn collect_unreached_datatypes<'tcx>( + ctxt: &Context<'tcx>, + state: &State, + datatypes: &mut Vec, + ty: &Ty<'tcx>, +) { + match ty.kind() { + TyKind::Ref(_, t, _) | TyKind::Slice(t) | TyKind::Array(t, _) => { + collect_unreached_datatypes(ctxt, state, datatypes, t); + } + TyKind::Adt(AdtDef(adt_def_data), args) => { + let did = adt_def_data.did; + let rust_item = verus_items::get_rust_item(ctxt.tcx, did); + let (is_user_adt, args) = adt_args(rust_item, args); + if is_user_adt && !state.reached.contains(&(None, did)) { + datatypes.push(did); + } + for arg in args.iter() { + match arg.unpack() { + rustc_middle::ty::GenericArgKind::Type(t) => { + collect_unreached_datatypes(ctxt, state, datatypes, &t); + } + _ => {} + } + } + } + _ => {} + } +} + fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ { match ty.kind() { TyKind::Bool | TyKind::Uint(_) | TyKind::Int(_) | TyKind::Char | TyKind::Str => { @@ -349,18 +418,7 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ let rust_item = verus_items::get_rust_item(ctxt.tcx, did); let mut typ_args: Vec = Vec::new(); - - let args = if rust_item == Some(RustItem::Box) - || rust_item == Some(RustItem::Rc) - || rust_item == Some(RustItem::Arc) - { - // For Box, Rc, Arc, skip the second argument (the Allocator) - // which is currently restricted to always be `Global`. - assert!(args.len() == 2); - &args[0..1] - } else { - &args - }; + let (_, args) = adt_args(rust_item, args); for arg in args.iter() { match arg.unpack() { @@ -1829,6 +1887,62 @@ fn erase_fn<'tcx>( ); } +fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: DefId) { + if !state.impl_to_remaining_typs.contains_key(&impl_id) { + // Already finished + return; + } + if state.impl_to_remaining_typs[&impl_id].1.len() > 0 { + // We haven't reached all the types we would need to justify this impl + return; + } + let (name, _) = state.impl_to_remaining_typs.remove(&impl_id).unwrap(); + let trait_ref = ctxt.tcx.impl_trait_ref(impl_id).expect("impl_trait_ref"); + for assoc_item in ctxt.tcx.associated_items(impl_id).in_definition_order() { + match assoc_item.kind { + rustc_middle::ty::AssocKind::Type => { + let impl_name = state.typ_param(&assoc_item.name.to_string(), None); + + let mut trait_typ_args: Vec = Vec::new(); + for ty in trait_ref.skip_binder().args.types().skip(1) { + trait_typ_args.push(erase_ty(ctxt, state, &ty)); + } + let mut lifetimes: Vec = Vec::new(); + let mut typ_params: Vec = Vec::new(); + let mut generic_bounds: Vec = Vec::new(); + erase_mir_generics( + ctxt, + state, + impl_id, + false, + &mut lifetimes, + &mut typ_params, + &mut generic_bounds, + ); + let mut trait_lifetime_args: Vec = Vec::new(); + for region in trait_ref.skip_binder().args.regions() { + if let Some(id) = erase_hir_region(ctxt, state, ®ion.0) { + trait_lifetime_args.push(id); + } + } + + let generic_params = lifetimes.into_iter().chain(typ_params.into_iter()).collect(); + let self_ty = ctxt.tcx.type_of(impl_id).skip_binder(); + let self_typ = erase_ty(ctxt, state, &self_ty); + let ty = ctxt.tcx.type_of(assoc_item.def_id).skip_binder(); + let typ = erase_ty(ctxt, state, &ty); + let trait_as_datatype = + Box::new(TypX::Datatype(name.clone(), trait_lifetime_args, trait_typ_args)); + let assoc = + AssocTypeImpl { generic_params, generic_bounds, self_typ, trait_as_datatype }; + let assoc_type = AssocTypeImplType { name: impl_name, typ }; + state.assoc_type_impls.entry(assoc).or_insert(Vec::new()).push(assoc_type); + } + _ => (), + } + } +} + fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) { if !state.reached.insert((None, trait_id)) { return; @@ -1874,58 +1988,20 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) { state.trait_decls.push(decl); for impl_id in ctxt.tcx.all_impls(trait_id) { + let mut datatypes: Vec = Vec::new(); let trait_ref = ctxt.tcx.impl_trait_ref(impl_id).expect("impl_trait_ref"); - for assoc_item in ctxt.tcx.associated_items(impl_id).in_definition_order() { - match assoc_item.kind { - rustc_middle::ty::AssocKind::Type => { - let impl_name = state.typ_param(&assoc_item.name.to_string(), None); - - let mut trait_typ_args: Vec = Vec::new(); - for ty in trait_ref.skip_binder().args.types().skip(1) { - trait_typ_args.push(erase_ty(ctxt, state, &ty)); - } - let mut lifetimes: Vec = Vec::new(); - let mut typ_params: Vec = Vec::new(); - let mut generic_bounds: Vec = Vec::new(); - erase_mir_generics( - ctxt, - state, - impl_id, - false, - &mut lifetimes, - &mut typ_params, - &mut generic_bounds, - ); - let mut trait_lifetime_args: Vec = Vec::new(); - for region in trait_ref.skip_binder().args.regions() { - if let Some(id) = erase_hir_region(ctxt, state, ®ion.0) { - trait_lifetime_args.push(id); - } - } - - let generic_params = - lifetimes.into_iter().chain(typ_params.into_iter()).collect(); - let self_ty = ctxt.tcx.type_of(impl_id).skip_binder(); - let self_typ = erase_ty(ctxt, state, &self_ty); - let ty = ctxt.tcx.type_of(assoc_item.def_id).skip_binder(); - let typ = erase_ty(ctxt, state, &ty); - let trait_as_datatype = Box::new(TypX::Datatype( - name.clone(), - trait_lifetime_args, - trait_typ_args, - )); - let assoc = AssocTypeImpl { - generic_params, - generic_bounds, - self_typ, - trait_as_datatype, - }; - let assoc_type = AssocTypeImplType { name: impl_name, typ }; - state.assoc_type_impls.entry(assoc).or_insert(Vec::new()).push(assoc_type); + for ty in trait_ref.skip_binder().args.types() { + collect_unreached_datatypes(ctxt, state, &mut datatypes, &ty); + for t in &datatypes { + if !state.typ_to_trait_impls.contains_key(t) { + state.typ_to_trait_impls.insert(*t, Vec::new()); } - _ => (), + state.typ_to_trait_impls.get_mut(&t).unwrap().push(impl_id); } } + assert!(!state.impl_to_remaining_typs.contains_key(&impl_id)); + state.impl_to_remaining_typs.insert(impl_id, (name.clone(), datatypes)); + erase_impl_assocs(ctxt, state, impl_id); } } } @@ -2144,10 +2220,9 @@ fn erase_mir_datatype<'tcx>(ctxt: &Context<'tcx>, state: &mut State, id: DefId) DatatypeTransparency::Never => true, DatatypeTransparency::WhenVisible(_) => false, }, - None => { - dbg!(id); - panic!("erase_mir_datatype: unrecognized datatype"); - } + // We may see extra datatypes from imported libraries that we + // use for associated types: + None => true, }; if is_external_body { erase_abstract_datatype(ctxt, state, span, id); diff --git a/source/rust_verify_test/tests/assoc_type_impls.rs b/source/rust_verify_test/tests/assoc_type_impls.rs index 37b0f89743..5ca319117e 100644 --- a/source/rust_verify_test/tests/assoc_type_impls.rs +++ b/source/rust_verify_test/tests/assoc_type_impls.rs @@ -376,3 +376,10 @@ test_verify_one_file! { } } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a trait definition, which may result in nontermination") } + +test_verify_one_file! { + #[test] mention_external_trait_with_assoc_type verus_code! { + fn foo(a: &A) { + } + } => Ok(()) +} From 8b2f900c3023c20fdddd44da7c9803de207a9961 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Wed, 10 Jan 2024 15:32:34 -0800 Subject: [PATCH 2/2] minor updates --- source/rust_verify/src/lifetime_generate.rs | 35 ++++++++++++--------- 1 file changed, 20 insertions(+), 15 deletions(-) diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index 8b7947b125..11eb8cd9c5 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -92,9 +92,9 @@ pub(crate) struct State { // (We add each impl for T to this when we process T) // (To avoid importing unnecessary impls, we delay processing impl until all t are used) // t1 -> impl, ..., tn -> impl - typ_to_trait_impls: HashMap>, + typs_used_in_trait_impls_reverse_map: HashMap>, // impl -> (t1, ..., tn) and process impl when t1...tn is empty - impl_to_remaining_typs: HashMap)>, + remaining_typs_needed_for_each_impl: HashMap)>, enclosing_fun_id: Option, } @@ -117,8 +117,8 @@ impl State { datatype_decls: Vec::new(), assoc_type_impls: HashMap::new(), fun_decls: Vec::new(), - typ_to_trait_impls: HashMap::new(), - impl_to_remaining_typs: HashMap::new(), + typs_used_in_trait_impls_reverse_map: HashMap::new(), + remaining_typs_needed_for_each_impl: HashMap::new(), enclosing_fun_id: None, } } @@ -214,10 +214,12 @@ impl State { self.reached.insert((None, id)); self.datatype_worklist.push(id); } - if let Some(impl_ids) = self.typ_to_trait_impls.remove(&id) { + if let Some(impl_ids) = self.typs_used_in_trait_impls_reverse_map.remove(&id) { // Wake up any impls waiting for our type to be reached for impl_id in impl_ids { - if let Some((_, ref mut ts)) = self.impl_to_remaining_typs.get_mut(&impl_id) { + if let Some((_, ref mut ts)) = + self.remaining_typs_needed_for_each_impl.get_mut(&impl_id) + { // Remove ourself from what impl_id is waiting on ts.retain(|t| *t != id); } @@ -1888,15 +1890,15 @@ fn erase_fn<'tcx>( } fn erase_impl_assocs<'tcx>(ctxt: &Context<'tcx>, state: &mut State, impl_id: DefId) { - if !state.impl_to_remaining_typs.contains_key(&impl_id) { + if !state.remaining_typs_needed_for_each_impl.contains_key(&impl_id) { // Already finished return; } - if state.impl_to_remaining_typs[&impl_id].1.len() > 0 { + if state.remaining_typs_needed_for_each_impl[&impl_id].1.len() > 0 { // We haven't reached all the types we would need to justify this impl return; } - let (name, _) = state.impl_to_remaining_typs.remove(&impl_id).unwrap(); + let (name, _) = state.remaining_typs_needed_for_each_impl.remove(&impl_id).unwrap(); let trait_ref = ctxt.tcx.impl_trait_ref(impl_id).expect("impl_trait_ref"); for assoc_item in ctxt.tcx.associated_items(impl_id).in_definition_order() { match assoc_item.kind { @@ -1993,14 +1995,17 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) { for ty in trait_ref.skip_binder().args.types() { collect_unreached_datatypes(ctxt, state, &mut datatypes, &ty); for t in &datatypes { - if !state.typ_to_trait_impls.contains_key(t) { - state.typ_to_trait_impls.insert(*t, Vec::new()); - } - state.typ_to_trait_impls.get_mut(&t).unwrap().push(impl_id); + state + .typs_used_in_trait_impls_reverse_map + .entry(*t) + .or_insert_with(|| Vec::new()) + .push(impl_id); } } - assert!(!state.impl_to_remaining_typs.contains_key(&impl_id)); - state.impl_to_remaining_typs.insert(impl_id, (name.clone(), datatypes)); + state + .remaining_typs_needed_for_each_impl + .insert(impl_id, (name.clone(), datatypes)) + .map(|_| panic!("already inserted")); erase_impl_assocs(ctxt, state, impl_id); } }