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 de.uka.ilkd.key.java.*;
020: import de.uka.ilkd.key.java.abstraction.ArrayType;
021: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
022: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
023: import de.uka.ilkd.key.java.expression.ArrayInitializer;
024: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
025: import de.uka.ilkd.key.java.expression.operator.NewArray;
026: import de.uka.ilkd.key.java.reference.ArrayReference;
027: import de.uka.ilkd.key.java.reference.ReferencePrefix;
028: import de.uka.ilkd.key.logic.ProgramElementName;
029: import de.uka.ilkd.key.logic.VariableNamer;
030: import de.uka.ilkd.key.logic.op.LocationVariable;
031: import de.uka.ilkd.key.logic.op.ProgramVariable;
032: import de.uka.ilkd.key.util.Debug;
033: import de.uka.ilkd.key.util.ExtList;
034:
035: /**
036: * Split an array creation expression with explicit array initializer,
037: * creating a creation expression with dimension expression and a list
038: * of assignments (-> Java language specification, 15.10)
039: */
040: public abstract class InitArray extends ProgramMetaConstruct {
041:
042: public InitArray(String name, ProgramElement body) {
043: super (name, body);
044: }
045:
046: /**
047: * Extract the variable initializers from the array initializer
048: */
049: protected ArrayOfExpression extractInitializers(
050: Expression p_creationExpression) {
051:
052: Debug.assertTrue(p_creationExpression instanceof NewArray,
053: "Don't know how to handle " + p_creationExpression);
054:
055: ArrayInitializer aInit = ((NewArray) p_creationExpression)
056: .getArrayInitializer();
057:
058: if (aInit == null)
059: // nothing to do for us
060: return null;
061:
062: return aInit.getArguments();
063: }
064:
065: protected KeYJavaType getElementType(Expression p_creationExpression) {
066: Debug.assertTrue(p_creationExpression instanceof NewArray,
067: "Don't know how to handle " + p_creationExpression);
068:
069: KeYJavaType aType = ((NewArray) p_creationExpression)
070: .getKeYJavaType();
071:
072: Debug.assertTrue(aType.getJavaType() instanceof ArrayType,
073: "Very strange are arrays of type "
074: + aType.getJavaType());
075:
076: return ((ArrayType) aType.getJavaType()).getBaseType()
077: .getKeYJavaType();
078: }
079:
080: /**
081: * Create an array creation expression for an array of the size
082: * given by the array initializer
083: */
084: protected Expression createArrayCreation(
085: Expression p_creationExpression) {
086:
087: ArrayOfExpression initializers = extractInitializers(p_creationExpression);
088:
089: if (initializers == null)
090: return p_creationExpression;
091:
092: KeYJavaType arrayType = ((NewArray) p_creationExpression)
093: .getKeYJavaType();
094:
095: ExtList children = new ExtList();
096: children.add(new IntLiteral(initializers.size()));
097: children.add(((NewArray) p_creationExpression)
098: .getTypeReference());
099:
100: return new NewArray(children, arrayType, null,
101: ((NewArray) p_creationExpression).getDimensions());
102: }
103:
104: /**
105: * The variable initializers have to be evaluated and assigned to
106: * temporary variables (the initializers may itself be array
107: * initializers, in which case valid creation expressions are
108: * created by inserting the new-operator)
109: */
110: protected ProgramVariable[] evaluateInitializers(
111: Statement[] p_stmnts, Expression p_creationExpression,
112: Services services) {
113:
114: ArrayOfExpression initializers = extractInitializers(p_creationExpression);
115:
116: if (initializers == null)
117: return new ProgramVariable[0];
118:
119: KeYJavaType elementType = getElementType(p_creationExpression);
120:
121: int i = initializers.size();
122: ProgramVariable[] res = new ProgramVariable[i];
123: VariableNamer varNamer = services.getVariableNamer();
124:
125: while (i-- != 0) {
126: ProgramElementName name = varNamer
127: .getTemporaryNameProposal("_tmpArray");
128: ProgramVariable var = new LocationVariable(name,
129: elementType);
130: p_stmnts[i] = KeYJavaASTFactory.declare(var, initializers
131: .getExpression(i), elementType);
132: res[i] = (ProgramVariable) ((LocalVariableDeclaration) p_stmnts[i])
133: .getVariables().getVariableSpecification(0)
134: .getProgramVariable();
135: }
136:
137: return res;
138: }
139:
140: /**
141: * Convert the variable initializers to assignments to the array
142: * elements (the initializers may itself be array initializers, in
143: * which case valid creation expressions are created by inserting
144: * the new-operator)
145: */
146: protected void createArrayAssignments(int p_start,
147: Statement[] p_statements, ProgramVariable[] p_initializers,
148: Expression p_array, Expression p_creationExpression) {
149:
150: if (p_initializers == null || p_initializers.length == 0) {
151: return;
152: }
153:
154: KeYJavaType elementType = p_initializers[0].getKeYJavaType();
155: ProgramElement baseType = ((NonTerminalProgramElement) p_creationExpression)
156: .getChildAt(0);
157:
158: int i = p_initializers.length;
159:
160: while (i-- != 0) {
161: p_statements[p_start + i] = createAssignment(p_array, i,
162: p_initializers[i], elementType, baseType);
163: }
164: }
165:
166: /**
167: * Convert one variable initializers to an assignment to the
168: * appropriate array element (the initializer may itself be an
169: * array initializer, in which case a valid creation expression is
170: * created by inserting the new-operator)
171: */
172: protected Statement createAssignment(Expression p_array,
173: int p_index, Expression p_initializer,
174: KeYJavaType p_elementType, ProgramElement p_baseType) {
175: if (p_initializer instanceof ArrayInitializer) {
176: Debug.assertTrue(
177: p_elementType.getJavaType() instanceof ArrayType,
178: "Very strange are arrays of type "
179: + p_elementType.getJavaType());
180:
181: ExtList children = new ExtList();
182: children.add(p_baseType);
183:
184: p_initializer = new NewArray(children, p_elementType,
185: (ArrayInitializer) p_initializer,
186: ((ArrayType) p_elementType.getJavaType())
187: .getDimension());
188: }
189:
190: Expression indexExpr = new IntLiteral(p_index);
191: Expression lhs = new ArrayReference((ReferencePrefix) p_array,
192: new Expression[] { indexExpr });
193:
194: return assign(lhs, p_initializer);
195: }
196: }
|