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 { .. } => {
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            // TODO: trait aliases (https://github.com/AeneasVerif/charon/issues/366)
97            TraitAlias { .. } => {}
98
99            Impl { of_trait: false } | Mod { .. } | ForeignMod { .. } => {
100                let Ok(def) = self.hax_def(def_id) else {
101                    return; // Error has already been emitted
102                };
103                let Ok(name) = self.def_id_to_name(&def.def_id) else {
104                    return; // Error has already been emitted
105                };
106                let opacity = self.opacity_for_name(&name);
107                let trans_src = TransItemSource::TraitImpl(def.def_id.clone());
108                let item_meta = self.translate_item_meta(&def, &trans_src, name, opacity);
109                let _ = self.register_module(item_meta, &def);
110            }
111
112            // We skip these
113            ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => {}
114            // We cannot encounter these since they're not top-level items.
115            AnonConst { .. }
116            | AssocTy { .. }
117            | Closure { .. }
118            | ConstParam { .. }
119            | Ctor { .. }
120            | Field { .. }
121            | InlineConst { .. }
122            | PromotedConst { .. }
123            | LifetimeParam { .. }
124            | OpaqueTy { .. }
125            | SyntheticCoroutineBody { .. }
126            | TyParam { .. }
127            | Variant { .. } => {
128                let span = self.def_span(def_id);
129                register_error!(
130                    self,
131                    span,
132                    "Cannot register item `{def_id:?}` with kind `{:?}`",
133                    def_id.kind
134                );
135            }
136        }
137    }
138
139    /// Register the items inside this module.
140    // TODO: we may want to accumulate the set of modules we found, to check that all
141    // the opaque modules given as arguments actually exist
142    fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) -> Result<(), Error> {
143        let opacity = item_meta.opacity;
144        if !opacity.is_transparent() {
145            return Ok(());
146        }
147        match def.kind() {
148            FullDefKind::InherentImpl { items, .. } => {
149                for (_, item_def) in items {
150                    self.register_module_item(&item_def.def_id);
151                }
152            }
153            FullDefKind::Mod { items, .. } => {
154                for (_, def_id) in items {
155                    self.register_module_item(def_id);
156                }
157            }
158            FullDefKind::ForeignMod { items, .. } => {
159                // Foreign modules can't be named or have attributes, so we can't mark them opaque.
160                for def_id in items {
161                    self.register_module_item(def_id);
162                }
163            }
164            _ => panic!("Item should be a module but isn't: {def:?}"),
165        }
166        Ok(())
167    }
168
169    pub(crate) fn register_id_no_enqueue(
170        &mut self,
171        src: &Option<DepSource>,
172        id: TransItemSource,
173    ) -> AnyTransId {
174        let item_id = match self.id_map.get(&id) {
175            Some(tid) => *tid,
176            None => {
177                let trans_id = match id {
178                    TransItemSource::Type(_) => {
179                        AnyTransId::Type(self.translated.type_decls.reserve_slot())
180                    }
181                    TransItemSource::TraitDecl(_) => {
182                        AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot())
183                    }
184                    TransItemSource::TraitImpl(_) | TransItemSource::ClosureTraitImpl(_, _) => {
185                        AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
186                    }
187                    TransItemSource::Global(_) => {
188                        AnyTransId::Global(self.translated.global_decls.reserve_slot())
189                    }
190                    TransItemSource::Fun(_) | TransItemSource::ClosureMethod(_, _) => {
191                        AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
192                    }
193                };
194                // Add the id to the queue of declarations to translate
195                self.id_map.insert(id.clone(), trans_id);
196                self.reverse_id_map.insert(trans_id, id.clone());
197                self.translated.all_ids.insert(trans_id);
198                // Store the name early so the name matcher can identify paths. We can't to it for
199                // trait impls because they register themselves when computing their name.
200                if !matches!(id, TransItemSource::TraitImpl(_)) {
201                    if let Ok(name) = self.def_id_to_name(id.as_def_id()) {
202                        self.translated.item_names.insert(trans_id, name);
203                    }
204                }
205                trans_id
206            }
207        };
208        self.errors
209            .borrow_mut()
210            .register_dep_source(src, item_id, id.as_def_id().is_local);
211        item_id
212    }
213
214    /// Register this id and enqueue it for translation.
215    pub(crate) fn register_and_enqueue_id(
216        &mut self,
217        src: &Option<DepSource>,
218        id: TransItemSource,
219    ) -> AnyTransId {
220        self.items_to_translate.insert(id.clone());
221        self.register_id_no_enqueue(src, id)
222    }
223
224    pub(crate) fn register_type_decl_id(
225        &mut self,
226        src: &Option<DepSource>,
227        id: &hax::DefId,
228    ) -> TypeDeclId {
229        *self
230            .register_and_enqueue_id(src, TransItemSource::Type(id.clone()))
231            .as_type()
232            .unwrap()
233    }
234
235    pub(crate) fn register_fun_decl_id(
236        &mut self,
237        src: &Option<DepSource>,
238        id: &hax::DefId,
239    ) -> FunDeclId {
240        *self
241            .register_and_enqueue_id(src, TransItemSource::Fun(id.clone()))
242            .as_fun()
243            .unwrap()
244    }
245
246    pub(crate) fn register_trait_decl_id(
247        &mut self,
248        src: &Option<DepSource>,
249        id: &hax::DefId,
250    ) -> TraitDeclId {
251        *self
252            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.clone()))
253            .as_trait_decl()
254            .unwrap()
255    }
256
257    pub(crate) fn register_trait_impl_id(
258        &mut self,
259        src: &Option<DepSource>,
260        id: &hax::DefId,
261    ) -> TraitImplId {
262        // Register the corresponding trait early so we can filter on its name.
263        if let Ok(def) = self.hax_def(id) {
264            let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else {
265                unreachable!()
266            };
267            let trait_rust_id = &trait_pred.trait_ref.def_id;
268            let _ = self.register_trait_decl_id(src, trait_rust_id);
269        }
270
271        *self
272            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id.clone()))
273            .as_trait_impl()
274            .unwrap()
275    }
276
277    pub(crate) fn register_closure_trait_impl_id(
278        &mut self,
279        src: &Option<DepSource>,
280        id: &hax::DefId,
281        kind: ClosureKind,
282    ) -> TraitImplId {
283        *self
284            .register_and_enqueue_id(src, TransItemSource::ClosureTraitImpl(id.clone(), kind))
285            .as_trait_impl()
286            .unwrap()
287    }
288
289    pub(crate) fn register_closure_method_decl_id(
290        &mut self,
291        src: &Option<DepSource>,
292        id: &hax::DefId,
293        kind: ClosureKind,
294    ) -> FunDeclId {
295        *self
296            .register_and_enqueue_id(src, TransItemSource::ClosureMethod(id.clone(), kind))
297            .as_fun()
298            .unwrap()
299    }
300
301    pub(crate) fn register_global_decl_id(
302        &mut self,
303        src: &Option<DepSource>,
304        id: &hax::DefId,
305    ) -> GlobalDeclId {
306        *self
307            .register_and_enqueue_id(src, TransItemSource::Global(id.clone()))
308            .as_global()
309            .unwrap()
310    }
311}
312
313impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
314    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
315        Some(DepSource {
316            src_id: self.item_id?,
317            span: self.def_id.is_local.then_some(span),
318        })
319    }
320
321    pub(crate) fn register_id_no_enqueue(&mut self, span: Span, id: TransItemSource) -> AnyTransId {
322        let src = self.make_dep_source(span);
323        self.t_ctx.register_id_no_enqueue(&src, id)
324    }
325
326    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
327        let src = self.make_dep_source(span);
328        self.t_ctx.register_type_decl_id(&src, id)
329    }
330
331    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
332        let src = self.make_dep_source(span);
333        self.t_ctx.register_fun_decl_id(&src, id)
334    }
335
336    pub(crate) fn register_fun_decl_id_no_enqueue(
337        &mut self,
338        span: Span,
339        id: &hax::DefId,
340    ) -> FunDeclId {
341        self.register_id_no_enqueue(span, TransItemSource::Fun(id.clone()))
342            .as_fun()
343            .copied()
344            .unwrap()
345    }
346
347    pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
348        let src = self.make_dep_source(span);
349        self.t_ctx.register_global_decl_id(&src, id)
350    }
351
352    pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
353        let src = self.make_dep_source(span);
354        self.t_ctx.register_trait_decl_id(&src, id)
355    }
356
357    pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
358        let src = self.make_dep_source(span);
359        self.t_ctx.register_trait_impl_id(&src, id)
360    }
361
362    pub(crate) fn register_closure_trait_impl_id(
363        &mut self,
364        span: Span,
365        id: &hax::DefId,
366        kind: ClosureKind,
367    ) -> TraitImplId {
368        let src = self.make_dep_source(span);
369        self.t_ctx.register_closure_trait_impl_id(&src, id, kind)
370    }
371
372    pub(crate) fn register_closure_method_decl_id(
373        &mut self,
374        span: Span,
375        id: &hax::DefId,
376        kind: ClosureKind,
377    ) -> FunDeclId {
378        let src = self.make_dep_source(span);
379        self.t_ctx.register_closure_method_decl_id(&src, id, kind)
380    }
381}
382
383#[tracing::instrument(skip(tcx))]
384pub fn translate<'tcx, 'ctx>(
385    options: &CliOpts,
386    tcx: TyCtxt<'tcx>,
387    sysroot: PathBuf,
388) -> TransformCtx {
389    let hax_state = hax::state::State::new(
390        tcx,
391        hax::options::Options {
392            inline_anon_consts: true,
393        },
394    );
395
396    // Retrieve the crate name: if the user specified a custom name, use it, otherwise retrieve it
397    // from hax.
398    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
399        .to_def_id()
400        .sinto(&hax_state);
401    let crate_name = crate_def_id.krate.clone();
402    trace!("# Crate: {}", crate_name);
403
404    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
405    let translate_options = TranslateOptions::new(&mut error_ctx, options);
406    let mut ctx = TranslateCtx {
407        tcx,
408        sysroot,
409        hax_state,
410        options: translate_options,
411        errors: RefCell::new(error_ctx),
412        translated: TranslatedCrate {
413            crate_name,
414            options: options.clone(),
415            ..TranslatedCrate::default()
416        },
417        id_map: Default::default(),
418        reverse_id_map: Default::default(),
419        file_to_id: Default::default(),
420        items_to_translate: Default::default(),
421        processed: Default::default(),
422        cached_item_metas: Default::default(),
423        cached_names: Default::default(),
424    };
425
426    if options.start_from.is_empty() {
427        // Recursively register all the items in the crate, starting from the crate root.
428        ctx.register_module_item(&crate_def_id);
429    } else {
430        // Start translating from the selected items.
431        for path in options.start_from.iter() {
432            let path = path.split("::").collect_vec();
433            let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
434            match resolved {
435                Ok(resolved) => {
436                    for def_id in resolved {
437                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
438                        ctx.register_module_item(&def_id);
439                    }
440                }
441                Err(path) => {
442                    let path = path.join("::");
443                    register_error!(
444                        ctx,
445                        Span::dummy(),
446                        "path {path} does not correspond to any item"
447                    );
448                }
449            }
450        }
451    }
452
453    trace!(
454        "Queue after we explored the crate:\n{:?}",
455        &ctx.items_to_translate
456    );
457
458    // Translate.
459    //
460    // For as long as the queue of items to translate is not empty, we pop the top item and
461    // translate it. If an item refers to non-translated (potentially external) items, we add them
462    // to the queue.
463    //
464    // Note that the order in which we translate the definitions doesn't matter:
465    // we never need to lookup a translated definition, and only use the map
466    // from Rust ids to translated ids.
467    while let Some(item_src) = ctx.items_to_translate.pop_first() {
468        trace!("About to translate item: {:?}", item_src);
469        if ctx.processed.insert(item_src.clone()) {
470            ctx.translate_item(&item_src);
471        }
472    }
473
474    // Return the context, dropping the hax state and rustc `tcx`.
475    TransformCtx {
476        options: ctx.options,
477        translated: ctx.translated,
478        errors: ctx.errors,
479    }
480}
charon_driver/translate/translate_crate.rs

charon_driver/translate/
translate_crate.rs
