Skip to content

Commit 0275a2b

Browse files
NadrierilNadrieril
authored
Merge pull request #1420 from Nadrieril/promoted-defid
Add a fake `DefId` for promoted constants
2 parents fc2599e + 02070be commit 0275a2b

File tree

11 files changed

+325
-168
lines changed

11 files changed

+325
-168
lines changed

‎engine/lib/concrete_ident/concrete_ident_view.ml

+4-4
Original file line numberDiff line numberDiff line change
@@ -128,12 +128,12 @@ let rec poly :
128128
(match List.last_exn (Explicit_def_id.to_def_id did).path with
129129
| { data = GlobalAsm; disambiguator } -> into_d did disambiguator
130130
| _ -> broken_invariant "last path chunk to be GlobalAsm" did)
131-
| TyParam | ConstParam | InlineConst | LifetimeParam | Closure
132-
| SyntheticCoroutineBody ->
131+
| TyParam | ConstParam | InlineConst | PromotedConst | LifetimeParam
132+
| Closure | SyntheticCoroutineBody ->
133133
(* It should be impossible for such items to ever be referenced by anyting in hax. *)
134134
broken_invariant
135-
"non (TyParam | ConstParam | InlineConst | LifetimeParam | Closure | \
136-
SyntheticCoroutineBody) identifier"
135+
"non (TyParam | ConstParam | InlineConst | PromotedConst | \
136+
LifetimeParam | Closure | SyntheticCoroutineBody) identifier"
137137
did
138138
in
139139
result

‎engine/names/extract/build.rs

+1
Original file line numberDiff line numberDiff line change
@@ -67,6 +67,7 @@ fn def_path_item_to_str(path_item: DefPathItem) -> String {
6767
DefPathItem::Closure => "Closure".into(),
6868
DefPathItem::Ctor => "Ctor".into(),
6969
DefPathItem::AnonConst => "AnonConst".into(),
70+
DefPathItem::PromotedConst => "PromotedConst".into(),
7071
DefPathItem::TypeNs(None) | DefPathItem::OpaqueTy => "OpaqueTy".into(),
7172
}
7273
}

‎engine/utils/ocaml_of_json_schema/ocaml_of_json_schema.js

