Struct test_generation::abstract_state::AbstractState

pub struct AbstractState {
    pub instantiation: Vec<AbilitySet>,
    pub module: InstantiableModule,
    pub acquires_global_resources: Vec<StructDefinitionIndex>,
    pub call_graph: CallGraph,
    /* private fields */
}

An AbstractState represents an abstract view of the execution of the Move VM. Rather than considering values of items on the stack or in the locals, we only consider their type, represented by a AbstractValue and their availibility, represented by the BorrowState.

Fields

instantiation: Vec<AbilitySet>

A vector of type kinds for any generic function type parameters of the function that we are in.

module: InstantiableModule

The module state

acquires_global_resources: Vec<StructDefinitionIndex>

The global resources acquired by the function corresponding to this abstract state

call_graph: CallGraph

Implementations

impl AbstractState

pub fn new() -> AbstractState

Create a new AbstractState with empty stack, locals, and register

pub fn from_locals( module: CompiledModule, locals: HashMap<usize, (AbstractValue, BorrowState)>, instantiation: Vec<AbilitySet>, acquires_global_resources: Vec<StructDefinitionIndex>, call_graph: CallGraph ) -> AbstractState

Create a new AbstractState given a list of SignatureTokens that will be the (available) locals that the state will have, as well as the module state

pub fn register_copy(&self) -> Option<AbstractValue>

Get the register value

pub fn register_move(&mut self) -> Option<AbstractValue>

Get the register value and set it to None

pub fn register_set(&mut self, value: AbstractValue)

Set the register value and set it to None

pub fn stack_push(&mut self, item: AbstractValue)

Add a AbstractValue to the stack

pub fn stack_push_register(&mut self) -> Result<(), VMError>

Add a AbstractValue to the stack from the register If the register is None return a VMError

pub fn stack_pop(&mut self) -> Result<(), VMError>

Remove an AbstractValue from the stack if it exists to the register If it does not exist return a VMError.

pub fn stack_peek(&self, index: usize) -> Option<AbstractValue>

Get the AbstractValue at index index on the stack if it exists. Index 0 is the top of the stack.

pub fn stack_len(&self) -> usize

Get the length of the stack.

pub fn local_exists(&self, i: usize) -> bool

Check if the local at index i exists

pub fn local_get(&self, i: usize) -> Option<&(AbstractValue, BorrowState)>

Get the local at index i if it exists

pub fn local_take(&mut self, i: usize) -> Result<(), VMError>

Place the local at index i if it exists into the register If it does not exist return a VMError.

pub fn local_take_borrow( &mut self, i: usize, mutability: Mutability ) -> Result<(), VMError>

Place a reference to the local at index i if it exists into the register If it does not exist return a VMError.

pub fn local_set( &mut self, i: usize, availability: BorrowState ) -> Result<(), VMError>

Set the availability of the local at index i If it does not exist return a VMError.

pub fn local_availability_is( &self, i: usize, availability: BorrowState ) -> Result<bool, VMError>

Check whether a local is in a particular BorrowState If the local does not exist return a VMError.

pub fn local_has_ability( &self, i: usize, ability: Ability ) -> Result<bool, VMError>

Check whether a local has a particular Ability If the local does not exist return a VMError.

pub fn local_insert( &mut self, i: usize, abstract_value: AbstractValue, availability: BorrowState )

Insert a local at index i as Available

pub fn local_place(&mut self, i: usize) -> Result<(), VMError>

Insert a local at index i as Available from the register If the register value is None return a VMError.

pub fn get_locals(&self) -> &HashMap<usize, (AbstractValue, BorrowState)>

Get all of the locals

pub fn abort(&mut self)

Set the abstract state to be aborted when a precondition of an instruction fails. (This will happen if NEGATE_PRECONDITIONs is true).

pub fn has_aborted(&self) -> bool

Whether the state is aborted

pub fn allow_control_flow(&mut self)

Set the abstract state to allow generation of control flow operations.

pub fn is_control_flow_allowed(&self) -> bool

Predicate determining if control flow instructions can be generated.

pub fn is_final(&self) -> bool

The final state is one where the stack is empty

Trait Implementations

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 Default for AbstractState

fn default() -> Self

Returns the “default value” for a type.

impl Display for AbstractState

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

Formats the value using the given formatter.