---

TransSystem Class Reference

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

Public Methods
	TransSystem (String name)
void	addTrans (Transformation trans)
void	addType (Type t)
Array	arrayType (Type baseType, ConstExpr size)
Bool	booleanType ()
Collection	collectionType (Type baseType, ConstExpr size)
String	createName (Object key, String proposedName)
BirThread	createThread (String proposedName, Object key)
void	declarePredicate (String proposedName, Expr expr)
StateVar	declareVar (Object key, String proposedName, BirThread thread, Type type, Expr initVal)
void	define (Object key, Definition definition)
Enumerated	enumeratedType ()
Definition	getDefinition (Object key)
Vector	getDefinitions ()
Object	getKeyOf (String name)
StateVarVector	getLocalStateVars (BirThread thread)
Location	getLocation (int id)
String	getName ()
String	getNameOf (Object key)
Vector	getPredicates ()
Object	getSource (Object birObject)
StateVarVector	getStateVars ()
ThreadVector	getThreads ()
TransVector	getTransformations ()
Vector	getTypes ()
StateVar	getVarOfKey (Object key)
Location	locationOfKey (Object key, BirThread thread)
Lock	lockType (boolean waiting, boolean reentrant)
void	numberLocations ()
String	predicateName (Object predicate)
Range	rangeType ()
Range	rangeType (ConstExpr lo, ConstExpr hi)
Record	recordType ()
Ref	refAnyType ()
Ref	refType ()
void	setSource (Object birObject, Object source)
BirThread	threadOfKey (Object key)
Private Methods
void	numberLoc (Location loc, LocVector threadLocVector)
void	reserveNames ()
Private Attributes
String	name
int	threadCount = 0
int	locCount = 0
int	stateSize = 0
ThreadVector	threadVector = new ThreadVector()
StateVarVector	stateVarVector = new StateVarVector()
TransVector	transVector = new TransVector()
Vector	definitionVector = new Vector()
Vector	typeVector = new Vector()
Hashtable	definitionTable = new Hashtable()
Hashtable	locationOfKey
Hashtable	stateVarOfKey
Hashtable	sourceMap
Location[]	locationTable
int	numberedLocs
Hashtable	nameTable = new Hashtable()
Hashtable	namedKeyTable = new Hashtable()
Hashtable	threadTable = new Hashtable()
Hashtable	predTable = new Hashtable()
Vector	predVector = new Vector()
StateVarVector	refTargets = new StateVarVector()
Ref	refAnyType = new Ref(refTargets,this)
Static Private Attributes
String[]	reservedNames

---

Detailed Description

A BIR transition system.

This is the top-level object encapsulating a transition system. It contains:

• A name for the system (this is used for filename generation).
• A set of threads.
• A set of state variables.
• A set of definitions.
• Tables associating BIR entities with external keys (useful when constructing the transition system from another representation).
• A naming service (for assigning globally unique names).

Definition at line 57 of file TransSystem.java.

---

Constructor & Destructor Documentation

TransSystem::TransSystem (  String   name )  [inline]

Create a transition system with the given name. Definition at line 198 of file TransSystem.java.

---

Member Function Documentation

void TransSystem::addTrans (  Transformation   trans )  [inline]

Add transformation. Definition at line 205 of file TransSystem.java.

Array TransSystem::arrayType (  Type   baseType, ConstExpr   size )  [inline]

Create array type Definition at line 215 of file TransSystem.java. Referenced by TypeExtractor::createArrayType().

Bool TransSystem::booleanType (    )  [inline]

Create boolean type Definition at line 224 of file TransSystem.java.

Collection TransSystem::collectionType (  Type   baseType, ConstExpr   size )  [inline]

Create collection type Definition at line 235 of file TransSystem.java. Referenced by TypeExtractor::createCollectionType().

String TransSystem::createName (  Object   key, String   proposedName )  [inline]

Create a unqiue name for an external key, given a proposed name Parameters: key   key of entity (may be null) proposedName   proposed name Returns: unique name close to proposed name To facilitate translation, we make the names of all declared entities (variables, threads, definitions) unique using this service. The actual name is constructed from the proposed name by replacing '$' and '.' (which appear in nested class/package names) with '_' (yielding a string we call the 'prefix') and proceding as follows: If the prefix is not yet taken, use it. Otherwise, if the prefix concatenated to "_0" is not yet taken, use it. Continue trying names formed by appending "_1", "_2", etc. to the prefix until we find a name that is not yet in use. Definition at line 263 of file TransSystem.java. Referenced by TypeExtractor::addFields(), TypeExtractor::createArrayType(), TypeExtractor::createRecordType(), and TypeExtractor::createRefType().

BirThread TransSystem::createThread (  String   proposedName, Object   key )  [inline]

Create a thread. Parameters: proposedName   the proposed name of the thread key   external key to associate with thread Returns: new thread Definition at line 284 of file TransSystem.java.

void TransSystem::declarePredicate (  String   proposedName, Expr   expr )  [inline]

Declare a predicate Parameters: proposedName   the proposed name expr   the value of the predicate (and expression on the state) Note: if the proposed name is not legal (e.g., is reserved or already taken), then the name is changed, but the front end is not informed---this should be fixed at some point. Definition at line 302 of file TransSystem.java. Referenced by Builder::declarePredicates().

StateVar TransSystem::declareVar (  Object   key, String   proposedName, BirThread   thread, Type   type, Expr   initVal )  [inline]

