---

Builder Class Reference

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

Static Public Methods
TransSystem	createTransSystem (SootClass[] sootClasses, String name, int maxArrayLength, int maxCollectSize, int minInt, int maxInt, PredicateSet predSet)
TransSystem	createTransSystem (SootClass[] sootClasses, String name, PredicateSet predSet)
JimpleTrace	interpretTrace (BirTrace trace)
Static Public Attributes
int	COLLECTION_SIZE = DefaultValues.birMaxInstances
int	MAX_ARRAY_LENGTH = DefaultValues.birMaxArrayLen
Private Methods
	Builder (BirThread thread, StmtGraph stmtGraph, SootMethod method)
void	findReachableFrom (Stmt stmt)
Vector	reachableFrom (Stmt stmt)
Static Private Methods
void	buildThread (SootClass sClass, boolean mainClass, PredicateSet predSet)
void	checkForStatics (DefinitionStmt defStmt, Hashtable done)
void	createCollections ()
void	createRecordAndArrayTypes ()
void	createRefTypes ()
void	declareClasses (SootClass[] sootClasses)
void	declareClassGlobals (SootClass sClass)
void	declareGlobals (SootClass[] sootClasses)
void	declarePredicates (PredicateSet predSet)
void	declareThread (SootClass sClass, boolean mainClass)
StateVar	declareVar (Object key, String name, Type sootType, BirThread thread)
void	identifyAllocatorsLocks (SootClass[] sootClasses)
void	initializeGlobal (StaticFieldRef lhs, Value rhs)
void	warn (String s)
Private Attributes
BirThread	thread
StmtGraph	stmtGraph
SootMethod	method
int	mark
Vector	reachableStmts
Static Private Attributes
TransSystem	system
TypeExtractor	typeExtract
DynamicMap	dynamicMap
HashSet	lockedClasses
HashSet	parentClasses

---

Detailed Description

Builder is the main class of BIRC, which extracts a transition system from a restricted Jimple representation of a Java program.

See the BIRC Release Notes for information on what subset of Jimple is currently supported by BIRC.

BIRC is invoked on an array of Soot classes as follows:

  // Parameters 
  SootClass [] staticClasses = ...; // An array of SootClass objects 
  String name = ...;                // Name of system (used for filenames) 
  PredicateSet preds = ...;         // Predicates to embed 
  // Invoke BIRC to build the transition system (BIR) 
  TransSystem system = Builder.createTransSystem(staticClasses, name, preds); 
  // An alternate version of this call allows for setting of default resource 
  // constraints in the transition system 
  // Print the BIR 
  PrintWriter writerOut = new PrintWriter(System.out, true); 
  BirPrinter.print(system, writerOut); 
 

Definition at line 85 of file Builder.java.

---

Member Function Documentation

void Builder::buildThread (  SootClass   sClass, boolean   mainClass, PredicateSet   predSet )  [inline, static, private]

Build a BIR thread from the run() method of a Jimple class. Note: all threads have already been declared (this allows cross references). Definition at line 118 of file Builder.java.

void Builder::checkForStatics (  DefinitionStmt   defStmt, Hashtable   done )  [inline, static, private]

Check for statics on the left and right side of a definition Stmt. If found, and the class of the static has not already been processed, declare a new BIR global variable for the static fields of the class. Definition at line 167 of file Builder.java.

void Builder::createCollections (    )  [inline, static, private]

Given the dynamic map, create a collection for each collection key that was declared in the map. The size of a collection is the sum of the sizes of all map entries stored in that collection. Definition at line 191 of file Builder.java.

void Builder::createRecordAndArrayTypes (    )  [inline, static, private]

For each Jimple class and array type, create a corresponding BIR record/array type using the type extractor. Definition at line 246 of file Builder.java.

void Builder::createRefTypes (    )  [inline, static, private]

Once the dynamic map has been constructed, create a reference type for each class, array type, and interface. These types will be used to represent the Java reference types of the Jimple. Note that, at this point, we have not yet created the collections, the the reference types are unresolved. Definition at line 300 of file Builder.java.

TransSystem Builder::createTransSystem (  SootClasssootClasses  [], String   name, PredicateSet   predSet )  [inline, static]