+1-1
Original file line numberDiff line numberDiff line change
@@ -364,7 +364,7 @@ let export_record = (fields, path, name) => {
364364
let record_expression = fields.map(([field, type, _doc], i) => {
365365
if (field == 'index' && name == 'def_id_contents') {
366366
// This is a hack to always parse Rust DefId indexes to `(0, 0)`
367-
return 'index = Base.Int64.(zero, zero)';
367+
return 'index = Base.Int64.(zero, zero, None)';
368368
}
369369
let p = [...path, 'field_' + field];
370370
let sub = mk_match('x', ocaml_arms_of_type_expr(type, p), p);

‎frontend/exporter/src/body.rs

+28
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,14 @@ mod module {
3030

3131
pub trait IsBody: Sized + Clone + 'static {
3232
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self;
33+
34+
/// Reuse a MIR body we already got. Panic if that's impossible.
35+
fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
36+
_s: &S,
37+
_body: rustc_middle::mir::Body<'tcx>,
38+
) -> Self {
39+
panic!("Can't convert MIR to the requested body type")
40+
}
3341
}
3442

3543
pub fn make_fn_def<'tcx, Body: IsBody, S: UnderOwnerState<'tcx>>(
@@ -67,6 +75,12 @@ mod module {
6775
use super::*;
6876
impl IsBody for () {
6977
fn body<'tcx, S: UnderOwnerState<'tcx>>(_did: RLocalDefId, _s: &S) -> Self {}
78+
fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
79+
_s: &S,
80+
_body: rustc_middle::mir::Body<'tcx>,
81+
) -> Self {
82+
()
83+
}
7084
}
7185
impl IsBody for ThirBody {
7286
fn body<'tcx, S: UnderOwnerState<'tcx>>(did: RLocalDefId, s: &S) -> Self {
@@ -106,6 +120,20 @@ mod module {
106120
});
107121
mir.s_unwrap(s)
108122
}
123+
fn from_mir<'tcx, S: UnderOwnerState<'tcx>>(
124+
s: &S,
125+
body: rustc_middle::mir::Body<'tcx>,
126+
) -> Self {
127+
let body = Rc::new(body.clone());
128+
let s = &State {
129+
base: s.base(),
130+
owner_id: s.owner_id(),
131+
mir: body.clone(),
132+
binder: (),
133+
thir: (),
134+
};
135+
body.sinto(s)
136+
}
109137
}
110138
}
111139

‎frontend/exporter/src/state.rs

+9-1
Original file line numberDiff line numberDiff line change
@@ -136,13 +136,21 @@ mod types {
136136
type Value<Body: TypeMappable> = Arc<FullDef<Body>>;
137137
}
138138

139+
/// Defines a mapping from types to types, for use with `TypeMap`.
140+
pub struct PromotedFullDefsMapper {}
141+
impl TypeMapper for PromotedFullDefsMapper {
142+
type Value<Body: TypeMappable> = HashMap<PromotedId, Arc<FullDef<Body>>>;
143+
}
144+
139145
/// Per-item cache
140146
#[derive(Default)]
141147
pub struct ItemCache<'tcx> {
142148
/// The translated `DefId`.
143149
pub def_id: Option<DefId>,
144-
/// The translated definitions, generic in the body.
150+
/// The translated definitions, generic in the Body kind.
145151
pub full_def: TypeMap<FullDefMapper>,
152+
/// The Promoted constants of this body, if any.
153+
pub promoteds: TypeMap<PromotedFullDefsMapper>,
146154
/// Cache the `Ty` translations.
147155
pub tys: HashMap<ty::Ty<'tcx>, Ty>,
148156
/// Cache the trait resolution engine for each item.

‎frontend/exporter/src/types/def_id.rs

+105-33
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ use crate::prelude::*;
1818
use crate::{AdtInto, JsonSchema};
1919

2020
#[cfg(feature = "rustc")]
21-
use {rustc_hir as hir, rustc_span::def_id::DefId as RDefId};
21+
use {rustc_hir as hir, rustc_hir::def_id::DefId as RDefId, rustc_middle::ty};
2222

2323
pub type Symbol = String;
2424

@@ -72,10 +72,29 @@ pub enum MacroKind {
7272
Derive,
7373
}
7474

75+
/// The id of a promoted MIR constant.
76+
///
77+
/// Reflects [`rustc_middle::mir::Promoted`].
78+
#[derive_group(Serializers)]
79+
#[derive(Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
80+
#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))]
81+
#[cfg_attr(not(feature = "extract_names_mode"), args(<S>, from: rustc_middle::mir::Promoted, state: S as _s))]
82+
pub struct PromotedId {
83+
#[cfg_attr(not(feature = "extract_names_mode"), value(self.as_u32()))]
84+
pub id: u32,
85+
}
86+
87+
#[cfg(feature = "rustc")]
88+
impl PromotedId {
89+
pub fn as_rust_promoted_id(&self) -> rustc_middle::mir::Promoted {
90+
rustc_middle::mir::Promoted::from_u32(self.id)
91+
}
92+
}
93+
7594
/// Reflects [`rustc_hir::def::DefKind`]
7695
#[derive_group(Serializers)]
7796
#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema, AdtInto))]
78-
#[cfg_attr(not(feature = "extract_names_mode"),args(<S>, from: rustc_hir::def::DefKind, state: S as tcx))]
97+
#[cfg_attr(not(feature = "extract_names_mode"), args(<S>, from: rustc_hir::def::DefKind, state: S as tcx))]
7998
#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
8099
pub enum DefKind {
81100
Mod,
@@ -106,6 +125,9 @@ pub enum DefKind {
106125
ForeignMod,
107126
AnonConst,
108127
InlineConst,
128+
#[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)]
129+
/// Added by hax: promoted constants don't have def_ids in rustc but they do in hax.
130+
PromotedConst,
109131
OpaqueTy,
110132
Field,
111133
LifetimeParam,
@@ -117,7 +139,8 @@ pub enum DefKind {
117139
SyntheticCoroutineBody,
118140
}
119141

120-
/// Reflects [`rustc_hir::def_id::DefId`]
142+
/// Reflects [`rustc_hir::def_id::DefId`], augmented to also give ids to promoted constants (which
143+
/// have their own ad-hoc numbering scheme in rustc for now).
121144
#[derive_group(Serializers)]
122145
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord)]
123146
#[cfg_attr(not(feature = "extract_names_mode"), derive(JsonSchema))]
@@ -132,30 +155,52 @@ pub struct DefIdContents {
132155
pub krate: String,
133156
pub path: Vec<DisambiguatedDefPathItem>,
134157
pub parent: Option<DefId>,
135-
/// Rustc's `CrateNum` and `DefIndex` raw indexes. This can be
136-
/// useful if one needs to convert a [`DefId`] into a
137-
/// [`rustc_hir::def_id::DefId`]; there is a `From` instance for
138-
/// that purpose.
158+
/// Stores rustc's `CrateNum`, `DefIndex` and `Promoted` raw indices. This can be useful if one
159+
/// needs to convert a [`DefId`] into a [`rustc_hir::def_id::DefId`]. If the promoted id is
160+
/// `Some`, then this `DefId` indicates the nth promoted constant associated with the item,
161+
/// which doesn't have a real `rustc::DefId`.
139162
///
140-
/// **Warning: this `index` field might not be safe to use**. They are
141-
/// valid only for one Rustc sesssion. Please do not rely on those
142-
/// indexes unless you cannot do otherwise.
143-
pub index: (u32, u32),
163+
/// **Warning: this `index` field might not be safe to use**. They are valid only for one Rustc
164+
/// sesssion. Please do not rely on those indices unless you cannot do otherwise.
165+
pub index: (u32, u32, Option<PromotedId>),
144166
pub is_local: bool,
145167

146168
/// The kind of definition this `DefId` points to.
147169
pub kind: crate::DefKind,
148170
}
149171

172+
#[cfg(feature = "rustc")]
173+
impl DefIdContents {
174+
pub fn make_def_id<'tcx, S: BaseState<'tcx>>(self, s: &S) -> DefId {
175+
let contents =
176+
s.with_global_cache(|cache| id_table::Node::new(self, &mut cache.id_table_session));
177+
DefId { contents }
178+
}
179+
}
180+
150181
#[cfg(feature = "rustc")]
151182
impl DefId {
152-
pub fn to_rust_def_id(&self) -> RDefId {
153-
let (krate, index) = self.index;
183+
/// The rustc def_id corresponding to this item, if there is one. Promoted constants don't have
184+
/// a rustc def_id.
185+
pub fn as_rust_def_id(&self) -> Option<RDefId> {
186+
let (_, _, promoted) = self.index;
187+
match promoted {
188+
None => Some(self.underlying_rust_def_id()),
189+
Some(_) => None,
190+
}
191+
}
192+
/// The def_id of this item or its parent if this is a promoted constant.
193+
pub fn underlying_rust_def_id(&self) -> RDefId {
194+
let (krate, index, _) = self.index;
154195
RDefId {
155196
krate: rustc_hir::def_id::CrateNum::from_u32(krate),
156197
index: rustc_hir::def_id::DefIndex::from_u32(index),
157198
}
158199
}
200+
pub fn promoted_id(&self) -> Option<PromotedId> {
201+
let (_, _, promoted) = self.index;
202+
promoted
203+
}
159204

160205
/// Iterate over this element and its parents.
161206
pub fn ancestry(&self) -> impl Iterator<Item = &Self> {
@@ -174,6 +219,31 @@ impl DefId {
174219
},
175220
})
176221
}
222+
223+
/// Construct a hax `DefId` for the nth promoted constant of the current item. That `DefId` has
224+
/// no corresponding rustc `DefId`.
225+
pub fn make_promoted_child<'tcx, S: BaseState<'tcx>>(
226+
&self,
227+
s: &S,
228+
promoted_id: PromotedId,
229+
) -> Self {
230+
let mut path = self.path.clone();
231+
path.push(DisambiguatedDefPathItem {
232+
data: DefPathItem::PromotedConst,
233+
// Reuse the promoted id as disambiguator, like for inline consts.
234+
disambiguator: promoted_id.id,
235+
});
236+
let (krate, index, _) = self.index;
237+
let contents = DefIdContents {
238+
krate: self.krate.clone(),
239+
path,
240+
parent: Some(self.clone()),
241+
is_local: self.is_local,
242+
index: (krate, index, Some(promoted_id)),
243+
kind: DefKind::PromotedConst,
244+
};
245+
contents.make_def_id(s)
246+
}
177247
}
178248

