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: package de.uka.ilkd.key.rule.metaconstruct;
011:
012: import java.util.ArrayList;
013: import java.util.LinkedList;
014: import java.util.ListIterator;
015:
016: import de.uka.ilkd.key.java.*;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
019: import de.uka.ilkd.key.java.statement.MethodFrame;
020: import de.uka.ilkd.key.java.statement.While;
021: import de.uka.ilkd.key.logic.*;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
024: import de.uka.ilkd.key.logic.sort.Sort;
025: import de.uka.ilkd.key.rule.inst.SVInstantiations;
026:
027: public class WhileInvRule extends AbstractMetaOperator {
028:
029: /** the outer label that is used to leave the while loop ('l1') */
030: private final SchemaVariable outerLabel = SchemaVariableFactory
031: .createProgramSV(new ProgramElementName("outer_label"),
032: ProgramSVSort.LABEL, false);
033: /** the inner label ('l2') */
034: private final SchemaVariable innerLabel = SchemaVariableFactory
035: .createProgramSV(new ProgramElementName("inner_label"),
036: ProgramSVSort.LABEL, false);
037: /** list of the labels */
038: private ListOfSchemaVariable instantiations = null;
039:
040: /** list of breaks that lead to abrupt termination
041: * of the loop to be transformed. Is initialised by
042: * the method neededInstantiations that is invoked
043: * before calculate
044: */
045: private LinkedList breakList;
046:
047: /** The JavaInfo object which is handed over as
048: * a parameter of calculate.
049: */
050: private JavaInfo javaInfo;
051: private TypeConverter typeConv;
052: private TermFactory tf;
053:
054: private ProgramElement body;
055: private Term inv, post;
056: private JavaNonTerminalProgramElement root;
057: private Modality modality;
058:
059: private KeYJavaType returnType;
060:
061: public WhileInvRule() {
062: super (new Name("#whileInvRule"), 2);
063: }
064:
065: /** Unlike other meta operators this one returns a formula
066: * not a term.
067: */
068: public Sort sort(Term[] term) {
069: return Sort.FORMULA;
070: }
071:
072: /**
073: * checks whether the top level structure of the given @link Term
074: * is syntactically valid, given the assumption that the top level
075: * operator of the term is the same as this Operator. The
076: * assumption that the top level operator and the term are equal
077: * is NOT checked.
078: * @return true iff the top level structure of
079: * the @link Term is valid.
080: */
081: public boolean validTopLevel(Term term) {
082: // a meta operator accepts almost everything
083: return term.arity() == arity();
084: }
085:
086: /**
087: * initialises this meta operator
088: * @param term the instantiated Term passed to the MetaOperator
089: * @param services the Services providing access to signature and
090: * type model
091: */
092: private void init(Term term, Services services) {
093: root = (JavaNonTerminalProgramElement) term.sub(0).javaBlock()
094: .program();
095: modality = (Modality) term.sub(0).op();
096:
097: ReplaceWhileLoop removeWhile = new ReplaceWhileLoop(root, null);
098: removeWhile.start();
099:
100: body = removeWhile.getTheLoop();
101:
102: // some initialisations...
103:
104: inv = term.sub(1);
105: post = term.sub(0).sub(0);
106:
107: javaInfo = services.getJavaInfo();
108: tf = TermFactory.DEFAULT;
109: typeConv = services.getTypeConverter();
110:
111: returnType = removeWhile.returnType();
112: }
113:
114: /** calculates the resulting term. */
115: public Term calculate(Term term, SVInstantiations svInst,
116: Services services) {
117:
118: // global initialisation
119: init(term, services);
120:
121: // local initialisation
122: ArrayList stmnt = new ArrayList();
123: ArrayList breakIfCascade = new ArrayList();
124:
125: ProgramVariable contFlag = getNewLocalvariable("cont",
126: "boolean", services);
127: ProgramVariable returnFlag = getNewLocalvariable("rtrn",
128: "boolean", services);
129: ProgramVariable breakFlag = getNewLocalvariable("brk",
130: "boolean", services);
131: // xxx how to ensure that "exc" has not been used before??
132: ProgramVariable excFlag = getNewLocalvariable("exc", "boolean",
133: services);
134: ProgramVariable excParam = getNewLocalvariable("e",
135: "java.lang.Throwable", services);
136: ProgramVariable thrownException = getNewLocalvariable(
137: "thrownExc", "java.lang.Throwable", services);
138:
139: ProgramVariable returnExpression = null;
140: if (returnType != null) {
141: returnExpression = getNewLocalvariable("returnExpr",
142: returnType, services);
143: }
144:
145: Term contFlagTerm = null;
146: Term returnFlagTerm = null;
147: Term breakFlagTerm = null;
148: Term excFlagTerm = null;
149:
150: // end of initialisation............
151:
152: int breakCounter = 0;
153: final ListIterator it = breakList.listIterator(0);
154: int numberOfBreaks = 0;
155: while (it.hasNext()) {
156: BreakToBeReplaced b = (BreakToBeReplaced) it.next();
157: ProgramVariable newVar = getNewLocalvariable("break_"
158: + breakCounter++, "boolean", services);
159: b.setProgramVariable(newVar);
160: stmnt.add(KeYJavaASTFactory.declare(newVar,
161: BooleanLiteral.FALSE, javaInfo
162: .getKeYJavaType("boolean")));
163: numberOfBreaks++;
164: Statement s;
165: if (b.getBreak().getLabel() != null)
166: s = KeYJavaASTFactory.breakStatement(b.getBreak()
167: .getLabel());
168: else
169: s = KeYJavaASTFactory.emptyStatement();
170: breakIfCascade.add(KeYJavaASTFactory.ifThen(newVar, s));
171: }
172:
173: WhileInvariantTransformation w = new WhileInvariantTransformation(
174: (While) body, (ProgramElementName) svInst
175: .getInstantiation(outerLabel),
176: (ProgramElementName) svInst
177: .getInstantiation(innerLabel), contFlag,
178: excFlag, excParam, thrownException, breakFlag,
179: returnFlag, returnExpression, breakList, services);
180: w.start();
181:
182: ArrayList resultSubterms = new ArrayList();
183:
184: // normal case and continue
185: if (w.continueOccurred()) {
186: stmnt.add(contFlagDecl(contFlag));
187: contFlagTerm = tf.createEqualityTerm(Op.EQUALS, typeConv
188: .convertToLogicElement(contFlag), typeConv
189: .getBooleanLDT().getTrueTerm());
190: }
191:
192: // exception case
193: resultSubterms.add(throwCase(excFlag, thrownException, post));
194:
195: // return case
196: if (w.returnOccurred()) {
197: stmnt.add(returnFlagDecl(returnFlag, svInst));
198: returnFlagTerm = typeConv.convertToLogicElement(returnFlag);
199: resultSubterms.add(returnCase(returnFlag, returnType,
200: returnExpression, post));
201:
202: if (returnType != null) {
203: stmnt.add(KeYJavaASTFactory.declare(returnExpression,
204: returnType));
205: }
206: }
207:
208: // break case
209: if (numberOfBreaks > 0) {
210: stmnt.add(breakFlagDecl(breakFlag));
211: breakFlagTerm = typeConv.convertToLogicElement(breakFlag);
212: resultSubterms.add(breakCase(breakFlag, post,
213: breakIfCascade));
214: }
215:
216: // we catch all exceptions
217: stmnt.add(KeYJavaASTFactory.declare(excFlag,
218: BooleanLiteral.FALSE, javaInfo
219: .getKeYJavaType("boolean")));
220: excFlagTerm = typeConv.convertToLogicElement(excFlag);
221: stmnt.add(KeYJavaASTFactory.declare(thrownException, javaInfo
222: .getKeYJavaType("java.lang.Throwable")));
223:
224: resultSubterms.add(normalCaseAndContinue(contFlagTerm,
225: returnFlagTerm, breakFlagTerm, excFlagTerm, inv));
226:
227: Term result = createLongJunctorTerm(Op.AND, resultSubterms);
228:
229: stmnt.add(w.result());
230: StatementBlock s = new StatementBlock((Statement[]) stmnt
231: .toArray(new Statement[0]));
232: Statement resSta;
233: if (svInst.getExecutionContext() != null)
234: resSta = new MethodFrame(null,
235: svInst.getExecutionContext(), s);
236: else
237: resSta = s;
238:
239: Modality loopBodyModality = modality;
240:
241: // This here is crucial for transactions. If you wonder why the conversion
242: // is so "irregular", well, that's the way it is ;) /Wojtek
243: if (modality == BOXTRC || modality == TOUTTRC)
244: loopBodyModality = BOX;
245: if (modality == DIATRC)
246: loopBodyModality = DIA;
247: return tf.createProgramTerm(loopBodyModality, JavaBlock
248: .createJavaBlock(new StatementBlock(resSta)), result);
249: }
250:
251: /**
252: * creates a new program variable
253: * @param varNameBase a String specifying the basename of the new variable
254: * @param varType a String specifying the typename of the new variable
255: * @param services the Services allowing access to the variablenaming facilities
256: * @return a new program variable of the given type and a name as near as possible
257: * to the given basename
258: */
259: private ProgramVariable getNewLocalvariable(String varNameBase,
260: String varType, Services services) {
261:
262: return getNewLocalvariable(varNameBase, javaInfo
263: .getKeYJavaType(varType), services);
264:
265: }
266:
267: /**
268: * creates a new program variable
269: * @param varNameBase a String specifying the basename of the new variable
270: * @param varType the KeYJavaType of the new variable
271: * @param services the Services allowing access to the variablenaming facilities
272: * @return a new program variable of the given type and a name as near as possible
273: * to the given basename
274: */
275: private ProgramVariable getNewLocalvariable(String varNameBase,
276: KeYJavaType varType, Services services) {
277: return KeYJavaASTFactory.localVariable(services
278: .getVariableNamer().getTemporaryNameProposal(
279: varNameBase), varType);
280:
281: }
282:
283: /** returns the schemavariables that are needed to transform the given
284: * loop. The unwind-loop construct may need labels if unlabeled breaks
285: * and/or continues occur in the loop. Often there will be uninstantiated
286: * Schemavariables in the loop that is why the found instantiations have to
287: * be given.
288: */
289: public ListOfSchemaVariable neededInstantiations(
290: ProgramElement originalLoop, SVInstantiations svInst) {
291: WhileInvariantTransformation w = new WhileInvariantTransformation(
292: originalLoop, svInst);
293: w.start();
294: instantiations = SLListOfSchemaVariable.EMPTY_LIST;
295: if (w.innerLabelNeeded()) {
296: instantiations = instantiations.prepend(innerLabel);
297: }
298: if (w.outerLabelNeeded()) {
299: instantiations = instantiations.prepend(outerLabel);
300: }
301: breakList = w.breakList();
302: return instantiations;
303: }
304:
305: //---------------------------------------------------------------
306: // --- private helper methods to construct the result term
307: //---------------------------------------------------------------
308:
309: private Term createLongJunctorTerm(Junctor junctor, ArrayList terms) {
310: if (terms.size() == 1)
311: return (Term) terms.get(0);
312: else if (terms.size() == 2)
313: return tf.createJunctorTerm(junctor, (Term) terms.get(0),
314: (Term) terms.get(1));
315: else {
316: Term arg1 = (Term) terms.get(0);
317: terms.remove(0);
318: return tf.createJunctorTerm(junctor, arg1,
319: createLongJunctorTerm(junctor, terms));
320: }
321: }
322:
323: private Statement returnFlagDecl(ProgramVariable returnFlag,
324: SVInstantiations svInst) {
325: return KeYJavaASTFactory.declare(returnFlag,
326: BooleanLiteral.FALSE, javaInfo
327: .getKeYJavaType("boolean"));
328: }
329:
330: private Term returnCase(ProgramVariable returnFlag,
331: KeYJavaType returnType, ProgramVariable returnExpression,
332: Term post) {
333: Term executeReturn = tf.createProgramTerm(modality, addContext(
334: root, new StatementBlock(KeYJavaASTFactory
335: .returnClause(returnExpression))), post);
336:
337: return tf.createJunctorTerm(Op.IMP, tf.createEqualityTerm(
338: Op.EQUALS, typeConv.convertToLogicElement(returnFlag),
339: typeConv.getBooleanLDT().getTrueTerm()), executeReturn);
340:
341: }
342:
343: private Statement breakFlagDecl(ProgramVariable breakFlag) {
344: return KeYJavaASTFactory.declare(breakFlag,
345: BooleanLiteral.FALSE, javaInfo
346: .getKeYJavaType("boolean"));
347: }
348:
349: private Statement contFlagDecl(ProgramVariable contFlag) {
350: return KeYJavaASTFactory.declare(contFlag,
351: BooleanLiteral.FALSE, javaInfo
352: .getKeYJavaType("boolean"));
353: }
354:
355: private Term breakCase(ProgramVariable breakFlag, Term post,
356: ArrayList breakIfCascade) {
357: Term executeBreak = tf.createProgramTerm(modality, addContext(
358: root, new StatementBlock((Statement[]) breakIfCascade
359: .toArray(new Statement[0]))), post);
360: return tf.createJunctorTerm(Op.IMP, tf.createEqualityTerm(
361: Op.EQUALS, typeConv.convertToLogicElement(breakFlag),
362: typeConv.getBooleanLDT().getTrueTerm()), executeBreak);
363: }
364:
365: private Term normalCaseAndContinue(Term contFlagTerm,
366: Term returnFlagTerm, Term breakFlagTerm, Term excFlagTerm,
367: Term inv) {
368:
369: final Term TRUE_TERM = typeConv.getBooleanLDT().getTrueTerm();
370:
371: ArrayList al = new ArrayList();
372:
373: if (returnFlagTerm != null)
374: al.add(tf.createEqualityTerm(Op.EQUALS, returnFlagTerm,
375: TRUE_TERM));
376: if (breakFlagTerm != null)
377: al.add(tf.createEqualityTerm(Op.EQUALS, breakFlagTerm,
378: TRUE_TERM));
379: if (excFlagTerm != null)
380: al.add(tf.createEqualityTerm(Op.EQUALS, excFlagTerm,
381: TRUE_TERM));
382:
383: if (al.size() == 0) {
384: if (contFlagTerm == null)
385: return inv;
386: else
387: return tf.createJunctorTerm(Op.IMP, contFlagTerm, inv);
388: } else {
389: Term premiss = tf.createJunctorTerm(Op.NOT,
390: createLongJunctorTerm(Op.OR, al));
391: if (contFlagTerm != null)
392: premiss = tf.createJunctorTerm(Op.OR, contFlagTerm,
393: premiss);
394:
395: return tf.createJunctorTerm(Op.IMP, premiss, inv);
396: }
397: }
398:
399: private Term throwCase(ProgramVariable excFlag,
400: ProgramVariable thrownException, Term post) {
401: Term throwException = tf.createProgramTerm(modality,
402: addContext(root, new StatementBlock(KeYJavaASTFactory
403: .throwClause(thrownException))), post);
404: return tf
405: .createJunctorTerm(Op.IMP, tf.createEqualityTerm(
406: Op.EQUALS, typeConv
407: .convertToLogicElement(excFlag),
408: typeConv.getBooleanLDT().getTrueTerm()),
409: throwException);
410: }
411:
412: protected JavaBlock addContext(JavaNonTerminalProgramElement root,
413: StatementBlock block) {
414: ReplaceWhileLoop replaceWhile = new ReplaceWhileLoop(root,
415: block);
416: replaceWhile.start();
417:
418: return JavaBlock.createJavaBlock((StatementBlock) replaceWhile
419: .result());
420:
421: }
422:
423: }
|