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
impl ReadWriteSetState
pub fn sub_actuals( accesses: AccessPathTrie<Access>, actuals: &[TempIndex], type_actuals: &[Type], fun_env: &FunctionEnv<'_>, sub_map: &dyn AccessPathMap<AbsAddr> ) -> AccessPathTrie<Access>
sourcepub fn apply_summary(
&mut self,
callee_summary_: &Self,
actuals: &[TempIndex],
type_actuals: &[Type],
returns: &[TempIndex],
caller_fun_env: &FunctionEnv<'_>,
callee_fun_env: &FunctionEnv<'_>
)
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.
- Substitute footprint values in the callee summary with their values in the caller state (including both actuals and values read from globals)
- Bind return values in the callee summary to the return variables in the caller state
- Join caller accesses and callee accesses
sourcepub fn copy_local(
&mut self,
lhs_index: TempIndex,
rhs_index: TempIndex,
fun_env: &FunctionEnv<'_>
)
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
pub fn assign_local( &mut self, lhs_index: TempIndex, rhs_index: TempIndex, func_env: &FunctionEnv<'_> )
sourcepub fn remove_global(
&mut self,
addr_idx: TempIndex,
mid: &ModuleId,
sid: StructId,
types: &[Type],
fun_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
>
sourcepub fn access_offset(
&mut self,
base: TempIndex,
offset: Offset,
access_type: Access,
fun_env: &FunctionEnv<'_>
)
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
sourcepub fn assign_offset(
&mut self,
ret: TempIndex,
base: TempIndex,
offset: Offset,
access_type: Option<Access>,
fun_env: &FunctionEnv<'_>
)
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
sourcepub fn write_ref(
&mut self,
lhs_ref: TempIndex,
rhs: TempIndex,
fun_env: &FunctionEnv<'_>
)
pub fn write_ref( &mut self, lhs_ref: TempIndex, rhs: TempIndex, fun_env: &FunctionEnv<'_> )
Write rhs
to lhs_ref
sourcepub fn substitute_footprint_concrete(
self,
actuals: &[TempIndex],
type_actuals: &[TypeTag],
func_env: &FunctionEnv<'_>,
sub_map: &dyn AccessPathMap<AbsAddr>,
env: &GlobalEnv
) -> SpecializedReadWriteSetState
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>
sourcepub fn display<'a>(
&'a self,
env: &'a FunctionEnv<'_>
) -> ReadWriteSetStateDisplay<'a>
pub fn display<'a>( &'a self, env: &'a FunctionEnv<'_> ) -> ReadWriteSetStateDisplay<'a>
Return a wrapper of self
that implements Display
using env
Trait Implementations§
source§impl AbstractDomain for ReadWriteSetState
impl AbstractDomain for ReadWriteSetState
fn join(&mut self, other: &Self) -> JoinResult
source§impl Clone for ReadWriteSetState
impl Clone for ReadWriteSetState
source§fn clone(&self) -> ReadWriteSetState
fn clone(&self) -> ReadWriteSetState
Returns a copy of the value. Read more
1.0.0 · source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from
source
. Read moresource§impl Debug for ReadWriteSetState
impl Debug for ReadWriteSetState
source§impl Default for ReadWriteSetState
impl Default for ReadWriteSetState
source§impl PartialEq<ReadWriteSetState> for ReadWriteSetState
impl PartialEq<ReadWriteSetState> for ReadWriteSetState
source§fn eq(&self, other: &ReadWriteSetState) -> bool
fn eq(&self, other: &ReadWriteSetState) -> bool
This method tests for
self
and other
values to be equal, and is used
by ==
.source§impl PartialOrd<ReadWriteSetState> for ReadWriteSetState
impl PartialOrd<ReadWriteSetState> for ReadWriteSetState
source§fn partial_cmp(&self, other: &ReadWriteSetState) -> Option<Ordering>
fn partial_cmp(&self, other: &ReadWriteSetState) -> Option<Ordering>
1.0.0 · source§fn le(&self, other: &Rhs) -> bool
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 moreimpl Eq for ReadWriteSetState
impl StructuralEq for ReadWriteSetState
impl StructuralPartialEq for ReadWriteSetState
Auto Trait Implementations§
impl RefUnwindSafe for ReadWriteSetState
impl Send for ReadWriteSetState
impl Sync for ReadWriteSetState
impl Unpin for ReadWriteSetState
impl UnwindSafe for ReadWriteSetState
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
Compare self to
key
and return true
if they are equal.