From 2966f15d251c3786643b0683f231a3fc287678f3 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 15:03:35 +0200 Subject: [PATCH 1/7] Make sure we use the `def_kind` workaround consistently --- frontend/exporter/src/types/def_id.rs | 16 ++++++++++++++-- frontend/exporter/src/types/new/full_def.rs | 13 +------------ 2 files changed, 15 insertions(+), 14 deletions(-) diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index fac5dddb0..9c8e96087 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -18,7 +18,7 @@ use crate::prelude::*; use crate::{AdtInto, JsonSchema}; #[cfg(feature = "rustc")] -use {rustc_hir as hir, rustc_span::def_id::DefId as RDefId}; +use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty}; pub type Symbol = String; @@ -210,6 +210,18 @@ impl std::hash::Hash for DefId { } } +/// Gets the kind of the definition. Can't use `def_kind` directly because this crashes on the +/// crate root. +#[cfg(feature = "rustc")] +pub(crate) fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> hir::def::DefKind { + if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() { + // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table + // isn't properly initialized otherwise. + let _ = tcx.def_span(def_id); + }; + tcx.def_kind(def_id) +} + #[cfg(feature = "rustc")] pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> DefId { let tcx = s.base().tcx; @@ -231,7 +243,7 @@ pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) rustc_hir::def_id::DefIndex::as_u32(def_id.index), ), is_local: def_id.is_local(), - kind: tcx.def_kind(def_id).sinto(s), + kind: get_def_kind(tcx, def_id).sinto(s), }; let contents = s.with_global_cache(|cache| id_table::Node::new(contents, &mut cache.id_table_session)); diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 8a1825c5a..cf79dd771 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -517,18 +517,7 @@ impl ImplAssocItem { } } -/// Gets the kind of the definition. -#[cfg(feature = "rustc")] -pub fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> RDefKind { - if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() { - // Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table - // isn't properly initialized otherwise. - let _ = tcx.def_span(def_id); - }; - tcx.def_kind(def_id) -} - -/// Gets the attributes of the definition. +/// Gets the span of the definition. #[cfg(feature = "rustc")] pub fn get_def_span<'tcx>( tcx: ty::TyCtxt<'tcx>, From 318bb2db0e5800ed084bea80620cfa18abf4e65a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 15:04:38 +0200 Subject: [PATCH 2/7] Add `DefId` methods to avoid `RDefId` roundtrips --- frontend/exporter/src/types/new/full_def.rs | 71 +++++++++++---------- 1 file changed, 38 insertions(+), 33 deletions(-) diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index cf79dd771..883433cae 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -39,21 +39,23 @@ where Body: IsBody + TypeMappable, { let tcx = s.base().tcx; + let hax_def_id: DefId = def_id.sinto(s); let def_kind = get_def_kind(tcx, def_id); let kind = { let state_with_id = with_owner_id(s.base(), (), (), def_id); def_kind.sinto(&state_with_id) }; + let def_span = hax_def_id.def_span(s); let source_span = def_id.as_local().map(|ldid| tcx.source_span(ldid)); let source_text = source_span .filter(|source_span| source_span.ctxt().is_root()) .and_then(|source_span| tcx.sess.source_map().span_to_snippet(source_span).ok()); FullDef { - def_id: def_id.sinto(s), + def_id: hax_def_id, parent: tcx.opt_parent(def_id).sinto(s), - span: get_def_span(tcx, def_id, def_kind).sinto(s), + span: def_span, source_span: source_span.sinto(s), source_text, attributes: get_def_attrs(tcx, def_id, def_kind).sinto(s), @@ -70,17 +72,31 @@ where } #[cfg(feature = "rustc")] -impl<'tcx, S, Body> SInto>> for RDefId -where - Body: IsBody + TypeMappable, - S: BaseState<'tcx>, -{ - fn sinto(&self, s: &S) -> Arc> { - if let Some(def) = s.with_item_cache(*self, |cache| cache.full_def.get().cloned()) { +impl DefId { + /// Get the span of the definition of this item. This is the span used in diagnostics when + /// referring to the item. + pub fn def_span<'tcx>(&self, s: &impl BaseState<'tcx>) -> Span { + use DefKind::*; + match &self.kind { + // These kinds cause `def_span` to panic. + ForeignMod => rustc_span::DUMMY_SP, + _ => s.base().tcx.def_span(self.to_rust_def_id()), + } + .sinto(s) + } + + /// Get the full definition of this item. + pub fn full_def<'tcx, S, Body>(&self, s: &S) -> Arc> + where + Body: IsBody + TypeMappable, + S: BaseState<'tcx>, + { + let def_id = self.to_rust_def_id(); + if let Some(def) = s.with_item_cache(def_id, |cache| cache.full_def.get().cloned()) { return def; } - let def = Arc::new(translate_full_def(s, *self)); - s.with_item_cache(*self, |cache| cache.full_def.insert(def.clone())); + let def = Arc::new(translate_full_def(s, def_id)); + s.with_item_cache(def_id, |cache| cache.full_def.insert(def.clone())); def } } @@ -186,9 +202,11 @@ pub enum FullDefKind { .tcx .associated_items(s.owner_id()) .in_definition_order() - .map(|assoc| (assoc, assoc.def_id)) + .map(|assoc| { + let def_id = assoc.def_id.sinto(s); + (assoc.sinto(s), def_id.full_def(s)) + }) .collect::>() - .sinto(s) )] items: Vec<(AssocItem, Arc>)>, }, @@ -517,21 +535,6 @@ impl ImplAssocItem { } } -/// Gets the span of the definition. -#[cfg(feature = "rustc")] -pub fn get_def_span<'tcx>( - tcx: ty::TyCtxt<'tcx>, - def_id: RDefId, - def_kind: RDefKind, -) -> rustc_span::Span { - use RDefKind::*; - match def_kind { - // These kinds cause `def_span` to panic. - ForeignMod => rustc_span::DUMMY_SP, - _ => tcx.def_span(def_id), - } -} - /// Gets the visibility (`pub` or not) of the definition. Returns `None` for defs that don't have a /// meaningful visibility. #[cfg(feature = "rustc")] @@ -654,9 +657,11 @@ where let items = tcx .associated_items(impl_def_id) .in_definition_order() - .map(|assoc| (assoc, assoc.def_id)) - .collect::>() - .sinto(s); + .map(|assoc| { + let def_id = assoc.def_id.sinto(s); + (assoc.sinto(s), def_id.full_def(s)) + }) + .collect::>(); FullDefKind::InherentImpl { param_env, ty: ty.sinto(s), @@ -684,7 +689,7 @@ where .in_definition_order() .map(|decl_assoc| { let decl_def_id = decl_assoc.def_id; - let decl_def = decl_def_id.sinto(s); + let decl_def = decl_def_id.sinto(s).full_def(s); // Impl exprs required by the item. let required_impl_exprs; let value = match item_map.remove(&decl_def_id) { @@ -700,7 +705,7 @@ where }; ImplAssocItemValue::Provided { - def: impl_assoc.def_id.sinto(s), + def: impl_assoc.def_id.sinto(s).full_def(s), is_override: decl_assoc.defaultness(tcx).has_value(), } } From 5160be0ba5887aac39e9ebd51bfe9d1473a4eaf7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 15:20:58 +0200 Subject: [PATCH 3/7] Make conversion to `RDefId` harder --- frontend/exporter/src/types/def_id.rs | 17 +---------------- frontend/exporter/src/types/new/full_def.rs | 7 +++---- 2 files changed, 4 insertions(+), 20 deletions(-) diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index 9c8e96087..3519b9c33 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -197,7 +197,7 @@ impl std::fmt::Debug for DefId { impl std::fmt::Debug for DefId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { // Use the more legible rustc debug implementation. - write!(f, "{:?}", rustc_span::def_id::DefId::from(self)) + write!(f, "{:?}", self.to_rust_def_id()) } } @@ -262,21 +262,6 @@ impl<'s, S: BaseState<'s>> SInto for RDefId { } } -#[cfg(feature = "rustc")] -impl From<&DefId> for RDefId { - fn from<'tcx>(def_id: &DefId) -> Self { - def_id.to_rust_def_id() - } -} - -// Impl to be able to use hax's `DefId` for many rustc queries. -#[cfg(feature = "rustc")] -impl rustc_middle::query::IntoQueryParam for &DefId { - fn into_query_param(self) -> RDefId { - self.into() - } -} - #[cfg(not(feature = "extract_names_mode"))] pub type Path = Vec; diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 883433cae..b0600896a 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -442,9 +442,8 @@ pub enum ImplAssocItemValue { } impl FullDef { - #[cfg(feature = "rustc")] - pub fn rust_def_id(&self) -> RDefId { - (&self.def_id).into() + pub fn def_id(&self) -> &DefId { + &self.def_id } pub fn kind(&self) -> &FullDefKind { @@ -503,7 +502,7 @@ impl FullDef { }; // Add inherent impl items if any. let tcx = s.base().tcx; - for impl_def_id in tcx.inherent_impls(self.rust_def_id()) { + for impl_def_id in tcx.inherent_impls(self.def_id.to_rust_def_id()) { children.extend( tcx.associated_items(impl_def_id) .in_definition_order() From 02ffaec85757c4fcc38393904a0c7382ac6213da Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 15:53:06 +0200 Subject: [PATCH 4/7] Give a fake DefId to promoted constants --- .../lib/concrete_ident/concrete_ident_view.ml | 8 +- engine/names/extract/build.rs | 1 + .../ocaml_of_json_schema.js | 2 +- frontend/exporter/src/types/def_id.rs | 96 +++++++++++++++---- frontend/exporter/src/types/mir.rs | 22 ++--- frontend/exporter/src/types/new/full_def.rs | 33 ++++--- .../toolchain__include-flag into-coq.snap | 2 +- 7 files changed, 115 insertions(+), 49 deletions(-) diff --git a/engine/lib/concrete_ident/concrete_ident_view.ml b/engine/lib/concrete_ident/concrete_ident_view.ml index 83b0f7960..d3b0d5a4d 100644 --- a/engine/lib/concrete_ident/concrete_ident_view.ml +++ b/engine/lib/concrete_ident/concrete_ident_view.ml @@ -128,12 +128,12 @@ let rec poly : (match List.last_exn (Explicit_def_id.to_def_id did).path with | { data = GlobalAsm; disambiguator } -> into_d did disambiguator | _ -> broken_invariant "last path chunk to be GlobalAsm" did) - | TyParam | ConstParam | InlineConst | LifetimeParam | Closure - | SyntheticCoroutineBody -> + | TyParam | ConstParam | InlineConst | PromotedConst | LifetimeParam + | Closure | SyntheticCoroutineBody -> (* It should be impossible for such items to ever be referenced by anyting in hax. *) broken_invariant - "non (TyParam | ConstParam | InlineConst | LifetimeParam | Closure | \ - SyntheticCoroutineBody) identifier" + "non (TyParam | ConstParam | InlineConst | PromotedConst | \ + LifetimeParam | Closure | SyntheticCoroutineBody) identifier" did in result diff --git a/engine/names/extract/build.rs b/engine/names/extract/build.rs index 44d18d8a1..4026bf4e9 100644 --- a/engine/names/extract/build.rs +++ b/engine/names/extract/build.rs @@ -67,6 +67,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String { DefPathItem::Closure => "Closure".into(), DefPathItem::Ctor => "Ctor".into(), DefPathItem::AnonConst => "AnonConst".into(), + DefPathItem::PromotedConst => "PromotedConst".into(), DefPathItem::TypeNs(None) | DefPathItem::OpaqueTy => "OpaqueTy".into(), } } diff --git a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js index 6decb4220..1a42a1c4d 100644 --- a/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js +++ b/engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js @@ -364,7 +364,7 @@ let export_record = (fields, path, name) => { let record_expression = fields.map(([field, type, _doc], i) => { if (field == 'index' && name == 'def_id_contents') { // This is a hack to always parse Rust DefId indexes to `(0, 0)` - return 'index = Base.Int64.(zero, zero)'; + return 'index = Base.Int64.(zero, zero, None)'; } let p = [...path, 'field_' + field]; let sub = mk_match('x', ocaml_arms_of_type_expr(type, p), p); diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index 3519b9c33..c2bd1bf59 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -72,10 +72,22 @@ pub enum MacroKind { Derive, } +/// The id of a promoted MIR constant. +/// +/// Reflects [`rustc_middle::mir::Promoted`]. +#[derive_group(Serializers)] +#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)] +#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))] +#[cfg_attr(not(feature = "extract_names_mode"), args(, from: rustc_middle::mir::Promoted, state: S as _s))] +pub struct PromotedId { + #[cfg_attr(not(feature = "extract_names_mode"), value(self.as_u32()))] + pub id: u32, +} + /// Reflects [`rustc_hir::def::DefKind`] #[derive_group(Serializers)] #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))] -#[cfg_attr(not(feature = "extract_names_mode"),args(, from: rustc_hir::def::DefKind, state: S as tcx))] +#[cfg_attr(not(feature = "extract_names_mode"), args(, from: rustc_hir::def::DefKind, state: S as tcx))] #[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)] pub enum DefKind { Mod, @@ -106,6 +118,9 @@ pub enum DefKind { ForeignMod, AnonConst, InlineConst, + #[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)] + /// Added by hax: promoted constants don't have def_ids in rustc but they do in hax. + PromotedConst, OpaqueTy, Field, LifetimeParam, @@ -117,7 +132,8 @@ pub enum DefKind { SyntheticCoroutineBody, } -/// Reflects [`rustc_hir::def_id::DefId`] +/// Reflects [`rustc_hir::def_id::DefId`], augmented to also give ids to promoted constants (which +/// have their own ad-hoc numbering scheme in rustc for now). #[derive_group(Serializers)] #[derive(Clone, PartialEq, Eq, PartialOrd, Ord)] #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))] @@ -132,30 +148,52 @@ pub struct DefIdContents { pub krate: String, pub path: Vec, pub parent: Option, - /// Rustc's `CrateNum` and `DefIndex` raw indexes. This can be - /// useful if one needs to convert a [`DefId`] into a - /// [`rustc_hir::def_id::DefId`]; there is a `From` instance for - /// that purpose. + /// Stores rustc's `CrateNum`, `DefIndex` and `Promoted` raw indices. This can be useful if one + /// needs to convert a [`DefId`] into a [`rustc_hir::def_id::DefId`]. If the promoted id is + /// `Some`, then this `DefId` indicates the nth promoted constant associated with the item, + /// which doesn't have a real `rustc::DefId`. /// - /// **Warning: this `index` field might not be safe to use**. They are - /// valid only for one Rustc sesssion. Please do not rely on those - /// indexes unless you cannot do otherwise. - pub index: (u32, u32), + /// **Warning: this `index` field might not be safe to use**. They are valid only for one Rustc + /// sesssion. Please do not rely on those indices unless you cannot do otherwise. + pub index: (u32, u32, Option), pub is_local: bool, /// The kind of definition this `DefId` points to. pub kind: crate::DefKind, } +#[cfg(feature = "rustc")] +impl DefIdContents { + pub fn make_def_id<'tcx, S: BaseState<'tcx>>(self, s: &S) -> DefId { + let contents = + s.with_global_cache(|cache| id_table::Node::new(self, &mut cache.id_table_session)); + DefId { contents } + } +} + #[cfg(feature = "rustc")] impl DefId { - pub fn to_rust_def_id(&self) -> RDefId { - let (krate, index) = self.index; + /// The rustc def_id corresponding to this item, if there is one. Promoted constants don't have + /// a rustc def_id. + pub fn as_rust_def_id(&self) -> Option { + let (_, _, promoted) = self.index; + match promoted { + None => Some(self.underlying_rust_def_id()), + Some(_) => None, + } + } + /// The def_id of this item or its parent if this is a promoted constant. + pub fn underlying_rust_def_id(&self) -> RDefId { + let (krate, index, _) = self.index; RDefId { krate: rustc_hir::def_id::CrateNum::from_u32(krate), index: rustc_hir::def_id::DefIndex::from_u32(index), } } + pub fn promoted_id(&self) -> Option { + let (_, _, promoted) = self.index; + promoted.map(|promoted| rustc_middle::mir::Promoted::from_u32(promoted.id)) + } /// Iterate over this element and its parents. pub fn ancestry(&self) -> impl Iterator { @@ -174,6 +212,31 @@ impl DefId { }, }) } + + /// Construct a hax `DefId` for the nth promoted constant of the current item. That `DefId` has + /// no corresponding rustc `DefId`. + pub fn make_promoted_child<'tcx, S: BaseState<'tcx>>( + &self, + s: &S, + promoted_id: PromotedId, + ) -> Self { + let mut path = self.path.clone(); + path.push(DisambiguatedDefPathItem { + data: DefPathItem::PromotedConst, + // Reuse the promoted id as disambiguator, like for inline consts. + disambiguator: promoted_id.id, + }); + let (krate, index, _) = self.index; + let contents = DefIdContents { + krate: self.krate.clone(), + path, + parent: Some(self.clone()), + is_local: self.is_local, + index: (krate, index, Some(promoted_id)), + kind: DefKind::PromotedConst, + }; + contents.make_def_id(s) + } } impl std::ops::Deref for DefId { @@ -197,7 +260,7 @@ impl std::fmt::Debug for DefId { impl std::fmt::Debug for DefId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { // Use the more legible rustc debug implementation. - write!(f, "{:?}", self.to_rust_def_id()) + write!(f, "{:?}", self.as_rust_def_id()) } } @@ -241,13 +304,12 @@ pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) index: ( rustc_hir::def_id::CrateNum::as_u32(def_id.krate), rustc_hir::def_id::DefIndex::as_u32(def_id.index), + None, ), is_local: def_id.is_local(), kind: get_def_kind(tcx, def_id).sinto(s), }; - let contents = - s.with_global_cache(|cache| id_table::Node::new(contents, &mut cache.id_table_session)); - DefId { contents } + contents.make_def_id(s) } #[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))] @@ -312,6 +374,8 @@ pub enum DefPathItem { Closure, Ctor, AnonConst, + #[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)] + PromotedConst, OpaqueTy, } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 2e3fb45ce..de99e1d38 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -159,22 +159,13 @@ pub mod mir_kinds { #[cfg(feature = "rustc")] pub use mir_kinds::IsMirKind; -#[derive_group(Serializers)] -#[derive(AdtInto, Clone, Debug, JsonSchema)] -#[args(<'tcx, S: BaseState<'tcx>>, from: rustc_middle::mir::Promoted, state: S as _s)] -pub struct PromotedId { - #[value(self.as_u32())] - pub id: u32, -} - /// Part of a MIR body that was promoted to be a constant. #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema)] pub struct PromotedConstant { - /// The `def_id` of the body this was extracted from. + /// The `def_id` of the constant. Note that rustc does not give a DefId to promoted constants, + /// but we do in hax. pub def_id: DefId, - /// The identifier for this sub-body. This is the contents of a `mir::Promoted` identifier. - pub promoted_id: PromotedId, /// The generics applied to the definition corresponding to `def_id`. pub args: Vec, /// The MIR for this sub-body. @@ -240,9 +231,14 @@ fn get_promoted_mir<'tcx, S: UnderOwnerState<'tcx>>( binder: (), thir: (), }; + // Construct a def_id for the promoted constant. + let def_id = { + let parent_def_id: DefId = def_id.sinto(s); + let promoted_id: PromotedId = promoted_id.sinto(s); + parent_def_id.make_promoted_child(s, promoted_id) + }; PromotedConstant { - def_id: def_id.sinto(s), - promoted_id: promoted_id.sinto(s), + def_id, args: uneval.args.sinto(s), mir: body.sinto(s), } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index b0600896a..a010cd807 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -80,7 +80,7 @@ impl DefId { match &self.kind { // These kinds cause `def_span` to panic. ForeignMod => rustc_span::DUMMY_SP, - _ => s.base().tcx.def_span(self.to_rust_def_id()), + _ => s.base().tcx.def_span(self.underlying_rust_def_id()), } .sinto(s) } @@ -91,13 +91,16 @@ impl DefId { Body: IsBody + TypeMappable, S: BaseState<'tcx>, { - let def_id = self.to_rust_def_id(); - if let Some(def) = s.with_item_cache(def_id, |cache| cache.full_def.get().cloned()) { - return def; + if let Some(def_id) = self.as_rust_def_id() { + if let Some(def) = s.with_item_cache(def_id, |cache| cache.full_def.get().cloned()) { + return def; + } + let def = Arc::new(translate_full_def(s, def_id)); + s.with_item_cache(def_id, |cache| cache.full_def.insert(def.clone())); + def + } else { + todo!("full_def for promoted constants") } - let def = Arc::new(translate_full_def(s, def_id)); - s.with_item_cache(def_id, |cache| cache.full_def.insert(def.clone())); - def } } @@ -501,13 +504,15 @@ impl FullDef { _ => vec![], }; // Add inherent impl items if any. - let tcx = s.base().tcx; - for impl_def_id in tcx.inherent_impls(self.def_id.to_rust_def_id()) { - children.extend( - tcx.associated_items(impl_def_id) - .in_definition_order() - .map(|assoc| (assoc.name, assoc.def_id).sinto(s)), - ); + if let Some(rust_def_id) = self.def_id.as_rust_def_id() { + let tcx = s.base().tcx; + for impl_def_id in tcx.inherent_impls(rust_def_id) { + children.extend( + tcx.associated_items(impl_def_id) + .in_definition_order() + .map(|assoc| (assoc.name, assoc.def_id).sinto(s)), + ); + } } children } diff --git a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap index b46940c46..de45cbda5 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-coq.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-coq.snap @@ -58,7 +58,7 @@ Class t_Trait `{v_Self : Type} : Type := Arguments t_Trait:clear implicits. Arguments t_Trait (_). -Instance t_Trait_373159623 : t_Trait ((t_Foo)) := +Instance t_Trait_257736684 : t_Trait ((t_Foo)) := { }. From ab9ccc81c98d92522516503720ede6b02612112a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 16:43:06 +0200 Subject: [PATCH 5/7] Generate a `FullDef` for promoted constants --- frontend/exporter/src/body.rs | 28 +++++ frontend/exporter/src/state.rs | 10 +- frontend/exporter/src/types/def_id.rs | 17 ++- frontend/exporter/src/types/mir.rs | 26 +++-- frontend/exporter/src/types/new/full_def.rs | 121 +++++++++++++++----- frontend/exporter/src/types/ty.rs | 7 ++ frontend/exporter/src/utils/type_map.rs | 9 ++ 7 files changed, 175 insertions(+), 43 deletions(-) diff --git a/frontend/exporter/src/body.rs b/frontend/exporter/src/body.rs index 654093ea9..83e6eac91 100644 --- a/frontend/exporter/src/body.rs +++ b/frontend/exporter/src/body.rs @@ -30,6 +30,14 @@ mod module { pub trait IsBody: Sized + Clone + 'static { fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self; + + /// Reuse a MIR body we already got. Panic if that's impossible. + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + _s: &S, + _body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + panic!("Can't convert MIR to the requested body type") + } } pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>( @@ -67,6 +75,12 @@ mod module { use super::*; impl IsBody for () { fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {} + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + _s: &S, + _body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + () + } } impl IsBody for ThirBody { fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self { @@ -106,6 +120,20 @@ mod module { }); mir.s_unwrap(s) } + fn from_mir<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + body: rustc_middle::mir::Body<'tcx>, + ) -> Self { + let body = Rc::new(body.clone()); + let s = &State { + base: s.base(), + owner_id: s.owner_id(), + mir: body.clone(), + binder: (), + thir: (), + }; + body.sinto(s) + } } } diff --git a/frontend/exporter/src/state.rs b/frontend/exporter/src/state.rs index 6f8e48d16..4bcc40d27 100644 --- a/frontend/exporter/src/state.rs +++ b/frontend/exporter/src/state.rs @@ -136,13 +136,21 @@ mod types { type Value = Arc>; } + /// Defines a mapping from types to types, for use with `TypeMap`. + pub struct PromotedFullDefsMapper {} + impl TypeMapper for PromotedFullDefsMapper { + type Value = HashMap>>; + } + /// Per-item cache #[derive(Default)] pub struct ItemCache<'tcx> { /// The translated `DefId`. pub def_id: Option, - /// The translated definitions, generic in the body. + /// The translated definitions, generic in the Body kind. pub full_def: TypeMap, + /// The Promoted constants of this body, if any. + pub promoteds: TypeMap, /// Cache the `Ty` translations. pub tys: HashMap, Ty>, /// Cache the trait resolution engine for each item. diff --git a/frontend/exporter/src/types/def_id.rs b/frontend/exporter/src/types/def_id.rs index c2bd1bf59..56ffc855d 100644 --- a/frontend/exporter/src/types/def_id.rs +++ b/frontend/exporter/src/types/def_id.rs @@ -84,6 +84,13 @@ pub struct PromotedId { pub id: u32, } +#[cfg(feature = "rustc")] +impl PromotedId { + pub fn as_rust_promoted_id(&self) -> rustc_middle::mir::Promoted { + rustc_middle::mir::Promoted::from_u32(self.id) + } +} + /// Reflects [`rustc_hir::def::DefKind`] #[derive_group(Serializers)] #[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))] @@ -190,9 +197,9 @@ impl DefId { index: rustc_hir::def_id::DefIndex::from_u32(index), } } - pub fn promoted_id(&self) -> Option { + pub fn promoted_id(&self) -> Option { let (_, _, promoted) = self.index; - promoted.map(|promoted| rustc_middle::mir::Promoted::from_u32(promoted.id)) + promoted } /// Iterate over this element and its parents. @@ -260,7 +267,11 @@ impl std::fmt::Debug for DefId { impl std::fmt::Debug for DefId { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { // Use the more legible rustc debug implementation. - write!(f, "{:?}", self.as_rust_def_id()) + write!(f, "{:?}", self.underlying_rust_def_id())?; + if let Some(promoted) = self.promoted_id() { + write!(f, "::promoted#{}", promoted.id)?; + } + Ok(()) } } diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index de99e1d38..54a8dd21d 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -206,14 +206,13 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto /// Retrieve the MIR for a promoted body. #[cfg(feature = "rustc")] -fn get_promoted_mir<'tcx, S: UnderOwnerState<'tcx>>( +pub(crate) fn get_promoted_mir<'tcx, S: BaseState<'tcx>>( s: &S, - uneval: mir::UnevaluatedConst<'tcx>, -) -> PromotedConstant { + def_id: RDefId, + promoted_id: mir::Promoted, +) -> mir::Body<'tcx> { let tcx = s.base().tcx; - let promoted_id = uneval.promoted.unwrap(); - let def_id = uneval.def; - let body = if let Some(local_def_id) = def_id.as_local() { + if let Some(local_def_id) = def_id.as_local() { let (_, promoteds) = tcx.mir_promoted(local_def_id); if !promoteds.is_stolen() { promoteds.borrow()[promoted_id].clone() @@ -222,7 +221,18 @@ fn get_promoted_mir<'tcx, S: UnderOwnerState<'tcx>>( } } else { tcx.promoted_mir(def_id)[promoted_id].clone() - }; + } +} + +/// Retrieve the MIR for a promoted body. +#[cfg(feature = "rustc")] +fn get_promoted_constant<'tcx, S: UnderOwnerState<'tcx>>( + s: &S, + uneval: mir::UnevaluatedConst<'tcx>, +) -> PromotedConstant { + let promoted_id = uneval.promoted.unwrap(); + let def_id = uneval.def; + let body = get_promoted_mir(s, def_id, promoted_id); let body = Rc::new(body); let s = &State { base: s.base(), @@ -274,7 +284,7 @@ fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( ); match ucv.promoted { Some(_) => { - let promoted = get_promoted_mir(s, ucv); + let promoted = get_promoted_constant(s, ucv); let evaluated = eval_mir_constant(s, konst).sinto(s); Promoted(promoted, evaluated) } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index a010cd807..d34d28c45 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -33,40 +33,82 @@ pub struct FullDef { } #[cfg(feature = "rustc")] -fn translate_full_def<'tcx, S, Body>(s: &S, def_id: RDefId) -> FullDef +fn translate_full_def<'tcx, S, Body>(s: &S, def_id: &DefId) -> FullDef where S: BaseState<'tcx>, Body: IsBody + TypeMappable, { let tcx = s.base().tcx; - let hax_def_id: DefId = def_id.sinto(s); - let def_kind = get_def_kind(tcx, def_id); - let kind = { - let state_with_id = with_owner_id(s.base(), (), (), def_id); - def_kind.sinto(&state_with_id) - }; + let rust_def_id = def_id.underlying_rust_def_id(); + let state_with_id = with_owner_id(s.base(), (), (), rust_def_id); + let source_span; + let attributes; + let visibility; + let lang_item; + let diagnostic_item; + let kind; + match def_id.promoted_id() { + None => { + let def_kind = get_def_kind(tcx, rust_def_id); + kind = def_kind.sinto(&state_with_id); + + source_span = rust_def_id.as_local().map(|ldid| tcx.source_span(ldid)); + attributes = get_def_attrs(tcx, rust_def_id, def_kind).sinto(s); + visibility = get_def_visibility(tcx, rust_def_id, def_kind); + lang_item = s + .base() + .tcx + .as_lang_item(rust_def_id) + .map(|litem| litem.name()) + .sinto(s); + diagnostic_item = tcx.get_diagnostic_name(rust_def_id).sinto(s); + } + + Some(promoted_id) => { + let parent_def = def_id.parent.as_ref().unwrap().full_def::<_, Body>(s); + let parent_param_env = parent_def.param_env().unwrap(); + let param_env = ParamEnv { + generics: TyGenerics { + parent: def_id.parent.clone(), + parent_count: parent_param_env.generics.count_total_params(), + params: vec![], + has_self: false, + has_late_bound_regions: None, + }, + predicates: GenericPredicates { predicates: vec![] }, + }; + let body = get_promoted_mir(s, rust_def_id, promoted_id.as_rust_promoted_id()); + let ty: Ty = body.local_decls[rustc_middle::mir::Local::ZERO] + .ty + .sinto(&state_with_id); + let body = Body::from_mir(&state_with_id, body); + kind = FullDefKind::PromotedConst { + param_env, + ty, + body, + }; + + source_span = None; + attributes = Default::default(); + visibility = Default::default(); + lang_item = Default::default(); + diagnostic_item = Default::default(); + } + } - let def_span = hax_def_id.def_span(s); - let source_span = def_id.as_local().map(|ldid| tcx.source_span(ldid)); let source_text = source_span .filter(|source_span| source_span.ctxt().is_root()) .and_then(|source_span| tcx.sess.source_map().span_to_snippet(source_span).ok()); - FullDef { - def_id: hax_def_id, - parent: tcx.opt_parent(def_id).sinto(s), - span: def_span, + def_id: def_id.clone(), + parent: def_id.parent.clone(), + span: def_id.def_span(s), source_span: source_span.sinto(s), source_text, - attributes: get_def_attrs(tcx, def_id, def_kind).sinto(s), - visibility: get_def_visibility(tcx, def_id, def_kind), - lang_item: s - .base() - .tcx - .as_lang_item(def_id) - .map(|litem| litem.name()) - .sinto(s), - diagnostic_item: tcx.get_diagnostic_name(def_id).sinto(s), + attributes, + visibility, + lang_item, + diagnostic_item, kind, } } @@ -91,16 +133,26 @@ impl DefId { Body: IsBody + TypeMappable, S: BaseState<'tcx>, { - if let Some(def_id) = self.as_rust_def_id() { - if let Some(def) = s.with_item_cache(def_id, |cache| cache.full_def.get().cloned()) { - return def; - } - let def = Arc::new(translate_full_def(s, def_id)); - s.with_item_cache(def_id, |cache| cache.full_def.insert(def.clone())); - def - } else { - todo!("full_def for promoted constants") + let rust_def_id = self.underlying_rust_def_id(); + if let Some(def) = s.with_item_cache(rust_def_id, |cache| match self.promoted_id() { + None => cache.full_def.get().cloned(), + Some(promoted_id) => cache.promoteds.or_default().get(&promoted_id).cloned(), + }) { + return def; } + let def = Arc::new(translate_full_def(s, self)); + s.with_item_cache(rust_def_id, |cache| match self.promoted_id() { + None => { + cache.full_def.insert(def.clone()); + } + Some(promoted_id) => { + cache + .promoteds + .or_default() + .insert(promoted_id, def.clone()); + } + }); + def } } @@ -332,6 +384,13 @@ pub enum FullDefKind { #[value(s.owner_id().as_local().map(|ldid| Body::body(ldid, s)))] body: Option, }, + /// A promoted constant, e.g. `&(1 + 2)` + #[disable_mapping] + PromotedConst { + param_env: ParamEnv, + ty: Ty, + body: Body, + }, Static { #[value(get_param_env(s, s.owner_id()))] param_env: ParamEnv, diff --git a/frontend/exporter/src/types/ty.rs b/frontend/exporter/src/types/ty.rs index b144f1b42..117bc73ba 100644 --- a/frontend/exporter/src/types/ty.rs +++ b/frontend/exporter/src/types/ty.rs @@ -647,6 +647,13 @@ pub struct TyGenerics { pub has_late_bound_regions: Option, } +#[cfg(feature = "rustc")] +impl TyGenerics { + pub(crate) fn count_total_params(&self) -> usize { + self.parent_count + self.params.len() + } +} + /// This type merges the information from /// `rustc_type_ir::AliasKind` and `ty::AliasTy` #[derive_group(Serializers)] diff --git a/frontend/exporter/src/utils/type_map.rs b/frontend/exporter/src/utils/type_map.rs index f7a3bc3a5..c7e1e0907 100644 --- a/frontend/exporter/src/utils/type_map.rs +++ b/frontend/exporter/src/utils/type_map.rs @@ -34,6 +34,15 @@ impl TypeMap { .map(|val: &mut Box| &mut **val) .and_then(|val: &mut dyn TypeMappable| (val as &mut dyn Any).downcast_mut()) } + pub fn or_default(&mut self) -> &mut M::Value + where + M::Value: Default, + { + if self.get::().is_none() { + self.insert::(Default::default()); + } + self.get_mut().unwrap() + } pub fn insert(&mut self, val: M::Value) -> Option>> { self.data From c94bbdb7882a45553ea6d39c6d4952ac73732834 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 24 Apr 2025 20:17:17 +0200 Subject: [PATCH 6/7] Rework `PromotedConstant` --- frontend/exporter/src/types/mir.rs | 83 +++++++-------------- frontend/exporter/src/types/new/full_def.rs | 2 +- 2 files changed, 26 insertions(+), 59 deletions(-) diff --git a/frontend/exporter/src/types/mir.rs b/frontend/exporter/src/types/mir.rs index 54a8dd21d..6af99486e 100644 --- a/frontend/exporter/src/types/mir.rs +++ b/frontend/exporter/src/types/mir.rs @@ -159,19 +159,6 @@ pub mod mir_kinds { #[cfg(feature = "rustc")] pub use mir_kinds::IsMirKind; -/// Part of a MIR body that was promoted to be a constant. -#[derive_group(Serializers)] -#[derive(Clone, Debug, JsonSchema)] -pub struct PromotedConstant { - /// The `def_id` of the constant. Note that rustc does not give a DefId to promoted constants, - /// but we do in hax. - pub def_id: DefId, - /// The generics applied to the definition corresponding to `def_id`. - pub args: Vec, - /// The MIR for this sub-body. - pub mir: MirBody<()>, -} - /// The contents of `Operand::Const`. #[derive_group(Serializers)] #[derive(Clone, Debug, JsonSchema)] @@ -186,14 +173,20 @@ pub struct ConstOperand { pub enum ConstOperandKind { /// An evaluated constant represented as an expression. Value(ConstantExpr), - /// A promoted constant, that may not be evaluatable because of generics. - Promoted(PromotedConstant, Option), + /// Part of a MIR body that was promoted to be a constant. May not be evaluatable because of + /// generics. + Promoted { + /// The `def_id` of the constant. Note that rustc does not give a DefId to promoted constants, + /// but we do in hax. + def_id: DefId, + /// The generics applied to the definition corresponding to `def_id`. + args: Vec, + impl_exprs: Vec, + }, } #[cfg(feature = "rustc")] -impl<'tcx, S: UnderOwnerState<'tcx>> SInto - for rustc_middle::mir::ConstOperand<'tcx> -{ +impl<'tcx, S: UnderOwnerState<'tcx>> SInto for mir::ConstOperand<'tcx> { fn sinto(&self, s: &S) -> ConstOperand { let kind = translate_mir_const(s, self.span, self.const_); ConstOperand { @@ -206,12 +199,11 @@ impl<'tcx, S: UnderOwnerState<'tcx>> SInto /// Retrieve the MIR for a promoted body. #[cfg(feature = "rustc")] -pub(crate) fn get_promoted_mir<'tcx, S: BaseState<'tcx>>( - s: &S, +pub fn get_promoted_mir<'tcx>( + tcx: ty::TyCtxt<'tcx>, def_id: RDefId, promoted_id: mir::Promoted, ) -> mir::Body<'tcx> { - let tcx = s.base().tcx; if let Some(local_def_id) = def_id.as_local() { let (_, promoteds) = tcx.mir_promoted(local_def_id); if !promoteds.is_stolen() { @@ -224,36 +216,6 @@ pub(crate) fn get_promoted_mir<'tcx, S: BaseState<'tcx>>( } } -/// Retrieve the MIR for a promoted body. -#[cfg(feature = "rustc")] -fn get_promoted_constant<'tcx, S: UnderOwnerState<'tcx>>( - s: &S, - uneval: mir::UnevaluatedConst<'tcx>, -) -> PromotedConstant { - let promoted_id = uneval.promoted.unwrap(); - let def_id = uneval.def; - let body = get_promoted_mir(s, def_id, promoted_id); - let body = Rc::new(body); - let s = &State { - base: s.base(), - owner_id: s.owner_id(), - mir: body.clone(), - binder: (), - thir: (), - }; - // Construct a def_id for the promoted constant. - let def_id = { - let parent_def_id: DefId = def_id.sinto(s); - let promoted_id: PromotedId = promoted_id.sinto(s); - parent_def_id.make_promoted_child(s, promoted_id) - }; - PromotedConstant { - def_id, - args: uneval.args.sinto(s), - mir: body.sinto(s), - } -} - #[cfg(feature = "rustc")] /// Translate a MIR constant. fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( @@ -283,10 +245,15 @@ fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( .unwrap_or_else(|| ucv.def.default_span(tcx)), ); match ucv.promoted { - Some(_) => { - let promoted = get_promoted_constant(s, ucv); - let evaluated = eval_mir_constant(s, konst).sinto(s); - Promoted(promoted, evaluated) + Some(promoted) => { + // Construct a def_id for the promoted constant. + let def_id = ucv.def.sinto(s).make_promoted_child(s, promoted.sinto(s)); + let impl_exprs = solve_item_required_traits(s, ucv.def, ucv.args); + Promoted { + def_id, + args: ucv.args.sinto(s), + impl_exprs, + } } None => Value(match translate_constant_reference(s, span, ucv.shrink()) { Some(val) => val, @@ -308,10 +275,10 @@ fn translate_mir_const<'tcx, S: UnderOwnerState<'tcx>>( impl<'tcx, S: UnderOwnerState<'tcx>> SInto for rustc_middle::mir::Const<'tcx> { fn sinto(&self, s: &S) -> ConstantExpr { match translate_mir_const(s, rustc_span::DUMMY_SP, *self) { - ConstOperandKind::Value(val) | ConstOperandKind::Promoted(_, Some(val)) => val, - ConstOperandKind::Promoted(body, None) => fatal!( + ConstOperandKind::Value(val) => val, + ConstOperandKind::Promoted { .. } => fatal!( s, "Cannot convert constant back to an expression"; - {body} + {self} ), } } diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index d34d28c45..0209aa9ea 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -77,7 +77,7 @@ where }, predicates: GenericPredicates { predicates: vec![] }, }; - let body = get_promoted_mir(s, rust_def_id, promoted_id.as_rust_promoted_id()); + let body = get_promoted_mir(tcx, rust_def_id, promoted_id.as_rust_promoted_id()); let ty: Ty = body.local_decls[rustc_middle::mir::Local::ZERO] .ty .sinto(&state_with_id); From 02070be5bfc59b1c794d379d55785bdb091953d9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 25 Apr 2025 08:52:02 +0200 Subject: [PATCH 7/7] Translate promoted source span --- frontend/exporter/src/types/new/full_def.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/frontend/exporter/src/types/new/full_def.rs b/frontend/exporter/src/types/new/full_def.rs index 0209aa9ea..7c627814e 100644 --- a/frontend/exporter/src/types/new/full_def.rs +++ b/frontend/exporter/src/types/new/full_def.rs @@ -78,6 +78,8 @@ where predicates: GenericPredicates { predicates: vec![] }, }; let body = get_promoted_mir(tcx, rust_def_id, promoted_id.as_rust_promoted_id()); + source_span = Some(body.span); + let ty: Ty = body.local_decls[rustc_middle::mir::Local::ZERO] .ty .sinto(&state_with_id); @@ -88,7 +90,7 @@ where body, }; - source_span = None; + // None of these make sense for a promoted constant. attributes = Default::default(); visibility = Default::default(); lang_item = Default::default();