From 08249a818345e7b5c2a09b3805c7ece6dbb0bc7d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 13 May 2025 16:37:15 +0200 Subject: [PATCH 1/4] Translate trait required predicates if any --- engine/lib/concrete_ident/concrete_ident.ml | 2 +- frontend/exporter/src/types/mir.rs | 4 +++- frontend/exporter/src/types/ty.rs | 8 ++++++-- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml index e098c7de4..5333c8485 100644 --- a/engine/lib/concrete_ident/concrete_ident.ml +++ b/engine/lib/concrete_ident/concrete_ident.ml @@ -483,7 +483,7 @@ module MakeRenderAPI (NP : NAME_POLICY) : RENDER_API = struct let*? _no_generics = List.is_empty impl_infos.generics.params in match impl_infos.trait_ref with | None -> Some ty - | Some { def_id = trait; generic_args = [ _self ] } -> + | Some { def_id = trait; generic_args = [ _self ]; _ } -> let* trait = Explicit_def_id.of_def_id trait in let trait = View.of_def_id trait in let*? _same_ns = [%eq: View.ModPath.t] namespace trait.mod_path in diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index d1b6c7e34..136061f4e 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -347,7 +347,7 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: UnderOwnerState<'tc generics: rustc_middle::ty::GenericArgsRef<'tcx>, ) -> (DefId, Vec, Vec, Option) { // Retrieve the trait requirements for the item. - let trait_refs = solve_item_required_traits(s, def_id, generics); + let mut trait_refs = solve_item_required_traits(s, def_id, generics); // If this is a trait method call, retreive the impl expr information for that trait. // Check if this is a trait method call: retrieve the trait source if @@ -369,8 +369,10 @@ pub(crate) fn get_function_from_def_id_and_generics<'tcx, S: UnderOwnerState<'tc // The generics for the call to `baz` will be the concatenation: ``, which we // split into `` and ``. let num_trait_generics = tinfo.r#trait.hax_skip_binder_ref().generic_args.len(); + let num_trait_trait_clauses = tinfo.r#trait.hax_skip_binder_ref().impl_exprs.len(); // Return only the method generics; the trait generics are included in `trait_impl_expr`. let method_generics = &generics[num_trait_generics..]; + trait_refs.drain(0..num_trait_trait_clauses); (method_generics.sinto(s), Some(tinfo)) } else { // Regular function call diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index ae1f6492a..cd008a0ed 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -1004,13 +1004,17 @@ pub type PolyFnSig = Binder; /// Reflects [`ty::TraitRef`] #[derive_group(Serializers)] #[derive(AdtInto)] -#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TraitRef<'tcx>, state: S as tcx)] +#[args(<'tcx, S: UnderOwnerState<'tcx>>, from: ty::TraitRef<'tcx>, state: S as s)] #[derive(Clone, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] pub struct TraitRef { pub def_id: DefId, #[from(args)] - /// reflects the `args` field + /// Generic arguments to the trait. The first type argument is the type on which the trait is + /// implemented. pub generic_args: Vec, + /// Implementations of the predicates required by the trait. + #[value(solve_item_required_traits(s, self.def_id, self.args))] + pub impl_exprs: Vec, } /// Reflects [`ty::TraitPredicate`] From 118fccfb64008ba9e0f18677ba04d9b1bab06809 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 12 May 2025 23:39:11 +0200 Subject: [PATCH 2/4] Optionally add `Drop` bounds everywhere --- cli/driver/src/exporter.rs | 1 + frontend/exporter/options/src/lib.rs | 3 ++ frontend/exporter/src/traits.rs | 12 +++-- frontend/exporter/src/traits/resolution.rs | 35 ++++++++---- frontend/exporter/src/traits/utils.rs | 60 +++++++++++++++++++-- frontend/exporter/src/types/new/full_def.rs | 6 +-- hax-types/src/cli_options/mod.rs | 1 + 7 files changed, 97 insertions(+), 21 deletions(-) diff --git a/cli/driver/src/exporter.rs b/cli/driver/src/exporter.rs index af08165ee..c78ca8fcb 100644 --- a/cli/driver/src/exporter.rs +++ b/cli/driver/src/exporter.rs @@ -194,6 +194,7 @@ impl From for hax_frontend_exporter_options::Options { fn from(opts: ExtractionCallbacks) -> hax_frontend_exporter_options::Options { hax_frontend_exporter_options::Options { inline_anon_consts: true, + resolve_drop_bounds: false, } } } diff --git a/frontend/exporter/options/src/lib.rs b/frontend/exporter/options/src/lib.rs index 19a1de9d7..977af7963 100644 --- a/frontend/exporter/options/src/lib.rs +++ b/frontend/exporter/options/src/lib.rs @@ -101,4 +101,7 @@ pub struct Options { /// blocks or advanced constant expressions as in `[T; N+1]`), or refer to them as /// `GlobalName`s. pub inline_anon_consts: bool, + /// Add `T: Drop` bounds to every type generic, so that we can build `ImplExpr`s to know what + /// code is run on drop. + pub resolve_drop_bounds: bool, } diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 8388272c2..5029ac01a 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -173,7 +173,13 @@ pub fn solve_trait<'tcx, S: BaseState<'tcx> + HasOwnerId>( let resolved = s.with_cache(|cache| { cache .predicate_searcher - .get_or_insert_with(|| PredicateSearcher::new_for_owner(s.base().tcx, s.owner_id())) + .get_or_insert_with(|| { + PredicateSearcher::new_for_owner( + s.base().tcx, + s.owner_id(), + s.base().options.resolve_drop_bounds, + ) + }) .resolve(&trait_ref, &warn) }); let impl_expr = match resolved { @@ -209,7 +215,7 @@ pub fn solve_item_required_traits<'tcx, S: UnderOwnerState<'tcx>>( } _ => {} } - let predicates = required_predicates(tcx, def_id); + let predicates = required_predicates(tcx, def_id, s.base().options.resolve_drop_bounds); impl_exprs.extend(solve_item_traits_inner(s, generics, predicates)); } let mut impl_exprs = vec![]; @@ -226,7 +232,7 @@ pub fn solve_item_implied_traits<'tcx, S: UnderOwnerState<'tcx>>( def_id: RDefId, generics: ty::GenericArgsRef<'tcx>, ) -> Vec { - let predicates = implied_predicates(s.base().tcx, def_id); + let predicates = implied_predicates(s.base().tcx, def_id, s.base().options.resolve_drop_bounds); solve_item_traits_inner(s, generics, predicates) } diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index 3d6a56c1e..ba141bd7b 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -121,10 +121,12 @@ pub struct AnnotatedTraitPred<'tcx> { fn initial_search_predicates<'tcx>( tcx: TyCtxt<'tcx>, def_id: rustc_span::def_id::DefId, + add_drop: bool, ) -> Vec> { fn acc_predicates<'tcx>( tcx: TyCtxt<'tcx>, def_id: rustc_span::def_id::DefId, + add_drop: bool, predicates: &mut Vec>, pred_id: &mut usize, ) { @@ -138,7 +140,7 @@ fn initial_search_predicates<'tcx>( // These inherit some predicates from their parent. AssocTy | AssocFn | AssocConst | Closure | Ctor(..) | Variant => { let parent = tcx.parent(def_id); - acc_predicates(tcx, parent, predicates, pred_id); + acc_predicates(tcx, parent, add_drop, predicates, pred_id); } Trait => { let self_pred = self_predicate(tcx, def_id).upcast(tcx); @@ -150,7 +152,7 @@ fn initial_search_predicates<'tcx>( _ => {} } predicates.extend( - required_predicates(tcx, def_id) + required_predicates(tcx, def_id, add_drop) .predicates .iter() .map(|(clause, _span)| *clause) @@ -164,7 +166,7 @@ fn initial_search_predicates<'tcx>( } let mut predicates = vec![]; - acc_predicates(tcx, def_id, &mut predicates, &mut 0); + acc_predicates(tcx, def_id, add_drop, &mut predicates, &mut 0); predicates } @@ -172,9 +174,10 @@ fn initial_search_predicates<'tcx>( fn parents_trait_predicates<'tcx>( tcx: TyCtxt<'tcx>, pred: PolyTraitPredicate<'tcx>, + add_drop: bool, ) -> Vec> { let self_trait_ref = pred.to_poly_trait_ref(); - implied_predicates(tcx, pred.def_id()) + implied_predicates(tcx, pred.def_id(), add_drop) .predicates .iter() .map(|(clause, _span)| *clause) @@ -200,11 +203,13 @@ pub struct PredicateSearcher<'tcx> { typing_env: rustc_middle::ty::TypingEnv<'tcx>, /// Local clauses available in the current context. candidates: HashMap, Candidate<'tcx>>, + /// Whether to add `T: Drop` bounds for every type generic and associated item. + add_drop: bool, } impl<'tcx> PredicateSearcher<'tcx> { /// Initialize the elaborator with the predicates accessible within this item. - pub fn new_for_owner(tcx: TyCtxt<'tcx>, owner_id: DefId) -> Self { + pub fn new_for_owner(tcx: TyCtxt<'tcx>, owner_id: DefId, add_drop: bool) -> Self { let mut out = Self { tcx, typing_env: TypingEnv { @@ -212,9 +217,10 @@ impl<'tcx> PredicateSearcher<'tcx> { typing_mode: TypingMode::PostAnalysis, }, candidates: Default::default(), + add_drop, }; out.extend( - initial_search_predicates(tcx, owner_id) + initial_search_predicates(tcx, owner_id, add_drop) .into_iter() .map(|clause| Candidate { path: vec![], @@ -251,8 +257,9 @@ impl<'tcx> PredicateSearcher<'tcx> { let tcx = self.tcx; // Then recursively add their parents. This way ensures a breadth-first order, // which means we select the shortest path when looking up predicates. + let add_drop = self.add_drop; self.extend(new_candidates.into_iter().flat_map(|candidate| { - parents_trait_predicates(tcx, candidate.pred) + parents_trait_predicates(tcx, candidate.pred, add_drop) .into_iter() .enumerate() .map(move |(index, parent_pred)| { @@ -292,7 +299,7 @@ impl<'tcx> PredicateSearcher<'tcx> { }; // The bounds that hold on the associated type. - let item_bounds = implied_predicates(tcx, alias_ty.def_id) + let item_bounds = implied_predicates(tcx, alias_ty.def_id, self.add_drop) .predicates .iter() .map(|(clause, _span)| *clause) @@ -480,7 +487,11 @@ impl<'tcx> PredicateSearcher<'tcx> { warn: &impl Fn(&str), ) -> Result>, String> { let tcx = self.tcx; - self.resolve_predicates(generics, required_predicates(tcx, def_id), warn) + self.resolve_predicates( + generics, + required_predicates(tcx, def_id, self.add_drop), + warn, + ) } /// Resolve the predicates implied by the given item. @@ -492,7 +503,11 @@ impl<'tcx> PredicateSearcher<'tcx> { warn: &impl Fn(&str), ) -> Result>, String> { let tcx = self.tcx; - self.resolve_predicates(generics, implied_predicates(tcx, def_id), warn) + self.resolve_predicates( + generics, + implied_predicates(tcx, def_id, self.add_drop), + warn, + ) } /// Apply the given generics to the provided clauses and resolve the trait references in the diff --git a/frontend/exporter/src/traits/utils.rs b/frontend/exporter/src/traits/utils.rs index 0ce812d1f..68c0da119 100644 --- a/frontend/exporter/src/traits/utils.rs +++ b/frontend/exporter/src/traits/utils.rs @@ -29,6 +29,7 @@ use rustc_hir::def::DefKind; use rustc_middle::ty::*; use rustc_span::def_id::DefId; +use rustc_span::DUMMY_SP; /// Returns a list of type predicates for the definition with ID `def_id`, including inferred /// lifetime constraints. This is the basic list of predicates we use for essentially all items. @@ -59,9 +60,16 @@ pub fn predicates_defined_on(tcx: TyCtxt<'_>, def_id: DefId) -> GenericPredicate /// type Type: Debug; /// } /// ``` -pub fn required_predicates<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> GenericPredicates<'tcx> { +/// +/// If `add_drop` is true, we add a `T: Drop` bound for every type generic. +pub fn required_predicates<'tcx>( + tcx: TyCtxt<'tcx>, + def_id: DefId, + add_drop: bool, +) -> GenericPredicates<'tcx> { use DefKind::*; - match tcx.def_kind(def_id) { + let def_kind = tcx.def_kind(def_id); + let mut predicates = match def_kind { AssocConst | AssocFn | AssocTy @@ -80,7 +88,28 @@ pub fn required_predicates<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> GenericPre Trait => Default::default(), // `predicates_defined_on` ICEs on other def kinds. _ => Default::default(), + }; + if add_drop { + // Add a `T: Drop` bound for every generic, unless the current trait is `Drop` itself, or + // `Sized`. + let drop_trait = tcx.lang_items().drop_trait().unwrap(); + let sized_trait = tcx.lang_items().sized_trait().unwrap(); + if def_id != drop_trait && def_id != sized_trait { + let extra_bounds = tcx + .generics_of(def_id) + .own_params + .iter() + .filter(|param| matches!(param.kind, GenericParamDefKind::Type { .. })) + .map(|param| tcx.mk_param_from_def(param)) + .map(|ty| Binder::dummy(TraitRef::new(tcx, drop_trait, [ty]))) + .map(|tref| tref.upcast(tcx)) + .map(|clause| (clause, DUMMY_SP)); + predicates.predicates = tcx + .arena + .alloc_from_iter(predicates.predicates.iter().copied().chain(extra_bounds)); + } } + predicates } /// The special "self" predicate on a trait. @@ -100,19 +129,40 @@ pub fn self_predicate<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> PolyTraitRef<'t /// type Type: Debug; /// } /// ``` -pub fn implied_predicates<'tcx>(tcx: TyCtxt<'tcx>, def_id: DefId) -> GenericPredicates<'tcx> { +/// +/// If `add_drop` is true, we add a `T: Drop` bound for every type generic and associated type. +pub fn implied_predicates<'tcx>( + tcx: TyCtxt<'tcx>, + def_id: DefId, + add_drop: bool, +) -> GenericPredicates<'tcx> { use DefKind::*; let parent = tcx.opt_parent(def_id); match tcx.def_kind(def_id) { // We consider all predicates on traits to be outputs Trait => predicates_defined_on(tcx, def_id), AssocTy if matches!(tcx.def_kind(parent.unwrap()), Trait) => { - GenericPredicates { + let mut predicates = GenericPredicates { parent, - // `skip_binder` is for an `EarlyBinder` + // `skip_binder` is for the GAT `EarlyBinder` predicates: tcx.explicit_item_bounds(def_id).skip_binder(), ..GenericPredicates::default() + }; + if add_drop { + // Add a `Drop` bound to the assoc item. + let drop_trait = tcx.lang_items().drop_trait().unwrap(); + let ty = + Ty::new_projection(tcx, def_id, GenericArgs::identity_for_item(tcx, def_id)); + let tref = Binder::dummy(TraitRef::new(tcx, drop_trait, [ty])); + predicates.predicates = tcx.arena.alloc_from_iter( + predicates + .predicates + .iter() + .copied() + .chain([(tref.upcast(tcx), DUMMY_SP)]), + ); } + predicates } _ => GenericPredicates::default(), } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 7c627814e..8b7206a93 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -217,7 +217,7 @@ pub enum FullDefKind { parent: DefId, #[value(get_param_env(s, s.owner_id()))] param_env: ParamEnv, - #[value(implied_predicates(s.base().tcx, s.owner_id()).sinto(s))] + #[value(implied_predicates(s.base().tcx, s.owner_id(), s.base().options.resolve_drop_bounds).sinto(s))] implied_predicates: GenericPredicates, #[value(s.base().tcx.associated_item(s.owner_id()).sinto(s))] associated_item: AssocItem, @@ -238,7 +238,7 @@ pub enum FullDefKind { Trait { #[value(get_param_env(s, s.owner_id()))] param_env: ParamEnv, - #[value(implied_predicates(s.base().tcx, s.owner_id()).sinto(s))] + #[value(implied_predicates(s.base().tcx, s.owner_id(), s.base().options.resolve_drop_bounds).sinto(s))] implied_predicates: GenericPredicates, /// The special `Self: Trait` clause. #[value({ @@ -919,6 +919,6 @@ fn get_param_env<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> ParamEnv { let s = &with_owner_id(s.base(), (), (), def_id); ParamEnv { generics: tcx.generics_of(def_id).sinto(s), - predicates: required_predicates(tcx, def_id).sinto(s), + predicates: required_predicates(tcx, def_id, s.base().options.resolve_drop_bounds).sinto(s), } } diff --git a/hax-types/src/cli_options/mod.rs b/hax-types/src/cli_options/mod.rs index 86c9a377d..4aaafac67 100644 --- a/hax-types/src/cli_options/mod.rs +++ b/hax-types/src/cli_options/mod.rs @@ -536,6 +536,7 @@ impl From for hax_frontend_exporter_options::Options { fn from(_opts: Options) -> hax_frontend_exporter_options::Options { hax_frontend_exporter_options::Options { inline_anon_consts: true, + resolve_drop_bounds: false, } } } From e618a18e9de3072012d9fdd13852790dfdbdcefa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 7 May 2025 09:53:54 +0200 Subject: [PATCH 3/4] Resolve virtual `Drop` trait refs --- engine/lib/import_thir.ml | 1 + frontend/exporter/src/traits.rs | 29 +++ frontend/exporter/src/traits/resolution.rs | 166 +++++++++++++++--- ...oolchain__attribute-opaque into-fstar.snap | 2 +- .../toolchain__traits into-fstar.snap | 22 +-- 5 files changed, 188 insertions(+), 32 deletions(-) diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 00f9627b0..dda8e2dd0 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -1147,6 +1147,7 @@ end) : EXPR = struct | Dyn -> Dyn | SelfImpl { path; _ } -> List.fold ~init:Self ~f:browse_path path | Builtin { trait; _ } -> Builtin (c_trait_ref span trait.value) + | Drop _ -> failwith @@ "impl_expr_atom: Drop" | Error str -> failwith @@ "impl_expr_atom: Error " ^ str and c_generic_value (span : Thir.span) (ty : Thir.generic_arg) : generic_value diff --git a/frontend/exporter/src/traits.rs b/frontend/exporter/src/traits.rs index 5029ac01a..f65ffd8c4 100644 --- a/frontend/exporter/src/traits.rs +++ b/frontend/exporter/src/traits.rs @@ -93,6 +93,11 @@ pub enum ImplExprAtom { /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that /// built-in implementation. Dyn, + /// A virtual `Drop` implementation. + /// `Drop` doesn't work like a real trait but we want to pretend it does. If a type has a + /// user-defined `impl Drop for X` we just use the `Concrete` variant, but if it doesn't we use + /// this variant to supply the data needed to know what code will run on drop. + Drop(DropData), /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This /// morally points to an invisible `impl` block; as such it contains the information we may /// need from one. @@ -109,6 +114,30 @@ pub enum ImplExprAtom { Error(String), } +#[derive(AdtInto)] +#[args(<'tcx, S: UnderOwnerState<'tcx> >, from: resolution::DropData<'tcx>, state: S as s)] +#[derive_group(Serializers)] +#[derive(Clone, Debug, Hash, PartialEq, Eq, PartialOrd, Ord, JsonSchema)] +pub enum DropData { + /// A drop that does nothing, e.g. for scalars and pointers. + Noop, + /// An implicit `Drop` local clause, if the `resolve_drop_bounds` option is `false`. If that + /// option is `true`, we'll add `Drop` bounds to every type param, and use that to resolve + /// `Drop` impls of generics. If it's `false`, we use this variant to indicate that the drop + /// clause comes from a generic or associated type. + Implicit, + /// The implicit `Drop` impl that exists for every type without an explicit `Drop` impl. The + /// virtual impl is considered to have one `T: Drop` bound for each generic argument of the + /// target type; it then simply drops each field in order. + Glue { + /// The type we're generating glue for. + ty: Ty, + /// The `ImplExpr`s for the `T: Drop` bounds of the virtual impl. There is one for each + /// generic argument, in order. + impl_exprs: Vec, + }, +} + /// An `ImplExpr` describes the full data of a trait implementation. Because of generics, this may /// need to combine several concrete trait implementation items. For example, `((1u8, 2u8), /// "hello").clone()` combines the generic implementation of `Clone` for `(A, B)` with the diff --git a/frontend/exporter/src/traits/resolution.rs b/frontend/exporter/src/traits/resolution.rs index ba141bd7b..9170e38e5 100644 --- a/frontend/exporter/src/traits/resolution.rs +++ b/frontend/exporter/src/traits/resolution.rs @@ -8,7 +8,7 @@ use std::collections::{hash_map::Entry, HashMap}; use rustc_hir::def::DefKind; use rustc_hir::def_id::DefId; use rustc_middle::traits::CodegenObligationError; -use rustc_middle::ty::*; +use rustc_middle::ty::{self, *}; use rustc_trait_selection::traits::ImplSource; use crate::{self_predicate, traits::utils::erase_and_norm}; @@ -73,6 +73,11 @@ pub enum ImplExprAtom<'tcx> { /// `dyn Trait` implements `Trait` using a built-in implementation; this refers to that /// built-in implementation. Dyn, + /// A virtual `Drop` implementation. + /// `Drop` doesn't work like a real trait but we want to pretend it does. If a type has a + /// user-defined `impl Drop for X` we just use the `Concrete` variant, but if it doesn't we use + /// this variant to supply the data needed to know what code will run on drop. + Drop(DropData<'tcx>), /// A built-in trait whose implementation is computed by the compiler, such as `FnMut`. This /// morally points to an invisible `impl` block; as such it contains the information we may /// need from one. @@ -89,6 +94,27 @@ pub enum ImplExprAtom<'tcx> { Error(String), } +#[derive(Debug, Clone)] +pub enum DropData<'tcx> { + /// A drop that does nothing, e.g. for scalars and pointers. + Noop, + /// An implicit `Drop` local clause, if the `resolve_drop_bounds` option is `false`. If that + /// option is `true`, we'll add `Drop` bounds to every type param, and use that to resolve + /// `Drop` impls of generics. If it's `false`, we use this variant to indicate that the drop + /// clause comes from a generic or associated type. + Implicit, + /// The implicit `Drop` impl that exists for every type without an explicit `Drop` impl. The + /// virtual impl is considered to have one `T: Drop` bound for each generic argument of the + /// target type; it then simply drops each field in order. + Glue { + /// The type we're generating glue for. + ty: Ty<'tcx>, + /// The `ImplExpr`s for the `T: Drop` bounds of the virtual impl. There is one for each + /// generic argument, in order. + impl_exprs: Vec>, + }, +} + #[derive(Clone, Debug)] pub struct ImplExpr<'tcx> { /// The trait this is an impl for. @@ -197,6 +223,22 @@ struct Candidate<'tcx> { origin: AnnotatedTraitPred<'tcx>, } +impl<'tcx> Candidate<'tcx> { + fn into_impl_expr(self, tcx: TyCtxt<'tcx>) -> ImplExprAtom<'tcx> { + let path = self.path; + let r#trait = self.origin.clause.to_poly_trait_ref(); + match self.origin.origin { + BoundPredicateOrigin::SelfPred => ImplExprAtom::SelfImpl { r#trait, path }, + BoundPredicateOrigin::Item(index) => ImplExprAtom::LocalBound { + predicate: self.origin.clause.upcast(tcx), + index, + r#trait, + path, + }, + } + } +} + /// Stores a set of predicates along with where they came from. pub struct PredicateSearcher<'tcx> { tcx: TyCtxt<'tcx>, @@ -375,10 +417,12 @@ impl<'tcx> PredicateSearcher<'tcx> { use rustc_trait_selection::traits::{ BuiltinImplSource, ImplSource, ImplSourceUserDefinedData, }; + let tcx = self.tcx; + let drop_trait = tcx.lang_items().drop_trait().unwrap(); let erased_tref = erase_and_norm(self.tcx, self.typing_env, *tref); + let trait_def_id = erased_tref.skip_binder().def_id; - let tcx = self.tcx; let impl_source = shallow_resolve_trait_ref(tcx, self.typing_env.param_env, erased_tref); let atom = match impl_source { Ok(ImplSource::UserDefined(ImplSourceUserDefinedData { @@ -397,21 +441,7 @@ impl<'tcx> PredicateSearcher<'tcx> { } Ok(ImplSource::Param(_)) => { match self.resolve_local(erased_tref.upcast(self.tcx), warn)? { - Some(candidate) => { - let path = candidate.path; - let r#trait = candidate.origin.clause.to_poly_trait_ref(); - match candidate.origin.origin { - BoundPredicateOrigin::SelfPred => { - ImplExprAtom::SelfImpl { r#trait, path } - } - BoundPredicateOrigin::Item(index) => ImplExprAtom::LocalBound { - predicate: candidate.origin.clause.upcast(tcx), - index, - r#trait, - path, - }, - } - } + Some(candidate) => candidate.into_impl_expr(tcx), None => { let msg = format!( "Could not find a clause for `{tref:?}` in the item parameters" @@ -424,9 +454,8 @@ impl<'tcx> PredicateSearcher<'tcx> { Ok(ImplSource::Builtin(BuiltinImplSource::Object { .. }, _)) => ImplExprAtom::Dyn, Ok(ImplSource::Builtin(_, _)) => { // Resolve the predicates implied by the trait. - let trait_def_id = erased_tref.skip_binder().def_id; // If we wanted to not skip this binder, we'd have to instantiate the bound - // regions, solve, then wrap the result in a binder. And track higher-kinded + // regions, solve, then wrap the result in a binder. And track higher-kinded // clauses better all over. let impl_exprs = self.resolve_item_implied_predicates( trait_def_id, @@ -463,9 +492,106 @@ impl<'tcx> PredicateSearcher<'tcx> { types, } } + // Resolve `Drop` trait impls by adding virtual impls when a real one can't be found. + Err(CodegenObligationError::Unimplemented) + if erased_tref.skip_binder().def_id == drop_trait => + { + // If we wanted to not skip this binder, we'd have to instantiate the bound + // regions, solve, then wrap the result in a binder. And track higher-kinded + // clauses better all over. + let mut resolve_drop = |ty: Ty<'tcx>| { + let tref = ty::Binder::dummy(ty::TraitRef::new(tcx, drop_trait, [ty])); + self.resolve(&tref, warn) + }; + let find_drop_impl = |ty: Ty<'tcx>| { + let mut dtor = None; + tcx.for_each_relevant_impl(drop_trait, ty, |impl_did| { + dtor = Some(impl_did); + }); + dtor + }; + // TODO: how to check if there is a real drop impl????? + let ty = erased_tref.skip_binder().args[0].as_type().unwrap(); + // Source of truth are `ty::needs_drop_components` and `tcx.needs_drop_raw`. + match ty.kind() { + // TODO: Does `UnsafeBinder` drop its contents? + ty::Bool + | ty::Char + | ty::Int(..) + | ty::Uint(..) + | ty::Float(..) + | ty::Foreign(..) + | ty::Str + | ty::RawPtr(..) + | ty::Ref(..) + | ty::FnDef(..) + | ty::FnPtr(..) + | ty::UnsafeBinder(..) + | ty::Never => ImplExprAtom::Drop(DropData::Noop), + ty::Array(inner_ty, _) | ty::Pat(inner_ty, _) | ty::Slice(inner_ty) => { + ImplExprAtom::Drop(DropData::Glue { + ty, + impl_exprs: vec![resolve_drop(*inner_ty)?], + }) + } + ty::Tuple(tys) => ImplExprAtom::Drop(DropData::Glue { + ty, + impl_exprs: tys.iter().map(resolve_drop).try_collect()?, + }), + ty::Adt(..) if let Some(_) = find_drop_impl(ty) => { + // We should have been able to resolve the `T: Drop` clause above, if we + // get here we don't know how to reconstruct the arguments to the impl. + let msg = format!("Cannot resolve clause `{tref:?}`"); + warn(&msg); + ImplExprAtom::Error(msg) + } + ty::Adt(_, args) + | ty::Closure(_, args) + | ty::Coroutine(_, args) + | ty::CoroutineClosure(_, args) + | ty::CoroutineWitness(_, args) => ImplExprAtom::Drop(DropData::Glue { + ty, + impl_exprs: args + .iter() + .filter_map(|arg| arg.as_type()) + .map(resolve_drop) + .try_collect()?, + }), + // Every `dyn` has a `Drop` in its vtable, ergo we pretend that every `dyn` has + // `Drop` in its list of traits. + ty::Dynamic(..) => ImplExprAtom::Dyn, + ty::Param(..) | ty::Alias(..) | ty::Bound(..) => { + if self.add_drop { + // We've added `Drop` impls on everything, we should be able to resolve + // it. + match self.resolve_local(erased_tref.upcast(self.tcx), warn)? { + Some(candidate) => candidate.into_impl_expr(tcx), + None => { + let msg = + format!("Cannot find virtual `Drop` clause: `{tref:?}`"); + warn(&msg); + ImplExprAtom::Error(msg) + } + } + } else { + ImplExprAtom::Drop(DropData::Implicit) + } + } + + ty::Placeholder(..) | ty::Infer(..) | ty::Error(..) => { + let msg = format!( + "Cannot resolve clause `{tref:?}` \ + because of a type error" + ); + warn(&msg); + ImplExprAtom::Error(msg) + } + } + } Err(e) => { let msg = format!( - "Could not find a clause for `{tref:?}` in the current context: `{e:?}`" + "Could not find a clause for `{tref:?}` \ + in the current context: `{e:?}`" ); warn(&msg); ImplExprAtom::Error(msg) diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index 4f728c82f..1059c7a8a 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -133,7 +133,7 @@ class t_T (v_Self: Type0) = { val impl_T_for_u8:t_T u8 class t_TrGeneric (v_Self: Type0) (v_U: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_11075708886900110455:Core.Clone.t_Clone v_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_16006850527666200319:Core.Clone.t_Clone v_U; f_f_pre:v_U -> Type0; f_f_post:v_U -> v_Self -> Type0; f_f:x0: v_U -> Prims.Pure v_Self (f_f_pre x0) (fun result -> f_f_post x0 result) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index b16d00eee..d1fec69be 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -35,11 +35,11 @@ open FStar.Mul class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 } class t_ParBlocksSizeUser (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_12386035071644742916:t_BlockSizeUser v_Self + [@@@ FStar.Tactics.Typeclasses.no_method]_super_7386178880507589171:t_BlockSizeUser v_Self } class t_BlockBackend (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_5078033630945970482:t_ParBlocksSizeUser v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_5132789780856779344:t_ParBlocksSizeUser v_Self; f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0; f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0; f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global @@ -55,7 +55,7 @@ open FStar.Mul class t_Bar (v_Self: Type0) (v_T: Type0) = { __marker_trait_t_Bar:Prims.unit } class t_Foo (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_13709452385921529338:t_Bar v_Self f_U; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_12633113900214769645:t_Bar v_Self f_U; f_U:Type0 } ''' @@ -425,11 +425,11 @@ let associated_function_caller () class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_5670955395916535991:t_Trait v_Self + [@@@ FStar.Tactics.Typeclasses.no_method]_super_2013377997652678570:t_Trait v_Self v_TypeArg v_ConstArg; f_AssocType:Type0; - f_AssocType_6891123870612467806:t_Trait f_AssocType v_TypeArg v_ConstArg + f_AssocType_4339496849715937257:t_Trait f_AssocType v_TypeArg v_ConstArg } ''' "Traits.Interlaced_consts_types.fst" = ''' @@ -506,11 +506,11 @@ open FStar.Mul class t_Trait1 (v_Self: Type0) = { f_T:Type0; - f_T_6736093233391770582:t_Trait1 f_T + f_T_14544816729875926394:t_Trait1 f_T } class t_Trait2 (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_15807083732906695011:t_Trait1 v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_17908617371471168181:t_Trait1 v_Self; f_U:Type0 } ''' @@ -567,7 +567,7 @@ open Core open FStar.Mul class t_SuperTrait (v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_16027770981543256320:Core.Clone.t_Clone v_Self; + [@@@ FStar.Tactics.Typeclasses.no_method]_super_12761901852309354934:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> Type0; f_function_of_super_trait_post:v_Self -> u32 -> Type0; f_function_of_super_trait:x0: v_Self @@ -579,7 +579,7 @@ class t_SuperTrait (v_Self: Type0) = { [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: t_SuperTrait i32 = { - _super_16027770981543256320 = FStar.Tactics.Typeclasses.solve; + _super_12761901852309354934 = FStar.Tactics.Typeclasses.solve; f_function_of_super_trait_pre = (fun (self: i32) -> true); f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true); f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl_i32__abs self <: i32) <: u32 @@ -651,7 +651,7 @@ let uuse_iimpl_trait (_: Prims.unit) : Prims.unit = class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_6638784903434849583:t_SuperTrait f_AssocType; + f_AssocType_16421706098796818672:t_SuperTrait f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> Type0; f_assoc_f_post:Prims.unit -> Prims.unit -> Type0; @@ -688,7 +688,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; - f_AssocType_6638784903434849583 = FStar.Tactics.Typeclasses.solve; + f_AssocType_16421706098796818672 = FStar.Tactics.Typeclasses.solve; f_N = mk_usize 32; f_assoc_f_pre = (fun (_: Prims.unit) -> true); f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true); From 8b45c8b64fd8c4ffaefc33a2510079790091f6d5 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 6 May 2025 15:58:51 +0200 Subject: [PATCH 4/4] Resolve `Drop` calls --- frontend/exporter/src/types/mir.rs | 40 +++++++++++++++++++++++++++++- 1 file changed, 39 insertions(+), 1 deletion(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 136061f4e..edecefd81 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -470,6 +470,38 @@ fn translate_terminator_kind_call<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasO } } +#[cfg(feature = "rustc")] +fn translate_terminator_kind_drop<'tcx, S: BaseState<'tcx> + HasMir<'tcx> + HasOwnerId>( + s: &S, + terminator: &rustc_middle::mir::TerminatorKind<'tcx>, +) -> TerminatorKind { + let tcx = s.base().tcx; + let mir::TerminatorKind::Drop { + place, + target, + unwind, + .. + } = terminator + else { + unreachable!() + }; + + let local_decls = &s.mir().local_decls; + let place_ty = place.ty(local_decls, tcx).ty; + let drop_trait = tcx.lang_items().drop_trait().unwrap(); + let impl_expr = solve_trait( + s, + ty::Binder::dummy(ty::TraitRef::new(tcx, drop_trait, [place_ty])), + ); + + TerminatorKind::Drop { + place: place.sinto(s), + impl_expr, + target: target.sinto(s), + unwind: unwind.sinto(s), + } +} + // We don't use the LitIntType on purpose (we don't want the "unsuffixed" case) #[derive_group(Serializers)] #[derive(Clone, Copy, Debug, JsonSchema, Hash, PartialEq, Eq, PartialOrd, Ord)] @@ -570,11 +602,17 @@ pub enum TerminatorKind { }, Return, Unreachable, + #[custom_arm( + x @ rustc_middle::mir::TerminatorKind::Drop { .. } => { + translate_terminator_kind_drop(s, x) + } + )] Drop { place: Place, + /// Implementation of `place.ty(): Drop`. + impl_expr: ImplExpr, target: BasicBlock, unwind: UnwindAction, - replace: bool, }, #[custom_arm( x @ rustc_middle::mir::TerminatorKind::Call { .. } => {