001: // This file is part of KeY - Integrated Deductive Software Design
002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003: // Universitaet Koblenz-Landau, Germany
004: // Chalmers University of Technology, Sweden
005: //
006: // The KeY system is protected by the GNU General Public License.
007: // See LICENSE.TXT for details.
008: //
009: //
010: //
011: //
012:
013: package de.uka.ilkd.key.rule.metaconstruct;
014:
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.java.Statement;
017: import de.uka.ilkd.key.java.StatementBlock;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.java.statement.MethodFrame;
020: import de.uka.ilkd.key.java.statement.While;
021: import de.uka.ilkd.key.java.visitor.CreatingASTVisitor;
022: import de.uka.ilkd.key.logic.op.IProgramVariable;
023: import de.uka.ilkd.key.rule.inst.SVInstantiations;
024: import de.uka.ilkd.key.util.ExtList;
025:
026: /**
027: * Walks through a java AST in depth-left-fist-order. This walker is used to
028: * transform a loop (not only while loops) according to the rules of the dynamic
029: * logic.
030: */
031: public class ReplaceWhileLoop extends CreatingASTVisitor {
032:
033: private boolean firstWhileFound = false;
034: private boolean replaced = false;
035: private StatementBlock toInsert = null;
036: private While theLoop = null;
037: private int lastMethodFrameBeforeLoop = -1;
038:
039: private KeYJavaType returnType = null;
040:
041: private int currentMethodFrame = -1;
042: private int firstLoopPos = -1;
043: /**
044: * if run in check mode there are normally schemavaribles, so we need the
045: * instantiations of them
046: */
047: protected SVInstantiations instantiations = SVInstantiations.EMPTY_SVINSTANTIATIONS;
048:
049: /**
050: * the result of the transformation
051: */
052: protected ProgramElement result = null;
053:
054: /**
055: * creates the WhileLoopTransformation for the transformation mode
056: *
057: * @param root
058: * the ProgramElement where to begin
059: * @param outerLabel
060: * the ProgramElementName of the outer label
061: * @param innerLabel
062: * the ProgramElementName of the inner label
063: */
064: public ReplaceWhileLoop(ProgramElement root, StatementBlock toInsert) {
065: super (root, true);
066: this .toInsert = toInsert;
067: firstWhileFound = false;
068: }
069:
070: /**
071: * creates the WhileLoopTransformation for the check mode
072: *
073: * @param root
074: * the ProgramElement where to begin
075: * @param inst
076: * the SVInstantiations if available
077: */
078: public ReplaceWhileLoop(ProgramElement root, SVInstantiations inst,
079: StatementBlock toInsert) {
080: super (root, true);
081: this .toInsert = toInsert;
082: firstWhileFound = false;
083: instantiations = (inst == null ? SVInstantiations.EMPTY_SVINSTANTIATIONS
084: : inst);
085: }
086:
087: protected void walk(ProgramElement node) {
088: if (node instanceof While && !firstWhileFound) {
089: firstWhileFound = true;
090: firstLoopPos = depth();
091: theLoop = ((While) node);
092: lastMethodFrameBeforeLoop = currentMethodFrame;
093: }
094: if (node instanceof MethodFrame) {
095: currentMethodFrame = depth();
096: }
097:
098: super .walk(node);
099: }
100:
101: public void start() {
102: stack.push(new ExtList());
103: walk(root());
104: ExtList el = stack.peek();
105: int i = 0;
106: while (!(el.get(i) instanceof ProgramElement)) {
107: i++;
108: }
109: result = (ProgramElement) stack.peek().get(i);
110: }
111:
112: public ProgramElement result() {
113: return result;
114: }
115:
116: public KeYJavaType returnType() {
117: return returnType;
118: }
119:
120: public Statement getTheLoop() {
121: return theLoop;
122: }
123:
124: public String toString() {
125: return stack.peek().toString();
126: }
127:
128: public void performActionOnMethodFrame(MethodFrame x) {
129: if (lastMethodFrameBeforeLoop == depth()) {
130: IProgramVariable res = x.getProgramVariable();
131: if (res != null)
132: returnType = res.getKeYJavaType();
133: }
134:
135: super .performActionOnMethodFrame(x);
136: }
137:
138: public void performActionOnWhile(While x) {
139: if (firstLoopPos == depth() && !replaced) {
140: replaced = true;
141: if (toInsert == null)
142: stack.pop();
143: else
144: addChild(toInsert);
145: changed();
146: } else {
147: super.performActionOnWhile(x);
148: }
149: }
150: }
|