Struct move_stackless_bytecode::read_write_set_analysis::ReadWriteSetState

pub struct ReadWriteSetState { /* private fields */ }

A record of the glocals and locals accessed by the current procedure + the address values stored by locals or globals

Implementations

impl ReadWriteSetState

pub fn sub_actuals(
    accesses: AccessPathTrie<Access>,
    actuals: &[TempIndex],
    type_actuals: &[Type],
    fun_env: &FunctionEnv<'_>,
    sub_map: &dyn AccessPathMap<AbsAddr>
) -> AccessPathTrie<Access>

pub fn apply_summary(
    &mut self,
    callee_summary_: &Self,
    actuals: &[TempIndex],
    type_actuals: &[Type],
    returns: &[TempIndex],
    caller_fun_env: &FunctionEnv<'_>,
    callee_fun_env: &FunctionEnv<'_>
)

Apply callee_summary to the caller state in self. There are three steps.

1. Substitute footprint values in the callee summary with their values in the caller state (including both actuals and values read from globals)
2. Bind return values in the callee summary to the return variables in the caller state
3. Join caller accesses and callee accesses

pub fn assign_local(
    &mut self,
    lhs_index: TempIndex,
    rhs_index: TempIndex,
    func_env: &FunctionEnv<'_>
)

pub fn assign_root(
    &mut self,
    lhs: Root,
    rhs_index: TempIndex,
    func_env: &FunctionEnv<'_>
)

pub fn remove_global(
    &mut self,
    addr_idx: TempIndex,
    mid: &ModuleId,
    sid: StructId,
    types: &[Type],
    fun_env: &FunctionEnv<'_>
)

Remove the local access paths rooted addr_idx/mid::sid<types>

pub fn access_offset(
    &mut self,
    base: TempIndex,
    offset: Offset,
    access_type: Access,
    fun_env: &FunctionEnv<'_>
)

Record an access of type access_type to the path base/offset

pub fn assign_offset(
    &mut self,
    ret: TempIndex,
    base: TempIndex,
    offset: Offset,
    access_type: Option<Access>,
    fun_env: &FunctionEnv<'_>
)

Assign ret = base/offset and record an access of type access_type to base/offset

pub fn write_ref(
    &mut self,
    lhs_ref: TempIndex,
    rhs: TempIndex,
    fun_env: &FunctionEnv<'_>
)

Write rhs to lhs_ref

pub fn substitute_footprint_concrete(
    self,
    actuals: &[TempIndex],
    type_actuals: &[TypeTag],
    func_env: &FunctionEnv<'_>,
    sub_map: &dyn AccessPathMap<AbsAddr>,
    env: &GlobalEnv
) -> SpecializedReadWriteSetState

Substitute concrete values actuals and type_actuals into self

pub fn accesses(&self) -> &AccessPathTrie<Access>

pub fn locals(&self) -> &AccessPathTrie<AbsAddr>

pub fn display<'a>(
    &'a self,
    env: &'a FunctionEnv<'_>
) -> ReadWriteSetStateDisplay<'a>

Return a wrapper of self that implements Display using env

impl ReadWriteSetState

pub fn normalize(&self, env: &GlobalEnv) -> ReadWriteSet

Trait Implementations

impl AbstractDomain for ReadWriteSetState

fn join(&mut self, other: &Self) -> JoinResult

impl Clone for ReadWriteSetState

fn clone(&self) -> ReadWriteSetState

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for ReadWriteSetState

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

Formats the value using the given formatter.

impl Default for ReadWriteSetState

fn default() -> Self

Returns the “default value” for a type.

impl PartialEq<ReadWriteSetState> for ReadWriteSetState

fn eq(&self, other: &ReadWriteSetState) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &ReadWriteSetState) -> bool

This method tests for !=.

impl PartialOrd<ReadWriteSetState> for ReadWriteSetState

fn partial_cmp(&self, other: &ReadWriteSetState) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

This method tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

This method tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

This method tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

This method tests greater than or equal to (for self and other) and is used by the >= operator.

impl Eq for ReadWriteSetState

impl StructuralEq for ReadWriteSetState

impl StructuralPartialEq for ReadWriteSetState