avrora.stack
Class StateSpace

java.lang.Object
  avrora.stack.StateSpace

public class StateSpace

extends java.lang.Object

The StateSpace class represents the reachable state space as it is explored by the Analyzer class. It stores reachable states and the outgoing edges that connect them.

Nested Class Summary

class	StateSpace.Link The Link inner class represents an edge between two states within the state space.
class	StateSpace.State The State class represents an immutable state within the state space of the program.

Constructor Summary

StateSpace(Program p)
The constructor for the StateSpace accepts a program as a parameter.

Method Summary

void	addEdge(StateSpace.State s, StateSpace.State t) The addEdge() method creates an edge between the specified states with weight 0.
void	addEdge(StateSpace.State s, StateSpace.State t, int weight) The addEdge() method creates an edge between the specified states with the given weight.
boolean	addFrontier(StateSpace.State s) The addFrontier method adds a state to the frontier.
boolean	addState(StateSpace.State s) The addState() method adds a state to the state space (marks it as explored).
StateSpace.State	getEdenState() The getEdenState() method gets the starting state of the abstract interpretation.
StateSpace.State	getFrontierState() The getFrontierState() chooses a state off of the state frontier, removes it from the state frontier, and returns it.
long	getSpecialStateCount() The getSpecialStateCount() method returns the number of special states that were created.
StateSpace.State	getStateFor(MutableState s) The getStateFor() method searches the state cache for an immutable state that corresponds to the given mutable state.
long	getStatesInSpaceCount() The getStatesInSpaceCount() method returns the number of unique states that have been added to this state space.
long	getTotalStateCount() The getTotalStateCount() method returns the internally recorded number of states created in this state space.
boolean	isExplored(StateSpace.State s) The isExplored() method checks whether the specified state has been added to this state space (i.e. it has been explored).
boolean	isFrontier(StateSpace.State s) The isFrontier() method checks whether the specified state is currently on the state frontier.
avrora.stack.StateSpace.SpecialState	makeSpecialState(java.lang.String name) The makeSpecialState() method creates a special state that represents something important to an analysis tool, such as a RETURN state.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

StateSpace

public StateSpace(Program p)

The constructor for the StateSpace accepts a program as a parameter. This is currently unused, but is reserved for use later.

Parameters:

p - the program to create the state space for

Method Detail

getEdenState

public StateSpace.State getEdenState()

The getEdenState() method gets the starting state of the abstract interpretation.

Returns:

the initial state to begin abstract interpretation

getFrontierState

public StateSpace.State getFrontierState()

The getFrontierState() chooses a state off of the state frontier, removes it from the state frontier, and returns it. If there are no states left on the state frontier, this method returns null. Note that initially there are no states on the frontier, not even the eden state.

Returns:

one of the states on the current state frontier; null if there are none.

isExplored

public boolean isExplored(StateSpace.State s)

The isExplored() method checks whether the specified state has been added to this state space (i.e. it has been explored). A state can be added at most once and cannot be removed from the state space.

Parameters:

s - the state to check

Returns:

true if the specified state has been explored; false otherwise

isFrontier

public boolean isFrontier(StateSpace.State s)

The isFrontier() method checks whether the specified state is currently on the state frontier.

Parameters:

s - the state to check

Returns:

true if the specified state is currently on the frontier; false otherwise

addState

public boolean addState(StateSpace.State s)

The addState() method adds a state to the state space (marks it as explored). A state can be added at most once and cannot be removed once it has been added. Note that being cached does not imply that the state is in the state space.

Parameters:

s - the state to add to the state space.

Returns:

true if this state is already in the state space; false otherwise

addFrontier

public boolean addFrontier(StateSpace.State s)

The addFrontier method adds a state to the frontier.

Parameters:

s - the state to add

Returns:

true if the state was already on the frontier; false otherwise

makeSpecialState

public avrora.stack.StateSpace.SpecialState makeSpecialState(java.lang.String name)

The makeSpecialState() method creates a special state that represents something important to an analysis tool, such as a RETURN state. These special states are not stored in the state cache.

Parameters:

name - the name of the special state

Returns:

an instance of the SpecialState class that is the newly created special states.

getStateFor

public StateSpace.State getStateFor(MutableState s)

The getStateFor() method searches the state cache for an immutable state that corresponds to the given mutable state. If no immutable state exists in the cache, one will be created and inserted.

Parameters:

s - the state to search for

Returns:

an instance of the StateSpace.State immutable state that corresponds to the given mutable state

addEdge

public void addEdge(StateSpace.State s,
                    StateSpace.State t,
                    int weight)

The addEdge() method creates an edge between the specified states with the given weight. No checking for duplicate edges is done.

Parameters:

s - the source state

t - the destination state

weight - the weight to assign to the edge

addEdge

public void addEdge(StateSpace.State s,
                    StateSpace.State t)

The addEdge() method creates an edge between the specified states with weight 0. No checking for duplicate edges is done.

Parameters:

s - the source state

t - the destination state

getTotalStateCount

public long getTotalStateCount()

The getTotalStateCount() method returns the internally recorded number of states created in this state space. This is mainly used for reporting purposes.

Returns:

the total number of states in the state cache

getStatesInSpaceCount

public long getStatesInSpaceCount()

The getStatesInSpaceCount() method returns the number of unique states that have been added to this state space. This is mainly used for reporting purposes.

Returns:

the number of states added to the state space

getSpecialStateCount

public long getSpecialStateCount()

The getSpecialStateCount() method returns the number of special states that were created. This is mainly used for reporting purposes.

Returns:

the number of special states created