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 id_map: HashMap<TransItemSource, AnyTransId>,
    pub reverse_id_map: HashMap<AnyTransId, TransItemSource>,
    pub file_to_id: HashMap<FileName, FileId>,
    pub errors: RefCell<ErrorCtx>,
    pub items_to_translate: BTreeSet<TransItemSource>,
    pub processed: HashSet<TransItemSource>,
    pub cached_names: HashMap<DefId, Name>,
    pub cached_item_metas: HashMap<DefId, 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.

id_map: HashMap<TransItemSource, AnyTransId>

The map from rustc id to translated id.

reverse_id_map: HashMap<AnyTransId, 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).

cached_names: HashMap<DefId, Name>

Cache the names to compute them only once each.

cached_item_metas: HashMap<DefId, ItemMeta>

Cache the ItemMetas to compute them only once each.

Implementations

impl TranslateCtx<'_>

pub fn get_mir( &mut self, def_id: &DefId, span: Span, ) -> Result<Option<MirBody<()>>, Error>

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

fn register_module_item(&mut self, def_id: &DefId)

Register a HIR item and all its children. We call this on the crate root items and end up exploring the whole crate.

fn register_module( &mut self, item_meta: ItemMeta, def: &FullDef, ) -> Result<(), Error>

Register the items inside this module.

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

pub(crate) fn translate_item_aux( &mut self, def_id: &DefId, trans_id: Option<AnyTransId>, ) -> Result<(), Error>

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

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

Span an error and register the error.

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.

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

pub fn hax_def_id_to_name(&mut self, def_id: &DefId) -> Result<Name, Error>

Retrieve an item name from a [DefId]. 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 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 hax_def(&mut self, def_id: &DefId) -> Result<Arc<FullDef>, Error>

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

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

Compute the meta information for a Rust item.

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

pub fn translate_raw_span(&mut self, rspan: &Span) -> RawSpan

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

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 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 opacity_for_name(&self, name: &Name) -> ItemOpacity

pub(crate) fn register_id_no_enqueue( &mut self, src: &Option<DepSource>, id: TransItemSource, ) -> AnyTransId

pub(crate) fn register_and_enqueue_id( &mut self, src: &Option<DepSource>, id: TransItemSource, ) -> AnyTransId

Register this id and enqueue it for translation.

pub(crate) fn register_type_decl_id( &mut self, src: &Option<DepSource>, id: &DefId, ) -> TypeDeclId

pub(crate) fn register_fun_decl_id( &mut self, src: &Option<DepSource>, id: &DefId, ) -> FunDeclId

pub(crate) fn register_trait_decl_id( &mut self, src: &Option<DepSource>, id: &DefId, ) -> TraitDeclId

pub(crate) fn register_trait_impl_id( &mut self, src: &Option<DepSource>, id: &DefId, ) -> TraitImplId

pub(crate) fn register_global_decl_id( &mut self, src: &Option<DepSource>, id: &DefId, ) -> GlobalDeclId

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

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

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

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)

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