charon_driver/translate/
translate_ctx.rs

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

charon_driver/translate/
translate_ctx.rs
