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>,
}
Expand description
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§
Source§impl<'tcx, 'tctx, 'ictx> BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> BodyTransCtx<'tcx, 'tctx, 'ictx>
pub(crate) fn new(i_ctx: &'ictx mut ItemTransCtx<'tcx, 'tctx>) -> Self
Source§impl BodyTransCtx<'_, '_, '_>
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>
Sourcefn translate_body_locals(
&mut self,
body: &MirBody<Unknown>,
) -> Result<(), Error>
fn translate_body_locals( &mut self, body: &MirBody<Unknown>, ) -> Result<(), Error>
Translate a function’s local variables by adding them in the environment.
Sourcefn translate_basic_block_id(&mut self, block_id: BasicBlock) -> BlockId
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>
Sourcefn translate_place(&mut self, span: Span, place: &Place) -> Result<Place, 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.
Sourcefn translate_operand_with_type(
&mut self,
span: Span,
operand: &Operand,
) -> Result<(Operand, Ty), Error>
fn translate_operand_with_type( &mut self, span: Span, operand: &Operand, ) -> Result<(Operand, Ty), Error>
Translate an operand with its type
Sourcefn translate_operand(
&mut self,
span: Span,
operand: &Operand,
) -> Result<Operand, Error>
fn translate_operand( &mut self, span: Span, operand: &Operand, ) -> Result<Operand, Error>
Translate an operand
Sourcefn translate_rvalue(
&mut self,
span: Span,
rvalue: &Rvalue,
tgt_ty: &Ty,
) -> Result<Rvalue, Error>
fn translate_rvalue( &mut self, span: Span, rvalue: &Rvalue, tgt_ty: &Ty, ) -> Result<Rvalue, Error>
Translate an rvalue
Sourcefn translate_statement(
&mut self,
body: &MirBody<Unknown>,
statement: &Statement,
) -> Result<Option<Statement>, Error>
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
…)
Sourcefn translate_terminator(
&mut self,
body: &MirBody<Unknown>,
terminator: &Terminator,
statements: &mut Vec<Statement>,
) -> Result<Terminator, Error>
fn translate_terminator( &mut self, body: &MirBody<Unknown>, terminator: &Terminator, statements: &mut Vec<Statement>, ) -> Result<Terminator, Error>
Translate a terminator
Sourcefn translate_switch_targets(
&mut self,
span: Span,
switch_ty: &Ty,
targets: &[(ScalarInt, BasicBlock)],
otherwise: &BasicBlock,
) -> Result<SwitchTargets, Error>
fn translate_switch_targets( &mut self, span: Span, switch_ty: &Ty, targets: &[(ScalarInt, BasicBlock)], otherwise: &BasicBlock, ) -> Result<SwitchTargets, Error>
Translate switch targets
Sourcefn translate_function_call(
&mut self,
span: Span,
fun: &FunOperand,
args: &Vec<Spanned<Operand>>,
destination: &Place,
target: &Option<BasicBlock>,
unwind: &UnwindAction,
) -> Result<TerminatorKind, Error>
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.
Sourcefn translate_arguments(
&mut self,
span: Span,
args: &Vec<Spanned<Operand>>,
) -> Result<Vec<Operand>, Error>
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.
Sourcefn translate_body_comments(
&mut self,
source_text: &Option<String>,
charon_span: Span,
) -> Vec<(usize, Vec<String>)>
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.
Sourcepub fn translate_def_body(
&mut self,
span: Span,
def: &FullDef,
) -> Result<Result<Body, Opaque>, Error>
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.
Sourcepub fn translate_body(
&mut self,
span: Span,
body: &MirBody<Unknown>,
source_text: &Option<String>,
) -> Result<Result<Body, Opaque>, Error>
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>
Sourcepub fn translate_closure_bound_type_ref(
&mut self,
span: Span,
closure: &ClosureArgs,
) -> Result<RegionBinder<TypeDeclRef>, 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.
Sourcepub fn translate_closure_type_ref(
&mut self,
span: Span,
closure: &ClosureArgs,
) -> Result<TypeDeclRef, Error>
pub fn translate_closure_type_ref( &mut self, span: Span, closure: &ClosureArgs, ) -> Result<TypeDeclRef, Error>
Translate a reference to the closure ADT.
Sourcepub fn translate_stateless_closure_as_fn_ref(
&mut self,
span: Span,
closure: &ClosureArgs,
) -> Result<RegionBinder<FunDeclRef>, Error>
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.
Sourcepub fn translate_closure_bound_impl_ref(
&mut self,
span: Span,
closure: &ClosureArgs,
target_kind: ClosureKind,
) -> Result<RegionBinder<TraitImplRef>, Error>
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.
Sourcepub fn translate_closure_impl_ref(
&mut self,
span: Span,
closure: &ClosureArgs,
target_kind: ClosureKind,
) -> Result<TraitImplRef, Error>
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>
Sourcefn translate_closure_method_sig(
&mut self,
def: &FullDef,
span: Span,
args: &ClosureArgs,
target_kind: ClosureKind,
) -> Result<FunSig, 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>
Sourcepub(crate) fn translate_constant_expr_to_constant_expr(
&mut self,
span: Span,
v: &ConstantExpr,
) -> Result<ConstantExpr, 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.
Sourcepub(crate) fn translate_constant_expr_to_const_generic(
&mut self,
span: Span,
v: &ConstantExpr,
) -> Result<ConstGeneric, Error>
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>
Sourcepub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
&mut self,
span: Span,
item_src: TransItemSource,
) -> T
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
Sourcepub(crate) fn register_item_maybe_enqueue<T: TryFrom<ItemId>>(
&mut self,
span: Span,
enqueue: bool,
item: &ItemRef,
kind: TransItemSourceKind,
) -> 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.
Sourcepub(crate) fn register_item<T: TryFrom<ItemId>>(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> T
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.
Sourcepub(crate) fn register_item_no_enqueue<T: TryFrom<ItemId>>(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> T
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.
Sourcepub(crate) fn translate_item_maybe_enqueue<T: TryFrom<ItemRef<ItemId>>>(
&mut self,
span: Span,
enqueue: bool,
item: &ItemRef,
kind: TransItemSourceKind,
) -> Result<T, Error>
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.
Sourcepub(crate) fn translate_item<T: TryFrom<ItemRef<ItemId>>>(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> Result<T, Error>
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 FnPtr
s use translate_fn_ptr
instead, as this handles late-bound variables
correctly. For TypeDeclRef
s use translate_type_decl_ref
instead, as this correctly
recognizes built-in types.
Sourcepub(crate) fn translate_item_no_enqueue<T: TryFrom<ItemRef<ItemId>>>(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> Result<T, Error>
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.
Sourcepub(crate) fn translate_type_decl_ref(
&mut self,
span: Span,
item: &ItemRef,
) -> Result<TypeDeclRef, Error>
pub(crate) fn translate_type_decl_ref( &mut self, span: Span, item: &ItemRef, ) -> Result<TypeDeclRef, Error>
Translate a type def id
Sourcepub(crate) fn translate_fun_item(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> Result<MaybeBuiltinFunDeclRef, Error>
pub(crate) fn translate_fun_item( &mut self, span: Span, item: &ItemRef, kind: TransItemSourceKind, ) -> Result<MaybeBuiltinFunDeclRef, Error>
Translate a function def id
Sourcepub(crate) fn translate_fn_ptr(
&mut self,
span: Span,
item: &ItemRef,
kind: TransItemSourceKind,
) -> Result<RegionBinder<FnPtr>, Error>
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>
Sourcepub fn monomorphize(&self) -> bool
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>
Sourcepub fn hax_def(&mut self, item: &ItemRef) -> Result<Arc<FullDef>, Error>
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>)
Sourcepub(crate) fn translate_function_signature(
&mut self,
def: &FullDef,
item_meta: &ItemMeta,
) -> Result<FunSig, Error>
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.
Sourcepub(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>
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.
Sourcepub(crate) fn recognize_builtin_fun(
&mut self,
item: &ItemRef,
) -> Result<Option<BuiltinFunId>, Error>
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.
Sourcepub(crate) fn the_only_binder(&self) -> &BindingLevel
pub(crate) fn the_only_binder(&self) -> &BindingLevel
Get the only binding level. Panics if there are other binding levels.
Sourcepub(crate) fn the_only_binder_mut(&mut self) -> &mut BindingLevel
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>
Sourcefn push_generics_for_def(
&mut self,
span: Span,
def: &FullDef,
is_parent: bool,
) -> 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.
Sourcefn push_generics_for_def_without_parents(
&mut self,
_span: Span,
def: &FullDef,
include_late_bound: bool,
) -> Result<(), Error>
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.
Sourcepub(crate) fn translate_def_generics(
&mut self,
span: Span,
def: &FullDef,
) -> Result<(), Error>
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.
Sourcepub(crate) fn translate_def_generics_without_parents(
&mut self,
span: Span,
def: &FullDef,
) -> Result<(), Error>
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.
Sourcepub(crate) fn translate_binder_for_def<F, U>(
&mut self,
span: Span,
kind: BinderKind,
def: &FullDef,
f: F,
) -> Result<Binder<U>, Error>
pub(crate) fn translate_binder_for_def<F, U>( &mut self, span: Span, kind: BinderKind, def: &FullDef, f: F, ) -> Result<Binder<U>, Error>
Push a new binding level corresponding to the provided def
for the duration of the inner
function call.
Sourcepub(crate) fn translate_region_binder<F, T, U>(
&mut self,
_span: Span,
binder: &Binder<T>,
f: F,
) -> Result<RegionBinder<U>, Error>
pub(crate) fn translate_region_binder<F, T, U>( &mut self, _span: Span, binder: &Binder<T>, f: F, ) -> Result<RegionBinder<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).
Sourcepub(crate) fn register_module(&mut self, item_meta: ItemMeta, def: &FullDef)
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>
Sourcepub fn translate_virtual_trait_impl(
&mut self,
def_id: TraitImplId,
item_meta: ItemMeta,
vimpl: &VirtualTraitImpl,
) -> Result<TraitImpl, 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
Sourcepub(crate) fn register_predicates(
&mut self,
preds: &GenericPredicates,
origin: PredicateOrigin,
) -> Result<(), Error>
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…).
Sourcepub(crate) fn translate_predicates(
&mut self,
preds: &GenericPredicates,
origin: PredicateOrigin,
) -> Result<GenericParams, Error>
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>
Sourcepub fn trait_is_dyn_compatible(&mut self, def_id: &DefId) -> Result<bool, 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.
Sourcefn pred_is_for_self(&self, tref: &TraitRef) -> bool
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>
Sourcepub fn translate_vtable_struct_ref_maybe_enqueue(
&mut self,
enqueue: bool,
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.
Sourcefn add_method_to_vtable_def(
&mut self,
span: Span,
trait_def: &FullDef,
mk_field: impl FnMut(String, Ty),
item: &AssocItem,
) -> Result<(), Error>
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.
Sourcefn add_supertraits_to_vtable_def(
&mut self,
span: Span,
mk_field: impl FnMut(String, Ty),
implied_predicates: &GenericPredicates,
) -> Result<(), Error>
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>
Sourcepub(crate) fn check_no_monomorphize(&self, span: Span) -> Result<(), 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>
Sourcefn get_vtable_instance_info<'a>(
&mut self,
span: Span,
impl_def: &'a FullDef,
impl_kind: &TraitImplSource,
) -> Result<(TraitImplRef, TypeDeclRef), 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>
Sourcefn gen_vtable_instance_init_body(
&mut self,
span: Span,
impl_def: &FullDef,
vtable_struct_ref: TypeDeclRef,
) -> Result<Body, 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;
Sourcefn translate_vtable_shim_body(
&mut self,
span: Span,
target_receiver: &Ty,
shim_signature: &FunSig,
impl_func_def: &FullDef,
) -> Result<Body, 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_region( &mut self, span: Span, region: &Region, ) -> Result<Region, Error>
Sourcepub(crate) fn translate_ty(&mut self, span: Span, ty: &Ty) -> Result<Ty, 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>
Sourcepub fn translate_generic_args(
&mut self,
span: Span,
substs: &[GenericArg],
trait_refs: &[ImplExpr],
) -> Result<GenericArgs, 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.
Sourcepub fn append_late_bound_to_generics(
&mut self,
span: Span,
generics: GenericArgs,
late_bound: Option<Binder<()>>,
) -> Result<RegionBinder<GenericArgs>, Error>
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.
Sourcepub(crate) fn recognize_builtin_type(
&mut self,
item: &ItemRef,
) -> Result<Option<BuiltinTy>, Error>
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.
Sourcepub fn translate_ptr_metadata(
&mut self,
span: Span,
item: &ItemRef,
) -> Result<PtrMetadata, Error>
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.
Sourcepub fn translate_layout(&self, item: &ItemRef) -> Option<Layout>
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
.
Sourcepub fn generate_naive_layout(
&self,
span: Span,
ty: &TypeDeclKind,
) -> Result<Layout, Error>
pub fn generate_naive_layout( &self, span: Span, ty: &TypeDeclKind, ) -> Result<Layout, Error>
Generate a naive layout for this type.
Sourcepub(crate) fn translate_adt_def(
&mut self,
trans_id: TypeDeclId,
def_span: Span,
item_meta: &ItemMeta,
def: &FullDef,
) -> Result<TypeDeclKind, Error>
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>>§
Sourcepub fn base_kind_for_item(
&mut self,
def_id: &DefId,
) -> Option<TransItemSourceKind>
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.
Sourcepub fn enqueue_module_item(&mut self, def_id: &DefId)
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>
Sourcepub(crate) fn register_and_enqueue<T: TryFrom<ItemId>>(
&mut self,
dep_src: &Option<DepSource>,
item_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)
Sourcepub fn span_err(&self, span: Span, msg: &str, level: Level<'_>) -> Error
pub fn span_err(&self, span: Span, msg: &str, level: Level<'_>) -> Error
Span an error and register the error.
Sourcepub fn catch_sinto<S, T, U>(
&mut self,
s: &S,
span: Span,
x: &T,
) -> Result<U, Error>where
T: Debug + SInto<S, U>,
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.
Sourcepub fn poly_hax_def(&mut self, def_id: &DefId) -> Result<Arc<FullDef>, Error>
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.
Sourcepub fn hax_def_for_item(
&mut self,
item: &RustcItem,
) -> Result<Arc<FullDef>, Error>
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,
) -> Twhere
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>
Sourcepub(crate) fn get_or_translate(
&mut self,
id: ItemId,
) -> Result<ItemRef<'_>, 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.
Sourcepub fn translate_unit_metadata_const(&mut self)
pub fn translate_unit_metadata_const(&mut self)
Add a const UNIT: () = ();
const, used as metadata for thin pointers/references.
Sourcefn register_file(&mut self, filename: FileName, span: Span) -> FileId
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
Sourcepub fn translate_span_from_source_info(
&mut self,
source_scopes: &IndexVec<SourceScope, SourceScopeData>,
source_info: &SourceInfo,
) -> Span
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>
Sourcefn name_for_item(&mut self, item: &RustcItem) -> Result<Name, 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")]
Sourcepub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error>
pub fn name_for_src(&mut self, src: &TransItemSource) -> Result<Name, Error>
Compute the name for an item.
Internal function, use translate_name
.
Sourcepub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error>
pub fn translate_name(&mut self, src: &TransItemSource) -> Result<Name, Error>
Retrieve the name for an item.
Sourcepub(crate) fn translate_trait_item_name(
&mut self,
def_id: &DefId,
) -> Result<TraitItemName, Error>
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
Sourcepub(crate) fn translate_attribute(
&mut self,
attr: &Attribute,
) -> Option<Attribute>
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 String
s for Attributes
.
pub(crate) fn translate_inline(&self, def: &FullDef) -> Option<InlineAttr>
pub(crate) fn translate_attr_info(&mut self, def: &FullDef) -> AttrInfo
Sourcepub(crate) fn is_extern_item(&mut self, def: &FullDef) -> bool
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.
Sourcepub(crate) fn translate_item_meta(
&mut self,
def: &FullDef,
item_src: &TransItemSource,
name: Name,
name_opacity: ItemOpacity,
) -> ItemMeta
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§
Source§impl<'tcx, 'tctx, 'ictx> Deref for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> Deref for BodyTransCtx<'tcx, 'tctx, 'ictx>
Source§impl<'tcx, 'tctx, 'ictx> DerefMut for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> DerefMut for BodyTransCtx<'tcx, 'tctx, 'ictx>
Auto Trait Implementations§
impl<'tcx, 'tctx, 'ictx> Freeze for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> !RefUnwindSafe for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> !Send for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> !Sync for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> Unpin for BodyTransCtx<'tcx, 'tctx, 'ictx>
impl<'tcx, 'tctx, 'ictx> !UnwindSafe for BodyTransCtx<'tcx, 'tctx, 'ictx>
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
§impl<I, T> ExtractContext<I, ()> for T
impl<I, T> ExtractContext<I, ()> for T
§fn extract_context(self, _original_input: I)
fn extract_context(self, _original_input: I)
§impl<T> Instrument for T
impl<T> Instrument for T
§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
self
into a Left
variant of Either<Self, Self>
if into_left
is true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
self
into a Left
variant of Either<Self, Self>
if into_left(&self)
returns true
.
Converts self
into a Right
variant of Either<Self, Self>
otherwise. Read more