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: package de.uka.ilkd.key.java;
010:
011: import java.util.HashMap;
012: import java.util.LinkedList;
013:
014: import de.uka.ilkd.key.java.abstraction.*;
015: import de.uka.ilkd.key.java.declaration.*;
016: import de.uka.ilkd.key.java.declaration.modifier.Private;
017: import de.uka.ilkd.key.java.declaration.modifier.Protected;
018: import de.uka.ilkd.key.java.declaration.modifier.Static;
019: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
020: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
021: import de.uka.ilkd.key.java.expression.literal.NullLiteral;
022: import de.uka.ilkd.key.java.expression.operator.LessThan;
023: import de.uka.ilkd.key.java.expression.operator.PostIncrement;
024: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
025: import de.uka.ilkd.key.java.recoderext.InstanceAllocationMethodBuilder;
026: import de.uka.ilkd.key.java.recoderext.PrepareObjectBuilder;
027: import de.uka.ilkd.key.java.reference.*;
028: import de.uka.ilkd.key.java.statement.For;
029: import de.uka.ilkd.key.java.statement.Return;
030: import de.uka.ilkd.key.logic.ProgramElementName;
031: import de.uka.ilkd.key.logic.op.LocationVariable;
032: import de.uka.ilkd.key.logic.op.ProgramMethod;
033: import de.uka.ilkd.key.logic.op.ProgramVariable;
034:
035: /**
036: * This class creates the <code><createArray></code> method for array
037: * creation and in particular its helper method
038: * <code><createArrayHelper></code>. This class hould be replaced by a
039: * recoder transformation as soon as we port our array data structures to
040: * RecodeR.
041: */
042: public class CreateArrayMethodBuilder extends KeYJavaASTFactory {
043:
044: public static final String IMPLICIT_ARRAY_CREATE = "<createArray>";
045:
046: public static final String IMPLICIT_ARRAY_CREATE_TRANSIENT = "<createTransientArray>";
047:
048: public static final String IMPLICIT_ARRAY_CREATION_HELPER = "<createArrayHelper>";
049:
050: public static final String IMPLICIT_ARRAY_TRANSIENT_CREATION_HELPER = "<createTransientArrayHelper>";
051:
052: // as these methods are thought to be only preliminary(we cache some
053: // information here)
054: private final HashMap cache = new HashMap(3);
055:
056: /**
057: * keeps the currently used integer type
058: */
059: protected final KeYJavaType integerType;
060:
061: /**
062: * stores the currently used object type
063: */
064: protected final KeYJavaType objectType;
065:
066: /** create the method builder for array implict creation methods */
067: public CreateArrayMethodBuilder(KeYJavaType integerType,
068: KeYJavaType objectType) {
069: this .integerType = integerType;
070: this .objectType = objectType;
071: }
072:
073: /**
074: * creates the statements which take the next object out of the list of
075: * available objects
076: *
077: * @return the statements which take the next object out of the list of
078: * available objects
079: */
080: protected LinkedList createArray(ListOfField fields) {
081: LinkedList result = new LinkedList();
082: ListOfField implicitFields = filterImplicitFields(fields);
083:
084: // declared only in Object so we have to look there
085: ProgramVariable initialized = findInObjectFields(ImplicitFieldAdder.IMPLICIT_INITIALIZED);
086: ProgramVariable trans;
087: if (initialized == null) {
088: // only if createObject for Object is called
089: initialized = find(ImplicitFieldAdder.IMPLICIT_INITIALIZED,
090: implicitFields);
091: trans = find(ImplicitFieldAdder.IMPLICIT_TRANSIENT,
092: implicitFields);
093: } else {
094: trans = findInObjectFields(ImplicitFieldAdder.IMPLICIT_TRANSIENT);
095: }
096:
097: result.addLast(assign(attribute(new ThisReference(), trans),
098: new IntLiteral(0)));
099:
100: result.addLast(assign(attribute(new ThisReference(),
101: initialized), BooleanLiteral.FALSE));
102: return result;
103: }
104:
105: /**
106: * extracts all field specifications out of the given list. Therefore it
107: * descends into field declarations.
108: *
109: * @param list
110: * the ArrayOfMemberDeclaration with the members of a type
111: * declaration
112: * @return a ListOfField the includes all field specifications found int the
113: * field declaration of the given list
114: */
115: protected ListOfField filterField(ArrayOfMemberDeclaration list) {
116: ListOfField result = SLListOfField.EMPTY_LIST;
117: for (int i = list.size() - 1; i >= 0; i--) {
118: MemberDeclaration pe = list.getMemberDeclaration(i);
119: if (pe instanceof FieldDeclaration) {
120: result = result
121: .append(filterField((FieldDeclaration) pe));
122: }
123: }
124: return result;
125: }
126:
127: /**
128: * extracts all fields out of fielddeclaration
129: *
130: * @param field
131: * the FieldDeclaration of which the field specifications have to
132: * be extracted
133: * @return a ListOfField the includes all field specifications found int the
134: * field declaration of the given list
135: */
136: protected final ListOfField filterField(FieldDeclaration field) {
137: ListOfField result = SLListOfField.EMPTY_LIST;
138: ArrayOfFieldSpecification spec = field.getFieldSpecifications();
139: for (int i = spec.size() - 1; i >= 0; i--) {
140: result = result.prepend(spec.getFieldSpecification(i));
141: }
142: return result;
143: }
144:
145: /**
146: * extracts all implicit field specifications out of the given list
147: *
148: * @param list
149: * the ListOfField from which the implicit ones have to be
150: * selected
151: * @return a list with all implicit fields found in 'list'
152: */
153: protected ListOfField filterImplicitFields(ListOfField list) {
154: ListOfField result = SLListOfField.EMPTY_LIST;
155: IteratorOfField it = list.iterator();
156: while (it.hasNext()) {
157: Field field = it.next();
158: if (field instanceof ImplicitFieldSpecification) {
159: result = result.append(field);
160: }
161: }
162: return result;
163: }
164:
165: /**
166: * retrieves a field with the given name out of the list
167: *
168: * @param name
169: * a String with the name of the field to be looked for
170: * @param fields
171: * the ListOfField where we have to look for the field
172: * @return the program variable of the given name or null if not found
173: */
174: protected ProgramVariable find(String name, ListOfField fields) {
175: IteratorOfField it = fields.iterator();
176: while (it.hasNext()) {
177: Field field = it.next();
178: final ProgramVariable fieldVar = (ProgramVariable) field
179: .getProgramVariable();
180: if (name.equals(fieldVar.getProgramElementName()
181: .getProgramName())) {
182: return fieldVar;
183: }
184: }
185: return null;
186: }
187:
188: protected ProgramVariable findInObjectFields(String name) {
189: ProgramVariable var = (ProgramVariable) cache.get(name);
190: if (var == null && objectType.getJavaType() != null) {
191: final ListOfField objectFields = filterImplicitFields(filterField(((ClassDeclaration) objectType
192: .getJavaType()).getMembers()));
193: var = find(name, objectFields);
194: if (var != null) { // may be null if object is currently created
195: cache.put(name, var);
196: }
197: }
198: return var;
199: }
200:
201: // ================ HELPER METHODS =========================
202:
203: /**
204: * creates the implicit method <code><allocate></code> which is a
205: * stump and given meaning by a contract
206: */
207: public ProgramMethod getArrayInstanceAllocatorMethod(
208: TypeReference arrayTypeReference) {
209:
210: final Modifier[] modifiers = new Modifier[] { new Private(),
211: new Static() };
212:
213: final KeYJavaType arrayType = arrayTypeReference
214: .getKeYJavaType();
215:
216: final MethodDeclaration md = new MethodDeclaration(
217: modifiers,
218: arrayTypeReference,
219: new ProgramElementName(
220: InstanceAllocationMethodBuilder.IMPLICIT_INSTANCE_ALLOCATE),
221: new ParameterDeclaration[0], null, null, false);
222:
223: return new ProgramMethod(md, arrayType, arrayType,
224: PositionInfo.UNDEFINED);
225: }
226:
227: protected StatementBlock getCreateArrayBody(TypeReference arrayRef,
228: ProgramVariable paramLength) {
229:
230: final LocalVariableDeclaration local = declare(
231: new ProgramElementName("newObject"), arrayRef);
232: final ProgramVariable newObject = (ProgramVariable) local
233: .getVariables().getVariableSpecification(0)
234: .getProgramVariable();
235: final LinkedList body = new LinkedList();
236:
237: body.addLast(local);
238: body
239: .addLast(assign(
240: newObject,
241: new MethodReference(
242: new ArrayOfExpression(),
243: new ProgramElementName(
244: InstanceAllocationMethodBuilder.IMPLICIT_INSTANCE_ALLOCATE),
245: arrayRef)));
246:
247: body
248: .add(new MethodReference(
249: new ArrayOfExpression(paramLength),
250: new ProgramElementName(
251: CreateArrayMethodBuilder.IMPLICIT_ARRAY_CREATION_HELPER),
252: newObject));
253:
254: body.add(new Return(newObject));
255:
256: return new StatementBlock((Statement[]) body
257: .toArray(new Statement[body.size()]));
258: }
259:
260: /**
261: * creates the body of method <code><createArrayHelper(int
262: * paramLength)></code>
263: * therefore it first adds the statements responsible to take the correct
264: * one out of the list, then the arrays length attribute is set followed by
265: * a call to <code><prepare>()</code> setting the arrays fields on
266: * their default value.
267: *
268: * @param length
269: * the final public ProgramVariable
270: * <code>length</length> of the array
271: * @param paramLength the ProgramVariable which is the parameter of
272: * the <code><createArray></code> method
273: * @param prepare the ProgramMethod <code><prepare>()</code>
274: * which will be called when executing
275: * <code><createArray></code>
276: * @param fields the ListOfFields of the current array
277: * @param createTransient a boolean indicating if a transient array has
278: * to be created (this is special to JavaCard)
279: * @param transientType a ProgramVariable identifying the kind of transient
280: * @return the StatementBlock which is the method's body <br></br>
281: * <code>
282: * {
283: * this.<nextToCreate> = this.<nextToCreate>.<next>;
284: * this.<initialized> = false;
285: * this.<created> = true;
286: * this.length = paramLength;
287: * this.<prepare>();
288: * this.<transient> = transientType;
289: * this.<initialized> = true;
290: * return this;
291: * }
292: * </code>
293: */
294: protected StatementBlock getCreateArrayHelperBody(
295: ProgramVariable length, ProgramVariable paramLength,
296: ListOfField fields, boolean createTransient,
297: ProgramVariable transientType) {
298:
299: final ThisReference this Ref = new ThisReference();
300:
301: final LinkedList body = createArray(fields);
302:
303: body.add(assign(attribute(this Ref, length), paramLength));
304:
305: body.add(new MethodReference(new ArrayOfExpression(),
306: new ProgramElementName(
307: PrepareObjectBuilder.IMPLICIT_OBJECT_PREPARE),
308: null));
309:
310: if (createTransient) {
311: body
312: .add(assign(
313: attribute(
314: this Ref,
315: findInObjectFields(ImplicitFieldAdder.IMPLICIT_TRANSIENT)),
316: transientType));
317: }
318:
319: body
320: .add(assign(
321: attribute(
322: this Ref,
323: findInObjectFields(ImplicitFieldAdder.IMPLICIT_INITIALIZED)),
324: BooleanLiteral.TRUE));
325:
326: body.add(new Return(this Ref));
327:
328: return new StatementBlock((Statement[]) body
329: .toArray(new Statement[body.size()]));
330: }
331:
332: /**
333: * create the method declaration of the
334: * <code><createArrayHelper></code> method
335: */
336: public ProgramMethod getCreateArrayHelperMethod(
337: TypeReference arrayTypeReference, ProgramVariable length,
338: ListOfField fields) {
339:
340: final Modifier[] modifiers = new Modifier[] { new Private() };
341: final KeYJavaType arrayType = arrayTypeReference
342: .getKeYJavaType();
343:
344: final ProgramVariable paramLength = new LocationVariable(
345: new ProgramElementName("length"), integerType);
346:
347: final ParameterDeclaration param = new ParameterDeclaration(
348: new Modifier[0], new TypeRef(integerType),
349: new VariableSpecification(paramLength), false);
350:
351: final MethodDeclaration md = new MethodDeclaration(modifiers,
352: arrayTypeReference, new ProgramElementName(
353: IMPLICIT_ARRAY_CREATION_HELPER),
354: new ParameterDeclaration[] { param }, null,
355: getCreateArrayHelperBody(length, paramLength, fields,
356: false, null), false);
357:
358: return new ProgramMethod(md, arrayType, arrayType,
359: PositionInfo.UNDEFINED);
360: }
361:
362: /**
363: * creates the implicit method <code><createArray></code> it
364: * fulfills a similar purpose as <code><createObject></code> in
365: * addition it sets the arrays length and calls the prepare method
366: */
367: public ProgramMethod getCreateArrayMethod(
368: TypeReference arrayTypeReference, ProgramMethod prepare,
369: ListOfField fields) {
370:
371: final Modifier[] modifiers = new Modifier[] { new Protected(),
372: new Static() };
373:
374: final KeYJavaType arrayType = arrayTypeReference
375: .getKeYJavaType();
376:
377: final ProgramVariable paramLength = new LocationVariable(
378: new ProgramElementName("length"), integerType);
379:
380: final ParameterDeclaration param = new ParameterDeclaration(
381: new Modifier[0], new TypeRef(integerType),
382: new VariableSpecification(paramLength), false);
383:
384: final MethodDeclaration md = new MethodDeclaration(modifiers,
385: arrayTypeReference, new ProgramElementName(
386: IMPLICIT_ARRAY_CREATE),
387: new ParameterDeclaration[] { param }, null,
388: getCreateArrayBody(arrayTypeReference, paramLength),
389: false);
390:
391: return new ProgramMethod(md, arrayType, arrayType,
392: PositionInfo.UNDEFINED);
393: }
394:
395: /**
396: * returns the default value of the given type according to JLS \S 4.5.5
397: *
398: * @return the default value of the given type according to JLS \S 4.5.5
399: */
400: protected Expression getDefaultValue(Type type) {
401: if (type instanceof PrimitiveType) {
402: return type.getDefaultValue();
403: }
404: return NullLiteral.NULL;
405: }
406:
407: /**
408: * returns the prepare method for arrays initialising all array fields with
409: * their default value
410: */
411: public ProgramMethod getPrepareArrayMethod(TypeRef arrayRef,
412: ProgramVariable length, Expression defaultValue,
413: ListOfField fields) {
414:
415: final KeYJavaType arrayType = arrayRef.getKeYJavaType();
416:
417: final IntLiteral zero = new IntLiteral(0);
418:
419: final LocalVariableDeclaration forInit = KeYJavaASTFactory
420: .declare(new ProgramElementName("i"), zero, integerType);
421:
422: final ProgramVariable pv = (ProgramVariable) forInit
423: .getVariables().getVariableSpecification(0)
424: .getProgramVariable();
425:
426: final For forLoop = new For(new LoopInitializer[] { forInit },
427: new LessThan(pv, new FieldReference(length,
428: new ThisReference())),
429: new Expression[] { new PostIncrement(pv) }, assign(
430: new ArrayReference(new ThisReference(),
431: new Expression[] { pv }), defaultValue));
432:
433: final StatementBlock body = new StatementBlock(
434: new Statement[] { forLoop });
435:
436: final MethodDeclaration md = new MethodDeclaration(
437: new Modifier[] { new Private() }, arrayRef,
438: new ProgramElementName(
439: PrepareObjectBuilder.IMPLICIT_OBJECT_PREPARE),
440: new ParameterDeclaration[0], null, body, false);
441:
442: final ProgramMethod result = new ProgramMethod(md, arrayType,
443: null, PositionInfo.UNDEFINED);
444:
445: return result;
446: }
447:
448: }
|