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

Class StackSlotIVisitor

java.lang.Object

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

All Implemented Interfaces:

com.ibm.wala.ssa.SSAInstruction.IVisitor

public class StackSlotIVisitor
extends java.lang.Object
implements com.ibm.wala.ssa.SSAInstruction.IVisitor

This visitor fills the stack slots for wala vars.

Field Summary

Fields

Modifier and Type	Field and Description
private com.ibm.wala.ssa.IR	ir
SlotParamTable	slotParamTable

Constructor Summary

Constructors

Constructor and Description
StackSlotIVisitor(com.ibm.wala.ssa.IR ir, SlotParamTable slotParamTable)

Method Summary

Modifier and Type	Method and Description
void	populateVars(com.ibm.wala.ssa.SSAInstruction ins, int var) This method is used only to get the stack slot of "use" vars, which are either already defined in a previous "def" and so it will be in the stackSlotMap.
void	visitArrayLength(com.ibm.wala.ssa.SSAArrayLengthInstruction ins)
void	visitArrayLoad(com.ibm.wala.ssa.SSAArrayLoadInstruction ins)
void	visitArrayStore(com.ibm.wala.ssa.SSAArrayStoreInstruction ins)
void	visitBinaryOp(com.ibm.wala.ssa.SSABinaryOpInstruction ins)
void	visitCheckCast(com.ibm.wala.ssa.SSACheckCastInstruction ins)
void	visitComparison(com.ibm.wala.ssa.SSAComparisonInstruction ins)
void	visitConditionalBranch(com.ibm.wala.ssa.SSAConditionalBranchInstruction ins)
void	visitConversion(com.ibm.wala.ssa.SSAConversionInstruction ins)
void	visitGet(com.ibm.wala.ssa.SSAGetInstruction ins)
void	visitGetCaughtException(com.ibm.wala.ssa.SSAGetCaughtExceptionInstruction ssaGetCaughtExceptionInstruction)
void	visitGoto(com.ibm.wala.ssa.SSAGotoInstruction ssaGotoInstruction)
void	visitInstanceof(com.ibm.wala.ssa.SSAInstanceofInstruction ins)
void	visitInvoke(com.ibm.wala.ssa.SSAInvokeInstruction ins)
void	visitLoadMetadata(com.ibm.wala.ssa.SSALoadMetadataInstruction ssaLoadMetadataInstruction)
void	visitMonitor(com.ibm.wala.ssa.SSAMonitorInstruction ssaMonitorInstruction)
void	visitNew(com.ibm.wala.ssa.SSANewInstruction ssaNewInstruction)
void	visitPhi(com.ibm.wala.ssa.SSAPhiInstruction ins)
void	visitPi(com.ibm.wala.ssa.SSAPiInstruction ssaPiInstruction)
void	visitPut(com.ibm.wala.ssa.SSAPutInstruction ins)
void	visitReturn(com.ibm.wala.ssa.SSAReturnInstruction ins)
void	visitSwitch(com.ibm.wala.ssa.SSASwitchInstruction ins)
void	visitThrow(com.ibm.wala.ssa.SSAThrowInstruction ssaThrowInstruction)
void	visitUnaryOp(com.ibm.wala.ssa.SSAUnaryOpInstruction ins)

Methods inherited from class java.lang.Object

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

Field Detail

slotParamTable

public final SlotParamTable slotParamTable

ir

private com.ibm.wala.ssa.IR ir

Constructor Detail

StackSlotIVisitor

public StackSlotIVisitor(com.ibm.wala.ssa.IR ir,
                         SlotParamTable slotParamTable)

Method Detail

visitGoto

public void visitGoto(com.ibm.wala.ssa.SSAGotoInstruction ssaGotoInstruction)

Specified by:

visitGoto in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayLoad

public void visitArrayLoad(com.ibm.wala.ssa.SSAArrayLoadInstruction ins)

Specified by:

visitArrayLoad in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayStore

public void visitArrayStore(com.ibm.wala.ssa.SSAArrayStoreInstruction ins)

Specified by:

visitArrayStore in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitBinaryOp

public void visitBinaryOp(com.ibm.wala.ssa.SSABinaryOpInstruction ins)

Specified by:

visitBinaryOp in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitUnaryOp

public void visitUnaryOp(com.ibm.wala.ssa.SSAUnaryOpInstruction ins)

Specified by:

visitUnaryOp in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitConversion

public void visitConversion(com.ibm.wala.ssa.SSAConversionInstruction ins)

Specified by:

visitConversion in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitComparison

public void visitComparison(com.ibm.wala.ssa.SSAComparisonInstruction ins)

Specified by:

visitComparison in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitConditionalBranch

public void visitConditionalBranch(com.ibm.wala.ssa.SSAConditionalBranchInstruction ins)

Specified by:

visitConditionalBranch in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitSwitch

public void visitSwitch(com.ibm.wala.ssa.SSASwitchInstruction ins)

Specified by:

visitSwitch in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitReturn

public void visitReturn(com.ibm.wala.ssa.SSAReturnInstruction ins)

Specified by:

visitReturn in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitGet

public void visitGet(com.ibm.wala.ssa.SSAGetInstruction ins)

Specified by:

visitGet in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPut

public void visitPut(com.ibm.wala.ssa.SSAPutInstruction ins)

Specified by:

visitPut in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitInvoke

public void visitInvoke(com.ibm.wala.ssa.SSAInvokeInstruction ins)

Specified by:

visitInvoke in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitNew

public void visitNew(com.ibm.wala.ssa.SSANewInstruction ssaNewInstruction)

Specified by:

visitNew in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitArrayLength

public void visitArrayLength(com.ibm.wala.ssa.SSAArrayLengthInstruction ins)

Specified by:

visitArrayLength in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitThrow

public void visitThrow(com.ibm.wala.ssa.SSAThrowInstruction ssaThrowInstruction)

Specified by:

visitThrow in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitMonitor

public void visitMonitor(com.ibm.wala.ssa.SSAMonitorInstruction ssaMonitorInstruction)

Specified by:

visitMonitor in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitCheckCast

public void visitCheckCast(com.ibm.wala.ssa.SSACheckCastInstruction ins)

Specified by:

visitCheckCast in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitInstanceof

public void visitInstanceof(com.ibm.wala.ssa.SSAInstanceofInstruction ins)

Specified by:

visitInstanceof in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPhi

public void visitPhi(com.ibm.wala.ssa.SSAPhiInstruction ins)

Specified by:

visitPhi in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitPi

public void visitPi(com.ibm.wala.ssa.SSAPiInstruction ssaPiInstruction)

Specified by:

visitPi in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitGetCaughtException

public void visitGetCaughtException(com.ibm.wala.ssa.SSAGetCaughtExceptionInstruction ssaGetCaughtExceptionInstruction)

Specified by:

visitGetCaughtException in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

visitLoadMetadata

public void visitLoadMetadata(com.ibm.wala.ssa.SSALoadMetadataInstruction ssaLoadMetadataInstruction)

Specified by:

visitLoadMetadata in interface com.ibm.wala.ssa.SSAInstruction.IVisitor

populateVars

public void populateVars(com.ibm.wala.ssa.SSAInstruction ins,
                         int var)

This method is used only to get the stack slot of "use" vars, which are either already defined in a previous "def" and so it will be in the stackSlotMap. This is done also for phiInstruction, but phi requires a fix point computation and propagation of vars to stack slot discovery. This happens during the construction of the stack slot table object.

Parameters:

ins - Instruction currently being explored for slots.

var - Variable that we try to find its stack slot.