Struct ItemTransCtx

pub(crate) struct ItemTransCtx<'tcx, 'ctx> {
    pub item_src: TransItemSource,
    pub item_id: Option<ItemId>,
    pub t_ctx: &'ctx mut TranslateCtx<'tcx>,
    pub hax_state_with_id: StateWithOwner<'tcx>,
    pub error_on_impl_expr_error: bool,
    pub binding_levels: BindingStack<BindingLevel>,
}

A translation context for items. Augments the TranslateCtx with type-level variables.

Fields

item_src: TransItemSource

The definition we are currently extracting.

item_id: Option<ItemId>

The id of the definition we are currently extracting, if there is one.

t_ctx: &'ctx mut TranslateCtx<'tcx>

The translation context containing the top-level definitions/ids.

hax_state_with_id: StateWithOwner<'tcx>

The Hax context with the current DefId.

error_on_impl_expr_error: bool

Whether to consider a ImplExprAtom::Error as an error for us. True except inside type aliases, because rust does not enforce correct trait bounds on type aliases.

binding_levels: BindingStack<BindingLevel>

The stack of generic parameter binders for the current context. Each binder introduces an entry in this stack, with the entry as index 0 being the innermost binder. These parameters are referenced using DeBruijnVar; see there for details.

Implementations

impl ItemTransCtx<'_, '_>

pub fn get_mir( &mut self, item_ref: &ItemRef, span: Span, ) -> Result<Option<MirBody<Unknown>>, Error>

fn get_mir_inner( &mut self, item_ref: &ItemRef, span: Span, ) -> Result<Option<MirBody<Unknown>>, Error>

impl ItemTransCtx<'_, '_>

pub fn translate_closure_info( &mut self, span: Span, args: &ClosureArgs, ) -> Result<ClosureInfo, Error>

pub fn translate_closure_bound_type_ref( &mut self, span: Span, closure: &ClosureArgs, ) -> Result<RegionBinder<TypeDeclRef>, Error>

Translate a reference to the closure ADT. The resulting type needs lifetime arguments for the upvars (captured variables). If you don’t know what to do about the bound lifetimes, use translate_closure_type_ref instead.

pub fn translate_closure_type_ref( &mut self, span: Span, closure: &ClosureArgs, ) -> Result<TypeDeclRef, Error>

Translate a reference to the closure ADT.

pub fn translate_stateless_closure_as_fn_ref( &mut self, span: Span, closure: &ClosureArgs, ) -> Result<RegionBinder<FunDeclRef>, Error>

For stateless closures, translate a function reference to the top-level function that executes the closure code without taking the state as parameter.

pub fn translate_closure_bound_impl_ref( &mut self, span: Span, closure: &ClosureArgs, target_kind: ClosureKind, ) -> Result<RegionBinder<TraitImplRef>, Error>

Translate a reference to the chosen closure impl. The resulting value needs lifetime arguments for late-bound lifetimes. If you don’t know what to do about the bound lifetimes, use translate_closure_impl_ref instead.

pub fn translate_closure_impl_ref( &mut self, span: Span, closure: &ClosureArgs, target_kind: ClosureKind, ) -> Result<TraitImplRef, Error>

Translate a reference to the chosen closure impl.

pub fn get_closure_state_ty( &mut self, span: Span, args: &ClosureArgs, ) -> Result<Ty, Error>

pub fn translate_closure_adt( &mut self, _trans_id: TypeDeclId, span: Span, args: &ClosureArgs, ) -> Result<TypeDeclKind, Error>

fn translate_closure_method_sig( &mut self, def: &FullDef, span: Span, args: &ClosureArgs, target_kind: ClosureKind, ) -> Result<FunSig, Error>

Given an item that is a closure, generate the signature of the call_once/call_mut/call method (depending on target_kind).

fn translate_closure_method_body( self, span: Span, def: &FullDef, target_kind: ClosureKind, args: &ClosureArgs, signature: &FunSig, ) -> Result<Result<Body, Opaque>, Error>

