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.java.visitor;
011:
012: import de.uka.ilkd.key.java.*;
013: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
014: import de.uka.ilkd.key.java.statement.LabeledStatement;
015: import de.uka.ilkd.key.java.statement.MethodFrame;
016: import de.uka.ilkd.key.java.statement.SynchronizedBlock;
017: import de.uka.ilkd.key.java.statement.Try;
018: import de.uka.ilkd.key.logic.IntIterator;
019: import de.uka.ilkd.key.logic.PosInProgram;
020: import de.uka.ilkd.key.rule.inst.ContextStatementBlockInstantiation;
021:
022: /**
023: * A context given as {@link ContextStatementBlockInstantiation} is wrapped
024: * around a given {@link ProgramElement}.
025: */
026: public class ProgramContextAdder {
027:
028: /**
029: * singleton instance of the program context adder
030: */
031: public final static ProgramContextAdder INSTANCE = new ProgramContextAdder();
032:
033: /**
034: * an empty private constructor to ensure the singleton property
035: */
036: private ProgramContextAdder() {
037: }
038:
039: /**
040: * wraps the context around the statements found in the putIn block
041: */
042: public JavaNonTerminalProgramElement start(
043: JavaNonTerminalProgramElement context,
044: StatementBlock putIn, ContextStatementBlockInstantiation ct) {
045:
046: return wrap(context, putIn, ct.prefix().iterator(), ct.prefix()
047: .depth(), ct.prefix(), ct.suffix());
048: }
049:
050: protected JavaNonTerminalProgramElement wrap(
051: JavaNonTerminalProgramElement context,
052: StatementBlock putIn, IntIterator prefixPos,
053: int prefixDepth, PosInProgram prefix, PosInProgram suffix) {
054:
055: JavaNonTerminalProgramElement body = null;
056:
057: ProgramElement next = prefixPos.hasNext() ? context
058: .getChildAt(prefixPos.next()) : null;
059:
060: if (!prefixPos.hasNext()) {
061: body = createWrapperBody(context, putIn, suffix);
062: // special case labeled statement as a label must not be
063: // succeeded by a statement block
064: if (context instanceof LabeledStatement) {
065: body = createLabeledStatementWrapper(
066: (LabeledStatement) context, body);
067: }
068: return body;
069: } else {
070: body = wrap((JavaNonTerminalProgramElement) next, putIn,
071: prefixPos, prefixDepth, prefix, suffix);
072: if (context instanceof StatementBlock) {
073: return createStatementBlockWrapper(
074: (StatementBlock) context, body);
075: } else if (context instanceof Try) {
076: return createTryStatementWrapper((StatementBlock) body,
077: (Try) context);
078: } else if (context instanceof MethodFrame) {
079: return createMethodFrameWrapper((MethodFrame) context,
080: (StatementBlock) body);
081: } else if (context instanceof LabeledStatement) {
082: return createLabeledStatementWrapper(
083: (LabeledStatement) context, body);
084: } else {
085: return createSynchronizedBlockWrapper(
086: (SynchronizedBlock) context,
087: (StatementBlock) body);
088: }
089: }
090: }
091:
092: /**
093: * inserts the content of the statement block <code>putIn</code> and
094: * adds succedding children of the innermost non terminal element
095: * (usually statement block) in the context.
096: * @param wrapper the JavaNonTerminalProgramElement with the context
097: * that has to be wrapped around the content of <code>putIn</code>
098: * @param putIn the StatementBlock with content that has to be
099: * wrapped by the elements hidden in the context
100: * @param suffix the PosInProgram describing the position of the
101: * first element before the suffix of the context
102: * @return the StatementBlock which encloses the content of
103: * <code>putIn</code> together with the succeeding context elements
104: * of the innermost context statemebt block (attention:
105: * in a case like
106: * <code>{{{oldStmnt; list of further stmnt;}} moreStmnts; }</code>
107: * only the underscored part is returned
108: * <code>{{ __{putIn;....}__ }moreStmnts;}</code>
109: * adding the other braces including the <code>moreStmnts;</code>
110: * part has to be done elsewhere.
111: */
112: private final StatementBlock createWrapperBody(
113: JavaNonTerminalProgramElement wrapper,
114: StatementBlock putIn, PosInProgram suffix) {
115:
116: final int putInLength = putIn.getChildCount();
117:
118: final int lastChild = suffix.last();
119:
120: final int childLeft = wrapper.getChildCount() - lastChild;
121:
122: final int childrenToAdd = putInLength + childLeft;
123:
124: if (childLeft == 0) {
125: return putIn;
126: }
127:
128: final Statement[] body = new Statement[childrenToAdd];
129:
130: putIn.getBody().arraycopy(0, body, 0, putInLength);
131:
132: for (int i = putInLength; i < childrenToAdd; i++) {
133: body[i] = (Statement) wrapper.getChildAt(lastChild
134: + (i - putInLength));
135: }
136:
137: /*
138: Example:
139: In <code>{{{oldStmnt; list of further stmnt;}} moreStmnts; }</code>
140: where <code>oldStmnt;</code> has to be replaced by the content of
141: <code>putIn</code>. Up to here (including the return
142: statement) the underscored part has been created:
143: <code>{{ __{putIn;....}__ }moreStmnts;}</code>
144: Attention: we have not yet added the enclosing braces or even
145: the <code>moreStmnts</code>
146: */
147: return new StatementBlock(new ArrayOfStatement(body));
148: }
149:
150: /**
151: * Replaces the first statement in the wrapper block. The
152: * replacement is optimized as it just returns the replacement block
153: * if it is the only child of the statement block to be constructed
154: * and the chld is a statementblock too.
155: * @param wrapper the StatementBlock where to replace the first
156: * statement
157: * @param replacement the StatementBlock that replaces the first
158: * statement of the block
159: * @return the resulting statement block
160: */
161: protected StatementBlock createStatementBlockWrapper(
162: StatementBlock wrapper,
163: JavaNonTerminalProgramElement replacement) {
164: int childrenCount = wrapper.getStatementCount();
165: if (childrenCount <= 1 && replacement instanceof StatementBlock) {
166: return (StatementBlock) replacement;
167: } else {
168: Statement[] body = new Statement[childrenCount > 0 ? childrenCount
169: : 1];
170: /* reconstruct block */
171: body[0] = (Statement) replacement;
172: if (childrenCount - 1 > 0) {
173: wrapper.getBody().arraycopy(1, body, 1,
174: childrenCount - 1);
175: }
176: return new StatementBlock(new ArrayOfStatement(body));
177: }
178: }
179:
180: protected Try createTryStatementWrapper(StatementBlock body, Try old) {
181: return new Try(body, old.getBranchList());
182: }
183:
184: protected MethodFrame createMethodFrameWrapper(MethodFrame old,
185: StatementBlock body) {
186: return new MethodFrame(old.getProgramVariable(), old
187: .getExecutionContext(), body, old.getProgramMethod(),
188: PositionInfo.UNDEFINED);
189: }
190:
191: protected LabeledStatement createLabeledStatementWrapper(
192: LabeledStatement old, JavaNonTerminalProgramElement body) {
193: return new LabeledStatement(
194: old.getLabel(),
195: body instanceof StatementBlock
196: && body.getChildCount() == 1
197: && !(body.getChildAt(0) instanceof LocalVariableDeclaration) ? (Statement) body
198: .getChildAt(0)
199: : (Statement) body);
200: }
201:
202: protected SynchronizedBlock createSynchronizedBlockWrapper(
203: SynchronizedBlock old, StatementBlock body) {
204: return new SynchronizedBlock(old.getExpression(), body);
205: }
206:
207: }
|