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 petgraph::graphmap::DiGraphMap;
12use rustc_hash::{FxHashMap as HashMap, FxHashSet as HashSet};
13use rustc_middle::ty::TyCtxt;
14use rustc_span::def_id::DefId as RDefId;
15use std::borrow::Cow;
16use std::cell::RefCell;
17use std::collections::VecDeque;
18use std::fmt::Debug;
19use std::ops::{Deref, DerefMut};
20use std::path::PathBuf;
21use std::sync::Arc;
22use std::{fmt, mem};
23
24// Re-export to avoid having to fix imports.
25pub(crate) use charon_lib::errors::{
26    DepSource, ErrorCtx, Level, error_assert, raise_error, register_error,
27};
28
29#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
30pub enum ItemOrModuleId {
31    Item(ItemId),
32    /// A module, foreign module, or inherent impl.
33    Module(RDefId),
34}
35
36// `DiGraphMap` requires ordered nodes. Rustc ids have no stable ordering across compilation
37// sessions, but ordering by their indices suffices for this graph within a single translation.
38impl Ord for ItemOrModuleId {
39    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
40        use std::cmp::Ordering;
41        match (self, other) {
42            (Self::Item(a), Self::Item(b)) => a.cmp(b),
43            (Self::Module(a), Self::Module(b)) => {
44                (a.krate.as_u32(), a.index.as_u32()).cmp(&(b.krate.as_u32(), b.index.as_u32()))
45            }
46            (Self::Item(_), Self::Module(_)) => Ordering::Less,
47            (Self::Module(_), Self::Item(_)) => Ordering::Greater,
48        }
49    }
50}
51
52impl PartialOrd for ItemOrModuleId {
53    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
54        Some(self.cmp(other))
55    }
56}
57
58impl ItemOrModuleId {
59    pub fn as_item(&self) -> Option<ItemId> {
60        match self {
61            Self::Item(id) => Some(*id),
62            Self::Module(_) => None,
63        }
64    }
65
66    pub fn expect_item<T: TryFrom<ItemId>>(&self) -> T {
67        self.as_item()
68            .expect("expected a translated item")
69            .try_into()
70            .ok()
71            .expect("unexpected item kind")
72    }
73}
74
75/// Nodes in the containment graph used to compute `ItemMeta::started_from`.
76#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
77pub enum ContainmentNode {
78    Start,
79    Item(ItemOrModuleId),
80    TraitMethod(TraitDeclId, TraitMethodId),
81}
82
83impl From<ItemOrModuleId> for ContainmentNode {
84    fn from(id: ItemOrModuleId) -> Self {
85        Self::Item(id)
86    }
87}
88
89impl From<ItemId> for ContainmentNode {
90    fn from(id: ItemId) -> Self {
91        Self::Item(ItemOrModuleId::Item(id))
92    }
93}
94
95/// Translation context used while translating the crate data into our representation.
96pub struct TranslateCtx<'tcx> {
97    /// The Rust compiler type context
98    pub tcx: TyCtxt<'tcx>,
99    /// Path to the toolchain root.
100    pub sysroot: PathBuf,
101    /// The Hax context
102    pub hax_state: hax::StateWithBase<'tcx>,
103
104    /// The options that control translation.
105    pub options: TranslateOptions,
106    /// The translated data.
107    pub translated: TranslatedCrate,
108
109    /// Record data for each method whether it is ever used (called or implemented) and the
110    /// `FunDeclId`s of the implementations. We use this to lazily translate methods, so that we
111    /// skip unused default methods of large traits like `Iterator`.
112    ///
113    /// The complete scheme works as follows: by default we enqueue no methods for translation.
114    /// When we find a use of a method, we mark it "used" using `mark_method_as_used`. This
115    /// enqueues all known and future impls of this method. We also mark a method as used if we
116    /// find an implementation of it in a non-opaque impl, and if the method is a required method.
117    pub method_status: IndexMap<TraitDeclId, IndexVec<TraitMethodId, MethodStatus>>,
118
119    /// The map from rustc id to translated id.
120    pub id_map: HashMap<TransItemSource<'tcx>, ItemId>,
121    /// The reverse map of ids.
122    pub reverse_id_map: HashMap<ItemId, TransItemSource<'tcx>>,
123    /// Map from rustc id to associated item id
124    pub assoc_item_id_map: HashMap<hax::DefId, AssocItemId>,
125    /// The reverse filename map.
126    pub file_to_id: HashMap<FileName, FileId>,
127
128    /// Context for tracking and reporting errors.
129    pub errors: RefCell<ErrorCtx>,
130    /// The declarations we came accross and which we haven't translated yet.
131    pub items_to_translate: VecDeque<TransItemSource<'tcx>>,
132    /// The declaration we've already processed (successfully or not).
133    pub processed: HashSet<TransItemSource<'tcx>>,
134    /// While translating, record which item is "contained" by another, in the sense that
135    /// `--start-from` the parent should make the child be considered started from too. We use this
136    /// to compute `ItemMeta.started_from` at the end of translation.
137    pub containment_graph: DiGraphMap<ContainmentNode, (), rustc_hash::FxBuildHasher>,
138    /// Stack of the translations currently happening. Used to avoid accidental cycles.
139    pub translate_stack: Vec<ItemOrModuleId>,
140    /// Cache of the translated span, as translating one is costly
141    pub cached_spans: HashMap<rustc_span::Span, meta::SpanData>,
142    /// Cache of file ids per rustc source file, to avoid recomputing file names for every span.
143    pub cached_file_ids: HashMap<rustc_span::StableSourceFileId, FileId>,
144    /// Cache the names to compute them only once each.
145    pub cached_names: HashMap<RustcItem<'tcx>, Name>,
146    /// Cache the `ItemMeta`s to compute them only once each.
147    pub cached_item_metas: HashMap<TransItemSource<'tcx>, ItemMeta>,
148    /// Compute which lifetimes are used in a `&'a mut T`. This is a global fixpoint analysis.
149    pub lt_mutability_computer: LifetimeMutabilityComputer,
150}
151
152/// Tracks whether a method is used (i.e. called or (non-opaquely) implemented).
153#[derive(Debug)]
154pub enum MethodStatus {
155    Unused {
156        /// The `FunDeclId`s of the method implementations. Because the method is unused, these
157        /// items are not enqueued for translation yet. When marking the method as used we'll
158        /// enqueue them.
159        implementors: HashSet<FunDeclId>,
160    },
161    Used,
162}
163
164impl Default for MethodStatus {
165    fn default() -> Self {
166        Self::Unused {
167            implementors: Default::default(),
168        }
169    }
170}
171
172/// A translation context for items.
173/// Augments the [TranslateCtx] with type-level variables.
174pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
175    /// The definition we are currently extracting.
176    pub item_src: TransItemSource<'tcx>,
177    /// The id of the definition we are currently extracting.
178    pub item_id: ItemOrModuleId,
179    /// The translation context containing the top-level definitions/ids.
180    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
181    /// The Hax context with the current `DefId`.
182    pub hax_state: hax::StateWithOwner<'tcx>,
183    /// Whether to consider a `TraitProofKind::Error` as an error for us. True except inside type
184    /// aliases, because rust does not enforce correct trait bounds on type aliases.
185    pub error_on_trait_proof_error: bool,
186
187    /// The stack of generic parameter binders for the current context. Each binder introduces an
188    /// entry in this stack, with the entry as index `0` being the innermost binder. These
189    /// parameters are referenced using [`DeBruijnVar`]; see there for details.
190    pub binding_levels: BindingStack<BindingLevel<'tcx>>,
191    /// When `Some`, translate any erased lifetime to a fresh `Region::Body` lifetime.
192    pub lifetime_freshener: Option<IndexMap<RegionId, ()>>,
193}
194
195/// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
196pub fn catch_sinto<S, T, U>(
197    s: &S,
198    err: &mut ErrorCtx,
199    krate: &TranslatedCrate,
200    span: Span,
201    x: &T,
202) -> Result<U, Error>
203where
204    T: Debug + SInto<S, U>,
205{
206    let unwind_safe_s = std::panic::AssertUnwindSafe(s);
207    let unwind_safe_x = std::panic::AssertUnwindSafe(x);
208    std::panic::catch_unwind(move || unwind_safe_x.sinto(*unwind_safe_s)).or_else(|_| {
209        raise_error!(
210            err,
211            crate(krate),
212            span,
213            "Hax panicked when translating `{x:?}`."
214        )
215    })
216}
217
218impl<'tcx> TranslateCtx<'tcx> {
219    /// Span an error and register the error.
220    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
221        self.errors
222            .borrow_mut()
223            .span_err(&self.translated, span, msg, level)
224    }
225
226    pub fn get_target_triple(&self) -> TargetTriple {
227        self.tcx.sess.opts.target_triple.tuple().to_owned()
228    }
229
230    /// Translates `T` into `U` using `hax`'s `SInto` trait, catching any hax panics.
231    pub fn catch_sinto<S, T, U>(&mut self, s: &S, span: Span, x: &T) -> Result<U, Error>
232    where
233        T: Debug + SInto<S, U>,
234    {
235        catch_sinto(s, &mut self.errors.borrow_mut(), &self.translated, span, x)
236    }
237
238    /// Return the polymorphic definition for this item. Use with care, prefer `hax_def` whenever
239    /// possible.
240    ///
241    /// Used for computing names, for associated items, and for various checks.
242    pub fn poly_hax_def(&mut self, def_id: &hax::DefId) -> Result<Arc<hax::FullDef<'tcx>>, Error> {
243        self.hax_def_for_item(&RustcItem::Poly(def_id.clone()))
244    }
245
246    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
247    /// depending on user choice.
248    pub fn hax_def_for_item(
249        &mut self,
250        item: &RustcItem<'tcx>,
251    ) -> Result<Arc<hax::FullDef<'tcx>>, Error> {
252        let def_id = item.def_id();
253        let span = self.def_span(def_id);
254        if let RustcItem::Mono(item_ref) = item
255            && item_ref.has_non_lt_param
256        {
257            raise_error!(self, span, "Item is not monomorphic: {item:?}")
258        }
259        // Hax takes care of caching the translation.
260        let _guard = charon_lib::timing::scope("hax-full-def");
261        let unwind_safe_s = std::panic::AssertUnwindSafe(&self.hax_state);
262        std::panic::catch_unwind(move || match item {
263            RustcItem::Poly(def_id) => def_id.full_def(*unwind_safe_s),
264            RustcItem::Mono(item_ref) => item_ref.instantiated_full_def(*unwind_safe_s),
265            RustcItem::MonoTrait(def_id) => def_id.full_def(*unwind_safe_s),
266        })
267        .or_else(|_| raise_error!(self, span, "Hax panicked when translating `{def_id:?}`."))
268    }
269
270    pub(crate) fn with_def_id<F, T>(
271        &mut self,
272        def_id: &hax::DefId,
273        item_id: &ItemOrModuleId,
274        f: F,
275    ) -> T
276    where
277        F: FnOnce(&mut Self) -> T,
278    {
279        let mut errors = self.errors.borrow_mut();
280        let current_def_id = mem::replace(&mut errors.def_id, item_id.as_item());
281        let current_def_id_is_local = mem::replace(&mut errors.def_id_is_local, def_id.is_local());
282        drop(errors); // important: release the refcell "lock"
283        let ret = f(self);
284        let mut errors = self.errors.borrow_mut();
285        errors.def_id = current_def_id;
286        errors.def_id_is_local = current_def_id_is_local;
287        ret
288    }
289}
290
291impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx> {
292    /// Create a new `ExecContext`.
293    pub(crate) fn new(
294        item_src: TransItemSource<'tcx>,
295        item_id: ItemOrModuleId,
296        t_ctx: &'ctx mut TranslateCtx<'tcx>,
297    ) -> Self {
298        use crate::hax::BaseState;
299        let hax_state_with_id = t_ctx.hax_state.clone().with_hax_owner(item_src.def_id());
300        ItemTransCtx {
301            item_src,
302            item_id,
303            t_ctx,
304            hax_state: hax_state_with_id,
305            error_on_trait_proof_error: true,
306            binding_levels: Default::default(),
307            lifetime_freshener: None,
308        }
309    }
310
311    /// Whether to monomorphize items we encounter.
312    pub fn monomorphize(&self) -> bool {
313        matches!(
314            self.item_src.item,
315            RustcItem::Mono(..) | RustcItem::MonoTrait(..)
316        )
317    }
318
319    /// Whether to translate this particular item monomorphically.
320    pub fn should_monomorphize_item(&self, item: &hax::ItemRef, kind: TransItemSourceKind) -> bool {
321        // Traits and vtables use `MonoTrait` in mono mode. Other items are translated
322        // monomorphically when their arguments are concrete, even if the context is poly.
323        self.options.monomorphize_with_hax && (kind.is_for_trait() || !item.has_non_lt_param)
324    }
325
326    pub fn span_err(&self, span: Span, msg: &str, level: Level) -> Error {
327        self.t_ctx.span_err(span, msg, level)
328    }
329
330    pub fn hax_state(&self) -> &hax::StateWithBase<'tcx> {
331        &self.t_ctx.hax_state
332    }
333
334    pub fn hax_state_with_id(&self) -> &hax::StateWithOwner<'tcx> {
335        &self.hax_state
336    }
337
338    pub fn catch_sinto<T, U>(&mut self, span: Span, x: &T) -> Result<U, Error>
339    where
340        T: Debug + SInto<hax::StateWithOwner<'tcx>, U>,
341    {
342        self.t_ctx.catch_sinto(&self.hax_state, span, x)
343    }
344
345    /// Return the definition for this item. This uses the polymorphic or monomorphic definition
346    /// depending on user choice. For `TraitDecl` or `VTable`, we always use polymorphic definitions.
347    pub fn hax_def(&mut self, item: &hax::ItemRef<'tcx>) -> Result<Arc<hax::FullDef<'tcx>>, Error> {
348        let item = if self.monomorphize() && !self.item_src.kind.is_for_trait() {
349            RustcItem::Mono(item.clone())
350        } else {
351            RustcItem::Poly(item.def_id.clone())
352        };
353        self.t_ctx.hax_def_for_item(&item)
354    }
355
356    pub(crate) fn poly_hax_def(
357        &mut self,
358        def_id: &hax::DefId,
359    ) -> Result<Arc<hax::FullDef<'tcx>>, Error> {
360        self.t_ctx.poly_hax_def(def_id)
361    }
362}
363
364impl<'tcx> Deref for ItemTransCtx<'tcx, '_> {
365    type Target = TranslateCtx<'tcx>;
366    fn deref(&self) -> &Self::Target {
367        self.t_ctx
368    }
369}
370impl<'tcx> DerefMut for ItemTransCtx<'tcx, '_> {
371    fn deref_mut(&mut self) -> &mut Self::Target {
372        self.t_ctx
373    }
374}
375
376impl<'a> IntoFormatter for &'a TranslateCtx<'_> {
377    type C = FmtCtx<'a>;
378    fn into_fmt(self) -> Self::C {
379        self.translated.into_fmt()
380    }
381}
382
383impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_> {
384    type C = FmtCtx<'a>;
385    fn into_fmt(self) -> Self::C {
386        FmtCtx {
387            translated: Some(&self.t_ctx.translated),
388            include_layouts: false,
389            include_safety: false,
390            hide_storage_statements: false,
391            current_type: None,
392            generics: self.binding_levels.map_ref(|bl| Cow::Borrowed(&bl.params)),
393            local_names: None,
394            indent_level: 0,
395        }
396    }
397}
398
399impl<'tcx> fmt::Display for TranslateCtx<'tcx> {
400    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
401        self.translated.fmt(f)
402    }
403}
charon_driver/translate/translate_ctx.rs

charon_driver/translate/
translate_ctx.rs
