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 java.util.LinkedList;
016: import java.util.ListIterator;
017:
018: import de.uka.ilkd.key.java.*;
019: import de.uka.ilkd.key.java.annotation.Annotation;
020: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
021: import de.uka.ilkd.key.java.statement.*;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.op.ProgramVariable;
024: import de.uka.ilkd.key.rule.inst.SVInstantiations;
025: import de.uka.ilkd.key.util.ExtList;
026:
027: /**
028: * Walks through a java AST in depth-left-fist-order.
029: * This walker is used to transform a loop (not only
030: * while loops) according to the rules of the dynamic logic.
031: */
032: public class WhileInvariantTransformation extends
033: WhileLoopTransformation {
034:
035: private Services services = null;
036: private JavaInfo javaInfo = null;
037:
038: private ProgramVariable cont = null;
039: private ProgramVariable exc = null;
040: private ProgramVariable rtrn = null;
041: private ProgramVariable brk = null;
042: private ProgramVariable thrownExc = null;
043: private ProgramVariable excParam = null;
044: private ProgramVariable returnExpr = null;
045:
046: private boolean continueOccurred = false;
047: private boolean returnOccurred = false;
048:
049: private LinkedList breakList = null;
050:
051: /**
052: * creates the WhileLoopTransformation for the transformation mode
053: * @param root the ProgramElement where to begin
054: * @param outerLabel the ProgramElementName of the outer label
055: * @param innerLabel the ProgramElementName of the inner label
056: */
057: public WhileInvariantTransformation(ProgramElement root,
058: ProgramElementName outerLabel,
059: ProgramElementName innerLabel, ProgramVariable cont,
060: ProgramVariable exc, ProgramVariable excParam,
061: ProgramVariable thrownException, ProgramVariable brk,
062: ProgramVariable rtrn, ProgramVariable returnExpr,
063: LinkedList breakList, Services services) {
064:
065: super (root, outerLabel, innerLabel);
066: this .services = services;
067: this .cont = cont;
068: this .exc = exc;
069: this .excParam = excParam;
070: this .thrownExc = thrownException;
071: this .rtrn = rtrn;
072: this .brk = brk;
073: this .returnExpr = returnExpr;
074: this .breakList = breakList;
075: this .javaInfo = this .services.getJavaInfo();
076: }
077:
078: /** creates the WhileLoopTransformation for the check mode
079: * @param root the ProgramElement where to begin
080: * @param inst the SVInstantiations if available
081: */
082: public WhileInvariantTransformation(ProgramElement root,
083: SVInstantiations inst) {
084: super (root, inst);
085: this .breakList = new LinkedList();
086: }
087:
088: /** returns true iff the loop to be transformed
089: * contains a continue referring to this loop
090: */
091: public boolean continueOccurred() {
092: return continueOccurred;
093: }
094:
095: /** return true iff the loop to be transformed
096: * contains a return statement leading to abrupt
097: * termination of the loop body
098: */
099: public boolean returnOccurred() {
100: return returnOccurred;
101: }
102:
103: /** returns a list of breaks that lead to
104: * abrupt termination of the loop and
105: * have to be replaced
106: */
107: public LinkedList breakList() {
108: return breakList;
109: }
110:
111: public void performActionOnReturn(Return x) {
112: boolean matched = true;
113: if (!methodStack.empty())
114: methodStack.pop();
115: else
116: matched = false;
117:
118: if (!matched) {
119: if (runMode == CHECK) {
120: needInnerLabel = true;
121: } else {
122: ExtList changeList = (ExtList) stack.peek();
123: if (!changeList.isEmpty()
124: && changeList.getFirst() == CHANGED) {
125: changeList.removeFirst();
126: }
127: returnOccurred = true;
128: Statement assignFlag = KeYJavaASTFactory.assign(rtrn,
129: BooleanLiteral.TRUE);
130: final Statement[] stmnts;
131: if (returnExpr != null) {
132: Statement assignExpr = KeYJavaASTFactory.assign(
133: returnExpr, x.getExpression());
134: stmnts = new Statement[] { assignFlag, assignExpr,
135: breakInnerLabel };
136: } else
137: stmnts = new Statement[] { assignFlag,
138: breakInnerLabel };
139: addChild(new StatementBlock(stmnts));
140: changed();
141: }
142: } else
143: doDefaultAction(x);
144: }
145:
146: protected void performActionOnAnnotationArray(Annotation[] a) {
147: //do nothing;
148: }
149:
150: public void performActionOnContinue(Continue x) {
151: if (replaceJumpStatement(x)
152: || ((x.getLabel() != null) && (labelStack.search(x
153: .getLabel()) == -1))) {
154: continueOccurred = true;
155: if (runMode == CHECK) {
156: needInnerLabel = true;
157: } else {
158: Statement assign = KeYJavaASTFactory.assign(cont,
159: BooleanLiteral.TRUE);
160: Statement[] stmnts = { assign, breakInnerLabel };
161: addChild(new StatementBlock(stmnts));
162: changed();
163: }
164: } else {
165: doDefaultAction(x);
166: }
167: }
168:
169: public void performActionOnBreak(Break x) {
170: boolean replaced = false;
171: if (replaceJumpStatement(x)
172: || ((x.getLabel() != null) && (labelStack.search(x
173: .getLabel()) == -1))) {
174: if (runMode == CHECK) {
175: needInnerLabel = true;
176: breakList.add(new BreakToBeReplaced(x));
177: } else {
178: ListIterator it = breakList.listIterator(0);
179: while (it.hasNext()) {
180: BreakToBeReplaced b = (BreakToBeReplaced) it.next();
181: if (x == b.getBreak()) {
182: Statement assignFlag = KeYJavaASTFactory
183: .assign(brk, BooleanLiteral.TRUE);
184: Statement assign = KeYJavaASTFactory.assign(b
185: .getProgramVariable(),
186: BooleanLiteral.TRUE);
187: Statement[] stmnts = { assignFlag, assign,
188: breakInnerLabel };
189: replaced = true;
190: addChild(new StatementBlock(stmnts));
191: changed();
192: break;
193: }
194: }
195: if (!replaced)
196: doDefaultAction(x);
197: }
198: } else {
199: doDefaultAction(x);
200: }
201: }
202:
203: public void performActionOnWhile(While x) {
204: ExtList changeList = (ExtList) stack.peek();
205: if (replaceBreakWithNoLabel == 0) {
206: // the most outer while loop
207: // get guard
208: if (changeList.getFirst() == CHANGED) {
209: changeList.removeFirst();
210: }
211: Expression guard = ((Guard) changeList.removeFirst())
212: .getExpression();
213: Statement body = (Statement) (changeList.isEmpty() ? null
214: : changeList.removeFirst());
215: body = KeYJavaASTFactory.ifThen(x.getGuardExpression(),
216: body);
217: if (breakInnerLabel != null) {
218: // an unlabeled continue needs to be handled with (replaced)
219: body = new LabeledStatement(breakInnerLabel.getLabel(),
220: body);
221: }
222: StatementBlock block = new StatementBlock(body);
223: Statement newBody = block;
224: if (breakOuterLabel != null) {
225: // an unlabeled break occurs in the
226: // while loop therefore we need a labeled statement
227: newBody = new LabeledStatement(breakOuterLabel
228: .getLabel(), block);
229:
230: }
231:
232: Statement[] catchStatements = {
233: KeYJavaASTFactory.assign(exc, BooleanLiteral.TRUE),
234: KeYJavaASTFactory.assign(thrownExc, excParam) };
235:
236: Catch ctch = KeYJavaASTFactory
237: .catchClause(
238: KeYJavaASTFactory
239: .parameterDeclaration(
240: javaInfo,
241: javaInfo
242: .getKeYJavaType("java.lang.Throwable"),
243: excParam),
244: new StatementBlock(catchStatements));
245:
246: Branch[] branch = { ctch };
247: Statement res = new Try(new StatementBlock(newBody), branch);
248: addChild(res);
249: changed();
250: } else {
251: if (!changeList.isEmpty()
252: && changeList.getFirst() == CHANGED) {
253: changeList.removeFirst();
254: Expression guard = ((Guard) changeList.removeFirst())
255: .getExpression();
256: Statement body = (Statement) (changeList.isEmpty() ? null
257: : changeList.removeFirst());
258: addChild(new While(guard, body, x.getPositionInfo(), x
259: .getAnnotations()));
260: changed();
261: } else {
262: doDefaultAction(x);
263: }
264: }
265: }
266:
267: }
|