---

BirState Class Reference

Inheritance diagram for BirState:[legend]Collaboration diagram for BirState:[legend]List of all members.

Public Methods
void	applyAction (Action action, int choice)
void	caseAddExpr (AddExpr expr)
void	caseAndExpr (AndExpr expr)
void	caseArrayExpr (ArrayExpr expr)
void	caseAssertAction (AssertAction assertAction)
void	caseAssignAction (AssignAction assign)
void	caseBoolLit (BoolLit expr)
void	caseChooseExpr (ChooseExpr expr)
void	caseConstant (Constant expr)
void	caseDerefExpr (DerefExpr expr)
void	caseDivExpr (DivExpr expr)
void	caseEqExpr (EqExpr expr)
void	caseInstanceOfExpr (InstanceOfExpr expr)
void	caseIntLit (IntLit expr)
void	caseLeExpr (LeExpr expr)
void	caseLengthExpr (LengthExpr expr)
void	caseLockAction (LockAction lockAction)
void	caseLockTest (LockTest lockTest)
void	caseLtExpr (LtExpr expr)
void	caseMulExpr (MulExpr expr)
void	caseNeExpr (NeExpr expr)
void	caseNewArrayExpr (NewArrayExpr expr)
void	caseNewExpr (NewExpr expr)
void	caseNotExpr (NotExpr expr)
void	caseNullExpr (NullExpr expr)
void	caseOrExpr (OrExpr expr)
void	casePrintAction (PrintAction printAction)
void	caseRecordExpr (RecordExpr expr)
void	caseRefExpr (RefExpr expr)
void	caseRemExpr (RemExpr expr)
void	caseStateVar (StateVar expr)
void	caseSubExpr (SubExpr expr)
void	caseThreadAction (ThreadAction threadAction)
void	caseThreadLocTest (ThreadLocTest threadLocTest)
void	caseThreadTest (ThreadTest threadTest)
void	completeTrans (Transformation trans)
BirState	copy ()
void	defaultCase (Object obj)
String	exprValue (Expr expr)
String	getOutput ()
Literal[]	getStore ()
TransSystem	getSystem ()
boolean	isActive (BirThread thread)
void	print ()
Static Public Methods
BirState	initialState (TransSystem system, TransVector transVector, Vector choiceVector)
int	setActualSizesFromTrace (TransSystem system, TransVector transVector, Vector choiceVector)
Private Methods
	BirState (TransSystem system)
Private Attributes
TransSystem	system
Literal[]	store
Location[]	location
boolean[]	threadActive
boolean	lhs = false
int	choice
String	output = ""

---

Detailed Description

A BirState represents a state of a BIR transition system in a trace.

The main parts of the state are:

• A "state vector": a Literal array storing the value of all state variables which are laid out as they might be in a compiler.
• A Location array storing the current location of each thread.
• A boolean array indicating whether each thread is active.

The interface Literal is implemented by a collection of classes that represent values of non-composite types (BoolLit, IntLit, LockLit, RefLit). These objects are the contents of the state vector.

This class is a BIR expression switch---it translates a BIR expression into either a Literal value (the r-value of the expression in this state) or an Integer (the address in the state vector of the l-value of the expression in this state). The rules are:

• Any expression with an array or record value always evaluates to the Integer address of that object in the state vector.
• If the LHS flag is set, then any expression will evaluate to the Integer address of that entity in the state vector (in this case, it is an error if the expression is not an l-value). This flag is set to true only while evaluating the left-hand-side of an assignment (since we want the address to update).
• Otherwise, the expression evaluates to a Literal representing the r-value of the expression in this state.

Definition at line 72 of file BirState.java.

---

Member Function Documentation

void BirState::caseAssignAction (  AssignAction   assign )  [inline, virtual]

Execute assignment. Reimplemented from ExprSwitch. Definition at line 132 of file BirState.java.

void BirState::completeTrans (  Transformation   trans )  [inline]

Update thread location once all transformation actions have completed. Definition at line 374 of file BirState.java. Referenced by BirTrace::done().

BirState BirState::copy (    )  [inline]

Make a copy of this state Definition at line 382 of file BirState.java. Referenced by BirTrace::done().

BirState BirState::initialState (  TransSystem   system, TransVector   transVector, Vector   choiceVector )  [inline, static]

Build the initial state of a BIR transition system. Definition at line 408 of file BirState.java.

int BirState::setActualSizesFromTrace (  TransSystem   system, TransVector   transVector, Vector   choiceVector )  [inline, static]

Given the trace, compute the size of the state vector (which holds the values of all state variables). This used to be done statically given the collection bounds in the BIR, but with dynamic verifiers like dSPIN (which ignore these bounds), we don't know how many collection elements are allocated until we see the trace. We also set the choice for each Allocator action to indicate the index into the collection of the instance that was allocated (this is just a count of the number allocated so far). Note that for NewArrayExpr, the choice that comes in is the actual length---we reset it to the instance index (the max length for the collection is computed and stored in the collection). Definition at line 477 of file BirState.java.

---

The documentation for this class was generated from the following file:

• BirState.java

---