charon_driver/translate/
translate_ctx.rs

1//! The translation contexts.
2use super::translate_crate::RustcItem;
3pub use super::translate_crate::{TraitImplSource, TransItemSource, TransItemSourceKind};
4use super::translate_generics::BindingLevel;
5use charon_lib::ast::*;
6use charon_lib::formatter::{FmtCtx, IntoFormatter};
7use charon_lib::options::TranslateOptions;
8use hax::SInto;
9use rustc_middle::ty::TyCtxt;
10use std::borrow::Cow;
11use std::cell::RefCell;
12use std::collections::{HashMap, HashSet, VecDeque};
13use std::fmt::Debug;
14use std::ops::{Deref, DerefMut};
15use std::path::PathBuf;
16use std::sync::Arc;
17use std::{fmt, mem};
18
19// Re-export to avoid having to fix imports.
20pub(crate) use charon_lib::errors::{
21    DepSource, ErrorCtx, Level, error_assert, raise_error, register_error,
22};
23
24/// Translation context used while translating the crate data into our representation.
25pub struct TranslateCtx<'tcx> {
26    /// The Rust compiler type context
27    pub tcx: TyCtxt<'tcx>,
28    /// Path to the toolchain root.
29    pub sysroot: PathBuf,
30    /// The Hax context
31    pub hax_state: hax::StateWithBase<'tcx>,
32
33    /// The options that control translation.
34    pub options: TranslateOptions,
35    /// The translated data.
36    pub translated: TranslatedCrate,
37
38    /// Record data for each method whether it is ever used (called or implemented) and the
39    /// `FunDeclId`s of the implementations. We use this to lazily translate methods, so that we
40    /// skip unused default methods of large traits like `Iterator`.
41    ///
42    /// The complete scheme works as follows: by default we enqueue no methods for translation.
43    /// When we find a use of a method, we mark it "used" using `mark_method_as_used`. This
44    /// enqueues all known and future impls of this method. We also mark a method as used if we
45    /// find an implementation of it in a non-opaque impl, and if the method is a required method.
46    pub method_status: IndexMap<TraitDeclId, HashMap<TraitItemName, MethodStatus>>,
47
48    /// The map from rustc id to translated id.
49    pub id_map: HashMap<TransItemSource, ItemId>,
50    /// The reverse map of ids.
51    pub reverse_id_map: HashMap<ItemId, TransItemSource>,
52    /// The reverse filename map.
53    pub file_to_id: HashMap<FileName, FileId>,
54
55    /// Context for tracking and reporting errors.
56    pub errors: RefCell<ErrorCtx>,
57    /// The declarations we came accross and which we haven't translated yet.
58    pub items_to_translate: VecDeque<TransItemSource>,
59    /// The declaration we've already processed (successfully or not).
60    pub processed: HashSet<TransItemSource>,
61    /// Stack of the translations currently happening. Used to avoid accidental cycles.
62    pub translate_stack: Vec<ItemId>,
63    /// Cache the names to compute them only once each.
64    pub cached_names: HashMap<RustcItem, Name>,
65    /// Cache the `ItemMeta`s to compute them only once each.
66    pub cached_item_metas: HashMap<TransItemSource, ItemMeta>,
67}
68
69/// Tracks whether a method is used (i.e. called or (non-opaquely) implemented).
70#[derive(Debug)]
71pub enum MethodStatus {
72    Unused {
73        /// The `FunDeclId`s of the method implementations. Because the method is unused, these
74        /// items are not enqueued for translation yet. When marking the method as used we'll
75        /// enqueue them.
76        implementors: HashSet<FunDeclId>,
77    },
78    Used,
79}
80
81impl Default for MethodStatus {
82    fn default() -> Self {
83        Self::Unused {
84            implementors: Default::default(),
85        }
86    }
87}
88
89/// A translation context for items.
90/// Augments the [TranslateCtx] with type-level variables.
91pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
92    /// The definition we are currently extracting.
93    pub item_src: TransItemSource,
94    /// The id of the definition we are currently extracting, if there is one.
95    pub item_id: Option<ItemId>,
96    /// The translation context containing the top-level definitions/ids.
97    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
98    /// The Hax context with the current `DefId`.
99    pub hax_state: hax::StateWithOwner<'tcx>,
100    /// Whether to consider a `ImplExprAtom::Error` as an error for us. True except inside type
101    /// aliases, because rust does not enforce correct trait bounds on type aliases.
102    pub error_on_impl_expr_error: bool,
103
104    /// The stack of generic parameter binders for the current context. Each binder introduces an
105    /// entry in this stack, with the entry as index `0` being the innermost binder. These
106    /// parameters are referenced using [`DeBruijnVar`]; see there for details.
107    pub binding_levels: BindingStack<BindingLevel>,
108    /// When `Some`, translate any erased lifetime to a fresh `Region::Body` lifetime.
109    pub lifetime_freshener: Option<IndexMap<RegionId, ()>>,
110}
111
112/// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
113pub fn catch_sinto<S, T, U>(
114    s: &S,
115    err: &mut ErrorCtx,
116    krate: &TranslatedCrate,
117    span: Span,
118    x: &T,
119) -> Result<U, Error>
120where
121    T: Debug + SInto<S, U>,
122{
123    let unwind_safe_s = std::panic::AssertUnwindSafe(s);
124    let unwind_safe_x = std::panic::AssertUnwindSafe(x);
125    std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
126        raise_error!(
127            err,
128            crate(krate),
129            span,
130            "Hax panicked when translating `{x:?}`."
131        )
132    })
133}
134
135impl<'tcx, 'ctx> TranslateCtx<'tcx> {
136    /// Span an error and register the error.
137    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
138        self.errors
139            .borrow_mut()
140            .span_err(&self.translated, span, msg, level)
141    }
142
143    /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
144    pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
145    where
146        T: Debug + SInto<S, U>,
147    {
148        catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
149    }
150
151    /// Return the polymorphic definition for this item. Use with care, prefer `hax_def` whenever
152    /// possible.
153    ///
154    /// Used for computing names, for associated items, and for various checks.
155    pub fn poly_hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
156        self.hax_def_for_item(&RustcItem::Poly(def_id.clone()))
157    }
158
159    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
160    /// depending on user choice.
161    pub fn hax_def_for_item(&mut self, item: &RustcItem) -> Result<Arc<hax::FullDef>, Error> {
162        let def_id = item.def_id();
163        let span = self.def_span(def_id);
164        if let RustcItem::Mono(item_ref) = item
165            && item_ref.has_non_lt_param
166        {
167            raise_error!(self, span, "Item is not monomorphic: {item:?}")
168        }
169        // Hax takes care of caching the translation.
170        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
171        std::panic::catch_unwind(move || match item {
172            RustcItem::Poly(def_id) => def_id.full_def(*unwind_safe_s),
173            RustcItem::Mono(item_ref) => item_ref.instantiated_full_def(*unwind_safe_s),
174        })
175        .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
176    }
177
178    pub(crate) fn with_def_id<F, T>(
179        &mut self,
180        def_id: &hax::DefId,
181        item_id: Option<ItemId>,
182        f: F,
183    ) -> T
184    where
185        F: FnOnce(&mut Self) -> T,
186    {
187        let mut errors = self.errors.borrow_mut();
188        let current_def_id = mem::replace(&mut errors.def_id, item_id);
189        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
190        drop(errors); // important: release the refcell "lock"
191        let ret = f(self);
192        let mut errors = self.errors.borrow_mut();
193        errors.def_id = current_def_id;
194        errors.def_id_is_local = current_def_id_is_local;
195        ret
196    }
197}
198
199impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
200    /// Create a new `ExecContext`.
201    pub(crate) fn new(
202        item_src: TransItemSource,
203        item_id: Option<ItemId>,
204        t_ctx: &'ctx mut TranslateCtx<'tcx>,
205    ) -> Self {
206        use hax::BaseState;
207        let def_id = item_src.def_id().underlying_rust_def_id();
208        let hax_state_with_id = t_ctx.hax_state.clone().with_owner_id(def_id);
209        ItemTransCtx {
210            item_src,
211            item_id,
212            t_ctx,
213            hax_state: hax_state_with_id,
214            error_on_impl_expr_error: true,
215            binding_levels: Default::default(),
216            lifetime_freshener: None,
217        }
218    }
219
220    /// Whether to monomorphize items we encounter.
221    pub fn monomorphize(&self) -> bool {
222        matches!(self.item_src.item, RustcItem::Mono(..))
223    }
224
225    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
226        self.t_ctx.span_err(span, msg, level)
227    }
228
229    pub fn hax_state(&self) -> &hax::StateWithBase<'tcx> {
230        &self.t_ctx.hax_state
231    }
232
233    pub fn hax_state_with_id(&self) -> &hax::StateWithOwner<'tcx> {
234        &self.hax_state
235    }
236
237    pub fn catch_sinto<T, U>(&mut self, span: Span, x: &T) -> Result<U, Error>
238    where
239        T: Debug + SInto<hax::StateWithOwner<'tcx>, U>,
240    {
241        self.t_ctx.catch_sinto(&self.hax_state, span, x)
242    }
243
244    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
245    /// depending on user choice.
246    pub fn hax_def(&mut self, item: &hax::ItemRef) -> Result<Arc<hax::FullDef>, Error> {
247        let item = if self.monomorphize() {
248            RustcItem::Mono(item.clone())
249        } else {
250            RustcItem::Poly(item.def_id.clone())
251        };
252        self.t_ctx.hax_def_for_item(&item)
253    }
254
255    pub(crate) fn poly_hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
256        self.t_ctx.poly_hax_def(def_id)
257    }
258}
259
260impl<'tcx> Deref for ItemTransCtx<'tcx, '_> {
261    type Target = TranslateCtx<'tcx>;
262    fn deref(&self) -> &Self::Target {
263        self.t_ctx
264    }
265}
266impl<'tcx> DerefMut for ItemTransCtx<'tcx, '_> {
267    fn deref_mut(&mut self) -> &mut Self::Target {
268        self.t_ctx
269    }
270}
271
272impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
273    type C = FmtCtx<'a>;
274    fn into_fmt(self) -> Self::C {
275        self.translated.into_fmt()
276    }
277}
278
279impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
280    type C = FmtCtx<'a>;
281    fn into_fmt(self) -> Self::C {
282        FmtCtx {
283            translated: Some(&self.t_ctx.translated),
284            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
285            locals: None,
286            indent_level: 0,
287        }
288    }
289}
290
291impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx> {
292    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
293        self.translated.fmt(f)
294    }
295}
charon_driver/translate/translate_ctx.rs

charon_driver/translate/
translate_ctx.rs
