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.java.statement;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.reference.*;
016: import de.uka.ilkd.key.java.visitor.Visitor;
017: import de.uka.ilkd.key.logic.op.IProgramVariable;
018: import de.uka.ilkd.key.logic.op.ProgramMethod;
019: import de.uka.ilkd.key.util.ExtList;
020:
021: /**
022: * A shortcut-statement for a method body, i.e. no dynamic dispatching
023: * any longer.<p />
024: * Please take care:
025: * only the method name plus the class in which class the method
026: * is implemented is part of the syntax representation of such a
027: * statement, but not the methods complete syntax. If there are
028: * two methods with an equal name, but different signature (i.e.
029: * parameter types), the pure syntax is ambigious. In fact the concrete body
030: * this method body statement represents depends on the static type of
031: * its arguments. <p />
032: * Therefore: Transformation of a method body statement <em>MUST</em> keep
033: * the static type of the arguments <em>unchanged</em>.
034: * <p />
035: *
036: *
037: */
038: public class MethodBodyStatement extends JavaNonTerminalProgramElement
039: implements Statement, NonTerminalProgramElement {
040:
041: /**
042: * the variable the result of the method execution is assigned to
043: * if the method is declared void or the result not assigned to a
044: * variable or field, this value is null.
045: */
046: private final IProgramVariable resultVar;
047:
048: /**
049: * This type reference determines the class where the represented method
050: * has to be implemented.
051: */
052: private final TypeReference bodySource;
053:
054: /**
055: * the reference describing the method signature
056: */
057: private final MethodReference methodReference;
058:
059: /** cache resolved method */
060: private ProgramMethod method;
061:
062: /** indicates whether this stands for the specifiction of
063: * a method rather than the concrete body*/
064: private boolean useSpecification;
065:
066: /**
067: * Construct a method body shortcut
068: * @param bodySource exact class where the body is declared
069: * @param resultVar the IProgramVariable to which the method's return value is assigned
070: * @param methodReference the MethodReference encapsulating the method's signature
071: */
072: public MethodBodyStatement(TypeReference bodySource,
073: IProgramVariable resultVar, MethodReference methodReference) {
074: this .bodySource = bodySource;
075: this .resultVar = resultVar;
076: this .methodReference = methodReference;
077:
078: assert methodReference != null : "Missing methodreference";
079: assert methodReference.getReferencePrefix() != null : "Method reference of a method body statement needs an "
080: + "explicit reference prefix.";
081: }
082:
083: public MethodBodyStatement(ExtList list) {
084: this .bodySource = (TypeReference) list.get(TypeReference.class);
085: this .resultVar = (IProgramVariable) list
086: .get(IProgramVariable.class);
087:
088: this .methodReference = (MethodReference) list
089: .get(MethodReference.class);
090:
091: assert methodReference != null : "Missing methodreference";
092: assert methodReference.getReferencePrefix() != null : "Method reference of a method body statement needs an "
093: + "explicit reference prefix.";
094: }
095:
096: public MethodBodyStatement(ProgramMethod method,
097: ReferencePrefix newContext, IProgramVariable res,
098: ArrayOfExpression args, boolean useSpecification) {
099: this .method = method;
100: this .bodySource = new TypeRef(method.getContainerType());
101: this .resultVar = res;
102: this .useSpecification = useSpecification;
103:
104: if (newContext == null) {
105: if (method.isStatic()) {
106: newContext = bodySource;
107: } else {
108: throw new IllegalArgumentException(
109: "The invocation target of a method body"
110: + "statement must be non null");
111: }
112: }
113:
114: this .methodReference = new MethodReference(args, method
115: .getProgramElementName(), newContext);
116: }
117:
118: public MethodBodyStatement(ProgramMethod method,
119: ReferencePrefix newContext, IProgramVariable res,
120: ArrayOfExpression args) {
121: this (method, newContext, res, args, false);
122: }
123:
124: /**
125: * Get method body.
126: * @return the Statement
127: */
128: public Statement getBody(Services services) {
129: if (method == null) {
130: resolveMethod(services);
131: }
132: return method.getBody();
133: }
134:
135: /**
136: * Returns the number of children of this node.
137: * @return an int giving the number of children of this node
138: */
139: public int getChildCount() {
140: int i = 0;
141: if (bodySource != null)
142: i++;
143: if (resultVar != null)
144: i++;
145: if (methodReference != null)
146: i++;
147: return i;
148: }
149:
150: public ReferencePrefix getDesignatedContext() {
151: return methodReference.getReferencePrefix();
152: }
153:
154: public ArrayOfExpression getArguments() {
155: return methodReference.getArguments();
156: }
157:
158: /**
159: * Returns the child at the specified index in this node's "virtual"
160: * child array.
161: * @param index an index into this node's "virtual" child array
162: * @return the program element at the given position
163: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
164: * of bounds
165: */
166: public ProgramElement getChildAt(int index) {
167: if (bodySource != null) {
168: if (index == 0) {
169: return bodySource;
170: }
171: index--;
172: }
173:
174: if (resultVar != null) {
175: if (index == 0) {
176: return resultVar;
177: }
178: index--;
179: }
180:
181: if (methodReference != null) {
182: if (index == 0) {
183: return methodReference;
184: }
185: }
186:
187: throw new ArrayIndexOutOfBoundsException();
188: }
189:
190: public boolean isStatic(Services services) {
191: if (method == null) {
192: resolveMethod(services);
193: }
194: return method.isStatic();
195: }
196:
197: /** calls the corresponding method of a visitor in order to
198: * perform some action/transformation on this element
199: * @param v the Visitor
200: */
201: public void visit(Visitor v) {
202: v.performActionOnMethodBodyStatement(this );
203: }
204:
205: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
206: p.printMethodBodyStatement(this );
207: }
208:
209: public IProgramVariable getResultVariable() {
210: return resultVar;
211: }
212:
213: public KeYJavaType getBodySource() {
214: return bodySource.getKeYJavaType();
215: }
216:
217: public TypeReference getBodySourceAsTypeReference() {
218: return bodySource;
219: }
220:
221: public ProgramMethod getProgramMethod(Services services) {
222: if (method == null) {
223: resolveMethod(services);
224: }
225: return method;
226: }
227:
228: private void resolveMethod(Services services) {
229: method = services.getJavaInfo().getProgramMethod(
230: getBodySource(),
231: methodReference.getName(),
232: services.getJavaInfo().createSignature(
233: methodReference.getArguments()),
234: getBodySource());
235: }
236:
237: public String reuseSignature(Services services, ExecutionContext ec) {
238: return super .reuseSignature(services, ec) + "("
239: + getBodySource().getName() + ")";
240: }
241:
242: public MethodReference getMethodReference() {
243: return methodReference;
244: }
245:
246: public boolean replaceBySpecification() {
247: return useSpecification;
248: }
249:
250: }
|