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

Class SpfCasesPass2Visitor

java.lang.Object

gov.nasa.jpf.symbc.veritesting.ast.transformations.SPFCases.SpfCasesPass2Visitor

All Implemented Interfaces:

AstVisitor<Stmt>

public class SpfCasesPass2Visitor
extends java.lang.Object
implements AstVisitor<Stmt>

This is the second pass of the SPFCases where the SPFCases nodes are eliminated and instead the dynamic region is populated with the predicates for the SPFCases. Some optimization are done here to maintain a minimal RangerIR for the dynamic Region.

Field Summary

Fields

Modifier and Type	Field and Description
private za.ac.sun.cs.green.expr.Expression	earlyReturnCondition
private java.util.LinkedHashSet<SPFCaseStmt>	spfCaseSet
private za.ac.sun.cs.green.expr.Expression	spfCondition

Constructor Summary

Constructors

Constructor and Description
SpfCasesPass2Visitor()

Method Summary

Modifier and Type	Method and Description
static DynamicRegion	execute(DynamicRegion dynRegion) This executes the second path of the SPFCases.
Stmt	visit(ArrayLengthInstruction c)
Stmt	visit(ArrayLoadInstruction c)
Stmt	visit(ArrayStoreInstruction c)
Stmt	visit(AssignmentStmt a)
Stmt	visit(CheckCastInstruction c)
Stmt	visit(CompositionStmt a)
Stmt	visit(GetInstruction c)
Stmt	visit(IfThenElseStmt a)
Stmt	visit(InstanceOfInstruction c)
Stmt	visit(InvokeInstruction c)
Stmt	visit(NewInstruction c)
Stmt	visit(PhiInstruction c)
Stmt	visit(PutInstruction c)
Stmt	visit(ReturnInstruction c)
Stmt	visit(SkipStmt a)
Stmt	visit(SPFCaseStmt c)
Stmt	visit(SwitchInstruction c)
Stmt	visit(ThrowInstruction c)

Methods inherited from class java.lang.Object

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

Field Detail

spfCondition

private za.ac.sun.cs.green.expr.Expression spfCondition

spfCaseSet

private final java.util.LinkedHashSet<SPFCaseStmt> spfCaseSet

earlyReturnCondition

private za.ac.sun.cs.green.expr.Expression earlyReturnCondition

Constructor Detail

SpfCasesPass2Visitor

public SpfCasesPass2Visitor()

Method Detail

visit

public Stmt visit(AssignmentStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(CompositionStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(IfThenElseStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(SkipStmt a)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(SPFCaseStmt c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(ArrayLoadInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(ArrayStoreInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(SwitchInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(ReturnInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(GetInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(PutInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(NewInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(InvokeInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(ArrayLengthInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(ThrowInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(CheckCastInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(InstanceOfInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

visit

public Stmt visit(PhiInstruction c)

Specified by:

visit in interface AstVisitor<Stmt>

execute

public static DynamicRegion execute(DynamicRegion dynRegion)

This executes the second path of the SPFCases. It removes all SPFCases nodes and creates a new condition instead onto the spfCaseSet. There is still one more step that SPFCases needs to go through which is actually generating a green expression out of the spfCaseSet, this happens seperately after the green transformation is done.

Parameters:

dynRegion - Dynamic region for which SPFCases nodes are going to be removed from the AST and replaced with a condition onto the spfCaseSet instead.

Returns:

Dynamic Region with a new AST and spfCaseSet populated.