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

Class SSAToStatIVisitor

java.lang.Object

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

All Implemented Interfaces:

com.ibm.wala.ssa.SSAInstruction.IVisitor

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

This visitor translates specific Wala SSAInstructions to RangerIR.

Field Summary

Fields

Modifier and Type	Field and Description
private java.util.Map<PhiEdge,java.util.List<PhiCondition>>	blockConditionMap A map that maps a PhiEdge with a list of all conditions that describe the path needs to be taken in the cfg to get to that edge of the phi.
boolean	canVeritest Used to indicate instructions that cannot be veritested.
private com.ibm.wala.ssa.ISSABasicBlock	currentBlock current block where the instruction lies.
private java.util.Deque<PhiCondition>	currentCondition Corresponds to the current condition during walking the CFG.
private com.ibm.wala.ssa.IR	ir IR of the region currently being translated to RangerIR Statement.
private StaticRegionException	pending Used to throw Static Region Exception.
static StaticRegionException	sre
Stmt	veriStatement A translated RangerIR statement.

Constructor Summary

Constructors

Constructor and Description
SSAToStatIVisitor(com.ibm.wala.ssa.IR ir, com.ibm.wala.ssa.ISSABasicBlock currentBlock, java.util.Map<PhiEdge,java.util.List<PhiCondition>> blockConditionMap, java.util.Deque<PhiCondition> currentCondition)

Method Summary

Modifier and Type	Method and Description
void	adjustForDepth(java.util.List<java.util.LinkedList<PhiCondition>> conds) Used to ignore the "out of scope" conditions corresponding to ancestor branches, if this is a phi is for a nested if/then/else,
private za.ac.sun.cs.green.expr.Expression	conjunct(java.util.List<za.ac.sun.cs.green.expr.Expression> le)
Stmt	convert(com.ibm.wala.ssa.SSAInstruction ssa)
private za.ac.sun.cs.green.expr.Expression	createGamma(java.util.List<java.util.LinkedList<PhiCondition>> conds, java.util.List<za.ac.sun.cs.green.expr.Expression> values) Creates Gamma Expression by visiting corresponding Phi
private za.ac.sun.cs.green.expr.Expression	getAndCheckCondition(java.util.List<java.util.LinkedList<PhiCondition>> conds)
Stmt	translatePhi(com.ibm.wala.ssa.SSAPhiInstruction ssaphi) Translates a phi to RangerIR assignment statement of a Gamma expression.
void	visitArrayLength(com.ibm.wala.ssa.SSAArrayLengthInstruction ssaArrayLengthInstruction) Creates RangerIR array length instruction out of SSA array length instruction.
void	visitArrayLoad(com.ibm.wala.ssa.SSAArrayLoadInstruction ssaArrayLoadInstruction) Create an ArrayLoad Instruction in RangerIR.
void	visitArrayStore(com.ibm.wala.ssa.SSAArrayStoreInstruction ssaArrayStoreInstruction) Create an ArrayStore Instruction in RangerIR.
void	visitBinaryOp(com.ibm.wala.ssa.SSABinaryOpInstruction ssa) Create an Assignment Statement in RangerIR for binary operations in Wala.
void	visitCheckCast(com.ibm.wala.ssa.SSACheckCastInstruction ssaCheckCastInstruction) Creates RangerIR check cast instruction out of SSA check cast instruction.
void	visitComparison(com.ibm.wala.ssa.SSAComparisonInstruction ssa) Translates a comparision instruction in Wala SSA to RangerIR assignment statement.
void	visitConditionalBranch(com.ibm.wala.ssa.SSAConditionalBranchInstruction ssa)
void	visitConversion(com.ibm.wala.ssa.SSAConversionInstruction ssa) Casts in SPF involving object creation are beyond what we can support currently in Static regions, else emulate the type casting between primitive types
void	visitGet(com.ibm.wala.ssa.SSAGetInstruction ssaGetInstruction) Creates RangerIR get instruction out of SSA get instruction.
void	visitGetCaughtException(com.ibm.wala.ssa.SSAGetCaughtExceptionInstruction ssaGetCaughtExceptionInstruction) RangerIR does not support getCaughtException.
void	visitGoto(com.ibm.wala.ssa.SSAGotoInstruction ssaGotoInstruction) Goto instructions are not translated to RangerIR and therefore should not be visited by this visitor.
void	visitInstanceof(com.ibm.wala.ssa.SSAInstanceofInstruction ssaInstanceofInstruction) Creates RangerIR instance of instruction out of SSA instance of instruction.
void	visitInvoke(com.ibm.wala.ssa.SSAInvokeInstruction ssaInvokeInstruction) Creates RangerIR invoke instruction out of SSA invoke instruction.
void	visitLoadMetadata(com.ibm.wala.ssa.SSALoadMetadataInstruction ssaLoadMetadataInstruction) RangerIR does not support SSALoadMeta data instruction.
void	visitMonitor(com.ibm.wala.ssa.SSAMonitorInstruction ssaMonitorInstruction) RangerIR currently does not support SSAMonitor instructions.
void	visitNew(com.ibm.wala.ssa.SSANewInstruction ssaNewInstruction) Creates RangerIR new instruction out of SSA new instruction.
void	visitPhi(com.ibm.wala.ssa.SSAPhiInstruction ssaPhiInstruction) Creates RangerIR phi instruction out of Wala's phi instruction.
void	visitPi(com.ibm.wala.ssa.SSAPiInstruction ssaPiInstruction) Ranger IR does not need to support Wala's Pi instruction.
void	visitPut(com.ibm.wala.ssa.SSAPutInstruction ssaPutInstruction) Creates RangerIR put instruction out of SSA put instruction.
void	visitReturn(com.ibm.wala.ssa.SSAReturnInstruction ssaReturnInstruction) Creates RangerIR return instruction out of SSA return instruction.
void	visitSwitch(com.ibm.wala.ssa.SSASwitchInstruction ssaSwitchInstruction) RangerIR currently does not support Switch instruction.
void	visitThrow(com.ibm.wala.ssa.SSAThrowInstruction ssaThrowInstruction) Creates RangerIR throw instruction out of SSA throw instruction.
void	visitUnaryOp(com.ibm.wala.ssa.SSAUnaryOpInstruction ssa) Translates a unary instruction in Wala SSA to RangerIR assignment statement.

