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

charon_driver/translate/
translate_ctx.rs
