charon_driver/translate/
translate_ctx.rs

1//! The translation contexts.
2use super::translate_crate::TransItemSource;
3use super::translate_generics::BindingLevel;
4use charon_lib::ast::*;
5use charon_lib::formatter::{FmtCtx, IntoFormatter};
6use charon_lib::ids::Vector;
7use charon_lib::options::TranslateOptions;
8use hax_frontend_exporter::{self as hax, DefId, SInto};
9use rustc_middle::ty::TyCtxt;
10use std::borrow::Cow;
11use std::cell::RefCell;
12use std::collections::{BTreeSet, HashMap, HashSet};
13use std::fmt::Debug;
14use std::path::PathBuf;
15use std::sync::Arc;
16use std::{fmt, mem};
17
18// Re-export to avoid having to fix imports.
19pub(crate) use charon_lib::errors::{
20    error_assert, raise_error, register_error, DepSource, ErrorCtx, Level,
21};
22
23/// Translation context used while translating the crate data into our representation.
24pub struct TranslateCtx<'tcx> {
25    /// The Rust compiler type context
26    pub tcx: TyCtxt<'tcx>,
27    /// Path to the toolchain root.
28    pub sysroot: PathBuf,
29    /// The Hax context
30    pub hax_state: hax::StateWithBase<'tcx>,
31
32    /// The options that control translation.
33    pub options: TranslateOptions,
34    /// The translated data.
35    pub translated: TranslatedCrate,
36
37    /// The map from rustc id to translated id.
38    pub id_map: HashMap<TransItemSource, AnyTransId>,
39    /// The reverse map of ids.
40    pub reverse_id_map: HashMap<AnyTransId, TransItemSource>,
41    /// The reverse filename map.
42    pub file_to_id: HashMap<FileName, FileId>,
43
44    /// Context for tracking and reporting errors.
45    pub errors: RefCell<ErrorCtx>,
46    /// The declarations we came accross and which we haven't translated yet. We keep them sorted
47    /// to make the output order a bit more stable.
48    pub items_to_translate: BTreeSet<TransItemSource>,
49    /// The declaration we've already processed (successfully or not).
50    pub processed: HashSet<TransItemSource>,
51    /// Cache the names to compute them only once each.
52    pub cached_names: HashMap<hax::DefId, Name>,
53    /// Cache the `ItemMeta`s to compute them only once each.
54    pub cached_item_metas: HashMap<TransItemSource, ItemMeta>,
55}
56
57/// A translation context for items.
58/// Augments the [TranslateCtx] with type-level variables.
59pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
60    /// The definition we are currently extracting.
61    pub item_src: TransItemSource,
62    /// The id of the definition we are currently extracting, if there is one.
63    pub item_id: Option<AnyTransId>,
64    /// The translation context containing the top-level definitions/ids.
65    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
66    /// Whether to consider a `ImplExprAtom::Error` as an error for us. True except inside type
67    /// aliases, because rust does not enforce correct trait bounds on type aliases.
68    pub error_on_impl_expr_error: bool,
69
70    /// The stack of generic parameter binders for the current context. Each binder introduces an
71    /// entry in this stack, with the entry as index `0` being the innermost binder. These
72    /// parameters are referenced using [`DeBruijnVar`]; see there for details.
73    pub binding_levels: BindingStack<BindingLevel>,
74    /// (For traits only) accumulated implied trait clauses.
75    pub parent_trait_clauses: Vector<TraitClauseId, TraitClause>,
76    /// (For traits only) accumulated trait clauses on associated types.
77    pub item_trait_clauses: HashMap<TraitItemName, Vector<TraitClauseId, TraitClause>>,
78    /// (For method declarations only) the clause id corresponding to the explicit `Self` clause.
79    /// If `None` then we're in a trait declaration and should use `TraitRefKind::Self` instead.
80    pub self_clause_id: Option<TraitClauseId>,
81}
82
83/// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
84pub fn catch_sinto<S, T, U>(
85    s: &S,
86    err: &mut ErrorCtx,
87    krate: &TranslatedCrate,
88    span: Span,
89    x: &T,
90) -> Result<U, Error>
91where
92    T: Debug + SInto<S, U>,
93{
94    let unwind_safe_s = std::panic::AssertUnwindSafe(s);
95    let unwind_safe_x = std::panic::AssertUnwindSafe(x);
96    std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
97        raise_error!(
98            err,
99            crate(krate),
100            span,
101            "Hax panicked when translating `{x:?}`."
102        )
103    })
104}
105
106impl<'tcx, 'ctx> TranslateCtx<'tcx> {
107    /// Span an error and register the error.
108    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
109        self.errors
110            .borrow_mut()
111            .span_err(&self.translated, span, msg, level)
112    }
113
114    /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
115    pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
116    where
117        T: Debug + SInto<S, U>,
118    {
119        catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
120    }
121
122    pub fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
123        let span = self.def_span(def_id);
124        // Hax takes care of caching the translation.
125        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
126        std::panic::catch_unwind(move || def_id.full_def(*unwind_safe_s))
127            .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
128    }
129
130    pub(crate) fn get_lang_item(&self, item: rustc_hir::LangItem) -> DefId {
131        self.tcx
132            .lang_items()
133            .get(item)
134            .unwrap()
135            .sinto(&self.hax_state)
136    }
137
138    pub(crate) fn with_def_id<F, T>(
139        &mut self,
140        def_id: &hax::DefId,
141        item_id: Option<AnyTransId>,
142        f: F,
143    ) -> T
144    where
145        F: FnOnce(&mut Self) -> T,
146    {
147        let mut errors = self.errors.borrow_mut();
148        let current_def_id = mem::replace(&mut errors.def_id, item_id);
149        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local);
150        drop(errors); // important: release the refcell "lock"
151        let ret = f(self);
152        let mut errors = self.errors.borrow_mut();
153        errors.def_id = current_def_id;
154        errors.def_id_is_local = current_def_id_is_local;
155        ret
156    }
157}
158
159impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
160    /// Create a new `ExecContext`.
161    pub(crate) fn new(
162        item_src: TransItemSource,
163        item_id: Option<AnyTransId>,
164        t_ctx: &'ctx mut TranslateCtx<'tcx>,
165    ) -> Self {
166        ItemTransCtx {
167            item_src,
168            item_id,
169            t_ctx,
170            error_on_impl_expr_error: true,
171            binding_levels: Default::default(),
172            parent_trait_clauses: Default::default(),
173            item_trait_clauses: Default::default(),
174            self_clause_id: Default::default(),
175        }
176    }
177
178    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
179        self.t_ctx.span_err(span, msg, level)
180    }
181
182    pub(crate) fn hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
183        self.t_ctx.hax_def(def_id)
184    }
185
186    pub(crate) fn get_lang_item(&self, item: rustc_hir::LangItem) -> DefId {
187        self.t_ctx.get_lang_item(item)
188    }
189}
190
191impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
192    type C = FmtCtx<'a>;
193    fn into_fmt(self) -> Self::C {
194        self.translated.into_fmt()
195    }
196}
197
198impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
199    type C = FmtCtx<'a>;
200    fn into_fmt(self) -> Self::C {
201        FmtCtx {
202            translated: Some(&self.t_ctx.translated),
203            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
204            locals: None,
205            indent_level: 0,
206        }
207    }
208}
209
210impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx> {
211    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
212        self.translated.fmt(f)
213    }
214}