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: IndexMap<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: VecDeque<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: IndexMap<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: VecDeque<TransItemSource>

The declarations we came accross and which we haven’t translated yet.

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> 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, span: 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(&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>

fn parse_attr_from_raw( &mut self, def_id: &DefId, raw_attr: RawAttribute, ) -> Result<Attribute, String>

Parse a raw attribute to recognize our special charon::*, aeneas::* and verify::* attributes.

fn parse_special_attr( &mut self, def_id: &DefId, attr_name: &str, raw_attr: &RawAttribute, ) -> Result<Option<Attribute>, String>

Parse a charon::*, aeneas::* or verify::* attribute.

pub(crate) fn translate_attribute( &mut self, def_id: &DefId, 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.

impl<'tcx> TranslateCtx<'tcx>

pub fn recognize_builtin_impl( &self, trait_data: &BuiltinTraitData, trait_def: &FullDef, ) -> Option<BuiltinImplData>

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

impl<'tcx> Visitor<'tcx> for TranslateCtx<'tcx>

fn visit_nested_item(&mut self, id: ItemId)

Invoked when a nested item is encountered. By default, when Self::NestedFilter is nested_filter::None, this method does nothing. You probably don’t want to override this method – instead, override [Self::NestedFilter] or use the “shallow” or “deep” visit patterns described at [rustc_hir::intravisit]. The only reason to override this method is if you want a nested pattern but cannot supply a TyCtxt; see maybe_tcx for advice.

type MaybeTyCtxt = <Self::NestedFilter as NestedFilter<'v>>::MaybeTyCtxt

type NestedFilter = None

Override this type to control which nested HIR are visited; see [NestedFilter] for details. If you override this type, you must also override maybe_tcx.

type Result = ()

The result type of the visit_* methods. Can be either (), or ControlFlow<T>.

fn maybe_tcx(&mut self) -> Self::MaybeTyCtxt

If type NestedFilter is set to visit nested items, this method must also be overridden to provide a map to retrieve nested items.

fn visit_nested_trait_item(&mut self, id: TraitItemId) -> Self::Result

Like visit_nested_item(), but for trait items. See visit_nested_item() for advice on when to override this method.

fn visit_nested_impl_item(&mut self, id: ImplItemId) -> Self::Result

Like visit_nested_item(), but for impl items. See visit_nested_item() for advice on when to override this method.

fn visit_nested_foreign_item(&mut self, id: ForeignItemId) -> Self::Result

Like visit_nested_item(), but for foreign items. See visit_nested_item() for advice on when to override this method.

fn visit_nested_body(&mut self, id: BodyId) -> Self::Result

Invoked to visit the body of a function, method or closure. Like visit_nested_item, does nothing by default unless you override Self::NestedFilter.

fn visit_param(&mut self, param: &'v Param<'v>) -> Self::Result

fn visit_item(&mut self, i: &'v Item<'v>) -> Self::Result

Visits the top-level item and (optionally) nested items / impl items. See visit_nested_item for details.

fn visit_body(&mut self, b: &Body<'v>) -> Self::Result

fn visit_id(&mut self, _hir_id: HirId) -> Self::Result

fn visit_name(&mut self, _name: Symbol) -> Self::Result

fn visit_ident(&mut self, ident: Ident) -> Self::Result

fn visit_mod(&mut self, m: &'v Mod<'v>, _s: Span, _n: HirId) -> Self::Result

fn visit_foreign_item(&mut self, i: &'v ForeignItem<'v>) -> Self::Result

fn visit_local(&mut self, l: &'v LetStmt<'v>) -> Self::Result

fn visit_block(&mut self, b: &'v Block<'v>) -> Self::Result

fn visit_stmt(&mut self, s: &'v Stmt<'v>) -> Self::Result

fn visit_arm(&mut self, a: &'v Arm<'v>) -> Self::Result

fn visit_pat(&mut self, p: &'v Pat<'v>) -> Self::Result

fn visit_pat_field(&mut self, f: &'v PatField<'v>) -> Self::Result

fn visit_pat_expr(&mut self, expr: &'v PatExpr<'v>) -> Self::Result

fn visit_lit( &mut self, _hir_id: HirId, _lit: Spanned<LitKind>, _negated: bool, ) -> Self::Result

fn visit_anon_const(&mut self, c: &'v AnonConst) -> Self::Result

fn visit_inline_const(&mut self, c: &'v ConstBlock) -> Self::Result

fn visit_generic_arg(&mut self, generic_arg: &'v GenericArg<'v>) -> Self::Result

fn visit_ty(&mut self, t: &'v Ty<'v, AmbigArg>) -> Self::Result

All types are treated as ambiguous types for the purposes of hir visiting in order to ensure that visitors can handle infer vars without it being too error-prone.

fn visit_const_item_rhs(&mut self, c: ConstItemRhs<'v>) -> Self::Result

fn visit_const_arg(&mut self, c: &'v ConstArg<'v, AmbigArg>) -> Self::Result

All consts are treated as ambiguous consts for the purposes of hir visiting in order to ensure that visitors can handle infer vars without it being too error-prone.

fn visit_infer( &mut self, inf_id: HirId, inf_span: Span, kind: InferKind<'v>, ) -> Self::Result

fn visit_lifetime(&mut self, lifetime: &'v Lifetime) -> Self::Result

fn visit_expr(&mut self, ex: &'v Expr<'v>) -> Self::Result

fn visit_expr_field(&mut self, field: &'v ExprField<'v>) -> Self::Result

fn visit_pattern_type_pattern(&mut self, p: &'v TyPat<'v>) -> Self::Result

fn visit_generic_param(&mut self, p: &'v GenericParam<'v>) -> Self::Result

fn visit_const_param_default( &mut self, _param: HirId, ct: &'v ConstArg<'v>, ) -> Self::Result

fn visit_generics(&mut self, g: &'v Generics<'v>) -> Self::Result

fn visit_where_predicate( &mut self, predicate: &'v WherePredicate<'v>, ) -> Self::Result

fn visit_fn_ret_ty(&mut self, ret_ty: &'v FnRetTy<'v>) -> Self::Result

fn visit_fn_decl(&mut self, fd: &'v FnDecl<'v>) -> Self::Result

fn visit_fn( &mut self, fk: FnKind<'v>, fd: &'v FnDecl<'v>, b: BodyId, _: Span, id: LocalDefId, ) -> Self::Result

fn visit_use( &mut self, path: &'v Path<'v, PerNS<Option<Res>>>, hir_id: HirId, ) -> Self::Result

fn visit_trait_item(&mut self, ti: &'v TraitItem<'v>) -> Self::Result

fn visit_trait_item_ref(&mut self, ii: &'v TraitItemId) -> Self::Result

fn visit_impl_item(&mut self, ii: &'v ImplItem<'v>) -> Self::Result

fn visit_foreign_item_ref(&mut self, ii: &'v ForeignItemId) -> Self::Result

fn visit_impl_item_ref(&mut self, ii: &'v ImplItemId) -> Self::Result

fn visit_trait_ref(&mut self, t: &'v TraitRef<'v>) -> Self::Result

fn visit_param_bound(&mut self, bounds: &'v GenericBound<'v>) -> Self::Result

fn visit_precise_capturing_arg( &mut self, arg: &'v PreciseCapturingArgKind<&'v Lifetime, PreciseCapturingNonLifetimeArg>, ) -> Self::Result

fn visit_poly_trait_ref(&mut self, t: &'v PolyTraitRef<'v>) -> Self::Result

fn visit_opaque_ty(&mut self, opaque: &'v OpaqueTy<'v>) -> Self::Result

fn visit_variant_data(&mut self, s: &'v VariantData<'v>) -> Self::Result

fn visit_field_def(&mut self, s: &'v FieldDef<'v>) -> Self::Result

fn visit_enum_def(&mut self, enum_definition: &'v EnumDef<'v>) -> Self::Result

fn visit_variant(&mut self, v: &'v Variant<'v>) -> Self::Result

fn visit_label(&mut self, label: &'v Label) -> Self::Result

fn visit_qpath( &mut self, qpath: &'v QPath<'v>, id: HirId, _span: Span, ) -> Self::Result

fn visit_path(&mut self, path: &Path<'v>, _id: HirId) -> Self::Result

fn visit_path_segment( &mut self, path_segment: &'v PathSegment<'v>, ) -> Self::Result

fn visit_generic_args( &mut self, generic_args: &'v GenericArgs<'v>, ) -> Self::Result

fn visit_assoc_item_constraint( &mut self, constraint: &'v AssocItemConstraint<'v>, ) -> Self::Result

fn visit_attribute(&mut self, _attr: &'v Attribute) -> Self::Result

fn visit_defaultness(&mut self, defaultness: &'v Defaultness) -> Self::Result

fn visit_inline_asm( &mut self, asm: &'v InlineAsm<'v>, id: HirId, ) -> Self::Result