charon_driver/translate/
translate_crate.rs

1use super::translate_ctx::*;
2use charon_lib::ast::*;
3use charon_lib::options::{CliOpts, TranslateOptions};
4use charon_lib::transform::TransformCtx;
5use hax::FullDefKind;
6use hax_frontend_exporter::{self as hax, SInto};
7use itertools::Itertools;
8use macros::VariantIndexArity;
9use rustc_middle::ty::TyCtxt;
10use std::cell::RefCell;
11use std::path::PathBuf;
12
13/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
14/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
15/// `FunDecl` one (for its initializer function).
16#[derive(Clone, Debug, PartialEq, Eq, Hash, VariantIndexArity)]
17pub enum TransItemSource {
18    Global(hax::DefId),
19    TraitDecl(hax::DefId),
20    TraitImpl(hax::DefId),
21    Fun(hax::DefId),
22    Type(hax::DefId),
23    /// An impl of the appropriate `Fn*` trait for the given closure type.
24    ClosureTraitImpl(hax::DefId, ClosureKind),
25    /// The `call_*` method of the appropriate `Fn*` trait.
26    ClosureMethod(hax::DefId, ClosureKind),
27}
28
29impl TransItemSource {
30    pub(crate) fn as_def_id(&self) -> &hax::DefId {
31        match self {
32            TransItemSource::Global(id)
33            | TransItemSource::TraitDecl(id)
34            | TransItemSource::TraitImpl(id)
35            | TransItemSource::Fun(id)
36            | TransItemSource::Type(id)
37            | TransItemSource::ClosureTraitImpl(id, _)
38            | TransItemSource::ClosureMethod(id, _) => id,
39        }
40    }
41}
42
43impl TransItemSource {
44    /// Value with which we order values.
45    fn sort_key(&self) -> impl Ord {
46        let (variant_index, _) = self.variant_index_arity();
47        let def_id = self.as_def_id();
48        let closure_kind = match self {
49            Self::ClosureTraitImpl(_, k) | Self::ClosureMethod(_, k) => match k {
50                ClosureKind::Fn => 1,
51                ClosureKind::FnMut => 2,
52                ClosureKind::FnOnce => 3,
53            },
54            _ => 0,
55        };
56        (def_id.index, variant_index, closure_kind)
57    }
58}
59
60/// Manual impls because `DefId` is not orderable.
61impl PartialOrd for TransItemSource {
62    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
63        Some(self.cmp(other))
64    }
65}
66impl Ord for TransItemSource {
67    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
68        self.sort_key().cmp(&other.sort_key())
69    }
70}
71
72impl<'tcx, 'ctx> TranslateCtx<'tcx> {
73    /// Register a HIR item and all its children. We call this on the crate root items and end up
74    /// exploring the whole crate.
75    fn register_module_item(&mut self, def_id: &hax::DefId) {
76        use hax::DefKind::*;
77        trace!("Registering {def_id:?}");
78
79        match &def_id.kind {
80            Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
81                let _ = self.register_type_decl_id(&None, def_id);
82            }
83            Fn { .. } | AssocFn { .. } => {
84                let _ = self.register_fun_decl_id(&None, def_id);
85            }
86            Const { .. } | Static { .. } | AssocConst { .. } => {
87                let _ = self.register_global_decl_id(&None, def_id);
88            }
89
90            Trait { .. } | TraitAlias { .. } => {
91                let _ = self.register_trait_decl_id(&None, def_id);
92            }
93            Impl { of_trait: true } => {
94                let _ = self.register_trait_impl_id(&None, def_id);
95            }
96
97            Impl { of_trait: false } | Mod { .. } | ForeignMod { .. } => {
98                let Ok(def) = self.hax_def(def_id) else {
99                    return; // Error has already been emitted
100                };
101                let Ok(name) = self.def_id_to_name(&def.def_id) else {
102                    return; // Error has already been emitted
103                };
104                let opacity = self.opacity_for_name(&name);
105                let trans_src = TransItemSource::TraitImpl(def.def_id.clone());
106                let item_meta = self.translate_item_meta(&def, &trans_src, name, opacity);
107                let _ = self.register_module(item_meta, &def);
108            }
109
110            // We skip these
111            ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => {}
112            // We cannot encounter these since they're not top-level items.
113            AnonConst { .. }
114            | AssocTy { .. }
115            | Closure { .. }
116            | ConstParam { .. }
117            | Ctor { .. }
118            | Field { .. }
119            | InlineConst { .. }
120            | PromotedConst { .. }
121            | LifetimeParam { .. }
122            | OpaqueTy { .. }
123            | SyntheticCoroutineBody { .. }
124            | TyParam { .. }
125            | Variant { .. } => {
126                let span = self.def_span(def_id);
127                register_error!(
128                    self,
129                    span,
130                    "Cannot register item `{def_id:?}` with kind `{:?}`",
131                    def_id.kind
132                );
133            }
134        }
135    }
136
137    /// Register the items inside this module.
138    // TODO: we may want to accumulate the set of modules we found, to check that all
139    // the opaque modules given as arguments actually exist
140    fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) -> Result<(), Error> {
141        let opacity = item_meta.opacity;
142        if !opacity.is_transparent() {
143            return Ok(());
144        }
145        match def.kind() {
146            FullDefKind::InherentImpl { items, .. } => {
147                for (_, item_def) in items {
148                    self.register_module_item(&item_def.def_id);
149                }
150            }
151            FullDefKind::Mod { items, .. } => {
152                for (_, def_id) in items {
153                    self.register_module_item(def_id);
154                }
155            }
156            FullDefKind::ForeignMod { items, .. } => {
157                // Foreign modules can't be named or have attributes, so we can't mark them opaque.
158                for def_id in items {
159                    self.register_module_item(def_id);
160                }
161            }
162            _ => panic!("Item should be a module but isn't: {def:?}"),
163        }
164        Ok(())
165    }
166
167    pub(crate) fn register_id_no_enqueue(
168        &mut self,
169        src: &Option<DepSource>,
170        id: TransItemSource,
171    ) -> AnyTransId {
172        let item_id = match self.id_map.get(&id) {
173            Some(tid) => *tid,
174            None => {
175                let trans_id = match id {
176                    TransItemSource::Type(_) => {
177                        AnyTransId::Type(self.translated.type_decls.reserve_slot())
178                    }
179                    TransItemSource::TraitDecl(_) => {
180                        AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot())
181                    }
182                    TransItemSource::TraitImpl(_) | TransItemSource::ClosureTraitImpl(_, _) => {
183                        AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
184                    }
185                    TransItemSource::Global(_) => {
186                        AnyTransId::Global(self.translated.global_decls.reserve_slot())
187                    }
188                    TransItemSource::Fun(_) | TransItemSource::ClosureMethod(_, _) => {
189                        AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
190                    }
191                };
192                // Add the id to the queue of declarations to translate
193                self.id_map.insert(id.clone(), trans_id);
194                self.reverse_id_map.insert(trans_id, id.clone());
195                // Store the name early so the name matcher can identify paths. We can't to it for
196                // trait impls because they register themselves when computing their name.
197                if !matches!(id, TransItemSource::TraitImpl(_)) {
198                    if let Ok(name) = self.def_id_to_name(id.as_def_id()) {
199                        self.translated.item_names.insert(trans_id, name);
200                    }
201                }
202                trans_id
203            }
204        };
205        self.errors
206            .borrow_mut()
207            .register_dep_source(src, item_id, id.as_def_id().is_local);
208        item_id
209    }
210
211    /// Register this id and enqueue it for translation.
212    pub(crate) fn register_and_enqueue_id(
213        &mut self,
214        src: &Option<DepSource>,
215        id: TransItemSource,
216    ) -> AnyTransId {
217        self.items_to_translate.insert(id.clone());
218        self.register_id_no_enqueue(src, id)
219    }
220
221    pub(crate) fn register_type_decl_id(
222        &mut self,
223        src: &Option<DepSource>,
224        id: &hax::DefId,
225    ) -> TypeDeclId {
226        *self
227            .register_and_enqueue_id(src, TransItemSource::Type(id.clone()))
228            .as_type()
229            .unwrap()
230    }
231
232    pub(crate) fn register_fun_decl_id(
233        &mut self,
234        src: &Option<DepSource>,
235        id: &hax::DefId,
236    ) -> FunDeclId {
237        *self
238            .register_and_enqueue_id(src, TransItemSource::Fun(id.clone()))
239            .as_fun()
240            .unwrap()
241    }
242
243    pub(crate) fn register_trait_decl_id(
244        &mut self,
245        src: &Option<DepSource>,
246        id: &hax::DefId,
247    ) -> TraitDeclId {
248        *self
249            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.clone()))
250            .as_trait_decl()
251            .unwrap()
252    }
253
254    pub(crate) fn register_trait_impl_id(
255        &mut self,
256        src: &Option<DepSource>,
257        id: &hax::DefId,
258    ) -> TraitImplId {
259        // Register the corresponding trait early so we can filter on its name.
260        if let Ok(def) = self.hax_def(id) {
261            let trait_id = match def.kind() {
262                hax::FullDefKind::TraitImpl { trait_pred, .. } => &trait_pred.trait_ref.def_id,
263                hax::FullDefKind::TraitAlias { .. } => id,
264                _ => unreachable!(),
265            };
266            let _ = self.register_trait_decl_id(src, trait_id);
267        }
268
269        *self
270            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id.clone()))
271            .as_trait_impl()
272            .unwrap()
273    }
274
275    pub(crate) fn register_closure_trait_impl_id(
276        &mut self,
277        src: &Option<DepSource>,
278        id: &hax::DefId,
279        kind: ClosureKind,
280    ) -> TraitImplId {
281        *self
282            .register_and_enqueue_id(src, TransItemSource::ClosureTraitImpl(id.clone(), kind))
283            .as_trait_impl()
284            .unwrap()
285    }
286
287    pub(crate) fn register_closure_method_decl_id(
288        &mut self,
289        src: &Option<DepSource>,
290        id: &hax::DefId,
291        kind: ClosureKind,
292    ) -> FunDeclId {
293        *self
294            .register_and_enqueue_id(src, TransItemSource::ClosureMethod(id.clone(), kind))
295            .as_fun()
296            .unwrap()
297    }
298
299    pub(crate) fn register_global_decl_id(
300        &mut self,
301        src: &Option<DepSource>,
302        id: &hax::DefId,
303    ) -> GlobalDeclId {
304        *self
305            .register_and_enqueue_id(src, TransItemSource::Global(id.clone()))
306            .as_global()
307            .unwrap()
308    }
309}
310
311// Id and item reference registration.
312impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
313    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
314        Some(DepSource {
315            src_id: self.item_id?,
316            span: self.def_id.is_local.then_some(span),
317        })
318    }
319
320    pub(crate) fn register_id_no_enqueue(&mut self, span: Span, id: TransItemSource) -> AnyTransId {
321        let src = self.make_dep_source(span);
322        self.t_ctx.register_id_no_enqueue(&src, id)
323    }
324
325    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
326        let src = self.make_dep_source(span);
327        self.t_ctx.register_type_decl_id(&src, id)
328    }
329
330    /// Translate a type def id
331    pub(crate) fn translate_type_id(
332        &mut self,
333        span: Span,
334        def_id: &hax::DefId,
335    ) -> Result<TypeId, Error> {
336        Ok(match self.recognize_builtin_type(def_id)? {
337            Some(id) => TypeId::Builtin(id),
338            None => TypeId::Adt(self.register_type_decl_id(span, def_id)),
339        })
340    }
341
342    pub(crate) fn translate_type_decl_ref(
343        &mut self,
344        span: Span,
345        item: &hax::ItemRef,
346    ) -> Result<TypeDeclRef, Error> {
347        let id = self.translate_type_id(span, &item.def_id)?;
348        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
349        Ok(TypeDeclRef {
350            id,
351            generics: Box::new(generics),
352        })
353    }
354
355    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
356        let src = self.make_dep_source(span);
357        self.t_ctx.register_fun_decl_id(&src, id)
358    }
359
360    pub(crate) fn register_fun_decl_id_no_enqueue(
361        &mut self,
362        span: Span,
363        id: &hax::DefId,
364    ) -> FunDeclId {
365        self.register_id_no_enqueue(span, TransItemSource::Fun(id.clone()))
366            .as_fun()
367            .copied()
368            .unwrap()
369    }
370
371    /// Translate a function def id
372    pub(crate) fn translate_fun_id(
373        &mut self,
374        span: Span,
375        def_id: &hax::DefId,
376    ) -> Result<FunId, Error> {
377        Ok(match self.recognize_builtin_fun(def_id)? {
378            Some(id) => FunId::Builtin(id),
379            None => FunId::Regular(self.register_fun_decl_id(span, def_id)),
380        })
381    }
382
383    /// Auxiliary function to translate function calls and references to functions.
384    /// Translate a function id applied with some substitutions.
385    #[tracing::instrument(skip(self, span))]
386    pub(crate) fn translate_fn_ptr(
387        &mut self,
388        span: Span,
389        item: &hax::ItemRef,
390    ) -> Result<RegionBinder<FnPtr>, Error> {
391        let fun_id = self.translate_fun_id(span, &item.def_id)?;
392        let late_bound = match self.hax_def(&item.def_id)?.kind() {
393            hax::FullDefKind::Fn { sig, .. } | hax::FullDefKind::AssocFn { sig, .. } => {
394                Some(sig.as_ref().rebind(()))
395            }
396            _ => None,
397        };
398        let bound_generics = self.translate_generic_args_with_late_bound(
399            span,
400            &item.generic_args,
401            &item.impl_exprs,
402            late_bound,
403        )?;
404        let fun_id = match &item.in_trait {
405            // Direct function call
406            None => FunIdOrTraitMethodRef::Fun(fun_id),
407            // Trait method
408            Some(impl_expr) => {
409                let trait_ref = self.translate_trait_impl_expr(span, impl_expr)?;
410                let name = self.t_ctx.translate_trait_item_name(&item.def_id)?;
411                let method_decl_id = *fun_id
412                    .as_regular()
413                    .expect("methods are not builtin functions");
414                FunIdOrTraitMethodRef::Trait(trait_ref.move_under_binder(), name, method_decl_id)
415            }
416        };
417        Ok(bound_generics.map(|generics| FnPtr {
418            func: Box::new(fun_id),
419            generics: Box::new(generics),
420        }))
421    }
422
423    pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
424        let src = self.make_dep_source(span);
425        self.t_ctx.register_global_decl_id(&src, id)
426    }
427
428    pub(crate) fn translate_global_decl_ref(
429        &mut self,
430        span: Span,
431        item: &hax::ItemRef,
432    ) -> Result<GlobalDeclRef, Error> {
433        let id = self.register_global_decl_id(span, &item.def_id);
434        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
435        Ok(GlobalDeclRef {
436            id,
437            generics: Box::new(generics),
438        })
439    }
440
441    pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
442        let src = self.make_dep_source(span);
443        self.t_ctx.register_trait_decl_id(&src, id)
444    }
445
446    pub(crate) fn translate_trait_decl_ref(
447        &mut self,
448        span: Span,
449        item: &hax::ItemRef,
450    ) -> Result<TraitDeclRef, Error> {
451        let id = self.register_trait_decl_id(span, &item.def_id);
452        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
453        Ok(TraitDeclRef {
454            id,
455            generics: Box::new(generics),
456        })
457    }
458
459    pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
460        let src = self.make_dep_source(span);
461        self.t_ctx.register_trait_impl_id(&src, id)
462    }
463
464    pub(crate) fn translate_trait_impl_ref(
465        &mut self,
466        span: Span,
467        item: &hax::ItemRef,
468    ) -> Result<TraitImplRef, Error> {
469        let id = self.register_trait_impl_id(span, &item.def_id);
470        let generics = self.translate_generic_args(span, &item.generic_args, &item.impl_exprs)?;
471        Ok(TraitImplRef {
472            id,
473            generics: Box::new(generics),
474        })
475    }
476
477    pub(crate) fn register_closure_trait_impl_id(
478        &mut self,
479        span: Span,
480        id: &hax::DefId,
481        kind: ClosureKind,
482    ) -> TraitImplId {
483        let src = self.make_dep_source(span);
484        self.t_ctx.register_closure_trait_impl_id(&src, id, kind)
485    }
486
487    pub(crate) fn register_closure_method_decl_id(
488        &mut self,
489        span: Span,
490        id: &hax::DefId,
491        kind: ClosureKind,
492    ) -> FunDeclId {
493        let src = self.make_dep_source(span);
494        self.t_ctx.register_closure_method_decl_id(&src, id, kind)
495    }
496}
497
498#[tracing::instrument(skip(tcx))]
499pub fn translate<'tcx, 'ctx>(
500    options: &CliOpts,
501    tcx: TyCtxt<'tcx>,
502    sysroot: PathBuf,
503) -> TransformCtx {
504    let hax_state = hax::state::State::new(
505        tcx,
506        hax::options::Options {
507            inline_anon_consts: true,
508            resolve_drop_bounds: false,
509        },
510    );
511
512    // Retrieve the crate name: if the user specified a custom name, use it, otherwise retrieve it
513    // from hax.
514    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
515        .to_def_id()
516        .sinto(&hax_state);
517    let crate_name = crate_def_id.krate.clone();
518    trace!("# Crate: {}", crate_name);
519
520    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
521    let translate_options = TranslateOptions::new(&mut error_ctx, options);
522    let mut ctx = TranslateCtx {
523        tcx,
524        sysroot,
525        hax_state,
526        options: translate_options,
527        errors: RefCell::new(error_ctx),
528        translated: TranslatedCrate {
529            crate_name,
530            options: options.clone(),
531            ..TranslatedCrate::default()
532        },
533        id_map: Default::default(),
534        reverse_id_map: Default::default(),
535        file_to_id: Default::default(),
536        items_to_translate: Default::default(),
537        processed: Default::default(),
538        cached_item_metas: Default::default(),
539        cached_names: Default::default(),
540    };
541
542    if options.start_from.is_empty() {
543        // Recursively register all the items in the crate, starting from the crate root.
544        ctx.register_module_item(&crate_def_id);
545    } else {
546        // Start translating from the selected items.
547        for path in options.start_from.iter() {
548            let path = path.split("::").collect_vec();
549            let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
550            match resolved {
551                Ok(resolved) => {
552                    for def_id in resolved {
553                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
554                        ctx.register_module_item(&def_id);
555                    }
556                }
557                Err(path) => {
558                    let path = path.join("::");
559                    register_error!(
560                        ctx,
561                        Span::dummy(),
562                        "path {path} does not correspond to any item"
563                    );
564                }
565            }
566        }
567    }
568
569    trace!(
570        "Queue after we explored the crate:\n{:?}",
571        &ctx.items_to_translate
572    );
573
574    // Translate.
575    //
576    // For as long as the queue of items to translate is not empty, we pop the top item and
577    // translate it. If an item refers to non-translated (potentially external) items, we add them
578    // to the queue.
579    //
580    // Note that the order in which we translate the definitions doesn't matter:
581    // we never need to lookup a translated definition, and only use the map
582    // from Rust ids to translated ids.
583    while let Some(item_src) = ctx.items_to_translate.pop_first() {
584        trace!("About to translate item: {:?}", item_src);
585        if ctx.processed.insert(item_src.clone()) {
586            ctx.translate_item(&item_src);
587        }
588    }
589
590    // Return the context, dropping the hax state and rustc `tcx`.
591    TransformCtx {
592        options: ctx.options,
593        translated: ctx.translated,
594        errors: ctx.errors,
595    }
596}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
