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 de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.java.Statement;
015: import de.uka.ilkd.key.java.StatementBlock;
016: import de.uka.ilkd.key.java.abstraction.*;
017: import de.uka.ilkd.key.java.declaration.Modifier;
018: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
019: import de.uka.ilkd.key.java.declaration.VariableSpecification;
020: import de.uka.ilkd.key.java.reference.ExecutionContext;
021: import de.uka.ilkd.key.java.reference.TypeRef;
022: import de.uka.ilkd.key.java.reference.VariableReference;
023: import de.uka.ilkd.key.java.statement.*;
024: import de.uka.ilkd.key.logic.*;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
027: import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor;
028: import de.uka.ilkd.key.rule.inst.SVInstantiations;
029: import de.uka.ilkd.key.util.ExtList;
030:
031: /**
032: * Replace context schema variables (.. ...) with nested method frames and try
033: * blocks, together with a number of statement skolem symbols to
034: * simulate code fragments.
035: */
036: public class ContextSkolemBuilder extends AbstractSkolemBuilder {
037:
038: // Statement SV that are used to represent enclosing code
039: private final Statement[] frameSVs;
040:
041: // Variables that describe the try-frame
042: private final Statement tryStatement;
043: private ListOfSchemaVariable tryVariables = SLListOfSchemaVariable.EMPTY_LIST;
044:
045: // Variables that describe the method frame
046: private Statement resultStatement = null;
047: private ListOfSchemaVariable resultVariables = null;
048: private SVTypeInfo resultSVTypeInfo = null;
049:
050: // The insertion point of the whole frame
051: private ListOfInteger insertionPoint = SLListOfInteger.EMPTY_LIST;
052:
053: public ContextSkolemBuilder(SkolemSet p_oriSkolemSet,
054: Services p_services) {
055: super (p_oriSkolemSet, p_services);
056:
057: frameSVs = createStatementSVs();
058: tryStatement = createTryStatement();
059: }
060:
061: public IteratorOfSkolemSet build() {
062: ListOfSkolemSet res = SLListOfSkolemSet.EMPTY_LIST;
063:
064: IteratorOfKeYJavaType typeIt = getTypeCandidates();
065: while (typeIt.hasNext()) {
066: setupFrame(typeIt.next());
067: res = res.append(createSkolemSet());
068: resetMethodFrame();
069: }
070:
071: return res.iterator();
072: }
073:
074: private SkolemSet createSkolemSet() {
075: final PosInProgram pip = toPosInProgram(insertionPoint);
076: final SVInstantiations svi = SVInstantiations.EMPTY_SVINSTANTIATIONS
077: .add(pip, pip, createDummyExecutionContext(), // TODO: something with execution context
078: resultStatement);
079:
080: SyntacticalReplaceVisitor srv = new SyntacticalReplaceVisitor(
081: getServices(), svi, Constraint.BOTTOM, false, null,
082: true, false);
083: getOriginalFormula().execPostOrder(srv);
084:
085: SkolemSet res = getOriginalSkolemSet()
086: .setFormula(srv.getTerm()).addMissing(
087: resultVariables.iterator());
088:
089: if (resultSVTypeInfo != null)
090: res = res.setSVTypeInfos(res.getSVTypeInfos().addInfo(
091: resultSVTypeInfo));
092:
093: return res;
094: }
095:
096: private PosInProgram toPosInProgram(ListOfInteger p) {
097: IteratorOfInteger it = p.iterator();
098: PosInProgram res = PosInProgram.TOP;
099:
100: while (it.hasNext())
101: res = res.down(it.next().intValue());
102:
103: return res;
104: }
105:
106: private void addTryVariable(SchemaVariable p_var) {
107: tryVariables = tryVariables.prepend(p_var);
108: }
109:
110: private void addResultVariable(SchemaVariable p_var) {
111: resultVariables = resultVariables.prepend(p_var);
112: }
113:
114: /**
115: * @return types that are possible result types of the method
116: * frame to be created; <code>null</code> means that the method frame
117: * should not have a result variable
118: */
119: private IteratorOfKeYJavaType getTypeCandidates() {
120: final Type[] primitiveTypes = new Type[] {
121: PrimitiveType.JAVA_LONG,
122: // PrimitiveType.JAVA_DOUBLE,
123: PrimitiveType.JAVA_BOOLEAN };
124:
125: ListOfKeYJavaType list = SLListOfKeYJavaType.EMPTY_LIST;
126: int i;
127:
128: for (i = 0; i != primitiveTypes.length; ++i)
129: list = list.prepend(getJavaInfo().getKeYJavaType(
130: primitiveTypes[i]));
131:
132: // <code>null</code> (i.e. no result variable) is added as the
133: // first possibility to consider (also see class <code>POBuilder</code>)
134: list = list.prepend((KeYJavaType) null);
135:
136: return list.iterator();
137: }
138:
139: /**
140: * Create the try frame
141: */
142: private Try createTryStatement() {
143: final Catch catchObj = createCatchBlock();
144:
145: final ExtList tryBodyStmts = new ExtList();
146: // an empty statement to mark the position of insertion
147: tryBodyStmts.add(new EmptyStatement());
148: tryBodyStmts.add(getFrameStatementSV(0));
149:
150: addTryVariable((SchemaVariable) getFrameStatementSV(0));
151:
152: final StatementBlock tryBody = new StatementBlock(tryBodyStmts);
153: up(0);
154: up(0);
155:
156: return new Try(tryBody, new Branch[] { catchObj });
157: }
158:
159: /**
160: * Create the catch block of the try block
161: */
162: private Catch createCatchBlock() {
163: final ParameterDeclaration thDecl = createTryGuardVariable();
164: final StatementBlock catchBody = new StatementBlock(
165: getFrameStatementSV(1));
166:
167: addTryVariable((SchemaVariable) getFrameStatementSV(1));
168:
169: return new Catch(thDecl, catchBody);
170: }
171:
172: /**
173: * Create the guard variable of the catch leg of the try block.
174: * @return a <code>ParameterDeclaration</code> of the variable
175: */
176: private ParameterDeclaration createTryGuardVariable() {
177: final KeYJavaType thType = getJavaInfo().getTypeByClassName(
178: "java.lang.Throwable");
179: final TypeRef thRef = new TypeRef(thType);
180:
181: final ProgramElementName thName = createUniquePEName("frame_th");
182: final SchemaVariable thVar = SchemaVariableFactory
183: .createProgramSV(thName, ProgramSVSort.VARIABLE, false);
184: final VariableSpecification thSpec = new VariableSpecification(
185: (IProgramVariable) thVar, thType);
186: final ParameterDeclaration thDecl = new ParameterDeclaration(
187: new Modifier[0], thRef, thSpec, false);
188:
189: addTryVariable(thVar);
190:
191: return thDecl;
192: }
193:
194: /**
195: * Create the complete frame statement for a given result type
196: */
197: private void setupFrame(KeYJavaType p_resultType) {
198: resultVariables = tryVariables;
199:
200: final MethodFrame mfObj = createMethodFrame(p_resultType);
201:
202: final ExtList topLevelStmts = new ExtList();
203: topLevelStmts.add(mfObj);
204: topLevelStmts.add(getFrameStatementSV(2));
205:
206: addResultVariable((SchemaVariable) getFrameStatementSV(2));
207:
208: resultStatement = new StatementBlock(topLevelStmts);
209: up(0);
210: }
211:
212: /**
213: * Create the method frame statement
214: */
215: private MethodFrame createMethodFrame(KeYJavaType p_resultType) {
216: final IProgramVariable resVar = createResultVariable(p_resultType);
217:
218: final StatementBlock mfBody = new StatementBlock(tryStatement);
219: up(0);
220:
221: final MethodFrame mfObj = new MethodFrame(resVar,
222: createDummyExecutionContext(), mfBody);
223: up(p_resultType == null ? 1 : 2);
224:
225: return mfObj;
226: }
227:
228: /**
229: * Create the result variable of the method frame
230: * @param p_resultType the type the variable should have, or
231: * <code>null</code> if the method frame is not to be given a result
232: * variable at all
233: * @return the result variable, or <code>null</code> for
234: * <code>p_resultType==null</code>
235: */
236: private IProgramVariable createResultVariable(
237: KeYJavaType p_resultType) {
238: if (p_resultType == null) {
239: resultSVTypeInfo = null;
240: return null;
241: }
242:
243: final IProgramVariable res = (IProgramVariable) SchemaVariableFactory
244: .createProgramSV(createUniquePEName("frame_res"),
245: ProgramSVSort.VARIABLE, false);
246:
247: resultSVTypeInfo = new SVTypeInfo(((SchemaVariable) res),
248: p_resultType);
249: addResultVariable((SchemaVariable) res);
250:
251: return res;
252: }
253:
254: /**
255: * HACK to create an execution context somehow
256: */
257: private ExecutionContext createDummyExecutionContext() {
258: ProgramElementName refName = new ProgramElementName("ref");
259: ProgramVariable refVar = new LocationVariable(refName,
260: getJavaInfo().getJavaLangObject());
261: VariableReference ref = new VariableReference(refVar);
262: ExecutionContext context = new ExecutionContext(new TypeRef(
263: getJavaInfo().getJavaLangObject()), ref);
264: return context;
265: }
266:
267: private void resetMethodFrame() {
268: insertionPoint = insertionPoint.tail().tail().tail();
269: }
270:
271: /**
272: * @param p_num the number of the SV to return;
273: * currently <code>p_num</code> has to be an element of [0, 3)
274: * @return frame statement SV with number <code>p_num</code>
275: */
276: private Statement getFrameStatementSV(int p_num) {
277: return frameSVs[p_num];
278: }
279:
280: /**
281: * Setup frame SV
282: */
283: private Statement[] createStatementSVs() {
284: int i = 3;
285: final Statement[] res = new Statement[i];
286:
287: while (i-- != 0) {
288: final ProgramElementName name = createUniquePEName("frame_s"
289: + i);
290: res[i] = (Statement) SchemaVariableFactory.createProgramSV(
291: name, ProgramSVSort.STATEMENT, false);
292: }
293:
294: return res;
295: }
296:
297: /**
298: * Modify the <code>insertionPoint</code> by increasing the depth by one;
299: * this means that the old frame is made a direct subtree of the new frame
300: */
301: private void up(int p) {
302: final Integer t = new Integer(p);
303: insertionPoint = insertionPoint.prepend(t);
304: }
305:
306: }
|