de.uka.ilkd.key.rule.metaconstruct

Class WhileLoopTransformation

java.lang.Object

de.uka.ilkd.key.java.visitor.JavaASTWalker

de.uka.ilkd.key.java.visitor.JavaASTVisitor

de.uka.ilkd.key.rule.metaconstruct.WhileLoopTransformation

All Implemented Interfaces:

Visitor

Direct Known Subclasses:

ForToWhileTransformation, WhileInvariantTransformation

public class WhileLoopTransformation
extends JavaASTVisitor

Walks through a java AST in depth-left-fist-order. This walker is used to transform a loop (not only while loops) according to the rules of the dynamic logic.

Nested Class Summary

Nested Classes

Modifier and Type	Class and Description
private class	WhileLoopTransformation.DefaultAction

Field Summary

Fields

Modifier and Type	Field and Description
protected Break	breakInnerLabel break innerlabel
protected Break	breakOuterLabel break outerlabel
protected static java.lang.Boolean	CHANGED
protected static int	CHECK
protected SVInstantiations	instantiations if run in check mode there are normally schemavaribles, so we need the instantiations of them
protected ExtList	labelList
protected java.util.Stack<Label>	labelStack
protected java.util.Stack<MethodFrame>	methodStack
protected boolean	needInnerLabel Indicates if an unlabled continue has been found or if a labelled continue with a label outside of the loop currently transformed has been found.
protected boolean	needOuterLabel indicates if an unlabled break has been found and an outer label is needed
protected int	newLabels counts the number of labelled continues with an label outside the while loop that is transformed
protected int	replaceBreakWithNoLabel if there is a loop inside the loop the breaks of these inner loops have not to be replaced.
protected ProgramElement	replacement the replacement element
protected ProgramElement	result the result of the transformation
protected int	runMode there are two modes the visitor can be run.
protected java.util.Stack<ExtList>	stack
protected static int	TRANSFORMATION

Fields inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

services

Constructor Summary

Constructors

Constructor and Description
WhileLoopTransformation(ProgramElement root, ProgramElementName outerLabel, ProgramElementName innerLabel, Services services) creates the WhileLoopTransformation for the transformation mode
WhileLoopTransformation(ProgramElement root, SVInstantiations inst, Services services) creates the WhileLoopTransformation for the check mode

Method Summary

