From f880ccf7bdb97a4f015d7a3de59abd4d5424dff2 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Tue, 21 May 2024 11:19:00 -0700 Subject: [PATCH] Support ?Sized bounds in lifetime*.rs (fixes https://github.com/verus-lang/verus/issues/1104 ) --- source/rust_verify/src/lifetime_ast.rs | 6 + source/rust_verify/src/lifetime_emit.rs | 108 +++++++++++++++--- source/rust_verify/src/lifetime_generate.rs | 12 +- .../tests/assoc_type_impls.rs | 15 +++ source/vstd/view.rs | 8 +- 5 files changed, 128 insertions(+), 21 deletions(-) diff --git a/source/rust_verify/src/lifetime_ast.rs b/source/rust_verify/src/lifetime_ast.rs index 04d2035d0..ea889065c 100644 --- a/source/rust_verify/src/lifetime_ast.rs +++ b/source/rust_verify/src/lifetime_ast.rs @@ -28,6 +28,9 @@ impl Id { pub(crate) fn to_string(&self) -> String { crate::lifetime_emit::encode_id(self.kind, self.rename_count, &self.raw_id) } + pub(crate) fn is_typ_param(&self) -> bool { + self.kind == IdKind::TypParam + } } pub(crate) type Typ = Box; @@ -35,6 +38,8 @@ pub(crate) type Typ = Box; pub(crate) enum TypX { Primitive(String), TypParam(Id), + // inside trait declarations, Self is special: + TraitSelf, Never, Ref(Typ, Option, Mutability), Phantom(Typ), @@ -136,6 +141,7 @@ pub(crate) enum ClosureKind { pub(crate) enum Bound { Copy, Clone, + Sized, Id(Id), // use TypX::Datatype to represent Trait bound Trait(Typ), diff --git a/source/rust_verify/src/lifetime_emit.rs b/source/rust_verify/src/lifetime_emit.rs index 48ab885ac..10a810f50 100644 --- a/source/rust_verify/src/lifetime_emit.rs +++ b/source/rust_verify/src/lifetime_emit.rs @@ -58,6 +58,7 @@ impl ToString for TypX { match self { TypX::Primitive(s) => s.clone(), TypX::TypParam(id) => id.to_string(), + TypX::TraitSelf => "Self".to_string(), TypX::Never => "!".to_string(), TypX::Ref(t, lifetime, Mutability::Not) => { "&".to_string() + &lifetime_string(lifetime) + &t.to_string() @@ -702,7 +703,7 @@ fn emit_generic_params(state: &mut EmitState, generics: &Vec) { } } -fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String { +fn emit_generic_bound(bound: &GenericBound, bare: bool, emit_sized: bool) -> String { let mut buf = String::new(); if !bare { buf += &bound.typ.to_string(); @@ -723,6 +724,11 @@ fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String { Bound::Clone => { buf += "Clone"; } + Bound::Sized => { + if emit_sized { + buf += "Sized"; + } + } Bound::Id(x) => { buf += &x.to_string(); } @@ -743,12 +749,75 @@ fn emit_generic_bound(bound: &GenericBound, bare: bool) -> String { buf } -fn emit_generic_bounds(state: &mut EmitState, bounds: &Vec) { - if bounds.len() > 0 { - state.write(" where "); - for bound in bounds.iter() { - state.write(emit_generic_bound(bound, false)); - state.write(", "); +// Return (bare bounds ": U", where bounds "where ...") +fn simplify_assoc_typ_bounds( + trait_name: &Id, + assoc_name: &Id, + bounds: Vec, +) -> (Vec, Vec) { + // When rustc sees "trait T { type X: U; }", + // it converts it into "trait T { type X where ::X: U; }". + // However, if we emit "where ::X: U" directly, + // rustc seems to lose track of the bound, as described in this issue: + // https://github.com/rust-lang/rust/issues/113195 + // Therefore, we need to convert the bound back to the simpler bare "X: U" syntax. + // (Also note that "type X: for<'a> U<'a>" becomes "type X where for<'a> ::X: U<'a>") + let mut bares: Vec = Vec::new(); + let mut wheres: Vec = Vec::new(); + for bound in bounds { + let is_bare = match &*bound.typ { + TypX::Projection { self_typ, trait_as_datatype, name } if name == assoc_name => { + match (&**self_typ, &**trait_as_datatype) { + (TypX::TraitSelf, TypX::Datatype(id, _, _)) if id == trait_name => true, + _ => false, + } + } + _ => false, + }; + if is_bare { + bares.push(bound); + } else { + wheres.push(bound); + } + } + (bares, wheres) +} + +fn emit_generic_bounds( + state: &mut EmitState, + params: &Vec, + bounds: &Vec, + emit_sized: bool, +) { + use std::collections::HashSet; + let mut printed_where = false; + let print_where = |state: &mut EmitState, printed_where: &mut bool| { + if !*printed_where { + *printed_where = true; + state.write(" where "); + } + }; + let mut sized: HashSet = HashSet::new(); + for bound in bounds.iter() { + print_where(state, &mut printed_where); + state.write(emit_generic_bound(bound, false, emit_sized)); + state.write(", "); + if !emit_sized && bound.bound == Bound::Sized { + if let TypX::TypParam(x) = &*bound.typ { + sized.insert(x.clone()); + } + } + } + if !emit_sized { + for param in params { + print_where(state, &mut printed_where); + if param.const_typ.is_none() + && param.name.is_typ_param() + && !sized.contains(¶m.name) + { + state.write(param.name.to_string()); + state.write(" : ?Sized, "); + } } } } @@ -787,7 +856,7 @@ pub(crate) fn emit_fun_decl(state: &mut EmitState, f: &FunDecl) { } } state.end_span(f.sig_span); - emit_generic_bounds(state, &f.generic_bounds); + emit_generic_bounds(state, &f.generic_params, &f.generic_bounds, false); match &*f.body { (_, ExpX::Block(..)) => { emit_exp(state, &f.body); @@ -857,7 +926,7 @@ fn emit_copy_clone( state.write(format!(" {bound_name} for ")); state.write(d.name.to_string()); emit_generic_params(state, &generic_args); - emit_generic_bounds(state, &generic_bounds); + emit_generic_bounds(state, &vec![], &generic_bounds, false); state.write(" "); state.write(body); } @@ -868,18 +937,25 @@ pub(crate) fn emit_trait_decl(state: &mut EmitState, t: &TraitDecl) { state.write("trait "); state.write(&t.name.to_string()); emit_generic_params(state, &t.generic_params); - emit_generic_bounds(state, &t.generic_bounds); + emit_generic_bounds(state, &t.generic_params, &t.generic_bounds, true); state.write(" {"); state.push_indent(); for (a, bounds) in &t.assoc_typs { + let (bares, wheres) = simplify_assoc_typ_bounds(&t.name, a, bounds.clone()); state.newline(); state.write("type "); state.write(a.to_string()); - if bounds.len() > 0 { + let sized = bares.iter().any(|b| b.bound == Bound::Sized); + let unsize = if sized { vec![] } else { vec!["?Sized".to_string()] }; + if bounds.len() + unsize.len() > 0 { state.write(" : "); - let bounds_strs: Vec<_> = - bounds.iter().map(|bound| emit_generic_bound(bound, true)).collect(); + let bounds_strs: Vec<_> = bares + .iter() + .map(|bound| emit_generic_bound(bound, true, false)) + .chain(unsize.into_iter()) + .collect(); state.write(bounds_strs.join("+")); + emit_generic_bounds(state, &vec![], &wheres, false); } state.write(";"); } @@ -901,7 +977,7 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) { let suffix_where = match &*d.datatype { Datatype::Struct(Fields::Pos(..)) => d.generic_bounds.len() > 0, _ => { - emit_generic_bounds(state, &d.generic_bounds); + emit_generic_bounds(state, &d.generic_params, &d.generic_bounds, false); false } }; @@ -910,7 +986,7 @@ pub(crate) fn emit_datatype_decl(state: &mut EmitState, d: &DatatypeDecl) { let suffix = if suffix_where { "" } else { ";" }; emit_fields(state, fields, suffix); if suffix_where { - emit_generic_bounds(state, &d.generic_bounds); + emit_generic_bounds(state, &d.generic_params, &d.generic_bounds, false); state.write(";"); } } @@ -948,7 +1024,7 @@ pub(crate) fn emit_assoc_type_impl( state.write(&trait_as_datatype.to_string()); state.write(" for "); state.write(&self_typ.to_string()); - emit_generic_bounds(state, &generic_bounds); + emit_generic_bounds(state, &generic_params, &generic_bounds, false); state.write(" {"); state.push_indent(); for fn_ in fns { diff --git a/source/rust_verify/src/lifetime_generate.rs b/source/rust_verify/src/lifetime_generate.rs index e11f3d6e1..548874679 100644 --- a/source/rust_verify/src/lifetime_generate.rs +++ b/source/rust_verify/src/lifetime_generate.rs @@ -96,6 +96,7 @@ pub(crate) struct State { remaining_typs_needed_for_each_impl: HashMap)>, enclosing_fun_id: Option, enclosing_trait_ids: Vec, + inside_trait_assoc_type: u32, } impl State { @@ -122,6 +123,7 @@ impl State { remaining_typs_needed_for_each_impl: HashMap::new(), enclosing_fun_id: None, enclosing_trait_ids: Vec::new(), + inside_trait_assoc_type: 0, } } @@ -401,7 +403,11 @@ fn erase_ty<'tcx>(ctxt: &Context<'tcx>, state: &mut State, ty: &Ty<'tcx>) -> Typ Box::new(TypX::Primitive(ty.to_string())) } TyKind::Param(p) if p.name == kw::SelfUpper => { - Box::new(TypX::TypParam(state.typ_param("Self", None))) + if state.inside_trait_assoc_type > 0 { + Box::new(TypX::TraitSelf) + } else { + Box::new(TypX::TypParam(state.typ_param("Self", None))) + } } TyKind::Param(p) => { let name = p.name.as_str(); @@ -1757,6 +1763,8 @@ fn erase_mir_predicates<'a, 'tcx>( let trait_path = def_id_to_vir_path(ctxt.tcx, &ctxt.verus_items, id); let bound = if Some(id) == ctxt.tcx.lang_items().copy_trait() { Some(Bound::Copy) + } else if Some(id) == ctxt.tcx.lang_items().sized_trait() { + Some(Bound::Sized) } else if state.trait_decl_set.contains(&trait_path) { let substs = pred.trait_ref.args; let (trait_typ_args, _) = erase_generic_args(ctxt, state, substs, true); @@ -2099,6 +2107,7 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) { let mut assoc_typs: Vec<(Id, Vec)> = Vec::new(); let assoc_items = ctxt.tcx.associated_items(trait_id); + state.inside_trait_assoc_type += 1; for assoc_item in assoc_items.in_definition_order() { match assoc_item.kind { rustc_middle::ty::AssocKind::Const => {} @@ -2161,6 +2170,7 @@ fn erase_trait<'tcx>(ctxt: &Context<'tcx>, state: &mut State, trait_id: DefId) { erase_impl_assocs(ctxt, state, impl_id); } } + state.inside_trait_assoc_type -= 1; assert!(state.enclosing_trait_ids.pop().is_some()); } diff --git a/source/rust_verify_test/tests/assoc_type_impls.rs b/source/rust_verify_test/tests/assoc_type_impls.rs index 6a2f5d9af..0106f2700 100644 --- a/source/rust_verify_test/tests/assoc_type_impls.rs +++ b/source/rust_verify_test/tests/assoc_type_impls.rs @@ -377,6 +377,21 @@ test_verify_one_file! { } => Err(err) => assert_vir_error_msg(err, "found a cyclic self-reference in a definition, which may result in nontermination") } +test_verify_one_file! { + #[test] view_ref_unsized verus_code! { + // https://github.com/verus-lang/verus/issues/1104 + use vstd::prelude::*; + fn id(t: T) -> T { + t + } + fn test() { + let bytes: [u8; 4] = [0, 0, 0, 0]; + let byte_slice: &[u8] = bytes.as_slice(); + id(byte_slice); + } + } => Ok(()) +} + test_verify_one_file! { #[test] mention_external_trait_with_assoc_type verus_code! { use vstd::prelude::*; diff --git a/source/vstd/view.rs b/source/vstd/view.rs index aedc19062..b3347e5ec 100644 --- a/source/vstd/view.rs +++ b/source/vstd/view.rs @@ -19,7 +19,7 @@ pub trait DeepView { spec fn deep_view(&self) -> Self::V; } -impl View for &A { +impl View for &A { type V = A::V; #[verifier::inline] @@ -28,7 +28,7 @@ impl View for &A { } } -impl DeepView for &A { +impl DeepView for &A { type V = A::V; #[verifier::inline] @@ -38,7 +38,7 @@ impl DeepView for &A { } #[cfg(feature = "alloc")] -impl View for alloc::boxed::Box { +impl View for alloc::boxed::Box { type V = A::V; #[verifier::inline] @@ -48,7 +48,7 @@ impl View for alloc::boxed::Box { } #[cfg(feature = "alloc")] -impl DeepView for alloc::boxed::Box { +impl DeepView for alloc::boxed::Box { type V = A::V; #[verifier::inline]