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: package de.uka.ilkd.key.rule.metaconstruct;
017:
018: import java.util.ArrayList;
019:
020: import de.uka.ilkd.key.java.*;
021: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
022: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
023: import de.uka.ilkd.key.java.expression.operator.New;
024: import de.uka.ilkd.key.java.reference.ExecutionContext;
025: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
026: import de.uka.ilkd.key.logic.Name;
027: import de.uka.ilkd.key.logic.op.ProgramMethod;
028: import de.uka.ilkd.key.logic.op.ProgramVariable;
029: import de.uka.ilkd.key.logic.op.SchemaVariable;
030: import de.uka.ilkd.key.rule.inst.SVInstantiations;
031: import de.uka.ilkd.key.util.Debug;
032:
033: /**
034: * The constructor call meta construct is used to handle a allocation expression
035: * like <code>new Class(...)</code>. Thereby it replaces the allocation
036: * expression by a method reference to an implict method called
037: * <code><init></code> that is mainly the constructor but in its
038: * normalform.
039: */
040: public class ConstructorCall extends ProgramMetaConstruct {
041:
042: private static final String NORMALFORM_IDENTIFIER = de.uka.ilkd.key.java.recoderext.ConstructorNormalformBuilder.CONSTRUCTOR_NORMALFORM_IDENTIFIER;
043:
044: private final SchemaVariable newObjectSV;
045:
046: /**
047: * creates the metaconstruct
048: */
049: public ConstructorCall(SchemaVariable newObjectSV,
050: ProgramElement consRef) {
051: super (new Name("constructor-call"), consRef);
052: this .newObjectSV = newObjectSV;
053: }
054:
055: /**
056: * transforms the constructor's body into its normalform and
057: * returns the result. Thereby all necessary references are
058: * resolved.
059: *
060: * The method is optimized in the sense that insetad of returning
061: * <code>newObject.<init>(args);</code>
062: * a statementblock is returned which evaluates the constructor's arguments
063: * and inserts a method body statement rather than the method call which avoids
064: * unneccessary proof branches. As <code>newObject</code> can never be
065: * <code>null</code> no null pointer scheck is necessary.
066: */
067: public ProgramElement symbolicExecution(ProgramElement pe,
068: Services services, SVInstantiations svInst) {
069:
070: New constructorReference = (New) pe;
071: ProgramVariable newObject = (ProgramVariable) svInst
072: .getInstantiation(newObjectSV);
073: KeYJavaType classType = constructorReference.getTypeReference()
074: .getKeYJavaType();
075:
076: final ExecutionContext ec = svInst.getExecutionContext();
077:
078: if (!(classType.getJavaType() instanceof ClassDeclaration)) {
079: // no implementation available
080: return pe;
081: }
082:
083: final ArrayOfExpression arguments = constructorReference
084: .getArguments();
085:
086: final ArrayList evaluatedArgs = new ArrayList();
087:
088: final ProgramVariable[] argumentVariables = new ProgramVariable[arguments
089: .size()];
090:
091: for (int i = 0, sz = arguments.size(); i < sz; i++) {
092: argumentVariables[i] = EvaluateArgs.evaluate(arguments
093: .getExpression(i), evaluatedArgs, services, svInst
094: .getExecutionContext());
095: }
096:
097: final ProgramMethod method = services.getJavaInfo()
098: .getProgramMethod(classType, NORMALFORM_IDENTIFIER,
099: (ProgramVariable[]) argumentVariables,
100: ec.getTypeReference().getKeYJavaType());
101:
102: Debug.assertTrue(method != null,
103: "Call to non-existant constructor.");
104:
105: final MethodBodyStatement mbs = new MethodBodyStatement(method,
106: newObject, null, new ArrayOfExpression(
107: argumentVariables));
108:
109: // the assignment statements + the method body statement
110: final Statement[] stmnts = new Statement[evaluatedArgs.size() + 1];
111:
112: for (int i = 0, sz = evaluatedArgs.size(); i < sz; i++) {
113: stmnts[i] = (Statement) evaluatedArgs.get(i);
114: }
115:
116: stmnts[stmnts.length - 1] = mbs;
117:
118: return new StatementBlock(stmnts);
119:
120: }
121:
122: }
|