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<()>) -> Result<(), Error>
fn translate_body_locals(&mut self, body: &MirBody<()>) -> 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<()>, 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,
) -> Result<Rvalue, Error>
fn translate_rvalue( &mut self, span: Span, rvalue: &Rvalue, ) -> Result<Rvalue, Error>
Translate an rvalue
Sourcefn translate_statement(
&mut self,
body: &MirBody<()>,
statement: &Statement,
) -> Result<Option<Statement>, Error>
fn translate_statement( &mut self, body: &MirBody<()>, 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<()>,
terminator: &Terminator,
statements: &mut Vec<Statement>,
) -> Result<Terminator, Error>
fn translate_terminator( &mut self, body: &MirBody<()>, 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,
statements: &mut Vec<Statement>,
span: Span,
fun: &FunOperand,
args: &Vec<Spanned<Operand>>,
destination: &Place,
target: &Option<BasicBlock>,
) -> Result<RawTerminator, Error>
fn translate_function_call( &mut self, statements: &mut Vec<Statement>, span: Span, fun: &FunOperand, args: &Vec<Spanned<Operand>>, destination: &Place, target: &Option<BasicBlock>, ) -> Result<RawTerminator, 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,
def: &FullDef,
charon_span: Span,
) -> Vec<(usize, Vec<String>)>
fn translate_body_comments( &mut self, def: &FullDef, charon_span: Span, ) -> Vec<(usize, Vec<String>)>
Gather all the lines that start with //
inside the given span.
Sourcepub fn translate_body(
&mut self,
span: Span,
def: &FullDef,
) -> Result<Result<Body, Opaque>, Error>
pub fn translate_body( &mut self, span: Span, def: &FullDef, ) -> Result<Result<Body, Opaque>, Error>
Translate a function body if we can (it has MIR) and we want to (we don’t translate bodies
declared opaque, and only translate non-local bodies if extract_opaque_bodies
is set).
fn translate_body_aux( &mut self, def: &FullDef, span: Span, ) -> Result<Result<Body, Opaque>, Error>
Methods from Deref<Target = ItemTransCtx<'tcx, 'tctx>>§
fn translate_constant_literal_to_raw_constant_expr( &mut self, span: Span, v: &ConstantLiteral, ) -> Result<RawConstantExpr, 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 fn span_err(&self, span: Span, msg: &str, level: Level<'_>) -> Error
pub(crate) fn translate_span_from_hax(&mut self, rspan: &Span) -> Span
pub(crate) fn hax_def(&mut self, def_id: &DefId) -> Result<Arc<FullDef>, Error>
pub(crate) fn def_span(&mut self, def_id: &DefId) -> Span
pub(crate) fn register_id_no_enqueue( &mut self, span: Span, id: TransItemSource, ) -> AnyTransId
pub(crate) fn register_type_decl_id( &mut self, span: Span, id: &DefId, ) -> TypeDeclId
pub(crate) fn register_fun_decl_id( &mut self, span: Span, id: &DefId, ) -> FunDeclId
pub(crate) fn register_fun_decl_id_no_enqueue( &mut self, span: Span, id: &DefId, ) -> FunDeclId
pub(crate) fn register_global_decl_id( &mut self, span: Span, id: &DefId, ) -> GlobalDeclId
Sourcepub(crate) fn register_trait_decl_id(
&mut self,
span: Span,
id: &DefId,
) -> TraitDeclId
pub(crate) fn register_trait_decl_id( &mut self, span: Span, id: &DefId, ) -> TraitDeclId
Returns an Option because we may ignore some builtin or auto traits like core::marker::Sized or core::marker::Sync.
Sourcepub(crate) fn register_trait_impl_id(
&mut self,
span: Span,
id: &DefId,
) -> TraitImplId
pub(crate) fn register_trait_impl_id( &mut self, span: Span, id: &DefId, ) -> TraitImplId
Returns an Option because we may ignore some builtin or auto traits like core::marker::Sized or core::marker::Sync.
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.
pub(crate) fn outermost_binder(&self) -> &BindingLevel
pub(crate) fn innermost_binder(&self) -> &BindingLevel
pub(crate) fn innermost_binder_mut(&mut self) -> &mut BindingLevel
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>
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 lookup_cached_type( &self, cache_key: &HashByAddr<Arc<TyKind>>, ) -> Option<Ty>
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 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.
pub(crate) fn make_dep_source(&self, span: Span) -> Option<DepSource>
pub(crate) fn get_item_kind( &mut self, span: Span, def: &FullDef, ) -> Result<ItemKind, Error>
Sourcefn translate_function_signature(
&mut self,
def: &FullDef,
item_meta: &ItemMeta,
) -> Result<FunSig, Error>
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.
Sourcefn build_ctor_body(
&mut self,
span: Span,
signature: &FunSig,
adt_def_id: &DefId,
ctor_of: &CtorOf,
variant_id: usize,
fields: &IndexVec<FieldIdx, FieldDef>,
output_ty: &Ty,
) -> Result<Body, Error>
fn build_ctor_body( &mut self, span: Span, signature: &FunSig, 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 translate_fn_ptr(
&mut self,
span: Span,
def_id: &DefId,
substs: &Vec<GenericArg>,
trait_refs: &Vec<ImplExpr>,
trait_info: &Option<ImplExpr>,
) -> Result<FnPtr, Error>
pub(crate) fn translate_fn_ptr( &mut self, span: Span, def_id: &DefId, substs: &Vec<GenericArg>, trait_refs: &Vec<ImplExpr>, trait_info: &Option<ImplExpr>, ) -> Result<FnPtr, Error>
Auxiliary function to translate function calls and references to functions. Translate a function id applied with some substitutions.
TODO: should we always erase the regions?
Sourcepub(crate) fn register_predicates(
&mut self,
preds: &GenericPredicates,
origin: PredicateOrigin,
location: &PredicateLocation,
) -> Result<(), Error>
pub(crate) fn register_predicates( &mut self, preds: &GenericPredicates, origin: PredicateOrigin, location: &PredicateLocation, ) -> Result<(), Error>
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_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 register_predicate( &mut self, clause: &Clause, hspan: &Span, origin: PredicateOrigin, location: &PredicateLocation, ) -> 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(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.
pub fn translate_generic_args( &mut self, span: Span, substs: &[GenericArg], trait_refs: &[ImplExpr], late_bound: Option<Binder<()>>, target: GenericsSource, ) -> Result<GenericArgs, Error>
Sourcefn recognize_builtin_type(
&mut self,
def_id: &DefId,
) -> Result<Option<BuiltinTy>, Error>
fn recognize_builtin_type( &mut self, def_id: &DefId, ) -> Result<Option<BuiltinTy>, Error>
Checks whether the given id corresponds to a built-in type.
Sourcepub(crate) fn translate_type_id(
&mut self,
span: Span,
def_id: &DefId,
) -> Result<TypeId, Error>
pub(crate) fn translate_type_id( &mut self, span: Span, def_id: &DefId, ) -> Result<TypeId, Error>
Translate a type def id
Sourcefn translate_adt_def(
&mut self,
trans_id: TypeDeclId,
def_span: Span,
item_meta: &ItemMeta,
adt: &AdtDef,
) -> Result<TypeDeclKind, Error>
fn translate_adt_def( &mut self, trans_id: TypeDeclId, def_span: Span, item_meta: &ItemMeta, adt: &AdtDef, ) -> 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<ScalarValue, Error>
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.
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.
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,
include_assoc_ty_clauses: bool,
) -> Result<(), Error>
fn push_generics_for_def_without_parents( &mut self, span: Span, def: &FullDef, include_late_bound: bool, include_assoc_ty_clauses: 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 push_generic_params( &mut self, generics: &TyGenerics, ) -> Result<(), Error>
pub(crate) fn push_generic_param( &mut self, param: &GenericParamDef, ) -> Result<(), Error>
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