Struct 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>>,
}

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.

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.