Struct TranslateCtx

pub struct TranslateCtx<'tcx> {

    pub tcx: TyCtxt<'tcx>,
    pub sysroot: PathBuf,
    pub hax_state: StateWithBase<'tcx>,
    pub options: TranslateOptions,
    pub translated: TranslatedCrate,
    pub method_status: Vector<TraitDeclId, HashMap<TraitItemName, MethodStatus>>,
    pub id_map: HashMap<TransItemSource, ItemId>,
    pub reverse_id_map: HashMap<ItemId, TransItemSource>,
    pub file_to_id: HashMap<FileName, FileId>,
    pub errors: RefCell<ErrorCtx>,
    pub items_to_translate: BTreeSet<TransItemSource>,
    pub processed: HashSet<TransItemSource>,
    pub translate_stack: Vec<ItemId>,
    pub cached_names: HashMap<RustcItem, Name>,
    pub cached_item_metas: HashMap<TransItemSource, ItemMeta>,
}

Translation context used while translating the crate data into our representation.

Fields

tcx: TyCtxt<'tcx>

The Rust compiler type context

sysroot: PathBuf

Path to the toolchain root.

hax_state: StateWithBase<'tcx>

The Hax context

options: TranslateOptions

The options that control translation.

translated: TranslatedCrate

The translated data.

method_status: Vector<TraitDeclId, HashMap<TraitItemName, MethodStatus>>

Record data for each method whether it is ever used (called or implemented) and the FunDeclIds of the implementations. We use this to lazily translate methods, so that we skip unused default methods of large traits like Iterator.

The complete scheme works as follows: by default we enqueue no methods for translation. When we find a use of a method, we mark it “used” using mark_method_as_used. This enqueues all known and future impls of this method. We also mark a method as used if we find an implementation of it in a non-opaque impl, and if the method is a required method.

id_map: HashMap<TransItemSource, ItemId>

The map from rustc id to translated id.

reverse_id_map: HashMap<ItemId, TransItemSource>

The reverse map of ids.

file_to_id: HashMap<FileName, FileId>

The reverse filename map.

errors: RefCell<ErrorCtx>

Context for tracking and reporting errors.

items_to_translate: BTreeSet<TransItemSource>

The declarations we came accross and which we haven’t translated yet. We keep them sorted to make the output order a bit more stable.

processed: HashSet<TransItemSource>

The declaration we’ve already processed (successfully or not).

translate_stack: Vec<ItemId>

Stack of the translations currently happening. Used to avoid accidental cycles.

cached_names: HashMap<RustcItem, Name>

Cache the names to compute them only once each.

cached_item_metas: HashMap<TransItemSource, ItemMeta>

Cache the ItemMetas to compute them only once each.

Implementations

impl<'tcx, 'ctx> TranslateCtx<'tcx>

pub fn base_kind_for_item( &mut self, def_id: &DefId, ) -> Option<TransItemSourceKind>

Returns the default translation kind for the given DefId. Returns None for items that we don’t translate. Errors on unexpected items.

pub fn enqueue_module_item(&mut self, def_id: &DefId)

Add this item to the queue of items to translate. Each translated item will then recursively register the items it refers to. We call this on the crate root and end up exploring the whole crate.

pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>( &mut self, dep_src: &Option<DepSource>, src: &TransItemSource, ) -> Option<T>

pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>( &mut self, dep_src: &Option<DepSource>, item_src: TransItemSource, ) -> Option<T>

Register this item source and enqueue it for translation.

pub(crate) fn enqueue_id(&mut self, id: impl Into<ItemId>)

Enqueue an item from its id.

pub(crate) fn register_target_info(&mut self)

impl<'tcx, 'ctx> TranslateCtx<'tcx>