Declare a new state variable. Parameters: key   external key associated with state variable proposedName   proposed name of variable thread   thread containing variable (null if global) type   type of variable initVal   initial value (if null, uses default for type) Returns: new state variable Definition at line 319 of file TransSystem.java. Referenced by Builder::createCollections(), and Builder::declareVar().

void TransSystem::define (  Object   key, Definition   definition )  [inline]

Add definition, associate it with a key. Definition at line 336 of file TransSystem.java. Referenced by TypeExtractor::createArrayType(), TypeExtractor::createRecordType(), and TypeExtractor::createRefType().

Enumerated TransSystem::enumeratedType (    )  [inline]

Create enumerated type Definition at line 343 of file TransSystem.java.

Definition TransSystem::getDefinition (  Object   key )  [inline]

Get definition associated with key. Definition at line 352 of file TransSystem.java.

Object TransSystem::getKeyOf (  String   name )  [inline]

Get the key associated with a name. Definition at line 359 of file TransSystem.java. Referenced by Ref::resolveTargets().

StateVarVector TransSystem::getLocalStateVars (  BirThread   thread )  [inline]

Get the local variables of a thread. Definition at line 366 of file TransSystem.java. Referenced by SmvTrans::translateThread().

String TransSystem::getNameOf (  Object   key )  [inline]

Get the name associated with a key. Definition at line 384 of file TransSystem.java. Referenced by TypeExtractor::addFields().

Object TransSystem::getSource (  Object   birObject )  [inline]

Get the source of a BIR object. Definition at line 391 of file TransSystem.java. Referenced by JimpleTrace::JimpleTrace(), and JimpleStore::getThreads().

TransVector TransSystem::getTransformations (    )  [inline]

Get the set of transformations (all threads). Definition at line 399 of file TransSystem.java.

StateVar TransSystem::getVarOfKey (  Object   key )  [inline]

Retrieve state variable associated with key. Definition at line 404 of file TransSystem.java. Referenced by TransExtractor::caseDefinitionStmt(), ExprExtractor::caseLocalExpr(), TransExtractor::getLiveVars(), Builder::initializeGlobal(), and Ref::resolveTargets().

Location TransSystem::locationOfKey (  Object   key, BirThread   thread )  [inline]

Retrieve location associated with key, or create a new location (if none is found). Parameters: key   external key associated with location thread   thread containing location Returns: new location or old location associated with key Definition at line 414 of file TransSystem.java. Referenced by Builder::buildThread(), TransExtractor::locationOfNextStmt(), TransExtractor::locationOfStmt(), and TransExtractor::makeLocation().

Lock TransSystem::lockType (  boolean   waiting, boolean   reentrant )  [inline]

Create lock type Definition at line 430 of file TransSystem.java. Referenced by TypeExtractor::createRecordType().

void TransSystem::numberLocations (    )  [inline]

Number the (reachable) locations depth first (chiefly so they'll print out in a nice order). Definition at line 452 of file TransSystem.java. Referenced by Builder::createTransSystem().

String TransSystem::predicateName (  Object   predicate )  [inline]

Retrieve the name of a predicate given its expression Definition at line 466 of file TransSystem.java. Referenced by SmvTrans::definitions(), and SpinTrans::predicates().

Range TransSystem::rangeType (  ConstExpr   lo, ConstExpr   hi )  [inline]

Create specific range type Definition at line 484 of file TransSystem.java.

Range TransSystem::rangeType (    )  [inline]

Create default range type Definition at line 472 of file TransSystem.java.

Record TransSystem::recordType (    )  [inline]

Create record type Definition at line 493 of file TransSystem.java. Referenced by TypeExtractor::createRecordType().

Ref TransSystem::refAnyType (    )  [inline]

Return ref any type Definition at line 503 of file TransSystem.java. Referenced by SpinTrans::refIndex(), SmvTrans::refIndex(), BirState::setActualSizesFromTrace(), and Ref::toString().

Ref TransSystem::refType (    )  [inline]

Create ref type Definition at line 509 of file TransSystem.java. Referenced by TypeExtractor::createRefType().

void TransSystem::setSource (  Object   birObject, Object   source )  [inline]

Set the source (an arbitrary object) of a BIR object This is used to map a BIR action back to the entity (e.g., a Jimple statement) from which it was generated. Definition at line 525 of file TransSystem.java. Referenced by TypeExtractor::addFields(), TypeExtractor::createRecordType(), and TransExtractor::makeTrans().

BirThread TransSystem::threadOfKey (  Object   key )  [inline]

Retrieve thread associated with key. Definition at line 531 of file TransSystem.java. Referenced by Builder::buildThread(), JimpleStore::isActive(), TransExtractor::oldThreadOperation(), and TransExtractor::threadOperation().

---

Member Data Documentation

Hashtable TransSystem::locationOfKey [private]

Initial value: new Hashtable() Definition at line 71 of file TransSystem.java.

String [] TransSystem::reservedNames [static, private]

This is the set of names that cannot be used for declared entities in a BIR transition system (because they are used by BIR or one of the translator input languages). Definition at line 98 of file TransSystem.java.

Hashtable TransSystem::sourceMap [private]

Initial value: new Hashtable() Definition at line 75 of file TransSystem.java.

Hashtable TransSystem::stateVarOfKey [private]

Initial value: new Hashtable() Definition at line 73 of file TransSystem.java.

---

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

• TransSystem.java

---