Methods inherited from class java.lang.Object

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

Field Detail

veriStatement

public Stmt veriStatement

A translated RangerIR statement.

canVeritest

public boolean canVeritest

Used to indicate instructions that cannot be veritested.

ir

private com.ibm.wala.ssa.IR ir

IR of the region currently being translated to RangerIR Statement.

blockConditionMap

private java.util.Map<PhiEdge,java.util.List<PhiCondition>> blockConditionMap

A map that maps a PhiEdge with a list of all conditions that describe the path needs to be taken in the cfg to get to that edge of the phi.

currentCondition

private java.util.Deque<PhiCondition> currentCondition

Corresponds to the current condition during walking the CFG.

currentBlock

private com.ibm.wala.ssa.ISSABasicBlock currentBlock

current block where the instruction lies.

pending

private StaticRegionException pending

Used to throw Static Region Exception.

sre

public static StaticRegionException sre

Constructor Detail

SSAToStatIVisitor

public SSAToStatIVisitor(com.ibm.wala.ssa.IR ir,
                         com.ibm.wala.ssa.ISSABasicBlock currentBlock,
                         java.util.Map<PhiEdge,java.util.List<PhiCondition>> blockConditionMap,
                         java.util.Deque<PhiCondition> currentCondition)

Method Detail

conjunct

private za.ac.sun.cs.green.expr.Expression conjunct(java.util.List<za.ac.sun.cs.green.expr.Expression> le)

getAndCheckCondition

private za.ac.sun.cs.green.expr.Expression getAndCheckCondition(java.util.List<java.util.LinkedList<PhiCondition>> conds)

createGamma

private za.ac.sun.cs.green.expr.Expression createGamma(java.util.List<java.util.LinkedList<PhiCondition>> conds,
                                                       java.util.List<za.ac.sun.cs.green.expr.Expression> values)
                                                throws StaticRegionException

Creates Gamma Expression by visiting corresponding Phi

Throws:

StaticRegionException

adjustForDepth

public void adjustForDepth(java.util.List<java.util.LinkedList<PhiCondition>> conds)

