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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016:
017: package de.uka.ilkd.key.rule.metaconstruct;
018:
019: import java.util.LinkedList;
020:
021: import de.uka.ilkd.key.java.*;
022: import de.uka.ilkd.key.java.abstraction.ArrayType;
023: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
024: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
025: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
026: import de.uka.ilkd.key.java.expression.ArrayInitializer;
027: import de.uka.ilkd.key.java.expression.literal.BooleanLiteral;
028: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
029: import de.uka.ilkd.key.java.expression.operator.*;
030: import de.uka.ilkd.key.java.reference.*;
031: import de.uka.ilkd.key.java.statement.For;
032: import de.uka.ilkd.key.java.statement.If;
033: import de.uka.ilkd.key.java.statement.Then;
034: import de.uka.ilkd.key.java.statement.Throw;
035: import de.uka.ilkd.key.logic.ProgramElementName;
036: import de.uka.ilkd.key.logic.VariableNamer;
037: import de.uka.ilkd.key.logic.op.LocationVariable;
038: import de.uka.ilkd.key.logic.op.ProgramVariable;
039: import de.uka.ilkd.key.logic.op.SchemaVariable;
040: import de.uka.ilkd.key.rule.inst.SVInstantiations;
041:
042: /**
043: * Split an array creation expression with explicit array initializer,
044: * creating a creation expression with dimension expression and a list
045: * of assignments (-> Java language specification, 15.10)
046: *
047: * This meta construct delivers the creation expression
048: */
049: public class InitArrayCreation extends InitArray {
050:
051: private final SchemaVariable newObjectSV;
052: private String createArrayName = "<createArray>";
053:
054: public InitArrayCreation(SchemaVariable newObjectSV,
055: ProgramElement newExpr) {
056: super ("init-array-creation", newExpr);
057: this .newObjectSV = newObjectSV;
058: }
059:
060: public InitArrayCreation(SchemaVariable newObjectSV,
061: ProgramElement newExpr, boolean transientArray) {
062: super ("init-array-creation", newExpr);
063: this .newObjectSV = newObjectSV;
064: if (transientArray)
065: this .createArrayName = "<createTransientArray>";
066: }
067:
068: /**
069: * trying to create an array of negative length causes a
070: * {@link java.lang.NegativeArraySizeException} to be thrown. The if
071: * statement implementing this behaviour is created by this method.
072: * @param cond the Expression representing the guard checking if the
073: * given length is negative or not
074: * @param services the Services offering access to the type model
075: * @return an if statement throwing a NegativeArraySizeException if
076: * cond is evaluated to false
077: */
078: private If checkNegativeDimension(Expression cond, Services services) {
079: final Then then = new Then(
080: new Throw(
081: new New(
082: new Expression[0],
083: new TypeRef(
084: services
085: .getJavaInfo()
086: .getKeYJavaType(
087: "java.lang.NegativeArraySizeException")),
088: null)));
089:
090: return new If(cond, then);
091: }
092:
093: /**
094: * creates statements for
095: * <ol>
096: * <li> evaluation of the dimension expressions, <li>
097: * <li> check if a dimension is non-negative </li>
098: * </ol>
099: * and adds them to given list of statements. Further more the new
100: * declared program variables initialised with the evaluated
101: * dimension expressions are returned
102: * @param bodyStmnts the LinkedList of statements where the new
103: * statements are inserted
104: * @param dimExpr the ArrayOfExpression which describe the array's
105: * dimensions
106: * @param services the Services object
107: */
108: private ProgramVariable[] evaluateAndCheckDimensionExpressions(
109: LinkedList bodyStmnts, ArrayOfExpression dimExpr,
110: Services services) {
111:
112: Expression checkDimensions = BooleanLiteral.FALSE;
113: ProgramVariable[] pvars = new ProgramVariable[dimExpr.size()];
114: final VariableNamer varNamer = services.getVariableNamer();
115: final KeYJavaType intType = services.getJavaInfo()
116: .getKeYJavaType(PrimitiveType.JAVA_INT);
117:
118: for (int i = 0; i < pvars.length; i++) {
119: final ProgramElementName name = varNamer
120: .getTemporaryNameProposal("dim" + i);
121:
122: final LocalVariableDeclaration argDecl = KeYJavaASTFactory
123: .declare(name, dimExpr.getExpression(i), intType);
124: pvars[i] = (ProgramVariable) argDecl.getVariables()
125: .getVariableSpecification(0).getProgramVariable();
126:
127: bodyStmnts.add(argDecl);
128: final LessThan negativeDimension = new LessThan(pvars[i],
129: new IntLiteral(0));
130: if (i == 0) {
131: checkDimensions = negativeDimension;
132: } else {
133: checkDimensions = new LogicalOr(checkDimensions,
134: negativeDimension);
135: }
136: }
137:
138: bodyStmnts
139: .add(checkNegativeDimension(checkDimensions, services));
140:
141: return pvars;
142: }
143:
144: /**
145: * creates an array of dimension <code>dimensions.length</code>
146: */
147: private void createNDimensionalArray(LinkedList bodyStmnts,
148: Expression resultVar, KeYJavaType arrayType,
149: ProgramVariable[] dimensions, Services services) {
150: bodyStmnts.add(assign(resultVar, new MethodReference(
151: new ArrayOfExpression(dimensions[0]),
152: new ProgramElementName(createArrayName), new TypeRef(
153: arrayType))));
154:
155: if (dimensions.length > 1) {
156: Expression[] baseDim = new Expression[dimensions.length - 1];
157: System.arraycopy(dimensions, 1, baseDim, 0,
158: dimensions.length - 1);
159: final VariableNamer varNamer = services.getVariableNamer();
160: final KeYJavaType intType = services.getJavaInfo()
161: .getKeYJavaType(PrimitiveType.JAVA_INT);
162: final ProgramElementName name = varNamer
163: .getTemporaryNameProposal("i");
164: final ProgramVariable var = new LocationVariable(name,
165: intType);
166: final LocalVariableDeclaration forInit = KeYJavaASTFactory
167: .declare(var, new IntLiteral(0), intType);
168:
169: final ProgramVariable pv = (ProgramVariable) forInit
170: .getVariables().getVariableSpecification(0)
171: .getProgramVariable();
172:
173: TypeReference baseTypeRef = ((ArrayType) arrayType
174: .getJavaType()).getBaseType();
175:
176: KeYJavaType baseType = baseTypeRef.getKeYJavaType();
177:
178: for (int i = 0; i < dimensions.length - 1; i++) {
179: baseTypeRef = ((ArrayType) baseType.getJavaType())
180: .getBaseType();
181: baseType = baseTypeRef.getKeYJavaType();
182: }
183:
184: final For forLoop = new For(
185: new LoopInitializer[] { forInit },
186: new LessThan(pv, dimensions[0]),
187: new Expression[] { new PostIncrement(pv) },
188: assign(
189: new ArrayReference(
190: (ReferencePrefix) resultVar,
191: new Expression[] { pv }),
192: new NewArray(
193: baseDim,
194: baseTypeRef,
195: baseType,
196: null,
197: (baseType.getJavaType() instanceof ArrayType) ? ((ArrayType) baseType
198: .getJavaType())
199: .getDimension()
200: : 0)));
201:
202: bodyStmnts.add(forLoop);
203: }
204:
205: }
206:
207: private void createOneDimensionalArrayTransient(
208: LinkedList bodyStmnts, Expression resultVar,
209: KeYJavaType arrayType, ProgramVariable[] dimensions,
210: Expression transientType, Services services) {
211: bodyStmnts.add(assign(resultVar, new MethodReference(
212: new ArrayOfExpression(new Expression[] { dimensions[0],
213: transientType }), new ProgramElementName(
214: createArrayName), new TypeRef(arrayType))));
215: }
216:
217: /**
218: * executes an array creation without initializers involved
219: */
220: private ProgramElement arrayCreationWithoutInitializers(
221: Expression newObject, NewArray na, Services services) {
222:
223: final LinkedList bodyStmnts = new LinkedList();
224:
225: final ProgramVariable[] dimensions = evaluateAndCheckDimensionExpressions(
226: bodyStmnts, na.getArguments(), services);
227:
228: final KeYJavaType arrayType = na.getKeYJavaType(services);
229:
230: createNDimensionalArray(bodyStmnts, newObject, arrayType,
231: dimensions, services);
232:
233: return new StatementBlock((Statement[]) bodyStmnts
234: .toArray(new Statement[bodyStmnts.size()]));
235:
236: }
237:
238: /**
239: * executes an array creation without initializers involved
240: */
241: private ProgramElement arrayCreationTransient(Expression newObject,
242: MethodReference mref, Services services, ExecutionContext ec) {
243:
244: LinkedList bodyStmnts = new LinkedList();
245:
246: ProgramVariable[] dimensions = evaluateAndCheckDimensionExpressions(
247: bodyStmnts, new ArrayOfExpression(
248: new Expression[] { mref.getArgumentAt(0) }),
249: services);
250:
251: createOneDimensionalArrayTransient(bodyStmnts, newObject, mref
252: .getKeYJavaType(services, ec), dimensions, mref
253: .getArgumentAt(1), services);
254:
255: return new StatementBlock((Statement[]) bodyStmnts
256: .toArray(new Statement[bodyStmnts.size()]));
257:
258: }
259:
260: public ProgramElement symbolicExecution(ProgramElement pe,
261: Services services, SVInstantiations svInst) {
262:
263: final Expression array = (Expression) svInst
264: .getInstantiation(newObjectSV);
265:
266: NewArray na = null;
267:
268: if (pe instanceof MethodReference
269: && ((MethodReference) pe).getName().toString()
270: .startsWith("jvmMakeTransient")) {
271: return arrayCreationTransient(array, (MethodReference) pe,
272: services, svInst.getExecutionContext());
273: } else if (pe instanceof NewArray) {
274: na = (NewArray) pe;
275: if (na.getArrayInitializer() == null) {
276: return arrayCreationWithoutInitializers(array, na,
277: services);
278: }
279: } else if (pe instanceof ArrayInitializer) {
280: final KeYJavaType kjt = array.getKeYJavaType(services,
281: svInst.getExecutionContext());
282: na = new NewArray(new Expression[0], ((ArrayType) kjt
283: .getJavaType()).getBaseType(), kjt,
284: (ArrayInitializer) pe, 0);
285: } else {
286: return pe;
287: }
288:
289: final int arrayLength = na.getArrayInitializer().getArguments()
290: .size();
291:
292: final Statement[] body = new Statement[2 * arrayLength + 1];
293: final ProgramVariable[] vars = evaluateInitializers(body, na,
294: services);
295:
296: body[arrayLength] = assign(array, createArrayCreation(na));
297:
298: createArrayAssignments(arrayLength + 1, body, vars, array, na);
299:
300: return new StatementBlock(body);
301: }
302:
303: }
|