gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment

Class SlotParamTable

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table<java.lang.Integer,V>

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable<int[]>

gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.SlotParamTable

public class SlotParamTable
extends StaticTable<int[]>

This is the basic table, on which the input and output of the region are defined. The table holds the wala vars -> stackSlot mapping if it is not a method region, if it is a method region, then wala vars to parameters to the method are instead populated in this table. In case of a non method region, the map holds for every var all the stackSlots that the var can map to, because a var can map to multiple locations. Also non-input an non-output vars mapping for non method regions can appear in this table if we were able to infer their stack slot.

Field Summary

Fields

Modifier and Type	Field and Description
private com.ibm.wala.ssa.IR	ir
private boolean	isMethodRegion
private Stmt	stmt

Fields inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

label1, label2, table, tableName

Constructor Summary

Constructors

Modifier	Constructor and Description
private	SlotParamTable(boolean isMethodRegion)
	SlotParamTable(com.ibm.wala.ssa.IR ir, java.lang.Boolean isMethodRegion, Stmt stmt)
	SlotParamTable(com.ibm.wala.ssa.IR ir, java.lang.Boolean isMethodRegion, Stmt stmt, Pair<java.lang.Integer,java.lang.Integer> firstUseLastDef, int startingBlockNumber, int terminusBlockNumber)

Method Summary

Modifier and Type	Method and Description
void	filterTable(Pair<java.lang.Integer,java.lang.Integer> firstUseLastDef, java.util.ArrayList<java.lang.Integer> allDefs, java.util.HashSet<java.lang.Integer> allUses)
private int[]	getOperandSlot(com.ibm.wala.ssa.SSAPhiInstruction phi)
java.util.HashSet	getSlots() Finds all unique slots in the stackSlotMap.
java.util.Set	getVarsOfSlot(int slot, java.lang.Integer firstVarId, java.lang.Integer lastVarId) Returns all vars that have the same stack slot entered, between boundaries.
boolean	isConstant(int operand1) Determines if a wala var is constant.
private void	populateParam()
private void	populateSlotsForVars(int startingBlockNumber, int terminusBlockNumber)
void	print() Basic print of the table.
private void	stackSlotPhiPropagation() This tries to infer the stack slots for phi "def" vars and phi "use" vars by either figuring out the stack slots of one "use" var and populate it to be for the phi "def" var, or the opposite, that is the stack slot of the phi "def" was known and so it is propagated to the "use" vars
private boolean	updatePhiUse(com.ibm.wala.ssa.SSAPhiInstruction phi, int[] slots)

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.StaticTable

getKeys, mergeTable, updateKey

Methods inherited from class gov.nasa.jpf.symbc.veritesting.ast.transformations.Environment.Table

add, lookup, mergeTable, remove

Methods inherited from class java.lang.Object

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

Field Detail

ir

private com.ibm.wala.ssa.IR ir

isMethodRegion

private boolean isMethodRegion

stmt

private Stmt stmt

Constructor Detail

SlotParamTable

public SlotParamTable(com.ibm.wala.ssa.IR ir,
                      java.lang.Boolean isMethodRegion,
                      Stmt stmt)

SlotParamTable

public SlotParamTable(com.ibm.wala.ssa.IR ir,
                      java.lang.Boolean isMethodRegion,
                      Stmt stmt,
                      Pair<java.lang.Integer,java.lang.Integer> firstUseLastDef,
                      int startingBlockNumber,
                      int terminusBlockNumber)

SlotParamTable

private SlotParamTable(boolean isMethodRegion)

Method Detail

populateParam

private void populateParam()

populateSlotsForVars

private void populateSlotsForVars(int startingBlockNumber,
                                  int terminusBlockNumber)

filterTable

public void filterTable(Pair<java.lang.Integer,java.lang.Integer> firstUseLastDef,
                        java.util.ArrayList<java.lang.Integer> allDefs,
                        java.util.HashSet<java.lang.Integer> allUses)

getSlots

public java.util.HashSet getSlots()

Finds all unique slots in the stackSlotMap. It attempts to do that by flattening out stackSlots of a single var, which can map to multiple locations.

Returns:

getVarsOfSlot

public java.util.Set getVarsOfSlot(int slot,
                                   java.lang.Integer firstVarId,
                                   java.lang.Integer lastVarId)

Returns all vars that have the same stack slot entered, between boundaries.

Parameters:

slot - A slot number that we wish to discover all vars attaching to it.

firstVarId - A lower bound on the var number to be discovered by this method.

lastVarId - An upper bound on the var numbers to be discovered by this method.

Returns:

All vars that have the same stack slot.

stackSlotPhiPropagation

private void stackSlotPhiPropagation()

This tries to infer the stack slots for phi "def" vars and phi "use" vars by either figuring out the stack slots of one "use" var and populate it to be for the phi "def" var, or the opposite, that is the stack slot of the phi "def" was known and so it is propagated to the "use" vars

updatePhiUse

private boolean updatePhiUse(com.ibm.wala.ssa.SSAPhiInstruction phi,
                             int[] slots)

getOperandSlot

private int[] getOperandSlot(com.ibm.wala.ssa.SSAPhiInstruction phi)

isConstant

public boolean isConstant(int operand1)

Determines if a wala var is constant.

print

public void print()

Description copied from class: Table

Basic print of the table. inside the table.

Overrides:

print in class Table<java.lang.Integer,int[]>