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

charon_driver/translate/
translate_ctx.rs
