Struct solana_libra_bytecode_verifier::abstract_state::AbstractState

pub struct AbstractState { /* fields omitted */ }

Methods

impl AbstractState

pub fn new(
    locals: BTreeMap<LocalIndex, AbstractValue>,
    globals: BTreeMap<StructDefinitionIndex, BTreeSet<Nonce>>
) -> Self

create a new abstract state

pub fn is_available(&self, idx: LocalIndex) -> bool

checks if local@idx is available

pub fn local(&self, idx: LocalIndex) -> &AbstractValue

returns local@idx

pub fn global(&mut self, idx: StructDefinitionIndex) -> &BTreeSet<Nonce>

returns global@idx

pub fn global_opt(&self, idx: StructDefinitionIndex) -> Option<&BTreeSet<Nonce>>

returns global@idx, None if not present

pub fn remove_local(&mut self, idx: LocalIndex) -> AbstractValue

removes local@idx

pub fn insert_local(&mut self, idx: LocalIndex, value: AbstractValue)

inserts local@idx

pub fn is_safe_to_destroy(&self) -> bool

Return true if self may safely be destroyed

pub fn is_local_safe_to_destroy(&self, idx: LocalIndex) -> bool

Return true if local@idx may safely be destroyed

pub fn destroy_local(&mut self, idx: LocalIndex)

destroys local@idx call only if self.is_local_safe_to_destroy(idx) returns true

pub fn add_nonce(&mut self, nonce: Nonce)

nonce must be fresh

pub fn destroy_nonce(&mut self, nonce: Nonce)

destroys nonce borrows of nonce become borrows of any nonce' such that nonce borrows from nonce'

pub fn is_full(&self, value: &AbstractValue) -> bool

checks if there are any pending borrows on value

pub fn borrowed_nonces_for_field(
    &self,
    idx: FieldDefinitionIndex,
    nonce: Nonce
) -> BTreeSet<Nonce>

returns the set of nonces borrowing from nonce that might alias some idx-extension of nonce

pub fn borrowed_nonces(&self, nonce: Nonce) -> BTreeSet<Nonce>

returns the set of nonces borrowing from nonce that might alias some extension of nonce

pub fn borrow_field_from_nonce(
    &mut self,
    idx: FieldDefinitionIndex,
    nonce: Nonce,
    new_nonce: Nonce
)

update self to reflect a borrow of idx from nonce by new_nonce

pub fn borrow_from_local_value(&mut self, idx: LocalIndex, new_nonce: Nonce)

update self to reflect a borrow of a value local@idx by new_nonce

pub fn borrow_from_local_reference(&mut self, idx: LocalIndex, new_nonce: Nonce)

update self to reflect a borrow of a reference local@idx by new_nonce

pub fn borrow_from_global_value(
    &mut self,
    idx: StructDefinitionIndex,
    new_nonce: Nonce
)

update self to reflect a borrow of a value global@idx by new_nonce

pub fn borrow_from_nonces(
    &mut self,
    to_borrow_from: &BTreeSet<Nonce>,
    new_nonce: Nonce
)

update self to reflect a borrow from each nonce in to_borrow_from by new_nonce

pub fn is_canonical(&self) -> bool

checks if self is canonical

pub fn construct_canonical_state(&self) -> Self

returns the canonical representation of self

Trait Implementations

impl AbstractDomain for AbstractState

fn join(&mut self, state: &AbstractState) -> JoinResult

attempts to join state to self and returns the result

impl Clone for AbstractState

fn clone(&self) -> AbstractState

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for AbstractState

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

Formats the value using the given formatter.

impl Eq for AbstractState

impl PartialEq<AbstractState> for AbstractState

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

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

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

This method tests for !=.

impl StructuralEq for AbstractState

impl StructuralPartialEq for AbstractState