179249
impl std::ops::Deref for DefId {
@@ -197,7 +267,11 @@ impl std::fmt::Debug for DefId {
197267
impl std::fmt::Debug for DefId {
198268
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
199269
// Use the more legible rustc debug implementation.
200-
write!(f, "{:?}", rustc_span::def_id::DefId::from(self))
270+
write!(f, "{:?}", self.underlying_rust_def_id())?;
271+
if let Some(promoted) = self.promoted_id() {
272+
write!(f, "::promoted#{}", promoted.id)?;
273+
}
274+
Ok(())
201275
}
202276
}
203277

@@ -210,6 +284,18 @@ impl std::hash::Hash for DefId {
210284
}
211285
}
212286

287+
/// Gets the kind of the definition. Can't use `def_kind` directly because this crashes on the
288+
/// crate root.
289+
#[cfg(feature = "rustc")]
290+
pub(crate) fn get_def_kind<'tcx>(tcx: ty::TyCtxt<'tcx>, def_id: RDefId) -> hir::def::DefKind {
291+
if def_id == rustc_span::def_id::CRATE_DEF_ID.to_def_id() {
292+
// Horrible hack: without this, `def_kind` crashes on the crate root. Presumably some table
293+
// isn't properly initialized otherwise.
294+
let _ = tcx.def_span(def_id);
295+
};
296+
tcx.def_kind(def_id)
297+
}
298+
213299
#[cfg(feature = "rustc")]
214300
pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId) -> DefId {
215301
let tcx = s.base().tcx;
@@ -229,13 +315,12 @@ pub(crate) fn translate_def_id<'tcx, S: BaseState<'tcx>>(s: &S, def_id: RDefId)
229315
index: (
230316
rustc_hir::def_id::CrateNum::as_u32(def_id.krate),
231317
rustc_hir::def_id::DefIndex::as_u32(def_id.index),
318+
None,
232319
),
233320
is_local: def_id.is_local(),
234-
kind: tcx.def_kind(def_id).sinto(s),
321+
kind: get_def_kind(tcx, def_id).sinto(s),
235322
};
236-
let contents =
237-
s.with_global_cache(|cache| id_table::Node::new(contents, &mut cache.id_table_session));
238-
DefId { contents }
323+
contents.make_def_id(s)
239324
}
240325

241326
#[cfg(all(not(feature = "extract_names_mode"), feature = "rustc"))]
@@ -250,21 +335,6 @@ impl<'s, S: BaseState<'s>> SInto<S, DefId> for RDefId {
250335
}
251336
}
252337

253-
#[cfg(feature = "rustc")]
254-
impl From<&DefId> for RDefId {
255-
fn from<'tcx>(def_id: &DefId) -> Self {
256-
def_id.to_rust_def_id()
257-
}
258-
}
259-
260-
// Impl to be able to use hax's `DefId` for many rustc queries.
261-
#[cfg(feature = "rustc")]
262-
impl rustc_middle::query::IntoQueryParam<RDefId> for &DefId {
263-
fn into_query_param(self) -> RDefId {
264-
self.into()
265-
}
266-
}
267-
268338
#[cfg(not(feature = "extract_names_mode"))]
269339
pub type Path = Vec<String>;
270340

@@ -315,6 +385,8 @@ pub enum DefPathItem {
315385
Closure,
316386
Ctor,
317387
AnonConst,
388+
#[cfg_attr(not(feature = "extract_names_mode"), disable_mapping)]
389+
PromotedConst,
318390
OpaqueTy,
319391
}
320392

0 commit comments

Comments
 (0)