Used to ignore the "out of scope" conditions corresponding to ancestor branches, if this is a phi is for a nested if/then/else,

Parameters:

conds - Current out of scope conditions.

translatePhi

public Stmt translatePhi(com.ibm.wala.ssa.SSAPhiInstruction ssaphi)
                  throws StaticRegionException

Translates a phi to RangerIR assignment statement of a Gamma expression.

Parameters:

ssaphi - Current PhiInstruction to be translated.

Returns:

A RangerIR assignment statement to a Gamma expression

Throws:

StaticRegionException - An exception that indicates that something went wrong during translation.

visitGoto

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

Goto instructions are not translated to RangerIR and therefore should not be visited by this visitor.

Specified by:

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

Parameters:

ssaGotoInstruction -

visitArrayLoad

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

Create an ArrayLoad Instruction in RangerIR.

Specified by:

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

Parameters:

ssaArrayLoadInstruction - Wala SSA instruction for ArrayLoad

visitArrayStore

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

Create an ArrayStore Instruction in RangerIR.

Specified by:

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

Parameters:

ssaArrayStoreInstruction - Wala SSA instruction for ArrayStore

visitBinaryOp

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

Create an Assignment Statement in RangerIR for binary operations in Wala.

Specified by:

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

Parameters:

ssa - Wala SSA binary instruction.

visitUnaryOp

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

Translates a unary instruction in Wala SSA to RangerIR assignment statement.

Specified by:

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

Parameters:

ssa - SSA unary instruction.

visitConversion

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

Casts in SPF involving object creation are beyond what we can support currently in Static regions, else emulate the type casting between primitive types

Specified by:

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

visitComparison

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

Translates a comparision instruction in Wala SSA to RangerIR assignment statement.

Specified by:

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

Parameters:

ssa - SSA comparision instruction.

visitConditionalBranch

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

Specified by:

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

visitSwitch

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

RangerIR currently does not support Switch instruction.

Specified by:

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

Parameters:

ssaSwitchInstruction -

visitReturn

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

Creates RangerIR return instruction out of SSA return instruction.

Specified by:

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

Parameters:

ssaReturnInstruction -

visitGet

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

Creates RangerIR get instruction out of SSA get instruction.

Specified by:

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

Parameters:

ssaGetInstruction -

visitPut

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

Creates RangerIR put instruction out of SSA put instruction.

Specified by:

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

Parameters:

ssaPutInstruction -

visitInvoke

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

Creates RangerIR invoke instruction out of SSA invoke instruction.

Specified by:

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

Parameters:

ssaInvokeInstruction -

visitNew

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

Creates RangerIR new instruction out of SSA new instruction.

Specified by:

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

Parameters:

ssaNewInstruction -

visitArrayLength

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

Creates RangerIR array length instruction out of SSA array length instruction.

Specified by:

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

Parameters:

ssaArrayLengthInstruction -

visitThrow

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

Creates RangerIR throw instruction out of SSA throw instruction.

Specified by:

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

Parameters:

ssaThrowInstruction -

visitMonitor

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

RangerIR currently does not support SSAMonitor instructions.

Specified by:

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

Parameters:

ssaMonitorInstruction -

visitCheckCast

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

Creates RangerIR check cast instruction out of SSA check cast instruction.

Specified by:

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

Parameters:

ssaCheckCastInstruction -

visitInstanceof

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

Creates RangerIR instance of instruction out of SSA instance of instruction.

Specified by:

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

Parameters:

ssaInstanceofInstruction -

visitPhi

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

Creates RangerIR phi instruction out of Wala's phi instruction.

Specified by:

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

Parameters:

ssaPhiInstruction -

visitPi

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

Ranger IR does not need to support Wala's Pi instruction.

Specified by:

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

Parameters:

ssaPiInstruction -

visitGetCaughtException

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

RangerIR does not support getCaughtException.

Specified by:

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

Parameters:

ssaGetCaughtExceptionInstruction -

visitLoadMetadata

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

RangerIR does not support SSALoadMeta data instruction.

Specified by:

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

Parameters:

ssaLoadMetadataInstruction -

convert

public Stmt convert(com.ibm.wala.ssa.SSAInstruction ssa)
             throws StaticRegionException

Throws:

StaticRegionException