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: package de.uka.ilkd.key.rule.soundness;
012:
013: import java.util.HashMap;
014: import java.util.Iterator;
015: import java.util.Map;
016: import java.util.Stack;
017:
018: import org.apache.log4j.Logger;
019:
020: import de.uka.ilkd.key.java.*;
021: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
022: import de.uka.ilkd.key.java.declaration.VariableDeclaration;
023: import de.uka.ilkd.key.java.declaration.VariableSpecification;
024: import de.uka.ilkd.key.java.statement.*;
025: import de.uka.ilkd.key.logic.ProgramElementName;
026: import de.uka.ilkd.key.logic.Term;
027: import de.uka.ilkd.key.logic.op.*;
028: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
029: import de.uka.ilkd.key.rule.inst.SVInstantiations;
030: import de.uka.ilkd.key.util.ExtList;
031:
032: public class SVPrefixCollector extends TacletVisitor {
033:
034: private final Stack prefixStack = new Stack();
035:
036: private static final Boolean LEVEL = new Boolean(true);
037: private static final Boolean SCOPE_LEVEL = new Boolean(true);
038: private static final Boolean HORIZON = new Boolean(true);
039:
040: private SVTypeInfos svTypeInfos;
041: private final Services services;
042:
043: private final Logger logger = Logger
044: .getLogger("key.taclet_soundness");
045:
046: public SVPrefixCollector(SVTypeInfos p_svTypeInfos,
047: Services p_services) {
048: svTypeInfos = p_svTypeInfos;
049: services = p_services;
050: }
051:
052: public Services getServices() {
053: return services;
054: }
055:
056: public TypeConverter getTypeConverter() {
057: return getServices().getTypeConverter();
058: }
059:
060: private void pushLevelMark() {
061: prefixStack.push(LEVEL);
062: }
063:
064: private void popLevelMark() {
065: Object o;
066: do {
067: o = prefixStack.pop();
068: } while (o != LEVEL);
069: }
070:
071: private static ListOfIProgramVariable toList(SetOfIProgramVariable p) {
072: IteratorOfIProgramVariable it = p.iterator();
073: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
074:
075: while (it.hasNext())
076: res = res.prepend(it.next());
077:
078: return res;
079: }
080:
081: private static ListOfSchemaVariable toList(SetOfSchemaVariable p) {
082: IteratorOfSchemaVariable it = p.iterator();
083: ListOfSchemaVariable res = SLListOfSchemaVariable.EMPTY_LIST;
084:
085: while (it.hasNext())
086: res = res.prepend(it.next());
087:
088: return res;
089: }
090:
091: private void addSVTypeInfo(SchemaVariable p_sv, KeYJavaType p_type) {
092: svTypeInfos = svTypeInfos.addInfo(new SVTypeInfo(p_sv, p_type));
093: }
094:
095: private JumpStatementPrefixesImpl jumpStatementPrefixes = new JumpStatementPrefixesImpl();
096:
097: private RawProgramVariablePrefixesImpl programVariablePrefixes = new RawProgramVariablePrefixesImpl();
098:
099: // VISITOR RELATED METHODS
100:
101: public void subtreeEntered(Term t) {
102: if (t.op() instanceof Modality) {
103: ProgramCollector c = new ProgramCollector(t.javaBlock()
104: .program());
105: c.start();
106: } else if (t.op() instanceof SchemaVariable) {
107: SchemaVariable sv = (SchemaVariable) t.op();
108:
109: programVariablePrefixes.addPrefix(sv,
110: SLListOfIProgramVariable.EMPTY_LIST);
111:
112: if (sv.isProgramSV()
113: && ((SortedSchemaVariable) sv).sort() == ProgramSVSort.VARIABLE)
114: programVariablePrefixes.addFreeSchemaVariable(sv);
115: } else if (t.op() instanceof IProgramVariable) {
116: // i.e. no schema variable!
117: programVariablePrefixes
118: .addFreeProgramVariable((IProgramVariable) t.op());
119: }
120: }
121:
122: /** is called by the execPostOrder-method of a term
123: * @param Term to checked if it is a Variable and if true the
124: * Variable is added to the list of found Variables
125: */
126: public void visit(Term t) {
127: }
128:
129: public JumpStatementPrefixes getJumpStatementPrefixes() {
130: return jumpStatementPrefixes;
131: }
132:
133: public SVTypeInfos getSVTypeInfos() {
134: return svTypeInfos;
135: }
136:
137: public RawProgramVariablePrefixes getRawProgramVariablePrefixes() {
138: return programVariablePrefixes;
139: }
140:
141: private class ProgramCollector extends
142: de.uka.ilkd.key.java.visitor.JavaASTVisitor {
143:
144: private Stack prefixStack = new Stack();
145:
146: private int startAtChild;
147: private boolean enter;
148:
149: public ProgramCollector(ProgramElement root) {
150: super (root);
151: }
152:
153: private void pushLevelMark() {
154: prefixStack.push(LEVEL);
155: }
156:
157: private void pushScopeLevelMark() {
158: prefixStack.push(SCOPE_LEVEL);
159: }
160:
161: private void pushHorizonMark() {
162: prefixStack.push(HORIZON);
163: }
164:
165: private void push(Object p) {
166: prefixStack.push(p);
167: }
168:
169: private Object pop() {
170: return prefixStack.pop();
171: }
172:
173: private boolean empty() {
174: return prefixStack.empty();
175: }
176:
177: private void popLevelMark() {
178: Object o;
179: do {
180: o = prefixStack.pop();
181: } while (o != LEVEL);
182: }
183:
184: private void addToLastVariableDeclaration(IProgramVariable p) {
185: Object o = pop();
186:
187: if (o instanceof VariableDeclarationUnit) {
188: VariableDeclarationUnit vdu = (VariableDeclarationUnit) o;
189: vdu.vars = vdu.vars.prepend(p);
190:
191: programVariablePrefixes
192: .addBoundSchemaVariable((SchemaVariable) p);
193: addSVTypeInfo((SchemaVariable) p, vdu.type);
194: } else
195: addToLastVariableDeclaration(p);
196:
197: push(o);
198: }
199:
200: private void addVariableDeclaration(VariableDeclaration x) {
201: Object o = pop();
202:
203: if (o == SCOPE_LEVEL)
204: push(new VariableDeclarationUnit(x.getTypeReference()
205: .getKeYJavaType()));
206: else
207: addVariableDeclaration(x);
208:
209: push(o);
210: }
211:
212: private SetOfIProgramVariable getProgramVariablePrefix() {
213: SetOfIProgramVariable prefix = SetAsListOfIProgramVariable.EMPTY_SET;
214:
215: if (!empty()) {
216: Object o = pop();
217:
218: if (o != HORIZON) {
219: prefix = getProgramVariablePrefix();
220:
221: if (o instanceof VariableDeclarationUnit) {
222: IteratorOfIProgramVariable it = ((VariableDeclarationUnit) o).vars
223: .iterator();
224: while (it.hasNext())
225: prefix = prefix.add(it.next());
226: }
227: }
228:
229: push(o);
230: }
231:
232: return prefix;
233: }
234:
235: /** walks through the AST. While keeping track of the current node
236: * @param node the JavaProgramElement the walker is at
237: */
238: protected void walk(ProgramElement node) {
239: pushLevelMark();
240:
241: enter = true;
242: startAtChild = 0;
243: doAction(node);
244:
245: if (node instanceof NonTerminalProgramElement) {
246: NonTerminalProgramElement nonTerminalNode = (NonTerminalProgramElement) node;
247: for (int i = startAtChild; i < nonTerminalNode
248: .getChildCount(); i++) {
249: walk(nonTerminalNode.getChildAt(i));
250: }
251: }
252:
253: enter = false;
254: doAction(node);
255:
256: popLevelMark();
257: }
258:
259: /** the action that is performed just before leaving the node the
260: * last time
261: */
262: protected void doAction(ProgramElement node) {
263: node.visit(this );
264: }
265:
266: /** starts the walker*/
267: public void start() {
268: walk(root());
269: }
270:
271: public ListOfStatement createJumpTable(SchemaVariable x) {
272: int i = prefixStack.size();
273: boolean emptyBreak = false;
274: boolean emptyContinue = false;
275: Object o;
276: ListOfStatement res = SLListOfStatement.EMPTY_LIST;
277:
278: if (x.isProgramSV()
279: && ((SortedSchemaVariable) x).sort() == ProgramSVSort.STATEMENT) {
280: while (i-- != 0 && (o = prefixStack.get(i)) != HORIZON) {
281: if (o instanceof JumpStatement) {
282: if (o instanceof LabelJumpStatement
283: && ((LabelJumpStatement) o).getLabel() == null) {
284: if (o instanceof Break && !emptyBreak)
285: emptyBreak = true;
286: else if (o instanceof Continue
287: && !emptyContinue)
288: emptyContinue = true;
289: else
290: continue;
291: }
292:
293: if (res.contains((Statement) o))
294: throw new InvalidPrefixException(
295: "Jump statement prefix of " + x
296: + " invalid");
297: res = res.prepend((Statement) o);
298: }
299: }
300: }
301:
302: return res;
303: }
304:
305: protected void doDefaultAction(SourceElement x) {
306: if (x instanceof VariableDeclaration)
307: performActionOnVariableDeclaration((VariableDeclaration) x);
308: else if (x instanceof LoopStatement)
309: performActionOnLoopStatement((LoopStatement) x);
310: else if (x instanceof Branch)
311: performActionOnBranch((Branch) x);
312: }
313:
314: public void performActionOnMethodFrame(MethodFrame x) {
315: if (enter) {
316: pushHorizonMark();
317: pushScopeLevelMark();
318:
319: ExtList children = new ExtList();
320: if (x.getProgramVariable() != null)
321: children.add(x.getProgramVariable());
322:
323: push(new Return(children));
324: }
325: }
326:
327: public void performActionOnBranch(Branch x) {
328: if (enter && !(x instanceof Case))
329: pushScopeLevelMark();
330: }
331:
332: public void performActionOnStatementBlock(StatementBlock x) {
333: if (enter)
334: pushScopeLevelMark();
335: }
336:
337: public void performActionOnSynchronizedBlock(SynchronizedBlock x) {
338: if (enter)
339: pushScopeLevelMark();
340: }
341:
342: public void performActionOnVariableDeclaration(
343: VariableDeclaration x) {
344: if (enter)
345: addVariableDeclaration(x);
346: }
347:
348: public void performActionOnVariableSpecification(
349: VariableSpecification x) {
350: if (enter)
351: startAtChild = 1;
352: else {
353: IProgramVariable pv = x.getProgramVariable();
354: if (pv instanceof SchemaVariable)
355: addToLastVariableDeclaration(pv);
356: else
357: throw new InvalidPrefixException(
358: "Native program variables must not occur bound within a taclet");
359: }
360: }
361:
362: public void performActionOnLabeledStatement(LabeledStatement x) {
363: if (enter) {
364: Label l = x.getLabel();
365: Statement s = x.getBody();
366:
367: push(new Break(l));
368:
369: if (s instanceof LoopStatement)
370: push(new Continue((ProgramElementName) l)); // Bug ???
371: // multiple labels before loops ???
372: }
373: }
374:
375: public void performActionOnLoopStatement(LoopStatement x) {
376: if (enter) {
377: pushScopeLevelMark();
378: push(new Break());
379: push(new Continue());
380: }
381: }
382:
383: public void performActionOnSwitch(Switch x) {
384: if (enter) {
385: pushScopeLevelMark();
386: push(new Break());
387: }
388: }
389:
390: public void performActionOnProgramVariable(ProgramVariable x) {
391: programVariablePrefixes.addFreeProgramVariable(x);
392: }
393:
394: public void performActionOnSchemaVariable(SchemaVariable x) {
395: if (enter) {
396: computeJumpStatementPrefix((SortedSchemaVariable) x);
397: computeProgramVariablePrefix((SortedSchemaVariable) x);
398: }
399: }
400:
401: private void computeJumpStatementPrefix(SortedSchemaVariable x) {
402: ListOfStatement prefix = createJumpTable(x);
403: ListOfStatement oldPrefix = jumpStatementPrefixes
404: .getPrefix(x);
405:
406: if (oldPrefix == null)
407: jumpStatementPrefixes.addPrefix(x, prefix);
408: else {
409: if (prefix.size() != oldPrefix.size())
410: prefixWarning(x, oldPrefix, prefix);
411:
412: ListOfStatement res = SLListOfStatement.EMPTY_LIST;
413: IteratorOfStatement it = oldPrefix.iterator();
414: Statement st;
415:
416: while (it.hasNext()) {
417: st = it.next();
418: if (containsModRenaming(prefix, st,
419: new NameAbstractionTable()))
420: res = res.prepend(st);
421: else
422: prefixWarning(x, oldPrefix, prefix);
423: }
424:
425: jumpStatementPrefixes.addPrefix(x, res);
426: }
427: }
428:
429: private void prefixWarning(SchemaVariable x,
430: ListOfStatement p_old, ListOfStatement p_new) {
431: logger.error("*** Warning: Prefixes of schema variable "
432: + x + " differ ***: ");
433: logger.error(" Old Prefix: " + p_old);
434: logger.error(" New Prefix: " + p_new);
435: }
436:
437: private void prefixWarning(SchemaVariable x,
438: ListOfIProgramVariable p_old,
439: SetOfIProgramVariable p_new) {
440: logger.error("*** Warning: Prefixes of schema variable "
441: + x + " differ ***: ");
442: logger.error(" Old Prefix: " + p_old);
443: logger.error(" New Prefix: " + p_new);
444: }
445:
446: // only because the equals-methods of jump statement do not
447: // work
448: private boolean containsModRenaming(ListOfStatement p_list,
449: Statement p_st, NameAbstractionTable p_nat) {
450: if (p_list == SLListOfStatement.EMPTY_LIST)
451: return false;
452: else
453: return p_st.equalsModRenaming(p_list.head(), p_nat)
454: || containsModRenaming(p_list.tail(), p_st,
455: p_nat);
456: }
457:
458: private void computeProgramVariablePrefix(SortedSchemaVariable x) {
459: SetOfIProgramVariable prefix = getProgramVariablePrefix();
460:
461: if (x.sort() == ProgramSVSort.VARIABLE
462: && !prefix.contains((ProgramSV) x))
463: programVariablePrefixes.addFreeSchemaVariable(x);
464:
465: ListOfIProgramVariable oldPrefix = programVariablePrefixes
466: .getPrefix(x);
467:
468: if (oldPrefix == null)
469: programVariablePrefixes.addPrefix(x, toList(prefix));
470: else {
471: if (prefix.size() != oldPrefix.size())
472: prefixWarning(x, oldPrefix, prefix);
473:
474: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
475: IteratorOfIProgramVariable it = oldPrefix.iterator();
476: IProgramVariable pv;
477:
478: while (it.hasNext()) {
479: pv = it.next();
480: if (prefix.contains(pv))
481: res = res.prepend(pv);
482: else
483: prefixWarning(x, oldPrefix, prefix);
484: }
485:
486: programVariablePrefixes.addPrefix(x, res);
487: }
488: }
489:
490: }
491:
492: private static class VariableDeclarationUnit {
493: public ListOfIProgramVariable vars = SLListOfIProgramVariable.EMPTY_LIST;
494: public KeYJavaType type;
495:
496: public VariableDeclarationUnit(KeYJavaType p_type) {
497: type = p_type;
498: }
499: }
500:
501: private static class JumpStatementPrefixesImpl implements
502: JumpStatementPrefixes {
503:
504: private HashMap prefixes = new HashMap();
505:
506: private void addPrefix(SchemaVariable p_sv,
507: ListOfStatement p_prefix) {
508: prefixes.put(p_sv, p_prefix);
509: }
510:
511: public ListOfStatement getPrefix(SchemaVariable p) {
512: return (ListOfStatement) prefixes.get(p);
513: }
514:
515: }
516:
517: private static class RawProgramVariablePrefixesImpl implements
518: RawProgramVariablePrefixes {
519:
520: private HashMap prefixes = new HashMap();
521:
522: private SetOfIProgramVariable freeProgramVariables = SetAsListOfIProgramVariable.EMPTY_SET;
523: private SetOfSchemaVariable freeSchemaVariables = SetAsListOfSchemaVariable.EMPTY_SET;
524: private SetOfSchemaVariable boundSchemaVariables = SetAsListOfSchemaVariable.EMPTY_SET;
525:
526: public void addFreeProgramVariable(IProgramVariable p) {
527: freeProgramVariables = freeProgramVariables.add(p);
528: }
529:
530: public void addFreeSchemaVariable(SchemaVariable p) {
531: if (boundSchemaVariables.contains(p))
532: throw new InvalidPrefixException(
533: "Schema variables must not occur both bound and free "
534: + "within a taclet");
535:
536: freeSchemaVariables = freeSchemaVariables.add(p);
537: }
538:
539: public void addBoundSchemaVariable(SchemaVariable p) {
540: if (freeSchemaVariables.contains(p))
541: throw new InvalidPrefixException(
542: "Schema variables must not occur both bound and free "
543: + "within a taclet");
544:
545: boundSchemaVariables = boundSchemaVariables.add(p);
546: }
547:
548: private void addPrefix(SchemaVariable p_sv,
549: ListOfIProgramVariable p_prefix) {
550: prefixes.put(p_sv, p_prefix);
551: }
552:
553: public ListOfIProgramVariable getFreeProgramVariables() {
554: return toList(freeProgramVariables);
555: }
556:
557: public ListOfSchemaVariable getFreeSchemaVariables() {
558: return toList(freeSchemaVariables);
559: }
560:
561: public ListOfSchemaVariable getBoundSchemaVariables() {
562: return toList(boundSchemaVariables);
563: }
564:
565: public ListOfIProgramVariable getPrefix(SchemaVariable p) {
566: return (ListOfIProgramVariable) prefixes.get(p);
567: }
568:
569: public ProgramVariablePrefixes instantiate(SVInstantiations p) {
570: ListOfIProgramVariable freePV = getFreeProgramVariables()
571: .prepend(toPV(getFreeSchemaVariables(), p));
572:
573: HashMap res = new HashMap();
574: Iterator entryIt = prefixes.entrySet().iterator();
575: Map.Entry entry;
576:
577: while (entryIt.hasNext()) {
578: entry = (Map.Entry) entryIt.next();
579: res.put(entry.getKey(), freePV.prepend(toPV(
580: (ListOfIProgramVariable) entry.getValue(), p)));
581: }
582:
583: return new ProgramVariablePrefixesImpl(res);
584: }
585:
586: private IProgramVariable toPV(SchemaVariable p_sv,
587: SVInstantiations p_svi) {
588: return (IProgramVariable) p_svi.getInstantiation(p_sv);
589: }
590:
591: private ListOfIProgramVariable toPV(ListOfSchemaVariable p_svs,
592: SVInstantiations p_svi) {
593: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
594: IteratorOfSchemaVariable it = p_svs.iterator();
595:
596: while (it.hasNext())
597: res = res.prepend(toPV(it.next(), p_svi));
598:
599: return res;
600: }
601:
602: private ListOfIProgramVariable toPV(
603: ListOfIProgramVariable p_svs, SVInstantiations p_svi) {
604: ListOfIProgramVariable res = SLListOfIProgramVariable.EMPTY_LIST;
605: IteratorOfIProgramVariable it = p_svs.iterator();
606:
607: while (it.hasNext())
608: res = res.prepend(toPV((SchemaVariable) it.next(),
609: p_svi));
610:
611: return res;
612: }
613:
614: }
615:
616: private static class ProgramVariablePrefixesImpl implements
617: ProgramVariablePrefixes {
618:
619: private HashMap prefixes;
620:
621: private ProgramVariablePrefixesImpl(HashMap p_prefixes) {
622: prefixes = p_prefixes;
623: }
624:
625: public ListOfIProgramVariable getPrefix(SchemaVariable p) {
626: return (ListOfIProgramVariable) prefixes.get(p);
627: }
628:
629: }
630:
631: }
|