pub struct ReadWriteSetState { /* private fields */ }
Expand description

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

Implementations§

source§

impl ReadWriteSetState

source

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

source

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
source

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

Copy the contents of rhs_index into lhs_index. Fails if rhs_index is not bound

source

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

source

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>

source

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

source

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

source

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

Write rhs to lhs_ref

source

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

source

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

source

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

source

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

Return a wrapper of self that implements Display using env

source§

impl ReadWriteSetState

source

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

Trait Implementations§

source§

impl AbstractDomain for ReadWriteSetState

source§

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

source§

impl Clone for ReadWriteSetState

source§

fn clone(&self) -> ReadWriteSetState

Returns a copy of the value. Read more
1.0.0 · source§

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

Performs copy-assignment from source. Read more
source§

impl Debug for ReadWriteSetState

source§

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

Formats the value using the given formatter. Read more
source§

impl Default for ReadWriteSetState

source§

fn default() -> Self

Returns the “default value” for a type. Read more
source§

impl PartialEq<ReadWriteSetState> for ReadWriteSetState

source§

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

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

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

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.
source§

impl PartialOrd<ReadWriteSetState> for ReadWriteSetState

source§

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

This method returns an ordering between self and other values if one exists. Read more
1.0.0 · source§

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

This method tests less than (for self and other) and is used by the < operator. Read more
1.0.0 · source§

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

This method tests less than or equal to (for self and other) and is used by the <= operator. Read more
1.0.0 · source§

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

This method tests greater than (for self and other) and is used by the > operator. Read more
1.0.0 · source§

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

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

impl Eq for ReadWriteSetState

source§

impl StructuralEq for ReadWriteSetState

source§

impl StructuralPartialEq for ReadWriteSetState

Auto Trait Implementations§

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
source§

impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,

source§

fn equivalent(&self, key: &K) -> bool

Compare self to key and return true if they are equal.
source§

impl<T> From<T> for T

const: unstable · source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

const: unstable · source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> Same<T> for T

§

type Output = T

Should always be Self
source§

impl<T> ToOwned for Twhere T: Clone,

§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
const: unstable · source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
const: unstable · source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for Twhere V: MultiLane<T>,

§

fn vzip(self) -> V