Struct move_stackless_bytecode::function_target::FunctionData

pub struct FunctionData {

    pub variant: FunctionVariant,
    pub type_args: Vec<Type>,
    pub code: Vec<Bytecode>,
    pub local_types: Vec<Type>,
    pub return_types: Vec<Type>,
    pub acquires_global_resources: Vec<StructId>,
    pub locations: BTreeMap<AttrId, Loc>,
    pub loop_invariants: BTreeSet<AttrId>,
    pub debug_comments: BTreeMap<AttrId, String>,
    pub vc_infos: BTreeMap<AttrId, String>,
    pub annotations: Annotations,
    pub name_to_index: BTreeMap<Symbol, usize>,
    pub modify_targets: BTreeMap<QualifiedId<StructId>, Vec<Exp>>,
    pub ghost_type_param_count: usize,
}

Holds the owned data belonging to a FunctionTarget, contained in a FunctionTargetsHolder.

Fields

variant: FunctionVariant

The function variant.

type_args: Vec<Type>

The type instantiation.

code: Vec<Bytecode>

The bytecode.

local_types: Vec<Type>

The locals, including parameters.

return_types: Vec<Type>

The return types.

acquires_global_resources: Vec<StructId>

The set of global resources acquired by this function.

locations: BTreeMap<AttrId, Loc>

A map from byte code attribute to source code location.

loop_invariants: BTreeSet<AttrId>

The set of asserts that represent loop invariants

debug_comments: BTreeMap<AttrId, String>

A map from byte code attribute to comments associated with this bytecode. These comments are generated by transformations and are intended for internal debugging when the bytecode is dumped.

vc_infos: BTreeMap<AttrId, String>

A map from byte code attribute to a message to be printed out if verification fails at this bytecode.

annotations: Annotations

Annotations associated with this function. This is shared between multiple function variants.

name_to_index: BTreeMap<Symbol, usize>

A mapping from symbolic names to temporaries.

modify_targets: BTreeMap<QualifiedId<StructId>, Vec<Exp>>

A cache of targets modified by this function.

ghost_type_param_count: usize

The number of ghost type parameters introduced in order to instantiate related invariants

Implementations

impl FunctionData

pub fn new(
    func_env: &FunctionEnv<'_>,
    code: Vec<Bytecode>,
    local_types: Vec<Type>,
    return_types: Vec<Type>,
    locations: BTreeMap<AttrId, Loc>,
    acquires_global_resources: Vec<StructId>,
    loop_invariants: BTreeSet<AttrId>
) -> Self

Creates new function target data.

pub fn next_free_attr_index(&self) -> usize

Computes the next available index for AttrId.

pub fn next_free_label_index(&self) -> usize

Computes the next available index for Label.

pub fn rename_vars<F>(&mut self, _f: &F) where
    F: Fn(TempIndex) -> TempIndex, 

Apply a variable renaming to this data, adjusting internal data structures.

pub fn fork(&self, new_variant: FunctionVariant) -> Self

Fork this function data, without annotations, and mark it as the given variant.

pub fn fork_with_instantiation(
    &self,
    env: &GlobalEnv,
    inst: &[Type],
    new_variant: FunctionVariant
) -> Self

Fork this function data with (potentially partial) instantiations.

pub fn get_type_instantiation(&self, _fun_env: &FunctionEnv<'_>) -> Vec<Type>

Get the instantiation of this function as a vector of types.

Trait Implementations

impl Clone for FunctionData

fn clone(&self) -> FunctionData

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for FunctionData

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.