charon_driver/translate/
translate_crate_to_ullbc.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 rustc_middle::ty::TyCtxt;
9use std::cell::RefCell;
10use std::path::PathBuf;
11
12impl<'tcx, 'ctx> TranslateCtx<'tcx> {
13    /// Register a HIR item and all its children. We call this on the crate root items and end up
14    /// exploring the whole crate.
15    fn register_module_item(&mut self, def_id: &hax::DefId) {
16        use hax::DefKind::*;
17        trace!("Registering {def_id:?}");
18
19        match &def_id.kind {
20            Enum { .. } | Struct { .. } | Union { .. } | TyAlias { .. } | ForeignTy => {
21                let _ = self.register_type_decl_id(&None, def_id);
22            }
23            Fn { .. } | AssocFn { .. } => {
24                let _ = self.register_fun_decl_id(&None, def_id);
25            }
26            Const { .. } | Static { .. } | AssocConst { .. } => {
27                let _ = self.register_global_decl_id(&None, def_id);
28            }
29
30            Trait { .. } => {
31                let _ = self.register_trait_decl_id(&None, def_id);
32            }
33            Impl { of_trait: true } => {
34                let _ = self.register_trait_impl_id(&None, def_id);
35            }
36            // TODO: trait aliases (https://github.com/AeneasVerif/charon/issues/366)
37            TraitAlias { .. } => {}
38
39            Impl { of_trait: false } | Mod { .. } | ForeignMod { .. } => {
40                let Ok(def) = self.hax_def(def_id) else {
41                    return; // Error has already been emitted
42                };
43                let Ok(name) = self.hax_def_id_to_name(&def.def_id) else {
44                    return; // Error has already been emitted
45                };
46                let opacity = self.opacity_for_name(&name);
47                let item_meta = self.translate_item_meta(&def, name, opacity);
48                let _ = self.register_module(item_meta, &def);
49            }
50
51            // We skip these
52            ExternCrate { .. } | GlobalAsm { .. } | Macro { .. } | Use { .. } => {}
53            // We cannot encounter these since they're not top-level items.
54            AnonConst { .. }
55            | AssocTy { .. }
56            | Closure { .. }
57            | ConstParam { .. }
58            | Ctor { .. }
59            | Field { .. }
60            | InlineConst { .. }
61            | PromotedConst { .. }
62            | LifetimeParam { .. }
63            | OpaqueTy { .. }
64            | SyntheticCoroutineBody { .. }
65            | TyParam { .. }
66            | Variant { .. } => {
67                let span = self.def_span(def_id);
68                register_error!(
69                    self,
70                    span,
71                    "Cannot register item `{def_id:?}` with kind `{:?}`",
72                    def_id.kind
73                );
74            }
75        }
76    }
77
78    /// Register the items inside this module.
79    // TODO: we may want to accumulate the set of modules we found, to check that all
80    // the opaque modules given as arguments actually exist
81    fn register_module(&mut self, item_meta: ItemMeta, def: &hax::FullDef) -> Result<(), Error> {
82        let opacity = item_meta.opacity;
83        if !opacity.is_transparent() {
84            return Ok(());
85        }
86        match def.kind() {
87            FullDefKind::InherentImpl { items, .. } => {
88                for (_, item_def) in items {
89                    self.register_module_item(&item_def.def_id);
90                }
91            }
92            FullDefKind::Mod { items, .. } => {
93                for (_, def_id) in items {
94                    self.register_module_item(def_id);
95                }
96            }
97            FullDefKind::ForeignMod { items, .. } => {
98                // Foreign modules can't be named or have attributes, so we can't mark them opaque.
99                for def_id in items {
100                    self.register_module_item(def_id);
101                }
102            }
103            _ => panic!("Item should be a module but isn't: {def:?}"),
104        }
105        Ok(())
106    }
107
108    pub(crate) fn translate_item(&mut self, item_src: &TransItemSource) {
109        let trans_id = self.id_map.get(&item_src).copied();
110        let def_id = item_src.as_def_id();
111        self.with_def_id(def_id, trans_id, |mut ctx| {
112            let span = ctx.def_span(def_id);
113            // Catch cycles
114            let res = {
115                // Stopgap measure because there are still many panics in charon and hax.
116                let mut ctx = std::panic::AssertUnwindSafe(&mut ctx);
117                std::panic::catch_unwind(move || ctx.translate_item_aux(def_id, trans_id))
118            };
119            match res {
120                Ok(Ok(())) => return,
121                // Translation error
122                Ok(Err(_)) => {
123                    register_error!(ctx, span, "Item `{def_id:?}` caused errors; ignoring.")
124                }
125                // Panic
126                Err(_) => register_error!(
127                    ctx,
128                    span,
129                    "Thread panicked when extracting item `{def_id:?}`."
130                ),
131            };
132        })
133    }
134
135    pub(crate) fn translate_item_aux(
136        &mut self,
137        def_id: &hax::DefId,
138        trans_id: Option<AnyTransId>,
139    ) -> Result<(), Error> {
140        // Translate the meta information
141        let name = self.hax_def_id_to_name(def_id)?;
142        if let Some(trans_id) = trans_id {
143            self.translated.item_names.insert(trans_id, name.clone());
144        }
145        let opacity = self.opacity_for_name(&name);
146        if opacity.is_invisible() {
147            // Don't even start translating the item. In particular don't call `hax_def` on it.
148            return Ok(());
149        }
150        let def = self.hax_def(def_id)?;
151        let item_meta = self.translate_item_meta(&def, name, opacity);
152
153        // Initialize the body translation context
154        let bt_ctx = ItemTransCtx::new(def_id.clone(), trans_id, self);
155        match trans_id {
156            Some(AnyTransId::Type(id)) => {
157                let ty = bt_ctx.translate_type(id, item_meta, &def)?;
158                self.translated.type_decls.set_slot(id, ty);
159            }
160            Some(AnyTransId::Fun(id)) => {
161                let fun_decl = bt_ctx.translate_function(id, item_meta, &def)?;
162                self.translated.fun_decls.set_slot(id, fun_decl);
163            }
164            Some(AnyTransId::Global(id)) => {
165                let global_decl = bt_ctx.translate_global(id, item_meta, &def)?;
166                self.translated.global_decls.set_slot(id, global_decl);
167            }
168            Some(AnyTransId::TraitDecl(id)) => {
169                let trait_decl = bt_ctx.translate_trait_decl(id, item_meta, &def)?;
170                self.translated.trait_decls.set_slot(id, trait_decl);
171            }
172            Some(AnyTransId::TraitImpl(id)) => {
173                let trait_impl = bt_ctx.translate_trait_impl(id, item_meta, &def)?;
174                self.translated.trait_impls.set_slot(id, trait_impl);
175            }
176            None => unimplemented!(),
177        }
178        Ok(())
179    }
180}
181
182#[tracing::instrument(skip(tcx))]
183pub fn translate<'tcx, 'ctx>(
184    options: &CliOpts,
185    tcx: TyCtxt<'tcx>,
186    sysroot: PathBuf,
187) -> TransformCtx {
188    let hax_state = hax::state::State::new(
189        tcx,
190        hax::options::Options {
191            inline_anon_consts: true,
192        },
193    );
194
195    // Retrieve the crate name: if the user specified a custom name, use it, otherwise retrieve it
196    // from hax.
197    let crate_def_id: hax::DefId = rustc_span::def_id::CRATE_DEF_ID
198        .to_def_id()
199        .sinto(&hax_state);
200    let crate_name = crate_def_id.krate.clone();
201    trace!("# Crate: {}", crate_name);
202
203    let mut error_ctx = ErrorCtx::new(!options.abort_on_error, options.error_on_warnings);
204    let translate_options = TranslateOptions::new(&mut error_ctx, options);
205    let mut ctx = TranslateCtx {
206        tcx,
207        sysroot,
208        hax_state,
209        options: translate_options,
210        errors: RefCell::new(error_ctx),
211        translated: TranslatedCrate {
212            crate_name,
213            options: options.clone(),
214            ..TranslatedCrate::default()
215        },
216        id_map: Default::default(),
217        reverse_id_map: Default::default(),
218        file_to_id: Default::default(),
219        items_to_translate: Default::default(),
220        processed: Default::default(),
221        cached_item_metas: Default::default(),
222        cached_names: Default::default(),
223    };
224
225    if options.start_from.is_empty() {
226        // Recursively register all the items in the crate, starting from the crate root.
227        ctx.register_module_item(&crate_def_id);
228    } else {
229        // Start translating from the selected items.
230        for path in options.start_from.iter() {
231            let path = path.split("::").collect_vec();
232            let resolved = super::resolve_path::def_path_def_ids(&ctx.hax_state, &path);
233            match resolved {
234                Ok(resolved) => {
235                    for def_id in resolved {
236                        let def_id: hax::DefId = def_id.sinto(&ctx.hax_state);
237                        ctx.register_module_item(&def_id);
238                    }
239                }
240                Err(path) => {
241                    let path = path.join("::");
242                    register_error!(
243                        ctx,
244                        Span::dummy(),
245                        "path {path} does not correspond to any item"
246                    );
247                }
248            }
249        }
250    }
251
252    trace!(
253        "Queue after we explored the crate:\n{:?}",
254        &ctx.items_to_translate
255    );
256
257    // Translate.
258    //
259    // For as long as the queue of items to translate is not empty, we pop the top item and
260    // translate it. If an item refers to non-translated (potentially external) items, we add them
261    // to the queue.
262    //
263    // Note that the order in which we translate the definitions doesn't matter:
264    // we never need to lookup a translated definition, and only use the map
265    // from Rust ids to translated ids.
266    while let Some(item_src) = ctx.items_to_translate.pop_first() {
267        trace!("About to translate item: {:?}", item_src);
268        if ctx.processed.insert(item_src.clone()) {
269            ctx.translate_item(&item_src);
270        }
271    }
272
273    // Return the context, dropping the hax state and rustc `tcx`.
274    TransformCtx {
275        options: ctx.options,
276        translated: ctx.translated,
277        errors: ctx.errors,
278    }
279}
charon_driver/translate/translate_crate_to_ullbc.rs

charon_driver/translate/
translate_crate_to_ullbc.rs
