Public Methods | |
TransExtractor (TransSystem system, BirThread thread, StmtGraph stmtGraph, LocalDefs localDefs, LiveLocals liveLocals, SootMethod method, TypeExtractor typeExtract, PredicateSet predSet) | |
void | caseAssignStmt (AssignStmt stmt) |
void | caseDefinitionStmt (DefinitionStmt stmt) |
void | caseEnterMonitorStmt (EnterMonitorStmt stmt) |
void | caseExitMonitorStmt (ExitMonitorStmt stmt) |
void | caseGotoStmt (GotoStmt stmt) |
void | caseIdentityStmt (IdentityStmt stmt) |
void | caseIfStmt (IfStmt stmt) |
void | caseInvokeStmt (InvokeStmt stmt) |
void | caseLookupSwitchStmt (LookupSwitchStmt stmt) |
void | caseNopStmt (NopStmt stmt) |
void | caseTableSwitchStmt (TableSwitchStmt stmt) |
void | defaultCase (Object o) |
boolean | typeRepresented (Type sootType) |
Private Methods | |
AssertAction | buildAssertAction (Stmt stmt, Value expr) |
PrintAction | buildPrintAction (Stmt stmt, Value stringArg) |
StateVarVector | getLiveVars (Stmt stmt) |
edu ksu cis bandera bir Expr | getLockFieldExpr (edu.ksu.cis.bandera.bir.Expr lockRef) |
boolean | ignoringMethodCall (InvokeExpr expr) |
Location | locationOfNextStmt (Stmt stmt) |
Location | locationOfStmt (Unit stmt) |
void | lockOperation (Stmt stmt, VirtualInvokeExpr expr, int opCode) |
Location | makeLocation () |
Transformation | makeTrans (Location fromLoc, Location toLoc, edu.ksu.cis.bandera.bir.Expr guard, Action action, StateVarVector liveVars, Stmt stmt, ExprExtractor extractor) |
edu ksu cis bandera bir Expr | matchCase (edu.ksu.cis.bandera.bir.Expr key, int value) |
boolean | observableLoc (Unit stmt) |
boolean | observableValue (ExprExtractor extractor) |
void | oldThreadOperation (Stmt stmt, StaticInvokeExpr expr, int opCode) |
void | threadOperation (Stmt stmt, VirtualInvokeExpr expr, int opCode) |
Private Attributes | |
TransSystem | system |
LocalDefs | localDefs |
LiveLocals | liveLocals |
BirThread | thread |
StmtGraph | stmtGraph |
SootMethod | method |
TypeExtractor | typeExtract |
PredicateSet | predSet |
SootClassManager | classManager |
Definition at line 66 of file TransExtractor.java.
|
Build an AssertAction from a Bandera.assert() statement. Definition at line 97 of file TransExtractor.java. |
|
Create a PrintAction for a Bandera.print() call. Note: this code is very brittle. It scans the Jimple looking for the arguments to Bandera.print(String s), which are concatentated using StringBuffer calls. Look at the Jimple to better understand the logic. Definition at line 117 of file TransExtractor.java. |
|
Create a transformation for an assignment statement. Definition at line 167 of file TransExtractor.java. |
|
Create transformation for enter monitor statement. Note: we actually create two transformatios. The first has the lockAvailable guard and the lock action. The second, has the hasLock guard. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 217 of file TransExtractor.java. |
|
Create a transformation for exit monitor statement. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 239 of file TransExtractor.java. |
|
Create transformation for goto statement. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 255 of file TransExtractor.java. |
|
Create transformations for IF statement. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 266 of file TransExtractor.java. |
|
Create transformation for method invokation. Most methods should have been inlined. Here, we handle only special cases (e.g., wait(), notify(), assert()). Reimplemented from AbstractBanderaStmtSwitch. Definition at line 299 of file TransExtractor.java. |
|
Create transformations for a lookup swicth statement. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 352 of file TransExtractor.java. |
|
Create transformations for table switch statement. Reimplemented from AbstractBanderaStmtSwitch. Definition at line 387 of file TransExtractor.java. |
|
Get the locals live before a Stmt. Definition at line 425 of file TransExtractor.java. |
|
Get the BIR expression for the lock field of a record. In Jimple, the argument to a lock operation is simply a reference to an object---the lock is implicitly part of that object. In BIR, locks are explicit fields of records. Here, we take a BIR expression that is a reference to a record (the translation of the Jimple expression naming the locked object) and we convert it to a BIR expression for the lock field of that record by dereferencing and selecting the special field BIRLock. Definition at line 452 of file TransExtractor.java. |
|
Test if method call should be ignored. Definition at line 466 of file TransExtractor.java. |
|
Get location of Jimple Stmt that follows a given statement. The Stmt must have at most one successor. Definition at line 481 of file TransExtractor.java. |
|
Get location associated with Jimple Stmt (created if it doesn't exist) Definition at line 504 of file TransExtractor.java. |
|
Build transformations for a lock operation (either wait() or notify()). Definition at line 511 of file TransExtractor.java. |
|
Create a new location. Definition at line 543 of file TransExtractor.java. |
|
Make transformation from one location to another with a given guard and action. This is used to create all transformations and is straightforward except for handling observable Stmts, some of which might translate (by default) to trivial transformations that would then be collapsed away by the Reducer. To prevent this, we test if either the Stmt itself is observable (via a ThreadLocTest) or if the Stmt contains some expression that is observable (e.g., by reference to a global). If so, we make sure there exists an action to mark observable by inserting an empty PrintAction. For thread location tests, we add an extra location just after the Stmt---the test will be true at that location (note: in this case, two transformations are added). Definition at line 563 of file TransExtractor.java. |
|
Generate an BIR equality test for a switch key value to be equal to an integer constant. Definition at line 598 of file TransExtractor.java. |
|
Check if Stmt is observable (appears in a ThreadLocTest). Definition at line 608 of file TransExtractor.java. |
|
Check if some value extracted from an expression is observable. Definition at line 615 of file TransExtractor.java. |
|
This method was used when thread operations were static. Definition at line 622 of file TransExtractor.java. |
|
Construct the transformations for a thread operation (e.g., start()). Note: this code is very brittle. The Jimple is expected to be in a certain form so that the class defining the thread can be found statically. Definition at line 649 of file TransExtractor.java. |
|
Return true if type represented. Definition at line 702 of file TransExtractor.java. |