Struct BodyTransCtx

pub(crate) struct BodyTransCtx<'tcx, 'tctx, 'ictx> {
    pub i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>,
    pub locals: Locals,
    pub locals_map: HashMap<usize, LocalId>,
    pub blocks: Vector<BlockId, BlockData>,
    pub blocks_map: HashMap<BasicBlock, BlockId>,
    pub blocks_stack: VecDeque<BasicBlock>,
}

A translation context for function bodies.

Fields

i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>

The translation context for the item.

locals: Locals

The (regular) variables in the current function body.

locals_map: HashMap<usize, LocalId>

The map from rust variable indices to translated variables indices.

blocks: Vector<BlockId, BlockData>

The translated blocks.

blocks_map: HashMap<BasicBlock, BlockId>

The map from rust blocks to translated blocks. Note that when translating terminators like DropAndReplace, we might have to introduce new blocks which don’t appear in the original MIR.

blocks_stack: VecDeque<BasicBlock>

We register the blocks to translate in a stack, so as to avoid writing the translation functions as recursive functions. We do so because we had stack overflows in the past.

Implementations

impl<'tcx, 'tctx, 'ictx> BodyTransCtx<'tcx, 'tctx, 'ictx>

pub(crate) fn new(i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>) -> Self

impl BodyTransCtx<'_, '_, '_>

pub(crate) fn translate_local(&self, local: &Local) -> Option<LocalId>

pub(crate) fn push_var(&mut self, rid: usize, ty: Ty, name: Option<String>)

fn translate_binaryop_kind( &mut self, _span: Span, binop: BinOp, ) -> Result<BinOp, Error>

fn translate_body_locals( &mut self, body: &MirBody<Unknown>, ) -> Result<(), Error>

Translate a function’s local variables by adding them in the environment.

fn translate_basic_block_id(&mut self, block_id: BasicBlock) -> BlockId

Translate a basic block id and register it, if it hasn’t been done.

fn translate_basic_block( &mut self, body: &MirBody<Unknown>, block: &BasicBlockData, ) -> Result<BlockData, Error>

fn translate_place(&mut self, span: Span, place: &Place) -> Result<Place, Error>

Translate a place TODO: Hax represents places in a different manner than MIR. We should update our representation of places to match the Hax representation.

fn translate_operand_with_type( &mut self, span: Span, operand: &Operand, ) -> Result<(Operand, Ty), Error>

Translate an operand with its type

fn translate_operand( &mut self, span: Span, operand: &Operand, ) -> Result<Operand, Error>

Translate an operand

fn translate_rvalue( &mut self, span: Span, rvalue: &Rvalue, tgt_ty: &Ty, ) -> Result<Rvalue, Error>

Translate an rvalue

fn translate_statement( &mut self, body: &MirBody<Unknown>, statement: &Statement, ) -> Result<Option<Statement>, Error>

Translate a statement

We return an option, because we ignore some statements (Nop, StorageLive…)

fn translate_terminator( &mut self, body: &MirBody<Unknown>, terminator: &Terminator, statements: &mut Vec<Statement>, ) -> Result<Terminator, Error>

Translate a terminator

fn translate_switch_targets( &mut self, span: Span, switch_ty: &Ty, targets: &[(ScalarInt, BasicBlock)], otherwise: &BasicBlock, ) -> Result<SwitchTargets, Error>

Translate switch targets

fn translate_function_call( &mut self, span: Span, fun: &FunOperand, args: &Vec<Spanned<Operand>>, destination: &Place, target: &Option<BasicBlock>, unwind: &UnwindAction, ) -> Result<TerminatorKind, Error>

Translate a function call statement. Note that body is the body of the function being translated, not of the function referenced in the function call: we need it in order to translate the blocks we go to after the function call returns.

fn translate_arguments( &mut self, span: Span, args: &Vec<Spanned<Operand>>, ) -> Result<Vec<Operand>, Error>

Evaluate function arguments in a context, and return the list of computed values.

fn translate_body_comments( &mut self, source_text: &Option<String>, charon_span: Span, ) -> Vec<(usize, Vec<String>)>

Gather all the lines that start with // inside the given span.

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

Translate the MIR body of this definition if it has one.

pub fn translate_body( &mut self, span: Span, body: &MirBody<Unknown>, source_text: &Option<String>, ) -> Result<Result<Body, Opaque>, Error>

Translate a function body.

fn translate_body_aux( &mut self, body: &MirBody<Unknown>, source_text: &Option<String>, ) -> Result<Result<Body, Opaque>, Error>

Methods from Deref<Target = ItemTransCtx<'tcx, 'tctx>>

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>

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_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.

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<ItemRef<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<ItemRef<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<ItemRef<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>

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>

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

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(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.

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 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_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.

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

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

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>

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>

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 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

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;

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_region( &mut self, span: Span, region: &Region, ) -> Result<Region, Error>

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, 'tctx, 'ictx> Deref for BodyTransCtx<'tcx, 'tctx, 'ictx>

type Target = ItemTransCtx<'tcx, 'tctx>

The resulting type after dereferencing.

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

Dereferences the value.

impl<'tcx, 'tctx, 'ictx> DerefMut for BodyTransCtx<'tcx, 'tctx, 'ictx>

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

Mutably dereferences the value.

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

type C = FmtCtx<'a>

fn into_fmt(self) -> Self::C