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.java;
012:
013: import java.io.IOException;
014:
015: import de.uka.ilkd.key.java.reference.ExecutionContext;
016: import de.uka.ilkd.key.java.reference.IExecutionContext;
017: import de.uka.ilkd.key.java.statement.MethodFrame;
018: import de.uka.ilkd.key.java.visitor.Visitor;
019: import de.uka.ilkd.key.logic.IntIterator;
020: import de.uka.ilkd.key.logic.PosInProgram;
021: import de.uka.ilkd.key.logic.ProgramPrefix;
022: import de.uka.ilkd.key.rule.MatchConditions;
023: import de.uka.ilkd.key.rule.inst.SVInstantiations;
024: import de.uka.ilkd.key.util.Debug;
025: import de.uka.ilkd.key.util.ExtList;
026:
027: /**
028: * In the DL-formulae description of Taclets the program part can have
029: * the following form < pi alpha;...; omega > Phi where pi is a prefix
030: * consisting of open brackets, try's and so on and omega is the rest
031: * of the program. Between the prefix pi and the postfix omega there
032: * can stand an arbitrary program. This pattern is realized using this
033: * class.
034: */
035:
036: public class ContextStatementBlock extends StatementBlock {
037:
038: /**
039: * the last execution context of the context term
040: */
041: private IExecutionContext executionContext;
042:
043: /** creates a ContextStatementBlock
044: * @param children the body of the context term
045: */
046: public ContextStatementBlock(ExtList children) {
047: super (children);
048: }
049:
050: /** creates a ContextStatementBlock
051: * @param children the body of the context term
052: * @param executionContext the required execution context
053: */
054: public ContextStatementBlock(ExtList children,
055: IExecutionContext executionContext) {
056: super (children);
057: this .executionContext = executionContext;
058: }
059:
060: public boolean requiresExplicitExecutionContextMatch() {
061: return executionContext != null;
062: }
063:
064: public IExecutionContext getExecutionContext() {
065: return executionContext;
066: }
067:
068: /**
069: * Returns the number of children of this node.
070: * @return an int giving the number of children of this node
071: */
072:
073: public int getChildCount() {
074: int count = 0;
075: if (executionContext != null)
076: count++;
077: count += super .getChildCount();
078: return count;
079: }
080:
081: /**
082: * Returns the child at the specified index in this node's "virtual"
083: * child array
084: * @param index an index into this node's "virtual" child array
085: * @return the program element at the given position
086: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
087: * of bounds
088: */
089: public ProgramElement getChildAt(int index) {
090: if (executionContext != null) {
091: if (index == 0) {
092: return executionContext;
093: }
094: index--;
095: }
096: return super .getChildAt(index);
097: }
098:
099: /** calls the corresponding method of a visitor in order to
100: * perform some action/transformation on this element
101: * @param v the Visitor
102: */
103: public void visit(Visitor v) {
104: v.performActionOnContextStatementBlock(this );
105: }
106:
107: public void prettyPrint(PrettyPrinter w) throws IOException {
108: w.printContextStatementBlock(this );
109: }
110:
111: /* toString */
112: public String toString() {
113: StringBuffer result = new StringBuffer();
114: result.append("..");
115: result.append(super .toString());
116: result.append("\n");
117: result.append("...");
118: return result.toString();
119: }
120:
121: public int getTypeDeclarationCount() {
122: throw new UnsupportedOperationException(getClass()
123: + ": We are not quite a StatementBlock");
124: }
125:
126: public de.uka.ilkd.key.java.declaration.TypeDeclaration getTypeDeclarationAt(
127: int index) {
128: throw new UnsupportedOperationException(getClass()
129: + ": We are not quite a StatementBlock");
130: }
131:
132: /**
133: * overrides the check of the superclass as unmatched elements will disappear in
134: * the suffix of this ContextStatementBlock
135: */
136: public boolean compatibleBlockSize(int pos, int max) {
137: return true;
138: }
139:
140: public MatchConditions match(SourceData source,
141: MatchConditions matchCond) {
142: SourceData newSource = source;
143:
144: if (matchCond.getInstantiations().getContextInstantiation() != null) {
145: // Currently we do not allow to context statement block
146: // occurrences in find or assumes clauses
147: return null;
148: }
149:
150: final ProgramElement src = newSource.getSource();
151: final Services services = source.getServices();
152:
153: ExecutionContext lastExecutionContext = null;
154:
155: final ProgramPrefix prefix;
156: int pos = -1;
157: PosInProgram relPos = PosInProgram.TOP;
158:
159: if (src instanceof ProgramPrefix) {
160: prefix = (ProgramPrefix) src;
161: final int srcPrefixLength = prefix.getPrefixLength();
162: final int patternPrefixLength = getPrefixLength();
163:
164: if (patternPrefixLength > srcPrefixLength) {
165: Debug
166: .out(
167: "Program match FAILED. Source has not enough prefix elements.",
168: this , source);
169: return null;
170: }
171:
172: pos = srcPrefixLength - patternPrefixLength;
173:
174: ProgramPrefix firstActiveStatement = prefix
175: .getPrefixElementAt(pos);
176:
177: relPos = firstActiveStatement.getFirstActiveChildPos();
178:
179: // firstActiveStatement contains the ProgramPrefix in front of the first active statement
180: // start denotes the child where to start to match
181: // in some cases firstActiveStatement already denotes the element to match
182: // (empty block, empty try block etc.) this is encoded by setting start to -1
183: int start = -1;
184:
185: if (relPos != PosInProgram.TOP) {
186: if (firstActiveStatement instanceof MethodFrame) {
187: lastExecutionContext = (ExecutionContext) ((MethodFrame) firstActiveStatement)
188: .getExecutionContext();
189: }
190:
191: start = relPos.get(relPos.depth() - 1);
192: if (relPos.depth() > 1) {
193: firstActiveStatement = (ProgramPrefix) PosInProgram
194: .getProgramAt(relPos.up(),
195: firstActiveStatement);
196: }
197: }
198: newSource = new SourceData(firstActiveStatement, start,
199: services);
200: } else {
201: prefix = null;
202: }
203: matchCond = matchInnerExecutionContext(matchCond, services,
204: lastExecutionContext, prefix, pos, src);
205:
206: if (matchCond == null) {
207: return null;
208: }
209:
210: // matching children
211: matchCond = matchChildren(newSource, matchCond,
212: executionContext == null ? 0 : 1);
213:
214: if (matchCond == null) {
215: return null;
216: }
217:
218: matchCond = makeContextInfoComplete(matchCond, newSource,
219: prefix, pos, relPos, src);
220:
221: if (matchCond == null) {
222: return null;
223: }
224:
225: Debug.out("Successful match.");
226: return matchCond;
227: }
228:
229: /**
230: * completes match of context block by adding the prefix end position
231: * and the suffix start position
232: */
233: private MatchConditions makeContextInfoComplete(
234: MatchConditions matchCond, SourceData newSource,
235: ProgramPrefix prefix, int pos, PosInProgram relPos,
236: ProgramElement src) {
237:
238: final SVInstantiations instantiations = matchCond
239: .getInstantiations();
240: final ExecutionContext lastExecutionContext = instantiations
241: .getExecutionContext();
242:
243: final PosInProgram prefixEnd = matchPrefixEnd(prefix, pos,
244: relPos);
245:
246: // compute position of the first element not matched
247: final int lastMatchedPos = newSource.getChildPos();
248: final PosInProgram suffixStart = prefixEnd.up().down(
249: lastMatchedPos);
250:
251: /** add context block instantiation */
252: matchCond = matchCond.setInstantiations(instantiations.replace(
253: prefixEnd, suffixStart, lastExecutionContext, src));
254: return matchCond;
255: }
256:
257: /**
258: * matches the inner most execution context in prefix, used to resolve references in
259: * succeeding matchings
260: * @param matchCond the MatchCond the matchonditions already found
261: * @param services the Services
262: * @param lastExecutionContext the ExecutionContext if already found
263: * @param prefix the oute rmost prefixelement of the original source
264: * @param pos an int as the number of prefix elements to disappear in the context
265: * @param src the original source
266: * @return the inner most execution context
267: */
268: private MatchConditions matchInnerExecutionContext(
269: MatchConditions matchCond, final Services services,
270: ExecutionContext lastExecutionContext,
271: final ProgramPrefix prefix, int pos,
272: final ProgramElement src) {
273:
274: // partial context instantiation
275:
276: ExecutionContext innerContext = lastExecutionContext;
277:
278: if (innerContext == null) {
279: innerContext = services.getJavaInfo()
280: .getDefaultExecutionContext();
281: if (prefix != null) {
282: for (int i = pos - 1; i >= 0; i--) {
283: final ProgramPrefix prefixEl = prefix
284: .getPrefixElementAt(i);
285: if (prefixEl instanceof MethodFrame) {
286: innerContext = (ExecutionContext) ((MethodFrame) prefixEl)
287: .getExecutionContext();
288: break;
289: }
290: }
291: }
292: }
293:
294: if (executionContext != null) {
295: matchCond = executionContext.match(new SourceData(
296: innerContext, -1, services), matchCond);
297: if (matchCond == null) {
298: Debug.out("Program match. ExecutionContext mismatch.");
299: return null;
300: }
301: Debug.out("Program match. ExecutionContext matched.");
302: }
303:
304: matchCond = matchCond
305: .setInstantiations(matchCond.getInstantiations().add(
306: null, null, innerContext, src));
307:
308: return matchCond;
309: }
310:
311: /**
312: * computes the PosInProgram of the first element, which is not part of the prefix
313: * @param prefix the ProgramPrefix the outer most prefix element of the source
314: * @param pos the number of elements to disappear in the context
315: * @param relPos the position of the first active statement of element
316: * prefix.getPrefixElementAt(pos);
317: * @return the PosInProgram of the first element, which is not part of the prefix
318: */
319: private PosInProgram matchPrefixEnd(final ProgramPrefix prefix,
320: int pos, PosInProgram relPos) {
321: PosInProgram prefixEnd = PosInProgram.TOP;
322: if (prefix != null) {
323: final IntIterator[] iterators = new IntIterator[pos + 1];
324: iterators[pos] = relPos.iterator();
325:
326: for (int i = pos - 1; i >= 0; i--) {
327: final ProgramPrefix prefixEl = prefix
328: .getPrefixElementAt(i);
329: iterators[i] = prefixEl.getFirstActiveChildPos()
330: .iterator();
331: }
332:
333: for (int i = 0; i < iterators.length; i++) {
334: final IntIterator it = iterators[i];
335: while (it.hasNext()) {
336: prefixEnd = prefixEnd.down(it.next());
337: }
338: }
339: } else {
340: prefixEnd = relPos;
341: }
342: return prefixEnd;
343: }
344: }
|