pub fn translate_closure_method( self, def_id: FunDeclId, item_meta: ItemMeta, def: &FullDef, target_kind: ClosureKind, ) -> Result<FunDecl, Error>

Given an item that is a closure, generate the call_once/call_mut/call method (depending on target_kind).

pub fn translate_closure_trait_impl( self, def_id: TraitImplId, item_meta: ItemMeta, def: &FullDef, target_kind: ClosureKind, ) -> Result<TraitImpl, Error>

pub fn translate_stateless_closure_as_fn( self, def_id: FunDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<FunDecl, Error>

Given an item that is a non-capturing closure, generate the equivalent function, by removing the state from the parameters and untupling the arguments.

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

fn translate_constant_literal_to_constant_expr_kind( &mut self, span: Span, v: &ConstantLiteral, ) -> Result<ConstantExprKind, Error>

pub(crate) fn translate_constant_expr_to_constant_expr( &mut self, span: Span, v: &ConstantExpr, ) -> Result<ConstantExpr, Error>

Remark: [hax::ConstantExpr] contains span information, but it is often the default span (i.e., it is useless), hence the additional span argument. TODO: the user_ty might be None because hax doesn’t extract it (because we are translating a ConstantExpr instead of a Constant. We need to update hax.

pub(crate) fn translate_constant_expr_to_const_generic( &mut self, span: Span, v: &ConstantExpr, ) -> Result<ConstGeneric, Error>

Remark: [hax::ConstantExpr] contains span information, but it is often the default span (i.e., it is useless), hence the additional span argument.

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource>

pub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>( &mut self, span: Span, item_src: TransItemSource, ) -> T

Register this item source and enqueue it for translation.

pub(crate) fn register_no_enqueue<T: TryFrom<ItemId>>( &mut self, span: Span, src: &TransItemSource, ) -> T

pub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>( &mut self, span: Span, enqueue: bool, item: &ItemRef, kind: TransItemSourceKind, ) -> T

Register this item and maybe enqueue it for translation.

pub(crate) fn register_item<T: TryFrom<ItemId>>( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> T

Register this item and enqueue it for translation.

pub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> T

Register this item without enqueueing it for translation.

pub(crate) fn translate_item_maybe_enqueue<T: TryFrom<DeclRef<ItemId>>>( &mut self, span: Span, enqueue: bool, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<T, Error>

Register this item and maybe enqueue it for translation.

pub(crate) fn translate_item<T: TryFrom<DeclRef<ItemId>>>( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<T, Error>

Register this item and enqueue it for translation.

Note: for FnPtrs use translate_fn_ptr instead, as this handles late-bound variables correctly. For TypeDeclRefs use translate_type_decl_ref instead, as this correctly recognizes built-in types.

pub(crate) fn translate_item_no_enqueue<T: TryFrom<DeclRef<ItemId>>>( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<T, Error>

Register this item and don’t enqueue it for translation.

pub(crate) fn translate_type_decl_ref( &mut self, span: Span, item: &ItemRef, ) -> Result<TypeDeclRef, Error>

Translate a type def id

pub(crate) fn translate_fun_item( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<MaybeBuiltinFunDeclRef, Error>

Translate a function def id

pub(crate) fn translate_fn_ptr( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<RegionBinder<FnPtr>, Error>

Auxiliary function to translate function calls and references to functions. Translate a function id applied with some substitutions.

pub(crate) fn translate_global_decl_ref( &mut self, span: Span, item: &ItemRef, ) -> Result<GlobalDeclRef, Error>

pub(crate) fn translate_trait_decl_ref( &mut self, span: Span, item: &ItemRef, ) -> Result<TraitDeclRef, Error>

pub(crate) fn translate_trait_impl_ref( &mut self, span: Span, item: &ItemRef, kind: TraitImplSource, ) -> Result<TraitImplRef, Error>

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

pub(crate) fn new( item_src: TransItemSource, item_id: Option<ItemId>, t_ctx: &'ctx mut TranslateCtx<'tcx>, ) -> Self

Create a new ExecContext.

pub fn monomorphize(&self) -> bool

Whether to monomorphize items we encounter.

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

pub fn hax_state(&self) -> &StateWithBase<'tcx>

pub fn hax_state_with_id(&self) -> &StateWithOwner<'tcx>

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

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

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

impl ItemTransCtx<'_, '_>

pub fn translate_empty_drop_method( self, def_id: FunDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<FunDecl, Error>

Translate the body of the fake Drop::drop_in_place method we’re adding to the Drop trait. It contains the drop glue for the type.

fn translate_drop_in_place_method_body( &mut self, span: Span, def: &FullDef, ) -> Result<Result<Body, Opaque>, Error>

pub fn translate_drop_in_place_method( self, def_id: FunDeclId, item_meta: ItemMeta, def: &FullDef, impl_kind: Option<TraitImplSource>, ) -> Result<FunDecl, Error>

Translate the body of the fake Drop::drop_in_place method we’re adding to the Drop trait. It contains the drop glue for the type.

pub fn prepare_drop_in_trait_method( &mut self, def: &FullDef, span: Span, drop_trait_id: TraitDeclId, impl_kind: Option<TraitImplSource>, ) -> (TraitItemName, Binder<FunDeclRef>)

pub fn translate_implicit_drop_impl( self, impl_id: TraitImplId, item_meta: ItemMeta, def: &FullDef, ) -> Result<TraitImpl, Error>

impl ItemTransCtx<'_, '_>

pub(crate) fn translate_function_signature( &mut self, def: &FullDef, item_meta: &ItemMeta, ) -> Result<FunSig, Error>

Translate a function’s signature, and initialize a body translation context at the same time - the function signature gives us the list of region and type parameters, that we put in the translation context.

pub(crate) fn build_ctor_body( &mut self, span: Span, def: &FullDef, adt_def_id: &DefId, ctor_of: &CtorOf, variant_id: usize, fields: &IndexVec<FieldIdx, FieldDef>, output_ty: &Ty, ) -> Result<Body, Error>

Generate a fake function body for ADT constructors.

pub(crate) fn recognize_builtin_fun( &mut self, item: &ItemRef, ) -> Result<Option<BuiltinFunId>, Error>

Checks whether the given id corresponds to a built-in type.

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

pub(crate) fn the_only_binder(&self) -> &BindingLevel

Get the only binding level. Panics if there are other binding levels.

pub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel

Get the only binding level. Panics if there are other binding levels.

pub(crate) fn outermost_binder(&self) -> &BindingLevel

pub(crate) fn outermost_binder_mut(&mut self) -> &mut BindingLevel

pub(crate) fn innermost_binder(&self) -> &BindingLevel

pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel

pub(crate) fn outermost_generics(&self) -> &GenericParams

pub(crate) fn outermost_generics_mut(&mut self) -> &mut GenericParams

pub(crate) fn innermost_generics(&self) -> &GenericParams

pub(crate) fn innermost_generics_mut(&mut self) -> &mut GenericParams

pub(crate) fn lookup_bound_region( &mut self, span: Span, dbid: DebruijnIndex, var: BoundVar, ) -> Result<RegionDbVar, Error>

pub(crate) fn lookup_param<Id: Copy>( &mut self, span: Span, f: impl for<'a> Fn(&'a BindingLevel) -> Option<Id>, mk_err: impl FnOnce() -> String, ) -> Result<DeBruijnVar<Id>, Error>

pub(crate) fn lookup_early_region( &mut self, span: Span, region: &EarlyParamRegion, ) -> Result<RegionDbVar, Error>

pub(crate) fn lookup_type_var( &mut self, span: Span, param: &ParamTy, ) -> Result<TypeDbVar, Error>

pub(crate) fn lookup_const_generic_var( &mut self, span: Span, param: &ParamConst, ) -> Result<ConstGenericDbVar, Error>

pub(crate) fn lookup_clause_var( &mut self, span: Span, id: usize, ) -> Result<ClauseDbVar, Error>

pub(crate) fn push_generic_params( &mut self, generics: &TyGenerics, ) -> Result<(), Error>

pub(crate) fn push_generic_param( &mut self, param: &GenericParamDef, ) -> Result<(), Error>

fn push_generics_for_def( &mut self, span: Span, def: &FullDef, is_parent: bool, ) -> Result<(), Error>

Add the generics and predicates of this item and its parents to the current context.

fn push_generics_for_def_without_parents( &mut self, _span: Span, def: &FullDef, include_late_bound: bool, ) -> Result<(), Error>

Add the generics and predicates of this item. This does not include the parent generics; use push_generics_for_def to get the full list.

pub(crate) fn translate_def_generics( &mut self, span: Span, def: &FullDef, ) -> Result<(), Error>

Translate the generics and predicates of this item and its parents. This adds generic parameters and predicates to the current environment (as a binder in self.binding_levels). This is necessary to translate types that depend on these generics (such as Ty and TraitRef). The constructed GenericParams can be recovered at the end using self.into_generics() and stored in the translated item.

pub(crate) fn translate_def_generics_without_parents( &mut self, span: Span, def: &FullDef, ) -> Result<(), Error>

Translate the generics and predicates of this item without its parents.

pub(crate) fn translate_binder_for_def<F, U>( &mut self, span: Span, kind: BinderKind, def: &FullDef, f: F, ) -> Result<Binder<U>, Error>

where F: FnOnce(&mut Self) -> Result<U, Error>,

Push a new binding level corresponding to the provided def for the duration of the inner function call.

pub(crate) fn translate_region_binder<F, T, U>( &mut self, _span: Span, binder: &Binder<T>, f: F, ) -> Result<RegionBinder<U>, Error>

where F: FnOnce(&mut Self, &T) -> Result<U, Error>,

Push a group of bound regions and call the continuation. We use this when diving into a for<'a>, or inside an arrow type (because it contains universally quantified regions).

pub(crate) fn into_generics(self) -> GenericParams

impl ItemTransCtx<'_, '_>

pub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &FullDef)

Register the items inside this module or inherent impl.

pub(crate) fn get_item_source( &mut self, span: Span, def: &FullDef, ) -> Result<ItemSource, Error>

pub fn translate_type_decl( self, trans_id: TypeDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<TypeDecl, Error>

Translate a type definition.

Note that we translate the types one by one: we don’t need to take into account the fact that some types are mutually recursive at this point (we will need to take that into account when generating the code in a file).

pub fn translate_function( self, def_id: FunDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<FunDecl, Error>

Translate one function.

pub fn translate_global( self, def_id: GlobalDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<GlobalDecl, Error>

Translate one global.

pub fn translate_trait_decl( self, def_id: TraitDeclId, item_meta: ItemMeta, def: &FullDef, ) -> Result<TraitDecl, Error>

pub fn translate_trait_impl( self, def_id: TraitImplId, item_meta: ItemMeta, def: &FullDef, ) -> Result<TraitImpl, Error>

pub fn translate_trait_alias_blanket_impl( self, def_id: TraitImplId, item_meta: ItemMeta, def: &FullDef, ) -> Result<TraitImpl, Error>

Generate a blanket impl for this trait, as in:

    trait Alias<U> = Trait<Option<U>, Item = u32> + Clone;

becomes:

    trait Alias<U>: Trait<Option<U>, Item = u32> + Clone {}
    impl<U, Self: Trait<Option<U>, Item = u32> + Clone> Alias<U> for Self {}

pub fn translate_virtual_trait_impl( &mut self, def_id: TraitImplId, item_meta: ItemMeta, vimpl: &VirtualTraitImpl, ) -> Result<TraitImpl, Error>

Make a trait impl from a hax VirtualTraitImpl. Used for constructing fake trait impls for builtin types like FnOnce.

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

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

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

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

pub(crate) fn register_predicates( &mut self, preds: &GenericPredicates, origin: PredicateOrigin, ) -> Result<(), Error>

Translates the given predicates and stores them as resuired preciates of the innermost binder.

This function should be called after we translated the generics (type parameters, regions…).

pub(crate) fn translate_predicates( &mut self, preds: &GenericPredicates, origin: PredicateOrigin, ) -> Result<GenericParams, Error>

Translates the given predicates. Returns a GenericParams that only contains predicates.

This function should be called after we translated the generics (type parameters, regions…).

pub(crate) fn translate_poly_trait_ref( &mut self, span: Span, bound_trait_ref: &Binder<TraitRef>, ) -> Result<PolyTraitDeclRef, Error>

pub(crate) fn translate_poly_trait_predicate( &mut self, span: Span, bound_trait_ref: &Binder<TraitPredicate>, ) -> Result<PolyTraitDeclRef, Error>

pub(crate) fn translate_trait_predicate( &mut self, span: Span, trait_pred: &TraitPredicate, ) -> Result<TraitDeclRef, Error>

pub(crate) fn translate_trait_ref( &mut self, span: Span, trait_ref: &TraitRef, ) -> Result<TraitDeclRef, Error>

pub(crate) fn translate_predicate( &mut self, clause: &Clause, hspan: &Span, origin: PredicateOrigin, into: &mut GenericParams, ) -> Result<(), Error>

pub(crate) fn translate_trait_impl_exprs( &mut self, span: Span, impl_sources: &[ImplExpr], ) -> Result<Vector<TraitClauseId, TraitRef>, Error>

pub(crate) fn translate_trait_impl_expr( &mut self, span: Span, impl_expr: &ImplExpr, ) -> Result<TraitRef, Error>

pub(crate) fn translate_trait_impl_expr_aux( &mut self, span: Span, impl_source: &ImplExpr, trait_decl_ref: PolyTraitDeclRef, ) -> Result<TraitRef, Error>

impl ItemTransCtx<'_, '_>

pub fn check_at_most_one_pred_has_methods( &mut self, span: Span, preds: &GenericPredicates, ) -> Result<(), Error>

pub fn translate_existential_predicates( &mut self, span: Span, self_ty: &ParamTy, preds: &GenericPredicates, region: &Region, ) -> Result<DynPredicate, Error>

impl ItemTransCtx<'_, '_>

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

Query whether a trait is dyn compatible. TODO(dyn): for now we return false if the trait has any associated types, as we don’t handle associated types in vtables.

fn pred_is_for_self(&self, tref: &TraitRef) -> bool

Check whether this trait ref is of the form Self: Trait<...>.

pub fn translate_vtable_struct_ref( &mut self, span: Span, tref: &TraitRef, ) -> Result<Option<TypeDeclRef>, Error>

pub fn translate_vtable_struct_ref_no_enqueue( &mut self, span: Span, tref: &TraitRef, ) -> Result<Option<TypeDeclRef>, Error>

pub fn translate_vtable_struct_ref_maybe_enqueue( &mut self, enqueue: bool, span: Span, tref: &TraitRef, ) -> Result<Option<TypeDeclRef>, Error>

Given a trait ref, return a reference to its vtable struct, if it is dyn compatible.

fn add_method_to_vtable_def( &mut self, span: Span, trait_def: &FullDef, mk_field: impl FnMut(String, Ty), item: &AssocItem, ) -> Result<(), Error>

Add a method_name: fn(...) -> ... field for the method.

fn add_supertraits_to_vtable_def( &mut self, span: Span, mk_field: impl FnMut(String, Ty), implied_predicates: &GenericPredicates, ) -> Result<(), Error>

Add super_trait_n: &'static SuperTraitNVTable fields.

fn gen_vtable_struct_fields( &mut self, span: Span, trait_def: &FullDef, implied_predicates: &GenericPredicates, ) -> Result<Vector<FieldId, Field>, Error>

pub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), Error>

This is a temporary check until we support dyn Trait with --monomorphize.

pub(crate) fn translate_vtable_struct( self, type_id: TypeDeclId, item_meta: ItemMeta, trait_def: &FullDef, ) -> Result<TypeDecl, Error>

Construct the type of the vtable for this trait.

It’s a struct that has for generics the generics of the trait + one parameter for each associated type of the trait and its parents.

struct TraitVTable<TraitArgs.., AssocTys..> { size: usize, align: usize, drop: fn(*mut dyn Trait<…>), method_name: fn(&dyn Trait<…>, Args..) -> Output, … other methods super_trait_0: &’static SuperTrait0VTable … other supertraits }

impl ItemTransCtx<'_, '_>

pub fn translate_vtable_instance_ref( &mut self, span: Span, trait_ref: &TraitRef, impl_ref: &ItemRef, ) -> Result<Option<GlobalDeclRef>, Error>

pub fn translate_vtable_instance_ref_no_enqueue( &mut self, span: Span, trait_ref: &TraitRef, impl_ref: &ItemRef, ) -> Result<Option<GlobalDeclRef>, Error>

pub fn translate_vtable_instance_ref_maybe_enqueue( &mut self, enqueue: bool, span: Span, trait_ref: &TraitRef, impl_ref: &ItemRef, ) -> Result<Option<GlobalDeclRef>, Error>

fn get_vtable_instance_info<'a>( &mut self, span: Span, impl_def: &'a FullDef, impl_kind: &TraitImplSource, ) -> Result<(TraitImplRef, TypeDeclRef), Error>

Local helper function to get the vtable struct reference and trait declaration reference

pub(crate) fn translate_vtable_instance( self, global_id: GlobalDeclId, item_meta: ItemMeta, impl_def: &FullDef, impl_kind: &TraitImplSource, ) -> Result<GlobalDecl, Error>

E.g.,

global {impl Trait for Foo}::vtable<Args..>: Trait::{vtable}<TraitArgs.., AssocTys..> {
    size: size_of(Foo),
    align: align_of(Foo),
    drop: <Foo as Drop>::drop,
    method_0: <Foo as Trait>::method_0::{shim},
    method_1: <Foo as Trait>::method_1::{shim},
    ...
    super_trait_0: SuperImpl0<..>::{vtable_instance}::<..>,
    super_trait_1: SuperImpl1<..>::{vtable_instance}::<..>,
    ...
}

fn add_method_to_vtable_value( &mut self, span: Span, impl_def: &FullDef, item: &ImplAssocItem, mk_field: impl FnMut(ConstantExprKind), ) -> Result<(), Error>

fn add_supertraits_to_vtable_value( &mut self, span: Span, trait_def: &FullDef, impl_def: &FullDef, mk_field: impl FnMut(ConstantExprKind), ) -> Result<(), Error>

fn gen_vtable_instance_init_body( &mut self, span: Span, impl_def: &FullDef, vtable_struct_ref: TypeDeclRef, ) -> Result<Body, Error>

Generate the body of the vtable instance function. This is for impl Trait for T implementation, it does NOT handle builtin impls.

let ret@0 : VTable;
ret@0 = VTable { ... };
return;

pub(crate) fn translate_vtable_instance_init( self, init_func_id: FunDeclId, item_meta: ItemMeta, impl_def: &FullDef, impl_kind: &TraitImplSource, ) -> Result<FunDecl, Error>

fn translate_vtable_shim_body( &mut self, span: Span, target_receiver: &Ty, shim_signature: &FunSig, impl_func_def: &FullDef, ) -> Result<Body, Error>

The target vtable shim body looks like:

local ret@0 : ReturnTy;
// the shim receiver of this shim function
local shim_self@1 : ShimReceiverTy;
// the arguments of the impl function
local arg1@2 : Arg1Ty;
...
local argN@N : ArgNTy;
// the target receiver of the impl function
local target_self@(N+1) : TargetReceiverTy;
// perform some conversion to cast / re-box the shim receiver to the target receiver
...
target_self@(N+1) := concretize_cast<ShimReceiverTy, TargetReceiverTy>(shim_self@1);
// call the impl function and assign the result to ret@0
ret@0 := impl_func(target_self@(N+1), arg1@2, ..., argN@N);

pub(crate) fn translate_vtable_shim( self, fun_id: FunDeclId, item_meta: ItemMeta, impl_func_def: &FullDef, ) -> Result<FunDecl, Error>

impl<'tcx, 'ctx> ItemTransCtx<'tcx, 'ctx>

pub(crate) fn translate_region( &mut self, span: Span, region: &Region, ) -> Result<Region, Error>

pub(crate) fn translate_hax_int_ty(int_ty: &IntTy) -> IntTy

pub(crate) fn translate_hax_uint_ty(uint_ty: &UintTy) -> UIntTy

pub(crate) fn translate_ty(&mut self, span: Span, ty: &Ty) -> Result<Ty, Error>

Translate a Ty.

Typically used in this module to translate the fields of a structure/ enumeration definition, or later to translate the type of a variable.

Note that we take as parameter a function to translate regions, because regions can be translated in several manners (non-erased region or erased regions), in which case the return type is different.

fn translate_ty_inner(&mut self, span: Span, ty: &Ty) -> Result<Ty, Error>

pub fn translate_fun_sig( &mut self, span: Span, sig: &Binder<TyFnSig>, ) -> Result<RegionBinder<(Vec<Ty>, Ty)>, Error>

pub fn translate_generic_args( &mut self, span: Span, substs: &[GenericArg], trait_refs: &[ImplExpr], ) -> Result<GenericArgs, Error>

Translate generic args. Don’t call directly; use translate_xxx_ref as much as possible.

pub fn append_late_bound_to_generics( &mut self, span: Span, generics: GenericArgs, late_bound: Option<Binder<()>>, ) -> Result<RegionBinder<GenericArgs>, Error>

Append the given late bound variables to the provided generics.

pub(crate) fn recognize_builtin_type( &mut self, item: &ItemRef, ) -> Result<Option<BuiltinTy>, Error>

Checks whether the given id corresponds to a built-in type.

pub fn translate_ptr_metadata( &mut self, span: Span, item: &ItemRef, ) -> Result<PtrMetadata, Error>

Translate a Dynamically Sized Type metadata kind.

Returns None if the type is generic, or if it is not a DST.

pub fn translate_layout(&self, item: &ItemRef) -> Option<Layout>

Translate a type layout.

Translates the layout as queried from rustc into the more restricted Layout.

pub fn generate_naive_layout( &self, span: Span, ty: &TypeDeclKind, ) -> Result<Layout, Error>

Generate a naive layout for this type.

pub(crate) fn translate_adt_def( &mut self, trans_id: TypeDeclId, def_span: Span, item_meta: &ItemMeta, def: &FullDef, ) -> Result<TypeDeclKind, Error>

Translate the body of a type declaration.

Note that the type may be external, in which case we translate the body only if it is public (i.e., it is a public enumeration, or it is a struct with only public fields).

fn translate_discriminant( &mut self, def_span: Span, discr: &DiscriminantValue, ) -> Result<Literal, Error>

pub fn translate_repr_options( &mut self, hax_repr_options: &ReprOptions, ) -> ReprOptions

Methods from Deref<Target = 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 register_target_info(&mut self)

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,

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.

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

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

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

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> Deref for ItemTransCtx<'tcx, '_>

type Target = TranslateCtx<'tcx>

The resulting type after dereferencing.

fn deref(&self) -> &Self::Target

Dereferences the value.

impl<'tcx> DerefMut for ItemTransCtx<'tcx, '_>

fn deref_mut(&mut self) -> &mut Self::Target

Mutably dereferences the value.

impl<'a> IntoFormatter for &'a ItemTransCtx<'_, '_>

type C = FmtCtx<'a>

fn into_fmt(self) -> Self::C