pub fn span_err(&self, span: Span, msg: &str, level: Level<'_>) -> Error

Span an error and register the error.

pub fn catch_sinto<S, T, U>( &mut self, s: &S, span: Span, x: &T, ) -> Result<U, Error>

where T: Debug + SInto<S, U>,

Translates T into U using hax’s SInto trait, catching any hax panics.

pub fn poly_hax_def(&mut self, def_id: &DefId) -> Result<Arc<FullDef>, Error>

Return the polymorphic definition for this item. Use with care, prefer hax_def whenever possible.

Used for computing names, for associated items, and for various checks.

pub fn hax_def_for_item( &mut self, item: &RustcItem, ) -> Result<Arc<FullDef>, Error>

Return the definition for this item. This uses the polymorphic or monomorphic definition depending on user choice.

pub(crate) fn with_def_id<F, T>( &mut self, def_id: &DefId, item_id: Option<ItemId>, f: F, ) -> T

where F: FnOnce(&mut Self) -> T,

impl<'tcx, 'ctx> TranslateCtx<'tcx>

pub(crate) fn translate_item(&mut self, item_src: &TransItemSource)

pub(crate) fn translate_item_aux( &mut self, item_src: &TransItemSource, trans_id: Option<ItemId>, ) -> Result<(), Error>

pub(crate) fn get_or_translate( &mut self, id: ItemId, ) -> Result<ItemRef<'_>, Error>

While translating an item you may need the contents of another. Use this to retreive the translated version of this item. Use with care as this could create cycles.

pub fn translate_unit_metadata_const(&mut self)

Add a const UNIT: () = (); const, used as metadata for thin pointers/references.

pub fn remove_unused_methods(&mut self)

Keep only the methods we marked as “used”.

impl<'tcx, 'ctx> TranslateCtx<'tcx>

fn register_file(&mut self, filename: FileName, span: Span) -> FileId

Register a file if it is a “real” file and was not already registered span must be a span from which we obtained that filename.

pub fn translate_filename(&mut self, name: &FileName) -> FileName

pub fn translate_span_data(&mut self, rspan: &Span) -> SpanData

pub fn translate_span_from_source_info( &mut self, source_scopes: &IndexVec<SourceScope, SourceScopeData>, source_info: &SourceInfo, ) -> Span

Compute span data from a Rust source scope

pub(crate) fn translate_span_from_hax(&mut self, span: &Span) -> Span

pub(crate) fn def_span(&mut self, def_id: &DefId) -> Span

impl<'tcx, 'ctx> TranslateCtx<'tcx>

fn path_elem_for_def( &mut self, span: Span, item: &RustcItem, ) -> Result<Option<PathElem>, Error>

fn name_for_item(&mut self, item: &RustcItem) -> Result<Name, Error>

Retrieve the name for this [hax::DefId]. Because a given DefId may give rise to several charon items, prefer to use translate_name when possible.

We lookup the path associated to an id, and convert it to a name. Paths very precisely identify where an item is. There are important subcases, like the items in an Impl block:

impl<T> List<T> {
  fn new() ...
}

One issue here is that “List” doesn’t appear in the path, which would look like the following:

TypeNS("Crate") :: Impl :: ValueNs("new") ^^^ This is where “List” should be

For this reason, whenever we find an Impl path element, we actually lookup the type of the sub-path, from which we can derive a name.

Besides, as there may be several “impl” blocks for one type, each impl block is identified by a unique number (rustc calls this a “disambiguator”), which we grab.

Example:

For instance, if we write the following code in crate test and module bla:

impl<T> Foo<T> {
  fn foo() { ... }
}

impl<T> Foo<T> {
  fn bar() { ... }
}

The names we will generate for foo and bar are: [Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(0)), Ident("foo")] [Ident("test"), Ident("bla"), Ident("Foo"), Impl(impl<T> Ty<T>, Disambiguator(1)), Ident("bar")]

pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error>

Compute the name for an item. Internal function, use translate_name.

pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error>

Retrieve the name for an item.

pub(crate) fn translate_trait_item_name( &mut self, def_id: &DefId, ) -> Result<TraitItemName, Error>

Remark: this doesn’t register the def id (on purpose)

pub(crate) fn opacity_for_name(&self, name: &Name) -> ItemOpacity

impl<'tcx, 'ctx> TranslateCtx<'tcx>

pub(crate) fn translate_attribute( &mut self, attr: &Attribute, ) -> Option<Attribute>

Translates a rust attribute. Returns None if the attribute is a doc comment (rustc encodes them as attributes). For now we use Strings for Attributes.

pub(crate) fn translate_inline(&self, def: &FullDef) -> Option<InlineAttr>

pub(crate) fn translate_attr_info(&mut self, def: &FullDef) -> AttrInfo

impl<'tcx, 'ctx> TranslateCtx<'tcx>

pub(crate) fn is_extern_item(&mut self, def: &FullDef) -> bool

Whether this item is in an extern { .. } block, in which case it has no body.

pub(crate) fn translate_item_meta( &mut self, def: &FullDef, item_src: &TransItemSource, name: Name, name_opacity: ItemOpacity, ) -> ItemMeta

Compute the meta information for a Rust item.

Trait Implementations

impl<'tcx, 'ctx> Display for TranslateCtx<'tcx>

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl<'a> IntoFormatter for &'a TranslateCtx<'_>

type C = FmtCtx<'a>

fn into_fmt(self) -> Self::C