flux_middle/
lib.rs

1//! This crate contains common type definitions that are used by other crates.
2#![feature(
3    associated_type_defaults,
4    box_patterns,
5    closure_track_caller,
6    if_let_guard,
7    map_try_insert,
8    min_specialization,
9    never_type,
10    rustc_private,
11    unwrap_infallible,
12    new_range_api
13)]
14
15extern crate rustc_abi;
16extern crate rustc_ast;
17extern crate rustc_data_structures;
18extern crate rustc_errors;
19extern crate rustc_hir;
20extern crate rustc_index;
21extern crate rustc_macros;
22extern crate rustc_middle;
23extern crate rustc_serialize;
24extern crate rustc_span;
25extern crate rustc_type_ir;
26
27extern crate self as flux_middle;
28
29pub mod big_int;
30pub mod cstore;
31pub mod def_id;
32pub mod fhir;
33pub mod global_env;
34pub mod metrics;
35pub mod pretty;
36pub mod queries;
37pub mod rty;
38mod sort_of;
39
40use std::sync::LazyLock;
41
42use flux_arc_interner::List;
43use flux_macros::fluent_messages;
44pub use flux_rustc_bridge::def_id_to_string;
45use flux_rustc_bridge::{
46    mir::{LocalDecls, PlaceElem},
47    ty::{self, GenericArgsExt},
48};
49use flux_syntax::surface::{self, NodeId};
50use global_env::GlobalEnv;
51use liquid_fixpoint::ThyFunc;
52use queries::QueryResult;
53use rty::VariantIdx;
54use rustc_abi::FieldIdx;
55use rustc_data_structures::{
56    fx::FxIndexMap,
57    unord::{UnordMap, UnordSet},
58};
59use rustc_hir::OwnerId;
60use rustc_macros::extension;
61use rustc_middle::ty::TyCtxt;
62use rustc_span::{
63    Symbol,
64    def_id::{DefId, LocalDefId},
65    symbol::Ident,
66};
67
68fluent_messages! { "../locales/en-US.ftl" }
69
70pub struct TheoryFunc {
71    pub name: Symbol,
72    pub sort: rty::PolyFuncSort,
73    pub itf: liquid_fixpoint::ThyFunc,
74}
75
76pub static THEORY_FUNCS: LazyLock<UnordMap<liquid_fixpoint::ThyFunc, TheoryFunc>> =
77    LazyLock::new(|| {
78        use rty::{BvSize, Sort::*};
79        liquid_fixpoint::ThyFunc::ALL
80            .into_iter()
81            .filter_map(|func| {
82                let func = TheoryFunc {
83                    name: Symbol::intern(name_of_thy_func(func)?),
84                    itf: func,
85                    sort: sort_of_thy_func(func)?,
86                };
87                Some(func)
88            })
89            .chain([
90                // we can't express these as function types so we add special case
91                TheoryFunc {
92                    name: Symbol::intern("bv_zero_extend_32_to_64"),
93                    itf: liquid_fixpoint::ThyFunc::BvZeroExtend(32),
94                    sort: rty::PolyFuncSort::new(
95                        List::empty(),
96                        rty::FuncSort::new(
97                            vec![BitVec(BvSize::Fixed(32))],
98                            BitVec(BvSize::Fixed(64)),
99                        ),
100                    ),
101                },
102                TheoryFunc {
103                    name: Symbol::intern("bv_sign_extend_32_to_64"),
104                    itf: liquid_fixpoint::ThyFunc::BvSignExtend(32),
105                    sort: rty::PolyFuncSort::new(
106                        List::empty(),
107                        rty::FuncSort::new(
108                            vec![BitVec(BvSize::Fixed(32))],
109                            BitVec(BvSize::Fixed(64)),
110                        ),
111                    ),
112                },
113            ])
114            .map(|func| (func.itf, func))
115            .collect()
116    });
117
118pub fn name_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<&'static str> {
119    let name = match func {
120        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
121        ThyFunc::StrLen => "str_len",
122        ThyFunc::StrConcat => "str_concat",
123        ThyFunc::StrPrefixOf => "str_prefix_of",
124        ThyFunc::StrSuffixOf => "str_suffix_of",
125        ThyFunc::StrContains => "str_contains",
126        ThyFunc::IntToBv8 => "bv_int_to_bv8",
127        ThyFunc::Bv8ToInt => "bv_bv8_to_int",
128        ThyFunc::IntToBv32 => "bv_int_to_bv32",
129        ThyFunc::Bv32ToInt => "bv_bv32_to_int",
130        ThyFunc::IntToBv64 => "bv_int_to_bv64",
131        ThyFunc::Bv64ToInt => "bv_bv64_to_int",
132        ThyFunc::BvUge => "bv_uge",
133        ThyFunc::BvSge => "bv_sge",
134        ThyFunc::BvUdiv => "bv_udiv",
135        ThyFunc::BvSdiv => "bv_sdiv",
136        ThyFunc::BvSrem => "bv_srem",
137        ThyFunc::BvUrem => "bv_urem",
138        ThyFunc::BvLshr => "bv_lshr",
139        ThyFunc::BvAshr => "bv_ashr",
140        ThyFunc::BvAnd => "bv_and",
141        ThyFunc::BvOr => "bv_or",
142        ThyFunc::BvXor => "bv_xor",
143        ThyFunc::BvNot => "bv_not",
144        ThyFunc::BvAdd => "bv_add",
145        ThyFunc::BvNeg => "bv_neg",
146        ThyFunc::BvSub => "bv_sub",
147        ThyFunc::BvMul => "bv_mul",
148        ThyFunc::BvShl => "bv_shl",
149        ThyFunc::BvUle => "bv_ule",
150        ThyFunc::BvSle => "bv_sle",
151        ThyFunc::BvUgt => "bv_ugt",
152        ThyFunc::BvSgt => "bv_sgt",
153        ThyFunc::BvUlt => "bv_ult",
154        ThyFunc::BvSlt => "bv_slt",
155        ThyFunc::SetEmpty => "set_empty",
156        ThyFunc::SetSng => "set_singleton",
157        ThyFunc::SetCup => "set_union",
158        ThyFunc::SetCap => "set_intersection",
159        ThyFunc::SetDif => "set_difference",
160        ThyFunc::SetSub => "set_subset",
161        ThyFunc::SetMem => "set_is_in",
162        ThyFunc::MapDefault => "map_default",
163        ThyFunc::MapSelect => "map_select",
164        ThyFunc::MapStore => "map_store",
165    };
166    Some(name)
167}
168
169fn sort_of_thy_func(func: liquid_fixpoint::ThyFunc) -> Option<rty::PolyFuncSort> {
170    use rty::{
171        BvSize, ParamSort,
172        Sort::{self, *},
173        SortCtor::*,
174        SortParamKind,
175    };
176    let param0 = ParamSort::from_u32(0);
177    let param1 = ParamSort::from_u32(1);
178    let bv_param0 = BvSize::Param(ParamSort::from_u32(0));
179
180    let sort = match func {
181        ThyFunc::BvZeroExtend(_) | ThyFunc::BvSignExtend(_) => return None,
182        ThyFunc::StrLen => {
183            // str -> int
184            rty::PolyFuncSort::new(List::empty(), rty::FuncSort::new(vec![rty::Sort::Str], Int))
185        }
186        ThyFunc::StrConcat => {
187            // (str, str) -> str
188            rty::PolyFuncSort::new(
189                List::empty(),
190                rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], rty::Sort::Str),
191            )
192        }
193        ThyFunc::StrPrefixOf | ThyFunc::StrSuffixOf | ThyFunc::StrContains => {
194            // (str, str) -> bool
195            rty::PolyFuncSort::new(
196                List::empty(),
197                rty::FuncSort::new(vec![rty::Sort::Str, rty::Sort::Str], Bool),
198            )
199        }
200        ThyFunc::IntToBv8 => {
201            // int -> BitVec<8>
202            rty::PolyFuncSort::new(
203                List::empty(),
204                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(8))),
205            )
206        }
207        ThyFunc::Bv8ToInt => {
208            // BitVec<8> -> int
209            rty::PolyFuncSort::new(
210                List::empty(),
211                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(8))], Int),
212            )
213        }
214        ThyFunc::IntToBv32 => {
215            // int -> BitVec<32>
216            rty::PolyFuncSort::new(
217                List::empty(),
218                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(32))),
219            )
220        }
221        ThyFunc::Bv32ToInt => {
222            // BitVec<32> -> int
223            rty::PolyFuncSort::new(
224                List::empty(),
225                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(32))], Int),
226            )
227        }
228        ThyFunc::IntToBv64 => {
229            // int -> BitVec<64>
230            rty::PolyFuncSort::new(
231                List::empty(),
232                rty::FuncSort::new(vec![rty::Sort::Int], BitVec(BvSize::Fixed(64))),
233            )
234        }
235        ThyFunc::Bv64ToInt => {
236            // BitVec<64> -> int
237            rty::PolyFuncSort::new(
238                List::empty(),
239                rty::FuncSort::new(vec![BitVec(BvSize::Fixed(64))], Int),
240            )
241        }
242        ThyFunc::BvUdiv
243        | ThyFunc::BvSdiv
244        | ThyFunc::BvSrem
245        | ThyFunc::BvUrem
246        | ThyFunc::BvLshr
247        | ThyFunc::BvAshr
248        | ThyFunc::BvAnd
249        | ThyFunc::BvOr
250        | ThyFunc::BvXor
251        | ThyFunc::BvAdd
252        | ThyFunc::BvSub
253        | ThyFunc::BvMul
254        | ThyFunc::BvShl => {
255            // ∀s. (BitVec<s>, BitVec<s>) -> BitVec<s>
256            rty::PolyFuncSort::new(
257                List::singleton(SortParamKind::BvSize),
258                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], BitVec(bv_param0)),
259            )
260        }
261        ThyFunc::BvNot | ThyFunc::BvNeg => {
262            // ∀s. BitVec<s> -> BitVec<s>
263            rty::PolyFuncSort::new(
264                List::singleton(SortParamKind::BvSize),
265                rty::FuncSort::new(vec![BitVec(bv_param0)], BitVec(bv_param0)),
266            )
267        }
268        ThyFunc::BvUgt
269        | ThyFunc::BvSgt
270        | ThyFunc::BvUlt
271        | ThyFunc::BvSlt
272        | ThyFunc::BvSle
273        | ThyFunc::BvUge
274        | ThyFunc::BvSge
275        | ThyFunc::BvUle => {
276            // ∀s. (BitVec<s>, BitVec<s>) -> bool
277            rty::PolyFuncSort::new(
278                List::singleton(SortParamKind::BvSize),
279                rty::FuncSort::new(vec![BitVec(bv_param0), BitVec(bv_param0)], Bool),
280            )
281        }
282        ThyFunc::SetEmpty => {
283            // ∀s. int -> Set<S> why does this take an int?
284            rty::PolyFuncSort::new(
285                List::singleton(SortParamKind::Sort),
286                rty::FuncSort::new(vec![Int], Sort::app(Set, List::singleton(Var(param0)))),
287            )
288        }
289        ThyFunc::SetSng => {
290            // ∀s. s -> Set<S>
291            rty::PolyFuncSort::new(
292                List::singleton(SortParamKind::Sort),
293                rty::FuncSort::new(vec![Var(param0)], Sort::app(Set, List::singleton(Var(param0)))),
294            )
295        }
296        ThyFunc::SetCup | ThyFunc::SetCap | ThyFunc::SetDif => {
297            // ∀s. (Set<S>, Set<S>) -> Set<S>
298            rty::PolyFuncSort::new(
299                List::singleton(SortParamKind::Sort),
300                rty::FuncSort::new(
301                    vec![
302                        Sort::app(Set, List::singleton(Var(param0))),
303                        Sort::app(Set, List::singleton(Var(param0))),
304                    ],
305                    Sort::app(Set, List::singleton(Var(param0))),
306                ),
307            )
308        }
309        ThyFunc::SetMem => {
310            // ∀s. (s, Set<S>) -> bool
311            rty::PolyFuncSort::new(
312                List::singleton(SortParamKind::Sort),
313                rty::FuncSort::new(
314                    vec![Var(param0), Sort::app(Set, List::singleton(Var(param0)))],
315                    Bool,
316                ),
317            )
318        }
319        ThyFunc::SetSub => {
320            // ∀s. (Set<s>, Set<s>) -> bool
321            rty::PolyFuncSort::new(
322                List::singleton(SortParamKind::Sort),
323                rty::FuncSort::new(
324                    vec![
325                        Sort::app(Set, List::singleton(Var(param0))),
326                        Sort::app(Set, List::singleton(Var(param0))),
327                    ],
328                    Bool,
329                ),
330            )
331        }
332
333        ThyFunc::MapDefault => {
334            // ∀k,v. v -> Map<k,v>
335            rty::PolyFuncSort::new(
336                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
337                rty::FuncSort::new(
338                    vec![Var(param1)],
339                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
340                ),
341            )
342        }
343        ThyFunc::MapSelect => {
344            // ∀k,v. (Map<k,v>, k) -> v
345            rty::PolyFuncSort::new(
346                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
347                rty::FuncSort::new(
348                    vec![Sort::app(Map, List::from_arr([Var(param0), Var(param1)])), Var(param0)],
349                    Var(param1),
350                ),
351            )
352        }
353        ThyFunc::MapStore => {
354            // ∀k,v. (Map<k,v>, k, v) -> Map<k, v>
355            rty::PolyFuncSort::new(
356                List::from_arr([SortParamKind::Sort, SortParamKind::Sort]),
357                rty::FuncSort::new(
358                    vec![
359                        Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
360                        Var(param0),
361                        Var(param1),
362                    ],
363                    Sort::app(Map, List::from_arr([Var(param0), Var(param1)])),
364                ),
365            )
366        }
367    };
368    Some(sort)
369}
370
371#[derive(Default)]
372pub struct Specs {
373    items: UnordMap<OwnerId, surface::Item>,
374    trait_items: UnordMap<OwnerId, surface::TraitItemFn>,
375    impl_items: UnordMap<OwnerId, surface::ImplItemFn>,
376    pub flux_items_by_parent: FxIndexMap<OwnerId, Vec<surface::FluxItem>>,
377    /// Set of dummy items generated by the extern spec macro we must completely ignore. This is
378    /// not the same as [ignored items] because, for ignored items, we still need to return errors
379    /// for queries and handle them gracefully in order to report them at the use it.
380    ///
381    /// If an item is in this set, all its descendants are also consider dummy (but they may not be
382    /// in the set).
383    ///
384    /// [ignored items]: Specs::ignores
385    dummy_extern: UnordSet<LocalDefId>,
386    extern_id_to_local_id: UnordMap<DefId, LocalDefId>,
387    local_id_to_extern_id: UnordMap<LocalDefId, DefId>,
388}
389
390impl Specs {
391    pub fn insert_extern_spec_id_mapping(
392        &mut self,
393        local_id: LocalDefId,
394        extern_id: DefId,
395    ) -> Result<(), ExternSpecMappingErr> {
396        #[expect(
397            clippy::disallowed_methods,
398            reason = "we are inserting the extern spec mapping and we want to ensure it doesn't point to a local item"
399        )]
400        if let Some(local) = extern_id.as_local() {
401            return Err(ExternSpecMappingErr::IsLocal(local));
402        }
403        if let Err(err) = self.extern_id_to_local_id.try_insert(extern_id, local_id) {
404            return Err(ExternSpecMappingErr::Dup(*err.entry.get()));
405        }
406        self.local_id_to_extern_id.insert(local_id, extern_id);
407        Ok(())
408    }
409
410    pub fn insert_dummy(&mut self, def_id: LocalDefId) {
411        self.dummy_extern.insert(def_id);
412    }
413
414    pub fn get_item(&self, owner_id: OwnerId) -> Option<&surface::Item> {
415        self.items.get(&owner_id)
416    }
417
418    pub fn insert_item(&mut self, owner_id: OwnerId, item: surface::Item) -> Option<surface::Item> {
419        if let Some(old) = self.items.insert(owner_id, item) {
420            return Some(old);
421        }
422        None
423    }
424
425    pub fn get_trait_item(&self, owner_id: OwnerId) -> Option<&surface::TraitItemFn> {
426        self.trait_items.get(&owner_id)
427    }
428
429    pub fn insert_trait_item(
430        &mut self,
431        owner_id: OwnerId,
432        trait_item: surface::TraitItemFn,
433    ) -> Option<surface::TraitItemFn> {
434        if let Some(old) = self.trait_items.insert(owner_id, trait_item) {
435            return Some(old);
436        }
437        None
438    }
439
440    pub fn get_impl_item(&self, owner_id: OwnerId) -> Option<&surface::ImplItemFn> {
441        self.impl_items.get(&owner_id)
442    }
443
444    pub fn insert_impl_item(
445        &mut self,
446        owner_id: OwnerId,
447        impl_item: surface::ImplItemFn,
448    ) -> Option<surface::ImplItemFn> {
449        if let Some(old) = self.impl_items.insert(owner_id, impl_item) {
450            return Some(old);
451        }
452        None
453    }
454}
455
456/// Represents errors that can occur when inserting a mapping between a `LocalDefId` and a `DefId`
457/// for an extern spec.
458pub enum ExternSpecMappingErr {
459    /// Indicates that the [`DefId`] we are trying to add extern specs to is actually local. Returns
460    /// the [`DefId`] as a [`LocalDefId`].
461    IsLocal(LocalDefId),
462
463    /// Indicates that there is an existing extern spec for the given extern id. Returns the existing
464    /// `LocalDefId` that maps to the extern id.
465    ///
466    /// NOTE: This currently only considers extern specs defined in the local crate. There could still
467    /// be duplicates if an extern spec is imported from an external crate. In such cases, the local
468    /// extern spec takes precedence. Probably, we should at least warn about this, but it's a bit
469    /// tricky because we need to look at the crate metadata which we don't have handy when
470    /// collecting specs.
471    Dup(LocalDefId),
472}
473
474#[derive(Default)]
475pub struct ResolverOutput {
476    pub path_res_map: UnordMap<NodeId, fhir::PartialRes>,
477    /// Resolution of explicitly and implicitly scoped parameters. The [`fhir::ParamId`] is unique
478    /// per item. The [`NodeId`] used as the key corresponds to the node introducing the parameter.
479    /// When explicit, this is the id of the [`surface::GenericArg`] or [`surface::RefineParam`],
480    /// when implicit, this is the id of the [`surface::RefineArg::Bind`] or [`surface::FnInput`].
481    pub param_res_map: UnordMap<NodeId, (fhir::ParamId, fhir::ParamKind)>,
482    /// List of implicitly scoped params defined in a scope. The [`NodeId`] used as key is the id of
483    /// the node introducing the scope, e.g., [`surface::FnSig`], [`surface::FnOutput`], or
484    /// [`surface::VariantDef`]. The [`NodeId`]s in the vectors are keys in [`Self::param_res_map`].
485    pub implicit_params: UnordMap<NodeId, Vec<(Ident, NodeId)>>,
486    pub sort_path_res_map: UnordMap<NodeId, fhir::SortRes>,
487    pub expr_path_res_map: UnordMap<NodeId, fhir::PartialRes<fhir::ParamId>>,
488    /// The resolved list of local qualifiers per function.
489    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
490    pub qualifier_res_map: UnordMap<NodeId, Vec<def_id::FluxLocalDefId>>,
491    /// The resolved list of local reveals per function
492    /// The [`NodeId`] corresponds to the [`surface::FnSpec`].
493    pub reveal_res_map: UnordMap<NodeId, Vec<def_id::FluxDefId>>,
494}
495
496#[extension(pub trait PlaceExt)]
497impl flux_rustc_bridge::mir::Place {
498    fn ty(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<PlaceTy> {
499        self.projection
500            .iter()
501            .try_fold(PlaceTy::from_ty(local_decls[self.local].ty.clone()), |place_ty, elem| {
502                place_ty.projection_ty(genv, *elem)
503            })
504    }
505
506    fn behind_raw_ptr(&self, genv: GlobalEnv, local_decls: &LocalDecls) -> QueryResult<bool> {
507        let mut place_ty = PlaceTy::from_ty(local_decls[self.local].ty.clone());
508        for elem in &self.projection {
509            if let (PlaceElem::Deref, ty::TyKind::RawPtr(..)) = (elem, place_ty.ty.kind()) {
510                return Ok(true);
511            }
512            place_ty = place_ty.projection_ty(genv, *elem)?;
513        }
514        Ok(false)
515    }
516}
517
518#[derive(Debug)]
519pub struct PlaceTy {
520    pub ty: ty::Ty,
521    /// Downcast to a particular variant of an enum or a generator, if included.
522    pub variant_index: Option<VariantIdx>,
523}
524
525impl PlaceTy {
526    fn from_ty(ty: ty::Ty) -> PlaceTy {
527        PlaceTy { ty, variant_index: None }
528    }
529
530    fn projection_ty(&self, genv: GlobalEnv, elem: PlaceElem) -> QueryResult<PlaceTy> {
531        if self.variant_index.is_some() && !matches!(elem, PlaceElem::Field(..)) {
532            Err(query_bug!("cannot use non field projection on downcasted place"))?;
533        }
534        let place_ty = match elem {
535            PlaceElem::Deref => PlaceTy::from_ty(self.ty.deref()),
536            PlaceElem::Field(fld) => PlaceTy::from_ty(self.field_ty(genv, fld)?),
537            PlaceElem::Downcast(_, variant_idx) => {
538                PlaceTy { ty: self.ty.clone(), variant_index: Some(variant_idx) }
539            }
540            PlaceElem::Index(_) | PlaceElem::ConstantIndex { .. } => {
541                if let ty::TyKind::Array(ty, _) | ty::TyKind::Slice(ty) = self.ty.kind() {
542                    PlaceTy::from_ty(ty.clone())
543                } else {
544                    return Err(query_bug!("cannot use non field projection on downcasted place"));
545                }
546            }
547        };
548        Ok(place_ty)
549    }
550
551    fn field_ty(&self, genv: GlobalEnv, f: FieldIdx) -> QueryResult<ty::Ty> {
552        match self.ty.kind() {
553            ty::TyKind::Adt(adt_def, args) => {
554                let variant_def = match self.variant_index {
555                    None => adt_def.non_enum_variant(),
556                    Some(variant_index) => {
557                        assert!(adt_def.is_enum());
558                        adt_def.variant(variant_index)
559                    }
560                };
561                let field_def = &variant_def.fields[f];
562                let ty = genv.lower_type_of(field_def.did)?;
563                Ok(ty.subst(args))
564            }
565            ty::TyKind::Tuple(tys) => Ok(tys[f.index()].clone()),
566            ty::TyKind::Closure(_, args) => Ok(args.as_closure().upvar_tys()[f.index()].clone()),
567            _ => Err(query_bug!("extracting field of non-tuple non-adt non-closure: {self:?}")),
568        }
569    }
570}
571
572/// The different reasons we issue fixpoint queries. This is used to dissambiguate queries that
573/// are issued for the same item.
574///
575/// NOTE: This is defined here because it's also used in [`timings`]
576#[derive(Debug, Hash, Clone, Copy)]
577pub enum FixpointQueryKind {
578    /// Query issued when checking an impl method is a subtype of the trait
579    Impl,
580    /// Query issued to check the body of a function
581    Body,
582    /// Query issued to check an (enum) invariant is implied by the type definition
583    Invariant,
584}
585
586impl FixpointQueryKind {
587    pub fn ext(self) -> &'static str {
588        match self {
589            FixpointQueryKind::Impl => "sub.fluxc",
590            FixpointQueryKind::Body => "fluxc",
591            FixpointQueryKind::Invariant => "fluxc",
592        }
593    }
594
595    /// A string that uniquely identifies a query given an item `DefId`
596    pub fn task_key(self, tcx: TyCtxt, def_id: DefId) -> String {
597        format!("{}###{:?}", tcx.def_path_str(def_id), self)
598    }
599}