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, LifetimeMutabilityComputer};
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    /// Compute which lifetimes are used in a `&'a mut T`. This is a global fixpoint analysis.
68    pub lt_mutability_computer: LifetimeMutabilityComputer,
69}
70
71/// Tracks whether a method is used (i.e. called or (non-opaquely) implemented).
72#[derive(Debug)]
73pub enum MethodStatus {
74    Unused {
75        /// The `FunDeclId`s of the method implementations. Because the method is unused, these
76        /// items are not enqueued for translation yet. When marking the method as used we'll
77        /// enqueue them.
78        implementors: HashSet<FunDeclId>,
79    },
80    Used,
81}
82
83impl Default for MethodStatus {
84    fn default() -> Self {
85        Self::Unused {
86            implementors: Default::default(),
87        }
88    }
89}
90
91/// A translation context for items.
92/// Augments the [TranslateCtx] with type-level variables.
93pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
94    /// The definition we are currently extracting.
95    pub item_src: TransItemSource,
96    /// The id of the definition we are currently extracting, if there is one.
97    pub item_id: Option<ItemId>,
98    /// The translation context containing the top-level definitions/ids.
99    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
100    /// The Hax context with the current `DefId`.
101    pub hax_state: hax::StateWithOwner<'tcx>,
102    /// Whether to consider a `ImplExprAtom::Error` as an error for us. True except inside type
103    /// aliases, because rust does not enforce correct trait bounds on type aliases.
104    pub error_on_impl_expr_error: bool,
105
106    /// The stack of generic parameter binders for the current context. Each binder introduces an
107    /// entry in this stack, with the entry as index `0` being the innermost binder. These
108    /// parameters are referenced using [`DeBruijnVar`]; see there for details.
109    pub binding_levels: BindingStack<BindingLevel>,
110    /// When `Some`, translate any erased lifetime to a fresh `Region::Body` lifetime.
111    pub lifetime_freshener: Option<IndexMap<RegionId, ()>>,
112}
113
114/// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
115pub fn catch_sinto<S, T, U>(
116    s: &S,
117    err: &mut ErrorCtx,
118    krate: &TranslatedCrate,
119    span: Span,
120    x: &T,
121) -> Result<U, Error>
122where
123    T: Debug + SInto<S, U>,
124{
125    let unwind_safe_s = std::panic::AssertUnwindSafe(s);
126    let unwind_safe_x = std::panic::AssertUnwindSafe(x);
127    std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
128        raise_error!(
129            err,
130            crate(krate),
131            span,
132            "Hax panicked when translating `{x:?}`."
133        )
134    })
135}
136
137impl<'tcx, 'ctx> TranslateCtx<'tcx> {
138    /// Span an error and register the error.
139    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
140        self.errors
141            .borrow_mut()
142            .span_err(&self.translated, span, msg, level)
143    }
144
145    /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
146    pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
147    where
148        T: Debug + SInto<S, U>,
149    {
150        catch_sinto(s, &mut *self.errors.borrow_mut(), &self.translated, span, x)
151    }
152
153    /// Return the polymorphic definition for this item. Use with care, prefer `hax_def` whenever
154    /// possible.
155    ///
156    /// Used for computing names, for associated items, and for various checks.
157    pub fn poly_hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
158        self.hax_def_for_item(&RustcItem::Poly(def_id.clone()))
159    }
160
161    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
162    /// depending on user choice.
163    pub fn hax_def_for_item(&mut self, item: &RustcItem) -> Result<Arc<hax::FullDef>, Error> {
164        let def_id = item.def_id();
165        let span = self.def_span(def_id);
166        if let RustcItem::Mono(item_ref) = item
167            && item_ref.has_non_lt_param
168        {
169            raise_error!(self, span, "Item is not monomorphic: {item:?}")
170        }
171        // Hax takes care of caching the translation.
172        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
173        std::panic::catch_unwind(move || match item {
174            RustcItem::Poly(def_id) => def_id.full_def(*unwind_safe_s),
175            RustcItem::Mono(item_ref) => item_ref.instantiated_full_def(*unwind_safe_s),
176        })
177        .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
178    }
179
180    pub(crate) fn with_def_id<F, T>(
181        &mut self,
182        def_id: &hax::DefId,
183        item_id: Option<ItemId>,
184        f: F,
185    ) -> T
186    where
187        F: FnOnce(&mut Self) -> T,
188    {
189        let mut errors = self.errors.borrow_mut();
190        let current_def_id = mem::replace(&mut errors.def_id, item_id);
191        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
192        drop(errors); // important: release the refcell "lock"
193        let ret = f(self);
194        let mut errors = self.errors.borrow_mut();
195        errors.def_id = current_def_id;
196        errors.def_id_is_local = current_def_id_is_local;
197        ret
198    }
199}
200
201impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
202    /// Create a new `ExecContext`.
203    pub(crate) fn new(
204        item_src: TransItemSource,
205        item_id: Option<ItemId>,
206        t_ctx: &'ctx mut TranslateCtx<'tcx>,
207    ) -> Self {
208        use hax::BaseState;
209        let hax_state_with_id = t_ctx.hax_state.clone().with_hax_owner(&item_src.def_id());
210        ItemTransCtx {
211            item_src,
212            item_id,
213            t_ctx,
214            hax_state: hax_state_with_id,
215            error_on_impl_expr_error: true,
216            binding_levels: Default::default(),
217            lifetime_freshener: None,
218        }
219    }
220
221    /// Whether to monomorphize items we encounter.
222    pub fn monomorphize(&self) -> bool {
223        matches!(self.item_src.item, RustcItem::Mono(..))
224    }
225
226    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
227        self.t_ctx.span_err(span, msg, level)
228    }
229
230    pub fn hax_state(&self) -> &hax::StateWithBase<'tcx> {
231        &self.t_ctx.hax_state
232    }
233
234    pub fn hax_state_with_id(&self) -> &hax::StateWithOwner<'tcx> {
235        &self.hax_state
236    }
237
238    pub fn catch_sinto<T, U>(&mut self, span: Span, x: &T) -> Result<U, Error>
239    where
240        T: Debug + SInto<hax::StateWithOwner<'tcx>, U>,
241    {
242        self.t_ctx.catch_sinto(&self.hax_state, span, x)
243    }
244
245    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
246    /// depending on user choice.
247    pub fn hax_def(&mut self, item: &hax::ItemRef) -> Result<Arc<hax::FullDef>, Error> {
248        let item = if self.monomorphize() {
249            RustcItem::Mono(item.clone())
250        } else {
251            RustcItem::Poly(item.def_id.clone())
252        };
253        self.t_ctx.hax_def_for_item(&item)
254    }
255
256    pub(crate) fn poly_hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef>, Error> {
257        self.t_ctx.poly_hax_def(def_id)
258    }
259}
260
261impl<'tcx> Deref for ItemTransCtx<'tcx, '_> {
262    type Target = TranslateCtx<'tcx>;
263    fn deref(&self) -> &Self::Target {
264        self.t_ctx
265    }
266}
267impl<'tcx> DerefMut for ItemTransCtx<'tcx, '_> {
268    fn deref_mut(&mut self) -> &mut Self::Target {
269        self.t_ctx
270    }
271}
272
273impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
274    type C = FmtCtx<'a>;
275    fn into_fmt(self) -> Self::C {
276        self.translated.into_fmt()
277    }
278}
279
280impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
281    type C = FmtCtx<'a>;
282    fn into_fmt(self) -> Self::C {
283        FmtCtx {
284            translated: Some(&self.t_ctx.translated),
285            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
286            locals: None,
287            indent_level: 0,
288        }
289    }
290}
291
292impl<'tcx, 'ctx> fmt::Display for TranslateCtx<'tcx> {
293    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
294        self.translated.fmt(f)
295    }
296}
charon_driver/translate/translate_ctx.rs

charon_driver/translate/
translate_ctx.rs
