charon_driver/translate/
translate_ctx.rs

1//! The translation contexts.
2use super::translate_types::translate_bound_region_kind_name;
3use charon_lib::ast::*;
4use charon_lib::common::hash_by_addr::HashByAddr;
5use charon_lib::formatter::{FmtCtx, IntoFormatter};
6use charon_lib::ids::Vector;
7use charon_lib::options::TranslateOptions;
8use hax_frontend_exporter::SInto;
9use hax_frontend_exporter::{self as hax, DefPathItem};
10use itertools::Itertools;
11use macros::VariantIndexArity;
12use rustc_middle::ty::TyCtxt;
13use std::borrow::Cow;
14use std::cell::RefCell;
15use std::cmp::Ord;
16use std::collections::{BTreeSet, HashMap, HashSet};
17use std::fmt::Debug;
18use std::path::{Component, PathBuf};
19use std::sync::Arc;
20use std::{fmt, mem};
21
22// Re-export to avoid having to fix imports.
23pub(crate) use charon_lib::errors::{
24    error_assert, raise_error, register_error, DepSource, ErrorCtx, Level,
25};
26
27/// The id of an untranslated item. Note that a given `DefId` may show up as multiple different
28/// item sources, e.g. a constant will have both a `Global` version (for the constant itself) and a
29/// `FunDecl` one (for its initializer function).
30#[derive(Clone, Debug, PartialEq, Eq, Hash, VariantIndexArity)]
31pub enum TransItemSource {
32    Global(hax::DefId),
33    TraitDecl(hax::DefId),
34    TraitImpl(hax::DefId),
35    Fun(hax::DefId),
36    Type(hax::DefId),
37}
38
39impl TransItemSource {
40    pub(crate) fn as_def_id(&self) -> &hax::DefId {
41        match self {
42            TransItemSource::Global(id)
43            | TransItemSource::TraitDecl(id)
44            | TransItemSource::TraitImpl(id)
45            | TransItemSource::Fun(id)
46            | TransItemSource::Type(id) => id,
47        }
48    }
49}
50
51impl TransItemSource {
52    /// Value with which we order values.
53    fn sort_key(&self) -> impl Ord {
54        let (variant_index, _) = self.variant_index_arity();
55        let def_id = self.as_def_id();
56        (def_id.index, variant_index)
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
72/// Translation context used while translating the crate data into our representation.
73pub struct TranslateCtx<'tcx> {
74    /// The Rust compiler type context
75    pub tcx: TyCtxt<'tcx>,
76    /// Path to the toolchain root.
77    pub sysroot: PathBuf,
78    /// The Hax context
79    pub hax_state: hax::StateWithBase<'tcx>,
80
81    /// The options that control translation.
82    pub options: TranslateOptions,
83    /// The translated data.
84    pub translated: TranslatedCrate,
85
86    /// The map from rustc id to translated id.
87    pub id_map: HashMap<TransItemSource, AnyTransId>,
88    /// The reverse map of ids.
89    pub reverse_id_map: HashMap<AnyTransId, TransItemSource>,
90    /// The reverse filename map.
91    pub file_to_id: HashMap<FileName, FileId>,
92
93    /// Context for tracking and reporting errors.
94    pub errors: RefCell<ErrorCtx>,
95    /// The declarations we came accross and which we haven't translated yet. We keep them sorted
96    /// to make the output order a bit more stable.
97    pub items_to_translate: BTreeSet<TransItemSource>,
98    /// The declaration we've already processed (successfully or not).
99    pub processed: HashSet<TransItemSource>,
100    /// Cache the names to compute them only once each.
101    pub cached_names: HashMap<hax::DefId, Name>,
102    /// Cache the `ItemMeta`s to compute them only once each.
103    pub cached_item_metas: HashMap<hax::DefId, ItemMeta>,
104}
105
106/// A level of binding for type-level variables. Each item has a top-level binding level
107/// corresponding to the parameters and clauses to the items. We may then encounter inner binding
108/// levels in the following cases:
109/// - `for<..>` binders in predicates;
110/// - `fn<..>` function pointer types;
111/// - `dyn Trait` types, represented as `dyn<T: Trait>` (TODO);
112/// - types in a trait declaration or implementation block (TODO);
113/// - methods in a trait declaration or implementation block (TODO).
114///
115/// At each level, we store two things: a `GenericParams` that contains the parameters bound at
116/// this level, and various maps from the rustc-internal indices to our indices.
117#[derive(Debug)]
118pub(crate) struct BindingLevel {
119    /// The parameters and predicates bound at this level.
120    pub params: GenericParams,
121    /// Whether this binder corresponds to an item (method, type) or not (`for<..>` predicate, `fn`
122    /// pointer, etc). This indicates whether it corresponds to a rustc `ParamEnv` and therefore
123    /// whether we should resolve rustc variables there.
124    pub is_item_binder: bool,
125    /// Rust makes the distinction between early and late-bound region parameters. We do not make
126    /// this distinction, and merge early and late bound regions. For details, see:
127    /// https://smallcultfollowing.com/babysteps/blog/2013/10/29/intermingled-parameter-lists/
128    /// https://smallcultfollowing.com/babysteps/blog/2013/11/04/intermingled-parameter-lists/
129    ///
130    /// The map from rust early regions to translated region indices.
131    pub early_region_vars: std::collections::BTreeMap<hax::EarlyParamRegion, RegionId>,
132    /// The map from rust late/bound regions to translated region indices.
133    pub bound_region_vars: Vec<RegionId>,
134    /// The map from rust type variable indices to translated type variable indices.
135    pub type_vars_map: HashMap<u32, TypeVarId>,
136    /// The map from rust const generic variables to translate const generic variable indices.
137    pub const_generic_vars_map: HashMap<u32, ConstGenericVarId>,
138    /// Cache the translation of types. This harnesses the deduplication of `TyKind` that hax does.
139    pub type_trans_cache: HashMap<HashByAddr<Arc<hax::TyKind>>, Ty>,
140}
141
142impl BindingLevel {
143    pub(crate) fn new(is_item_binder: bool) -> Self {
144        Self {
145            params: Default::default(),
146            is_item_binder,
147            early_region_vars: Default::default(),
148            bound_region_vars: Default::default(),
149            type_vars_map: Default::default(),
150            const_generic_vars_map: Default::default(),
151            type_trans_cache: Default::default(),
152        }
153    }
154
155    /// Important: we must push all the early-bound regions before pushing any other region.
156    pub(crate) fn push_early_region(&mut self, region: hax::EarlyParamRegion) -> RegionId {
157        let name = super::translate_types::translate_region_name(&region);
158        // Check that there are no late-bound regions
159        assert!(
160            self.bound_region_vars.is_empty(),
161            "Early regions must be tralsnated before late ones"
162        );
163        let rid = self
164            .params
165            .regions
166            .push_with(|index| RegionVar { index, name });
167        self.early_region_vars.insert(region, rid);
168        rid
169    }
170
171    /// Important: we must push all the early-bound regions before pushing any other region.
172    pub(crate) fn push_bound_region(&mut self, region: hax::BoundRegionKind) -> RegionId {
173        let name = translate_bound_region_kind_name(&region);
174        let rid = self
175            .params
176            .regions
177            .push_with(|index| RegionVar { index, name });
178        self.bound_region_vars.push(rid);
179        rid
180    }
181
182    pub(crate) fn push_type_var(&mut self, rid: u32, name: String) -> TypeVarId {
183        let var_id = self.params.types.push_with(|index| TypeVar { index, name });
184        self.type_vars_map.insert(rid, var_id);
185        var_id
186    }
187
188    pub(crate) fn push_const_generic_var(&mut self, rid: u32, ty: LiteralTy, name: String) {
189        let var_id = self
190            .params
191            .const_generics
192            .push_with(|index| ConstGenericVar { index, name, ty });
193        self.const_generic_vars_map.insert(rid, var_id);
194    }
195
196    /// Translate a binder of regions by appending the stored reguions to the given vector.
197    pub(crate) fn push_params_from_binder(&mut self, binder: hax::Binder<()>) -> Result<(), Error> {
198        use hax::BoundVariableKind::*;
199        for p in binder.bound_vars {
200            match p {
201                Region(region) => {
202                    self.push_bound_region(region);
203                }
204                Ty(_) => {
205                    panic!("Unexpected locally bound type variable");
206                }
207                Const => {
208                    panic!("Unexpected locally bound const generic variable");
209                }
210            }
211        }
212        Ok(())
213    }
214}
215
216/// A translation context for items.
217/// Augments the [TranslateCtx] with type-level variables.
218pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
219    /// The definition we are currently extracting.
220    /// TODO: this duplicates the field of [ErrorCtx]
221    pub def_id: hax::DefId,
222    /// The id of the definition we are currently extracting, if there is one.
223    pub item_id: Option<AnyTransId>,
224    /// The translation context containing the top-level definitions/ids.
225    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
226    /// Whether to consider a `ImplExprAtom::Error` as an error for us. True except inside type
227    /// aliases, because rust does not enforce correct trait bounds on type aliases.
228    pub error_on_impl_expr_error: bool,
229
230    /// The stack of generic parameter binders for the current context. Each binder introduces an
231    /// entry in this stack, with the entry as index `0` being the innermost binder. These
232    /// parameters are referenced using [`DeBruijnVar`]; see there for details.
233    pub binding_levels: BindingStack<BindingLevel>,
234    /// (For traits only) accumulated implied trait clauses.
235    pub parent_trait_clauses: Vector<TraitClauseId, TraitClause>,
236    /// (For traits only) accumulated trait clauses on associated types.
237    pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
238}
239
240/// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
241pub fn catch_sinto<S, T, U>(
242    s: &S,
243    err: &mut ErrorCtx,
244    krate: &TranslatedCrate,
245    span: Span,
246    x: &T,
247) -> Result<U, Error>
248where
249    T: Debug + SInto<S, U>,
250{
251    let unwind_safe_s = std::panic::AssertUnwindSafe(s);
252    let unwind_safe_x = std::panic::AssertUnwindSafe(x);
253    std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
254        raise_error!(
255            err,
256            crate(krate),
257            span,
258            "Hax panicked when translating `{x:?}`."
259        )
260    })
261}
262
263impl<'tcx, 'ctx> TranslateCtx<'tcx> {
264    /// Span an error and register the error.
265    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
266        self.errors
267            .borrow_mut()
268            .span_err(&self.translated, span, msg, level)
269    }
270
271    /// Register a file if it is a "real" file and was not already registered
272    /// `span` must be a span from which we obtained that filename.
273    fn register_file(&mut self, filename: FileName, span: rustc_span::Span) -> FileId {
274        // Lookup the file if it was already registered
275        match self.file_to_id.get(&filename) {
276            Some(id) => *id,
277            None => {
278                let source_file = self.tcx.sess.source_map().lookup_source_file(span.lo());
279                let file = File {
280                    name: filename.clone(),
281                    contents: source_file.src.as_deref().cloned(),
282                };
283                let id = self.translated.files.push(file);
284                self.file_to_id.insert(filename, id);
285                id
286            }
287        }
288    }
289
290    fn path_elem_for_def(
291        &mut self,
292        span: Span,
293        def_id: &hax::DefId,
294    ) -> Result<Option<PathElem>, Error> {
295        let path_elem = def_id.path_item();
296        // Disambiguator disambiguates identically-named (but distinct) identifiers. This happens
297        // notably with macros and inherent impl blocks.
298        let disambiguator = Disambiguator::new(path_elem.disambiguator as usize);
299        // Match over the key data
300        let path_elem = match path_elem.data {
301            DefPathItem::CrateRoot { name, .. } => {
302                // Sanity check
303                error_assert!(self, span, path_elem.disambiguator == 0);
304                Some(PathElem::Ident(name.clone(), disambiguator))
305            }
306            // We map the three namespaces onto a single one. We can always disambiguate by looking
307            // at the definition.
308            DefPathItem::TypeNs(None) => None,
309            DefPathItem::TypeNs(Some(symbol))
310            | DefPathItem::ValueNs(symbol)
311            | DefPathItem::MacroNs(symbol) => Some(PathElem::Ident(symbol, disambiguator)),
312            DefPathItem::Impl => {
313                let full_def = self.hax_def(def_id)?;
314                // Two cases, depending on whether the impl block is
315                // a "regular" impl block (`impl Foo { ... }`) or a trait
316                // implementation (`impl Bar for Foo { ... }`).
317                let impl_elem = match full_def.kind() {
318                    // Inherent impl ("regular" impl)
319                    hax::FullDefKind::InherentImpl { ty, .. } => {
320                        // We need to convert the type, which may contain quantified
321                        // substs and bounds. In order to properly do so, we introduce
322                        // a body translation context.
323                        let mut bt_ctx = ItemTransCtx::new(def_id.clone(), None, self);
324                        bt_ctx.translate_def_generics(span, &full_def)?;
325                        let ty = bt_ctx.translate_ty(span, &ty)?;
326                        ImplElem::Ty(Binder {
327                            kind: BinderKind::InherentImplBlock,
328                            params: bt_ctx.into_generics(),
329                            skip_binder: ty,
330                        })
331                    }
332                    // Trait implementation
333                    hax::FullDefKind::TraitImpl { .. } => {
334                        let impl_id = self.register_trait_impl_id(&None, def_id);
335                        ImplElem::Trait(impl_id)
336                    }
337                    _ => unreachable!(),
338                };
339
340                Some(PathElem::Impl(impl_elem, disambiguator))
341            }
342            // TODO: do nothing for now
343            DefPathItem::OpaqueTy => None,
344            // TODO: this is not very satisfactory, but on the other hand
345            // we should be able to extract closures in local let-bindings
346            // (i.e., we shouldn't have to introduce top-level let-bindings).
347            DefPathItem::Closure => Some(PathElem::Ident("closure".to_string(), disambiguator)),
348            // Do nothing, functions in `extern` blocks are in the same namespace as the
349            // block.
350            DefPathItem::ForeignMod => None,
351            // Do nothing, the constructor of a struct/variant has the same name as the
352            // struct/variant.
353            DefPathItem::Ctor => None,
354            DefPathItem::Use => Some(PathElem::Ident("{use}".to_string(), disambiguator)),
355            DefPathItem::AnonConst => Some(PathElem::Ident("{const}".to_string(), disambiguator)),
356            DefPathItem::PromotedConst => Some(PathElem::Ident(
357                "{promoted_const}".to_string(),
358                disambiguator,
359            )),
360            _ => {
361                raise_error!(
362                    self,
363                    span,
364                    "Unexpected DefPathItem for `{def_id:?}`: {path_elem:?}"
365                );
366            }
367        };
368        Ok(path_elem)
369    }
370
371    /// Retrieve an item name from a [DefId].
372    /// We lookup the path associated to an id, and convert it to a name.
373    /// Paths very precisely identify where an item is. There are important
374    /// subcases, like the items in an `Impl` block:
375    /// ```ignore
376    /// impl<T> List<T> {
377    ///   fn new() ...
378    /// }
379    /// ```
380    ///
381    /// One issue here is that "List" *doesn't appear* in the path, which would
382    /// look like the following:
383    ///
384    ///   `TypeNS("Crate") :: Impl :: ValueNs("new")`
385    ///                       ^^^
386    ///           This is where "List" should be
387    ///
388    /// For this reason, whenever we find an `Impl` path element, we actually
389    /// lookup the type of the sub-path, from which we can derive a name.
390    ///
391    /// Besides, as there may be several "impl" blocks for one type, each impl
392    /// block is identified by a unique number (rustc calls this a
393    /// "disambiguator"), which we grab.
394    ///
395    /// Example:
396    /// ========
397    /// For instance, if we write the following code in crate `test` and module
398    /// `bla`:
399    /// ```ignore
400    /// impl<T> Foo<T> {
401    ///   fn foo() { ... }
402    /// }
403    ///
404    /// impl<T> Foo<T> {
405    ///   fn bar() { ... }
406    /// }
407    /// ```
408    ///
409    /// The names we will generate for `foo` and `bar` are:
410    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")]`
411    /// `[Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]`
412    pub fn hax_def_id_to_name(&mut self, def_id: &hax::DefId) -> Result<Name, Error> {
413        if let Some(name) = self.cached_names.get(&def_id) {
414            return Ok(name.clone());
415        }
416        trace!("Computing name for `{def_id:?}`");
417
418        let parent_name = if let Some(parent) = &def_id.parent {
419            self.hax_def_id_to_name(parent)?
420        } else {
421            Name { name: Vec::new() }
422        };
423        let span = self.def_span(def_id);
424        let mut name = parent_name;
425        if let Some(path_elem) = self.path_elem_for_def(span, &def_id)? {
426            name.name.push(path_elem);
427        }
428
429        trace!("Computed name for `{def_id:?}`: `{name:?}`");
430        self.cached_names.insert(def_id.clone(), name.clone());
431        Ok(name)
432    }
433
434    /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
435    pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
436    where
437        T: Debug + SInto<S, U>,
438    {
439        catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
440    }
441
442    pub fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
443        let span = self.def_span(def_id);
444        // Hax takes care of caching the translation.
445        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
446        std::panic::catch_unwind(move || def_id.full_def(*unwind_safe_s))
447            .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
448    }
449
450    pub(crate) fn translate_attr_info(&mut self, def: &hax::FullDef) -> AttrInfo {
451        // Default to `false` for impl blocks and closures.
452        let public = def.visibility.unwrap_or(false);
453        let inline = self.translate_inline(def);
454        let attributes = def
455            .attributes
456            .iter()
457            .filter_map(|attr| self.translate_attribute(&attr))
458            .collect_vec();
459
460        let rename = {
461            let mut renames = attributes.iter().filter_map(|a| a.as_rename()).cloned();
462            let rename = renames.next();
463            if renames.next().is_some() {
464                let span = self.translate_span_from_hax(&def.span);
465                register_error!(
466                    self,
467                    span,
468                    "There should be at most one `charon::rename(\"...\")` \
469                    or `aeneas::rename(\"...\")` attribute per declaration",
470                );
471            }
472            rename
473        };
474
475        AttrInfo {
476            attributes,
477            inline,
478            public,
479            rename,
480        }
481    }
482
483    /// Compute the meta information for a Rust item.
484    pub(crate) fn translate_item_meta(
485        &mut self,
486        def: &hax::FullDef,
487        name: Name,
488        name_opacity: ItemOpacity,
489    ) -> ItemMeta {
490        if let Some(item_meta) = self.cached_item_metas.get(&def.def_id) {
491            return item_meta.clone();
492        }
493        let span = def.source_span.as_ref().unwrap_or(&def.span);
494        let span = self.translate_span_from_hax(span);
495        let attr_info = self.translate_attr_info(def);
496        let is_local = def.def_id.is_local;
497        let lang_item = def
498            .lang_item
499            .clone()
500            .or_else(|| def.diagnostic_item.clone());
501
502        let opacity = if self.is_extern_item(def)
503            || attr_info.attributes.iter().any(|attr| attr.is_opaque())
504        {
505            // Force opaque in these cases.
506            ItemOpacity::Opaque.max(name_opacity)
507        } else {
508            name_opacity
509        };
510
511        let item_meta = ItemMeta {
512            name,
513            span,
514            source_text: def.source_text.clone(),
515            attr_info,
516            is_local,
517            opacity,
518            lang_item,
519        };
520        self.cached_item_metas
521            .insert(def.def_id.clone(), item_meta.clone());
522        item_meta
523    }
524
525    pub fn translate_filename(&mut self, name: &hax::FileName) -> meta::FileName {
526        match name {
527            hax::FileName::Real(name) => {
528                use hax::RealFileName;
529                match name {
530                    RealFileName::LocalPath(path) => {
531                        let path = if let Ok(path) = path.strip_prefix(&self.sysroot) {
532                            // The path to files in the standard library may be full paths to somewhere
533                            // in the sysroot. This may depend on how the toolchain is installed
534                            // (rustup vs nix), so we normalize the paths here to avoid
535                            // inconsistencies in the translation.
536                            if let Ok(path) = path.strip_prefix("lib/rustlib/src/rust") {
537                                let mut rewritten_path: PathBuf = "/rustc".into();
538                                rewritten_path.extend(path);
539                                rewritten_path
540                            } else {
541                                // Unclear if this can happen, but just in case.
542                                let mut rewritten_path: PathBuf = "/toolchain".into();
543                                rewritten_path.extend(path);
544                                rewritten_path
545                            }
546                        } else {
547                            path.clone()
548                        };
549                        FileName::Local(path)
550                    }
551                    RealFileName::Remapped { virtual_name, .. } => {
552                        // We use the virtual name because it is always available.
553                        // That name normally starts with `/rustc/<hash>/`. For our purposes we hide
554                        // the hash.
555                        let mut components_iter = virtual_name.components();
556                        if let Some(
557                            [Component::RootDir, Component::Normal(rustc), Component::Normal(hash)],
558                        ) = components_iter.by_ref().array_chunks().next()
559                            && rustc.to_str() == Some("rustc")
560                            && hash.len() == 40
561                        {
562                            let path_without_hash = [Component::RootDir, Component::Normal(rustc)]
563                                .into_iter()
564                                .chain(components_iter)
565                                .collect();
566                            FileName::Virtual(path_without_hash)
567                        } else {
568                            FileName::Virtual(virtual_name.clone())
569                        }
570                    }
571                }
572            }
573            // We use the debug formatter to generate a filename.
574            // This is not ideal, but filenames are for debugging anyway.
575            _ => FileName::NotReal(format!("{name:?}")),
576        }
577    }
578
579    pub fn translate_raw_span(&mut self, rspan: &hax::Span) -> meta::RawSpan {
580        let filename = self.translate_filename(&rspan.filename);
581        let rust_span = rspan.rust_span_data.unwrap().span();
582        let file_id = match &filename {
583            FileName::NotReal(_) => {
584                // For now we forbid not real filenames
585                unimplemented!();
586            }
587            FileName::Virtual(_) | FileName::Local(_) => self.register_file(filename, rust_span),
588        };
589
590        fn convert_loc(loc: &hax::Loc) -> Loc {
591            Loc {
592                line: loc.line,
593                col: loc.col,
594            }
595        }
596        let beg = convert_loc(&rspan.lo);
597        let end = convert_loc(&rspan.hi);
598
599        // Put together
600        meta::RawSpan { file_id, beg, end }
601    }
602
603    /// Compute span data from a Rust source scope
604    pub fn translate_span_from_source_info(
605        &mut self,
606        source_scopes: &hax::IndexVec<hax::SourceScope, hax::SourceScopeData>,
607        source_info: &hax::SourceInfo,
608    ) -> Span {
609        // Translate the span
610        let span = self.translate_raw_span(&source_info.span);
611
612        // Lookup the top-most inlined parent scope.
613        let mut parent_span = None;
614        let mut scope_data = &source_scopes[source_info.scope];
615        while let Some(parent_scope) = scope_data.inlined_parent_scope {
616            scope_data = &source_scopes[parent_scope];
617            parent_span = Some(&scope_data.span);
618        }
619
620        if let Some(parent_span) = parent_span {
621            let parent_span = self.translate_raw_span(parent_span);
622            Span {
623                span: parent_span,
624                generated_from_span: Some(span),
625            }
626        } else {
627            Span {
628                span,
629                generated_from_span: None,
630            }
631        }
632    }
633
634    pub(crate) fn translate_span_from_hax(&mut self, span: &hax::Span) -> Span {
635        Span {
636            span: self.translate_raw_span(span),
637            generated_from_span: None,
638        }
639    }
640
641    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
642        let span = def_id.def_span(&self.hax_state);
643        self.translate_span_from_hax(&span)
644    }
645
646    /// Translates a rust attribute. Returns `None` if the attribute is a doc comment (rustc
647    /// encodes them as attributes). For now we use `String`s for `Attributes`.
648    pub(crate) fn translate_attribute(&mut self, attr: &hax::Attribute) -> Option<Attribute> {
649        use hax::Attribute as Haxttribute;
650        use hax::AttributeKind as HaxttributeKind;
651        match attr {
652            Haxttribute::Parsed(HaxttributeKind::DocComment { comment, .. }) => {
653                Some(Attribute::DocComment(comment.to_string()))
654            }
655            Haxttribute::Parsed(_) => None,
656            Haxttribute::Unparsed(attr) => {
657                let raw_attr = RawAttribute {
658                    path: attr.path.clone(),
659                    args: match &attr.args {
660                        hax::AttrArgs::Empty => None,
661                        hax::AttrArgs::Delimited(args) => Some(args.tokens.clone()),
662                        hax::AttrArgs::Eq { expr, .. } => self
663                            .tcx
664                            .sess
665                            .source_map()
666                            .span_to_snippet(expr.span.rust_span_data.unwrap().span())
667                            .ok(),
668                    },
669                };
670                match Attribute::parse_from_raw(raw_attr) {
671                    Ok(a) => Some(a),
672                    Err(msg) => {
673                        let span = self.translate_span_from_hax(&attr.span);
674                        register_error!(self, span, "Error parsing attribute: {msg}");
675                        None
676                    }
677                }
678            }
679        }
680    }
681
682    pub(crate) fn translate_inline(&self, def: &hax::FullDef) -> Option<InlineAttr> {
683        match def.kind() {
684            hax::FullDefKind::Fn { inline, .. } | hax::FullDefKind::AssocFn { inline, .. } => {
685                match inline {
686                    hax::InlineAttr::None => None,
687                    hax::InlineAttr::Hint => Some(InlineAttr::Hint),
688                    hax::InlineAttr::Never => Some(InlineAttr::Never),
689                    hax::InlineAttr::Always => Some(InlineAttr::Always),
690                    hax::InlineAttr::Force { .. } => Some(InlineAttr::Always),
691                }
692            }
693            _ => None,
694        }
695    }
696
697    /// Whether this item is in an `extern { .. }` block, in which case it has no body.
698    pub(crate) fn is_extern_item(&mut self, def: &hax::FullDef) -> bool {
699        def.parent.as_ref().is_some_and(|parent| {
700            self.hax_def(parent).is_ok_and(|parent_def| {
701                matches!(parent_def.kind(), hax::FullDefKind::ForeignMod { .. })
702            })
703        })
704    }
705
706    pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity {
707        self.options.opacity_for_name(&self.translated, name)
708    }
709
710    pub(crate) fn register_id_no_enqueue(
711        &mut self,
712        src: &Option<DepSource>,
713        id: TransItemSource,
714    ) -> AnyTransId {
715        let item_id = match self.id_map.get(&id) {
716            Some(tid) => *tid,
717            None => {
718                let trans_id = match id {
719                    TransItemSource::Type(_) => {
720                        AnyTransId::Type(self.translated.type_decls.reserve_slot())
721                    }
722                    TransItemSource::TraitDecl(_) => {
723                        AnyTransId::TraitDecl(self.translated.trait_decls.reserve_slot())
724                    }
725                    TransItemSource::TraitImpl(_) => {
726                        AnyTransId::TraitImpl(self.translated.trait_impls.reserve_slot())
727                    }
728                    TransItemSource::Global(_) => {
729                        AnyTransId::Global(self.translated.global_decls.reserve_slot())
730                    }
731                    TransItemSource::Fun(_) => {
732                        AnyTransId::Fun(self.translated.fun_decls.reserve_slot())
733                    }
734                };
735                // Add the id to the queue of declarations to translate
736                self.id_map.insert(id.clone(), trans_id);
737                self.reverse_id_map.insert(trans_id, id.clone());
738                self.translated.all_ids.insert(trans_id);
739                // Store the name early so the name matcher can identify paths. We can't to it for
740                // trait impls because they register themselves when computing their name.
741                if !matches!(id, TransItemSource::TraitImpl(_)) {
742                    if let Ok(name) = self.hax_def_id_to_name(id.as_def_id()) {
743                        self.translated.item_names.insert(trans_id, name);
744                    }
745                }
746                trans_id
747            }
748        };
749        self.errors
750            .borrow_mut()
751            .register_dep_source(src, item_id, id.as_def_id().is_local);
752        item_id
753    }
754
755    /// Register this id and enqueue it for translation.
756    pub(crate) fn register_and_enqueue_id(
757        &mut self,
758        src: &Option<DepSource>,
759        id: TransItemSource,
760    ) -> AnyTransId {
761        self.items_to_translate.insert(id.clone());
762        self.register_id_no_enqueue(src, id)
763    }
764
765    pub(crate) fn register_type_decl_id(
766        &mut self,
767        src: &Option<DepSource>,
768        id: &hax::DefId,
769    ) -> TypeDeclId {
770        *self
771            .register_and_enqueue_id(src, TransItemSource::Type(id.clone()))
772            .as_type()
773            .unwrap()
774    }
775
776    pub(crate) fn register_fun_decl_id(
777        &mut self,
778        src: &Option<DepSource>,
779        id: &hax::DefId,
780    ) -> FunDeclId {
781        *self
782            .register_and_enqueue_id(src, TransItemSource::Fun(id.clone()))
783            .as_fun()
784            .unwrap()
785    }
786
787    pub(crate) fn register_trait_decl_id(
788        &mut self,
789        src: &Option<DepSource>,
790        id: &hax::DefId,
791    ) -> TraitDeclId {
792        *self
793            .register_and_enqueue_id(src, TransItemSource::TraitDecl(id.clone()))
794            .as_trait_decl()
795            .unwrap()
796    }
797
798    pub(crate) fn register_trait_impl_id(
799        &mut self,
800        src: &Option<DepSource>,
801        id: &hax::DefId,
802    ) -> TraitImplId {
803        // Register the corresponding trait early so we can filter on its name.
804        if let Ok(def) = self.hax_def(id) {
805            let hax::FullDefKind::TraitImpl { trait_pred, .. } = def.kind() else {
806                unreachable!()
807            };
808            let trait_rust_id = &trait_pred.trait_ref.def_id;
809            let _ = self.register_trait_decl_id(src, trait_rust_id);
810        }
811
812        *self
813            .register_and_enqueue_id(src, TransItemSource::TraitImpl(id.clone()))
814            .as_trait_impl()
815            .unwrap()
816    }
817
818    pub(crate) fn register_global_decl_id(
819        &mut self,
820        src: &Option<DepSource>,
821        id: &hax::DefId,
822    ) -> GlobalDeclId {
823        *self
824            .register_and_enqueue_id(src, TransItemSource::Global(id.clone()))
825            .as_global()
826            .unwrap()
827    }
828
829    pub(crate) fn with_def_id<F, T>(
830        &mut self,
831        def_id: &hax::DefId,
832        item_id: Option<AnyTransId>,
833        f: F,
834    ) -> T
835    where
836        F: FnOnce(&mut Self) -> T,
837    {
838        let mut errors = self.errors.borrow_mut();
839        let current_def_id = mem::replace(&mut errors.def_id, item_id);
840        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local);
841        drop(errors); // important: release the refcell "lock"
842        let ret = f(self);
843        let mut errors = self.errors.borrow_mut();
844        errors.def_id = current_def_id;
845        errors.def_id_is_local = current_def_id_is_local;
846        ret
847    }
848}
849
850impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
851    /// Create a new `ExecContext`.
852    pub(crate) fn new(
853        def_id: hax::DefId,
854        item_id: Option<AnyTransId>,
855        t_ctx: &'ctx mut TranslateCtx<'tcx>,
856    ) -> Self {
857        ItemTransCtx {
858            def_id,
859            item_id,
860            t_ctx,
861            error_on_impl_expr_error: true,
862            binding_levels: Default::default(),
863            parent_trait_clauses: Default::default(),
864            item_trait_clauses: Default::default(),
865        }
866    }
867
868    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
869        self.t_ctx.span_err(span, msg, level)
870    }
871
872    pub(crate) fn translate_span_from_hax(&mut self, rspan: &hax::Span) -> Span {
873        self.t_ctx.translate_span_from_hax(rspan)
874    }
875
876    pub(crate) fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
877        self.t_ctx.hax_def(def_id)
878    }
879
880    pub(crate) fn def_span(&mut self, def_id: &hax::DefId) -> Span {
881        self.t_ctx.def_span(def_id)
882    }
883
884    pub(crate) fn register_id_no_enqueue(&mut self, span: Span, id: TransItemSource) -> AnyTransId {
885        let src = self.make_dep_source(span);
886        self.t_ctx.register_id_no_enqueue(&src, id)
887    }
888
889    pub(crate) fn register_type_decl_id(&mut self, span: Span, id: &hax::DefId) -> TypeDeclId {
890        let src = self.make_dep_source(span);
891        self.t_ctx.register_type_decl_id(&src, id)
892    }
893
894    pub(crate) fn register_fun_decl_id(&mut self, span: Span, id: &hax::DefId) -> FunDeclId {
895        let src = self.make_dep_source(span);
896        self.t_ctx.register_fun_decl_id(&src, id)
897    }
898
899    pub(crate) fn register_fun_decl_id_no_enqueue(
900        &mut self,
901        span: Span,
902        id: &hax::DefId,
903    ) -> FunDeclId {
904        self.register_id_no_enqueue(span, TransItemSource::Fun(id.clone()))
905            .as_fun()
906            .copied()
907            .unwrap()
908    }
909
910    pub(crate) fn register_global_decl_id(&mut self, span: Span, id: &hax::DefId) -> GlobalDeclId {
911        let src = self.make_dep_source(span);
912        self.t_ctx.register_global_decl_id(&src, id)
913    }
914
915    /// Returns an [Option] because we may ignore some builtin or auto traits
916    /// like [core::marker::Sized] or [core::marker::Sync].
917    pub(crate) fn register_trait_decl_id(&mut self, span: Span, id: &hax::DefId) -> TraitDeclId {
918        let src = self.make_dep_source(span);
919        self.t_ctx.register_trait_decl_id(&src, id)
920    }
921
922    /// Returns an [Option] because we may ignore some builtin or auto traits
923    /// like [core::marker::Sized] or [core::marker::Sync].
924    pub(crate) fn register_trait_impl_id(&mut self, span: Span, id: &hax::DefId) -> TraitImplId {
925        let src = self.make_dep_source(span);
926        self.t_ctx.register_trait_impl_id(&src, id)
927    }
928
929    /// Get the only binding level. Panics if there are other binding levels.
930    pub(crate) fn the_only_binder(&self) -> &BindingLevel {
931        assert_eq!(self.binding_levels.len(), 1);
932        &self.outermost_binder()
933    }
934
935    pub(crate) fn outermost_binder(&self) -> &BindingLevel {
936        self.binding_levels.outermost()
937    }
938
939    pub(crate) fn innermost_binder(&self) -> &BindingLevel {
940        self.binding_levels.innermost()
941    }
942
943    pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel {
944        self.binding_levels.innermost_mut()
945    }
946
947    pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams {
948        &mut self.innermost_binder_mut().params
949    }
950
951    pub(crate) fn lookup_bound_region(
952        &mut self,
953        span: Span,
954        dbid: hax::DebruijnIndex,
955        var: hax::BoundVar,
956    ) -> Result<RegionDbVar, Error> {
957        let dbid = DeBruijnId::new(dbid);
958        if let Some(rid) = self
959            .binding_levels
960            .get(dbid)
961            .and_then(|bl| bl.bound_region_vars.get(var))
962        {
963            Ok(DeBruijnVar::bound(dbid, *rid))
964        } else {
965            raise_error!(
966                self,
967                span,
968                "Unexpected error: could not find region '{dbid}_{var}"
969            )
970        }
971    }
972
973    fn lookup_param<Id: Copy>(
974        &mut self,
975        span: Span,
976        f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>,
977        mk_err: impl FnOnce() -> String,
978    ) -> Result<DeBruijnVar<Id>, Error> {
979        for (dbid, bl) in self.binding_levels.iter_enumerated() {
980            if let Some(id) = f(bl) {
981                return Ok(DeBruijnVar::bound(dbid, id));
982            }
983        }
984        let err = mk_err();
985        raise_error!(self, span, "Unexpected error: could not find {}", err)
986    }
987
988    pub(crate) fn lookup_early_region(
989        &mut self,
990        span: Span,
991        region: &hax::EarlyParamRegion,
992    ) -> Result<RegionDbVar, Error> {
993        self.lookup_param(
994            span,
995            |bl| bl.early_region_vars.get(region).copied(),
996            || format!("the region variable {region:?}"),
997        )
998    }
999
1000    pub(crate) fn lookup_type_var(
1001        &mut self,
1002        span: Span,
1003        param: &hax::ParamTy,
1004    ) -> Result<TypeDbVar, Error> {
1005        self.lookup_param(
1006            span,
1007            |bl| bl.type_vars_map.get(&param.index).copied(),
1008            || format!("the type variable {}", param.name),
1009        )
1010    }
1011
1012    pub(crate) fn lookup_const_generic_var(
1013        &mut self,
1014        span: Span,
1015        param: &hax::ParamConst,
1016    ) -> Result<ConstGenericDbVar, Error> {
1017        self.lookup_param(
1018            span,
1019            |bl| bl.const_generic_vars_map.get(&param.index).copied(),
1020            || format!("the const generic variable {}", param.name),
1021        )
1022    }
1023
1024    pub(crate) fn lookup_clause_var(
1025        &mut self,
1026        span: Span,
1027        mut id: usize,
1028    ) -> Result<ClauseDbVar, Error> {
1029        // The clause indices returned by hax count clauses in order, starting from the parentmost.
1030        // While adding clauses to a binding level we already need to translate types and clauses,
1031        // so the innermost item binder may not have all the clauses yet. Hence for that binder we
1032        // ignore the clause count.
1033        let innermost_item_binder_id = self
1034            .binding_levels
1035            .iter_enumerated()
1036            .find(|(_, bl)| bl.is_item_binder)
1037            .unwrap()
1038            .0;
1039        // Iterate over the binders, starting from the outermost.
1040        for (dbid, bl) in self.binding_levels.iter_enumerated().rev() {
1041            let num_clauses_bound_at_this_level = bl.params.trait_clauses.elem_count();
1042            if id < num_clauses_bound_at_this_level || dbid == innermost_item_binder_id {
1043                let id = TraitClauseId::from_usize(id);
1044                return Ok(DeBruijnVar::bound(dbid, id));
1045            } else {
1046                id -= num_clauses_bound_at_this_level
1047            }
1048        }
1049        // Actually unreachable
1050        raise_error!(
1051            self,
1052            span,
1053            "Unexpected error: could not find clause variable {}",
1054            id
1055        )
1056    }
1057
1058    pub(crate) fn lookup_cached_type(
1059        &self,
1060        cache_key: &HashByAddr<Arc<hax::TyKind>>,
1061    ) -> Option<Ty> {
1062        // Important: we can't reuse type caches from earlier binders as the new binder may change
1063        // what a given variable resolves to.
1064        self.innermost_binder()
1065            .type_trans_cache
1066            .get(&cache_key)
1067            .cloned()
1068    }
1069
1070    /// Push a group of bound regions and call the continuation.
1071    /// We use this when diving into a `for<'a>`, or inside an arrow type (because
1072    /// it contains universally quantified regions).
1073    pub(crate) fn translate_region_binder<F, T, U>(
1074        &mut self,
1075        _span: Span,
1076        binder: &hax::Binder<T>,
1077        f: F,
1078    ) -> Result<RegionBinder<U>, Error>
1079    where
1080        F: FnOnce(&mut Self, &T) -> Result<U, Error>,
1081    {
1082        assert!(!self.binding_levels.is_empty());
1083
1084        // Register the variables
1085        let mut binding_level = BindingLevel::new(false);
1086        binding_level.push_params_from_binder(binder.rebind(()))?;
1087        self.binding_levels.push(binding_level);
1088
1089        // Call the continuation. Important: do not short-circuit on error here.
1090        let res = f(self, binder.hax_skip_binder_ref());
1091
1092        // Reset
1093        let regions = self.binding_levels.pop().unwrap().params.regions;
1094
1095        // Return
1096        res.map(|skip_binder| RegionBinder {
1097            regions,
1098            skip_binder,
1099        })
1100    }
1101
1102    /// Push a new binding level corresponding to the provided `def` for the duration of the inner
1103    /// function call.
1104    pub(crate) fn translate_binder_for_def<F, U>(
1105        &mut self,
1106        span: Span,
1107        kind: BinderKind,
1108        def: &hax::FullDef,
1109        f: F,
1110    ) -> Result<Binder<U>, Error>
1111    where
1112        F: FnOnce(&mut Self) -> Result<U, Error>,
1113    {
1114        assert!(!self.binding_levels.is_empty());
1115
1116        // Register the type-level parameters. This pushes a new binding level.
1117        self.translate_def_generics_without_parents(span, def)?;
1118
1119        // Call the continuation. Important: do not short-circuit on error here.
1120        let res = f(self);
1121
1122        // Reset
1123        let params = self.binding_levels.pop().unwrap().params;
1124
1125        // Return
1126        res.map(|skip_binder| Binder {
1127            kind,
1128            params,
1129            skip_binder,
1130        })
1131    }
1132
1133    pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource> {
1134        Some(DepSource {
1135            src_id: self.item_id?,
1136            span: self.def_id.is_local.then_some(span),
1137        })
1138    }
1139}
1140
1141impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
1142    type C = FmtCtx<'a>;
1143    fn into_fmt(self) -> Self::C {
1144        self.translated.into_fmt()
1145    }
1146}
1147
1148impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
1149    type C = FmtCtx<'a>;
1150    fn into_fmt(self) -> Self::C {
1151        FmtCtx {
1152            translated: Some(&self.t_ctx.translated),
1153            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
1154            locals: None,
1155        }
1156    }
1157}
1158
1159impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx> {
1160    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
1161        self.translated.fmt(f)
1162    }
1163}
charon_driver/translate/translate_ctx.rs

charon_driver/translate/
translate_ctx.rs