Modifier and Type	Method and Description
protected void	addChild(SourceElement x)
protected void	changed()
protected void	doAction(ProgramElement node) the action that is performed just before leaving the node the last time
protected void	doDefaultAction(SourceElement x) the implemented default action is called if a program element is, and if it has children all its children too are left unchanged
private static Guard	getForGuard(For x, ExtList changeList)
private static Statement[]	getInnerBlockStatements(IForUpdates updates, Statement body, For remainder, int updateSize)
boolean	innerLabelNeeded() returns true if an inner label is needed
boolean	outerLabelNeeded() returns true if an outer label is needed
void	performActionOnBreak(Break x)
void	performActionOnCase(Case x)
void	performActionOnCatch(Catch x)
void	performActionOnContinue(Continue x)
void	performActionOnCopyAssignment(CopyAssignment x)
void	performActionOnDefault(Default x)
void	performActionOnDo(Do x)
void	performActionOnElse(Else x)
void	performActionOnEnhancedFor(EnhancedFor x) perform the loop transformation on an enhanced for loop (Java5) If the enhanced for loop is the toplevel loop nothing happens - return the loop itself, as enhanced for loops cannot be unwound, a log message is issued.
void	performActionOnFinally(Finally x)
void	performActionOnFor(For x) public void performActionOnFor(For x) { ExtList changeList = stack.peek(); if (replaceBreakWithNoLabel==0) { //most outer for loop if (changeList.getFirst() == CHANGED) changeList.removeFirst(); LoopInitializer init[] = new LoopInitializer[x.getInitializers().size()]; Expression[] updates = new Expression[x.getUpdates().size()]; s //the unchanged updates need to be extracted to initialize the //remainding 'for' statement Expression[] unchangedUpdates = new Expression[x.getUpdates().size()]; Expression guard = null; Statement body = null; ProgramElement element = (ProgramElement) (changeList.isEmpty() ?
void	performActionOnIf(If x)
void	performActionOnLabeledStatement(LabeledStatement x)
void	performActionOnLocalVariableDeclaration(LocalVariableDeclaration x)
void	performActionOnMethodFrame(MethodFrame x)
void	performActionOnSchemaVariable(SchemaVariable sv)
void	performActionOnStatementBlock(StatementBlock x)
void	performActionOnSwitch(Switch x)
void	performActionOnSynchronizedBlock(SynchronizedBlock x)
void	performActionOnThen(Then x)
void	performActionOnTry(Try x)
void	performActionOnWhile(While x) Performs the unwinding of the loop Warning: The unwinding does not comply with the rule in the KeY book up to 100% The difference is revealed by the following example: Label1:while(c){b} According to the KeY book the transformation should be if(c) l':{l'':{p#} Label1:while(c){b}} This implementation creates however.
protected boolean	replaceJumpStatement(LabelJumpStatement x)
ProgramElement	result()
void	start() starts the walker
java.lang.String	toString()
protected void	walk(ProgramElement node) walks through the AST.

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTVisitor

performActionOnAbstractProgramElement, performActionOnAllFields, performActionOnAllObjects, performActionOnArrayDeclaration, performActionOnArrayInitializer, performActionOnArrayLengthReference, performActionOnArrayReference, performActionOnAssert, performActionOnBinaryAnd, performActionOnBinaryAndAssignment, performActionOnBinaryNot, performActionOnBinaryOr, performActionOnBinaryOrAssignment, performActionOnBinaryXOr, performActionOnBinaryXOrAssignment, performActionOnBlockContract, performActionOnBlockContract, performActionOnBooleanLiteral, performActionOnCatchAllStatement, performActionOnCharLiteral, performActionOnClassDeclaration, performActionOnClassInitializer, performActionOnComment, performActionOnCompilationUnit, performActionOnConditional, performActionOnConstructorDeclaration, performActionOnContextStatementBlock, performActionOnDivide, performActionOnDivideAssignment, performActionOnDLEmbeddedExpression, performActionOnDoubleLiteral, performActionOnEmptyMapLiteral, performActionOnEmptySeqLiteral, performActionOnEmptySetLiteral, performActionOnEmptyStatement, performActionOnEquals, performActionOnExactInstanceof, performActionOnExecutionContext, performActionOnExtends, performActionOnFieldDeclaration, performActionOnFieldReference, performActionOnFieldSpecification, performActionOnFloatLiteral, performActionOnForUpdates, performActionOnGreaterOrEquals, performActionOnGreaterThan, performActionOnGuard, performActionOnImplements, performActionOnImplicitFieldSpecification, performActionOnImport, performActionOnInstanceof, performActionOnInterfaceDeclaration, performActionOnIntersect, performActionOnIntLiteral, performActionOnIProgramVariable, performActionOnLessOrEquals, performActionOnLessThan, performActionOnLocationVariable, performActionOnLogicalAnd, performActionOnLogicalNot, performActionOnLogicalOr, performActionOnLongLiteral, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopContract, performActionOnLoopInit, performActionOnLoopInvariant, performActionOnLoopScopeBlock, performActionOnMergeContract, performActionOnMergePointStatement, performActionOnMetaClassReference, performActionOnMethod, performActionOnMethodBodyStatement, performActionOnMethodDeclaration, performActionOnMethodReference, performActionOnMinus, performActionOnMinusAssignment, performActionOnModifier, performActionOnModulo, performActionOnModuloAssignment, performActionOnNegative, performActionOnNew, performActionOnNewArray, performActionOnNotEquals, performActionOnNullLiteral, performActionOnPackageReference, performActionOnPackageSpecification, performActionOnParameterDeclaration, performActionOnParenthesizedExpression, performActionOnPassiveExpression, performActionOnPlus, performActionOnPlusAssignment, performActionOnPositive, performActionOnPostDecrement, performActionOnPostIncrement, performActionOnPreDecrement, performActionOnPreIncrement, performActionOnProgramConstant, performActionOnProgramElementName, performActionOnProgramMetaConstruct, performActionOnProgramMethod, performActionOnProgramVariable, performActionOnReturn, performActionOnSchematicFieldReference, performActionOnSeqConcat, performActionOnSeqGet, performActionOnSeqIndexOf, performActionOnSeqLength, performActionOnSeqReverse, performActionOnSeqSingleton, performActionOnSeqSub, performActionOnSetMinus, performActionOnSetUnion, performActionOnShiftLeft, performActionOnShiftLeftAssignment, performActionOnShiftRight, performActionOnShiftRightAssignment, performActionOnSingleton, performActionOnStringLiteral, performActionOnSuperArrayDeclaration, performActionOnSuperConstructorReference, performActionOnSuperReference, performActionOnThisConstructorReference, performActionOnThisReference, performActionOnThrow, performActionOnThrows, performActionOnTimes, performActionOnTimesAssignment, performActionOnTransactionStatement, performActionOnTypeCast, performActionOnTypeReference, performActionOnUnsignedShiftRight, performActionOnUnsignedShiftRightAssignment, performActionOnVariableDeclaration, performActionOnVariableReference, performActionOnVariableSpecification

Methods inherited from class de.uka.ilkd.key.java.visitor.JavaASTWalker

depth, root

Methods inherited from class java.lang.Object

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

Field Detail

CHANGED

protected static final java.lang.Boolean CHANGED

TRANSFORMATION

protected static final int TRANSFORMATION

See Also:

Constant Field Values

CHECK

protected static final int CHECK

See Also:

Constant Field Values

replacement

protected ProgramElement replacement

the replacement element

breakOuterLabel

protected Break breakOuterLabel

break outerlabel

breakInnerLabel

protected Break breakInnerLabel

break innerlabel

labelList

protected ExtList labelList

stack

protected java.util.Stack<ExtList> stack

replaceBreakWithNoLabel

protected int replaceBreakWithNoLabel

if there is a loop inside the loop the breaks of these inner loops have not to be replaced. The replaceBreakWithNoLabel counts the depth of the loop cascades. Replacements are only performed if the value of the variable is zero.

runMode

protected int runMode

there are two modes the visitor can be run. The check and transformation mode. In the check mode it is only looked if there are unlabeled break and continues that needs to be replaced, the transformation mode performs the unwinding of the loop with all necessary replacements

needOuterLabel

protected boolean needOuterLabel

indicates if an unlabled break has been found and an outer label is needed

needInnerLabel

protected boolean needInnerLabel

Indicates if an unlabled continue has been found or if a labelled continue with a label outside of the loop currently transformed has been found. Then an inner label is needed.

newLabels

protected int newLabels

counts the number of labelled continues with an label outside the while loop that is transformed

instantiations

protected SVInstantiations instantiations

if run in check mode there are normally schemavaribles, so we need the instantiations of them

result

protected ProgramElement result

the result of the transformation

labelStack

protected java.util.Stack<Label> labelStack

methodStack

protected java.util.Stack<MethodFrame> methodStack

Constructor Detail

WhileLoopTransformation

public WhileLoopTransformation(ProgramElement root,
                               ProgramElementName outerLabel,
                               ProgramElementName innerLabel,
                               Services services)

creates the WhileLoopTransformation for the transformation mode

Parameters:

root - the ProgramElement where to begin

outerLabel - the ProgramElementName of the outer label

innerLabel - the ProgramElementName of the inner label

services - services instance

WhileLoopTransformation

public WhileLoopTransformation(ProgramElement root,
                               SVInstantiations inst,
                               Services services)

creates the WhileLoopTransformation for the check mode

Parameters:

root - the ProgramElement where to begin

inst - the SVInstantiations if available

services - services instance

Method Detail

getForGuard

private static Guard getForGuard(For x,
                                 ExtList changeList)

getInnerBlockStatements

private static Statement[] getInnerBlockStatements(IForUpdates updates,
                                                   Statement body,
                                                   For remainder,
                                                   int updateSize)

innerLabelNeeded

public boolean innerLabelNeeded()

returns true if an inner label is needed

Returns:

boolean as described above

outerLabelNeeded

public boolean outerLabelNeeded()

returns true if an outer label is needed

Returns:

boolean as described above

doAction

protected void doAction(ProgramElement node)

the action that is performed just before leaving the node the last time

Overrides:

doAction in class JavaASTVisitor

Parameters:

node - respective node as program element

start

public void start()

starts the walker

Overrides:

start in class JavaASTWalker

result

public ProgramElement result()

walk

protected void walk(ProgramElement node)

walks through the AST. While keeping track of the current node

Overrides:

walk in class JavaASTVisitor

Parameters:

node - the JavaProgramElement the walker is at

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

doDefaultAction

protected void doDefaultAction(SourceElement x)

the implemented default action is called if a program element is, and if it has children all its children too are left unchanged

Specified by:

doDefaultAction in class JavaASTVisitor

Parameters:

x - source element

performActionOnSchemaVariable

public void performActionOnSchemaVariable(SchemaVariable sv)

Specified by:

performActionOnSchemaVariable in interface Visitor

Overrides:

performActionOnSchemaVariable in class JavaASTVisitor

performActionOnLocalVariableDeclaration

public void performActionOnLocalVariableDeclaration(LocalVariableDeclaration x)

Specified by:

performActionOnLocalVariableDeclaration in interface Visitor

Overrides:

performActionOnLocalVariableDeclaration in class JavaASTVisitor

performActionOnStatementBlock

public void performActionOnStatementBlock(StatementBlock x)

Specified by:

performActionOnStatementBlock in interface Visitor

Overrides:

performActionOnStatementBlock in class JavaASTVisitor

replaceJumpStatement

protected boolean replaceJumpStatement(LabelJumpStatement x)

performActionOnBreak

public void performActionOnBreak(Break x)

Specified by:

performActionOnBreak in interface Visitor

Overrides:

performActionOnBreak in class JavaASTVisitor

performActionOnContinue

public void performActionOnContinue(Continue x)

Specified by:

performActionOnContinue in interface Visitor

Overrides:

performActionOnContinue in class JavaASTVisitor

performActionOnFor

public void performActionOnFor(For x)

public void performActionOnFor(For x) { ExtList changeList = stack.peek(); if (replaceBreakWithNoLabel==0) { //most outer for loop if (changeList.getFirst() == CHANGED) changeList.removeFirst(); LoopInitializer init[] = new LoopInitializer[x.getInitializers().size()]; Expression[] updates = new Expression[x.getUpdates().size()]; s //the unchanged updates need to be extracted to initialize the //remainding 'for' statement Expression[] unchangedUpdates = new Expression[x.getUpdates().size()]; Expression guard = null; Statement body = null; ProgramElement element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); // get loop initializers int foundInitializers = 0; while (element instanceof LoopInitializer) { init[foundInitializers] = (LoopInitializer) element; element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); foundInitializers++; } de.uka.ilkd.key.util.Debug.assertTrue (init.length == x.getInitializers().size(), "Critical Error: not all initializers found. "+ "performActionOnFor in WhileLoopTransformation."); // get guard if (x.getGuard() != null) { guard = (Expression)element; } // getUpdates int foundUpdates = 0; element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); while (element instanceof Expression && foundUpdates(innerBlockStatements)))); //outerBlockStatements[init.length+1] = remainder; if (breakOuterLabel!=null) addChild(new LabeledStatement(breakOuterLabel.getLabel(), new StatementBlock( new ArrayOf(outerBlockStatements)))); else addChild(new StatementBlock(new ArrayOf(outerBlockStatements))); changed(); } else { if (changeList.getFirst() == CHANGED) { changeList.removeFirst(); LoopInitializer init[] = new LoopInitializer[x.getInitializers().size()]; Expression[] updates = new Expression[x.getUpdates().size()]; Expression guard = null; Statement body = null; ProgramElement element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); // get loop initializers int foundInitializers = 0; while (element instanceof LoopInitializer) { init[foundInitializers] = (LoopInitializer) element; element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); foundInitializers++; } de.uka.ilkd.key.util.Debug.assertTrue (init.length == x.getInitializers().size(), "Critical Error: not all initializers found. "+ "performActionOnFor in WhileLoopTransformation."); // get guard if (x.getGuard() != null) { guard = (Expression)element; } // getUpdates int foundUpdates = 0; element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); while (element instanceof Expression) { updates[foundUpdates] = (Expression) element; element = (ProgramElement) (changeList.isEmpty() ? null : changeList.removeFirst()); foundUpdates++; } de.uka.ilkd.key.util.Debug.assertTrue (updates.length == x.getUpdates().size(), "Critical Error: not all updates found. "+ "performActionOnFor in WhileLoopTransformation."); // getBody body = (Statement) element; addChild(new For(init, guard, updates, body)); changed(); } else { doDefaultAction(x); } } }

Specified by:

performActionOnFor in interface Visitor

Overrides:

performActionOnFor in class JavaASTVisitor

Parameters:

x - For loop statement

performActionOnEnhancedFor

public void performActionOnEnhancedFor(EnhancedFor x)

perform the loop transformation on an enhanced for loop (Java5) If the enhanced for loop is the toplevel loop nothing happens - return the loop itself, as enhanced for loops cannot be unwound, a log message is issued. If it is a loop deeper in the AST a new object is created if needed or the original loop returned.

Specified by:

performActionOnEnhancedFor in interface Visitor

Overrides:

performActionOnEnhancedFor in class JavaASTVisitor

Parameters:

x - EnhancedFor loop statement

performActionOnWhile

public void performActionOnWhile(While x)

Performs the unwinding of the loop Warning: The unwinding does not comply with the rule in the KeY book up to 100% The difference is revealed by the following example: Label1:while(c){b} According to the KeY book the transformation should be if(c) l':{l'':{p#} Label1:while(c){b}} This implementation creates however. Label1:if(c) l':{l'':{p#} while(c){b}} Check if this is ok when labeled continue statements are involved.

Specified by:

performActionOnWhile in interface Visitor

Overrides:

performActionOnWhile in class JavaASTVisitor

Parameters:

x - the while statement

performActionOnDo

public void performActionOnDo(Do x)

Specified by:

performActionOnDo in interface Visitor

Overrides:

performActionOnDo in class JavaASTVisitor

performActionOnIf

public void performActionOnIf(If x)

Specified by:

performActionOnIf in interface Visitor

Overrides:

performActionOnIf in class JavaASTVisitor

performActionOnSwitch

public void performActionOnSwitch(Switch x)

Specified by:

performActionOnSwitch in interface Visitor

Overrides:

performActionOnSwitch in class JavaASTVisitor

performActionOnTry

public void performActionOnTry(Try x)

Specified by:

performActionOnTry in interface Visitor

Overrides:

performActionOnTry in class JavaASTVisitor

performActionOnLabeledStatement

public void performActionOnLabeledStatement(LabeledStatement x)

Specified by:

performActionOnLabeledStatement in interface Visitor

Overrides:

performActionOnLabeledStatement in class JavaASTVisitor

performActionOnMethodFrame

public void performActionOnMethodFrame(MethodFrame x)

Specified by:

performActionOnMethodFrame in interface Visitor

Overrides:

performActionOnMethodFrame in class JavaASTVisitor

performActionOnSynchronizedBlock

public void performActionOnSynchronizedBlock(SynchronizedBlock x)

Specified by:

performActionOnSynchronizedBlock in interface Visitor

Overrides:

performActionOnSynchronizedBlock in class JavaASTVisitor

performActionOnCopyAssignment

public void performActionOnCopyAssignment(CopyAssignment x)

Specified by:

performActionOnCopyAssignment in interface Visitor

Overrides:

performActionOnCopyAssignment in class JavaASTVisitor

performActionOnThen

public void performActionOnThen(Then x)

Specified by:

performActionOnThen in interface Visitor

Overrides:

performActionOnThen in class JavaASTVisitor

performActionOnElse

public void performActionOnElse(Else x)

Specified by:

performActionOnElse in interface Visitor

Overrides:

performActionOnElse in class JavaASTVisitor

performActionOnCase

public void performActionOnCase(Case x)

Specified by:

performActionOnCase in interface Visitor

Overrides:

performActionOnCase in class JavaASTVisitor

performActionOnCatch

public void performActionOnCatch(Catch x)

Specified by:

performActionOnCatch in interface Visitor

Overrides:

performActionOnCatch in class JavaASTVisitor

performActionOnDefault

public void performActionOnDefault(Default x)

Specified by:

performActionOnDefault in interface Visitor

Overrides:

performActionOnDefault in class JavaASTVisitor

performActionOnFinally

public void performActionOnFinally(Finally x)

Specified by:

performActionOnFinally in interface Visitor

Overrides:

performActionOnFinally in class JavaASTVisitor

changed

protected void changed()

addChild

protected void addChild(SourceElement x)