Creates a transition system from a set of Soot classes. Parameters: threadClasses   an array of SootClass objects containing methods that represent the code executed by threads. The first class must have a static method main() and the remaining classes must each have a method run(). allClasses   an array of SootClass objects referenced name   name of transition system (used to generate filenames) predSet   set of predicates to embed (can be null) Returns: a transition system representing the Soot classes Definition at line 370 of file Builder.java.

TransSystem Builder::createTransSystem (  SootClasssootClasses  [], String   name, int   maxArrayLength, int   maxCollectSize, int   minInt, int   maxInt, PredicateSet   predSet )  [inline, static]

Creates a transition system from a set of Soot classes. Parameters: sootClasses   an array of SootClass objects containing methods that represent the code executed by threads. The first class must have a static method main() and the remaining classes must each have a static method run(). name   name of transition system (used to generate filenames) predSet   set of predicates to embed (can be null) maxArrayLength   maximum length of an array maxCollectSize   maximum size of a heap collection minInt   minimum value for integer maxInt   maximum value for integer Returns: a transition system representing the Soot classes Definition at line 344 of file Builder.java.

void Builder::declareClassGlobals (  SootClass   sClass )  [inline, static, private]

Declare a BIR variable for each static field of a class. Note: we ignore the built-in classes in any subpackage of java.* Definition at line 409 of file Builder.java.

void Builder::declareGlobals (  SootClasssootClasses  [] )  [inline, static, private]

Declare global BIR variables for all Jimple static variables referenced in the body of some thread. Also declare a 'this' variable for each thread except the main thread to hold the reference to the Runnable or Thread object that owns the thread's run() method. Definition at line 451 of file Builder.java.

void Builder::declarePredicates (  PredicateSet   predSet )  [inline, static, private]

For each predicate declared, use an expression extractor to translate the Jimple Expr for the predicate into a BIR Expr, then declare that as the BIR predciate. Definition at line 482 of file Builder.java.

StateVar Builder::declareVar (  Object   key, String   name, Type   sootType, BirThread   thread )  [inline, static, private]

Declare a BIR variable in the transition system. The type extractor is used to convert the SootType into a BIR type. If the SootType is not representable (type extractor returns null), then we ignore this variable (with a warning). Definition at line 508 of file Builder.java.

void Builder::identifyAllocatorsLocks (  SootClasssootClasses  [] )  [inline, static, private]

Heap objects are stored in BIR collections, which must be declared. We build a "dynamic map" that defines, for each allocator site (NewExpr or NewArrayExpr), which collection will hold the elements of that site. Currently, we simply create a collection for each allocator site. This method accepts the soot classes that define the bodies of the threads, and it looks for allocator expressions in the code for these threads, defining a dynamic map entry for each. In addition this code determines the set of types that are explicitly locked in statements that are reachable from the threads. These will be used to determine which classes need to have locks allocated in the model. Definition at line 552 of file Builder.java.

void Builder::initializeGlobal (  StaticFieldRef   lhs, Value   rhs )  [inline, static, private]

Set initial value of static field. Currently, this only works if the assigned value is static. Definition at line 636 of file Builder.java.

JimpleTrace Builder::interpretTrace (  BirTrace   trace )  [inline, static]

Interpret a BIR trace in terms of the Jimple code from which it was created. Parameters: trace   - a BIR trace of a transition system created by BIRC Returns: the corresponding Jimple trace Definition at line 653 of file Builder.java.

Vector Builder::reachableFrom (  Stmt   stmt )  [inline, private]

Do a depth first search of the statement graph and return a vector of all statements reachable from a given statement. We do this to eliminate exception handlers, which are not reachable in the BriefStmtGraph (the CompleteStmtGraph contains arcs representing possible exception raising, so the exception handlers are reachable in that graph). Definition at line 667 of file Builder.java. Referenced by buildThread().

---

Member Data Documentation

int Builder::COLLECTION_SIZE = DefaultValues.birMaxInstances [static]

These are the default sizes of collections and arrays. In the future, these should come from the front end. Definition at line 91 of file Builder.java.

---

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

• Builder.java

---