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.reference;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
016: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
017: import de.uka.ilkd.key.java.expression.ExpressionStatement;
018: import de.uka.ilkd.key.java.visitor.Visitor;
019: import de.uka.ilkd.key.logic.Name;
020: import de.uka.ilkd.key.logic.ProgramElementName;
021: import de.uka.ilkd.key.logic.op.ProgramMethod;
022: import de.uka.ilkd.key.logic.op.ProgramSV;
023: import de.uka.ilkd.key.logic.op.SortedSchemaVariable;
024: import de.uka.ilkd.key.util.Debug;
025: import de.uka.ilkd.key.util.ExtList;
026:
027: /**
028: * Method reference.
029: * @author <TT>AutoDoc</TT>
030: */
031: public class MethodReference extends JavaNonTerminalProgramElement
032: implements MemberReference, ReferencePrefix, ReferenceSuffix,
033: ExpressionStatement, TypeReferenceContainer, NameReference {
034:
035: /**
036: Access path.
037: */
038: protected final ReferencePrefix prefix;
039:
040: /**
041: * Name.
042: */
043: protected final MethodName name;
044:
045: /**
046: * Arguments.
047: */
048: protected final ArrayOfExpression arguments;
049:
050: public MethodReference(ArrayOfExpression args, MethodName n,
051: ReferencePrefix p) {
052: this .prefix = p;
053: name = n;
054: Debug.assertTrue(name != null,
055: "Tried to reference unnamed method.");
056: this .arguments = args;
057: }
058:
059: public MethodReference(ArrayOfExpression args, MethodName n,
060: ReferencePrefix p, PositionInfo pos) {
061: super (pos);
062: this .prefix = p;
063: name = n;
064: Debug.assertTrue(name != null,
065: "Tried to reference unnamed method.");
066: this .arguments = args;
067: }
068:
069: public MethodReference(ExtList children, MethodName n,
070: ReferencePrefix p) {
071: this (new ArrayOfExpression((Expression[]) children
072: .collect(Expression.class)), n, p,
073: (PositionInfo) children.get(PositionInfo.class));
074: }
075:
076: public MethodReference(ExtList children, MethodName n,
077: ReferencePrefix p, PositionInfo pos) {
078: this (new ArrayOfExpression((Expression[]) children
079: .collect(Expression.class)), n, p, pos);
080: }
081:
082: public SourceElement getFirstElement() {
083: return (prefix == null) ? getChildAt(0).getFirstElement()
084: : prefix.getFirstElement();
085: }
086:
087: /**
088: * Get reference prefix.
089: * @return the reference prefix.
090: */
091: public ReferencePrefix getReferencePrefix() {
092: return prefix;
093: }
094:
095: /**
096: * Returns the number of children of this node.
097: * @return an int giving the number of children of this node
098: */
099:
100: public int getChildCount() {
101: int result = 0;
102: if (prefix != null)
103: result++;
104: if (name != null)
105: result++;
106: if (arguments != null)
107: result += arguments.size();
108: return result;
109: }
110:
111: /**
112: * Returns the child at the specified index in this node's "virtual"
113: * child array
114: * @param index an index into this node's "virtual" child array
115: * @return the program element at the given position
116: * @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
117: * of bounds
118: */
119: public ProgramElement getChildAt(int index) {
120: if (prefix != null) {
121: if (index == 0)
122: return prefix;
123: index--;
124: }
125: if (name != null) {
126: if (index == 0)
127: return name;
128: index--;
129: }
130: if (arguments != null) {
131: return arguments.getExpression(index);
132: }
133: throw new ArrayIndexOutOfBoundsException();
134: }
135:
136: /**
137: * Get the number of type references in this container.
138: * @return the number of type references.
139: */
140: public int getTypeReferenceCount() {
141: return (prefix instanceof TypeReference) ? 1 : 0;
142: }
143:
144: /*
145: Return the type reference at the specified index in this node's
146: "virtual" type reference array.
147: @param index an index for a type reference.
148: @return the type reference with the given index.
149: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
150: of bounds.
151: */
152: public TypeReference getTypeReferenceAt(int index) {
153: if (prefix instanceof TypeReference && index == 0) {
154: return (TypeReference) prefix;
155: }
156: throw new ArrayIndexOutOfBoundsException();
157: }
158:
159: /**
160: * Get the number of expressions in this container.
161: * @return the number of expressions.
162: */
163: public int getExpressionCount() {
164: int result = 0;
165: if (prefix instanceof Expression)
166: result += 1;
167: if (arguments != null) {
168: result += arguments.size();
169: }
170: return result;
171: }
172:
173: /*
174: Return the expression at the specified index in this node's
175: "virtual" expression array.
176: @param index an index for an expression.
177: @return the expression with the given index.
178: @exception ArrayIndexOutOfBoundsException if <tt>index</tt> is out
179: of bounds.
180: */
181: public Expression getExpressionAt(int index) {
182: if (prefix instanceof Expression) {
183: if (index == 0) {
184: return (Expression) prefix;
185: }
186: index -= 1;
187: }
188: if (arguments != null) {
189: return arguments.getExpression(index);
190: }
191: throw new ArrayIndexOutOfBoundsException();
192: }
193:
194: /**
195: * Get name.
196: * @return the string.
197: */
198: public final String getName() {
199: return (name == null) ? null : name.toString();
200: }
201:
202: /**
203: * Get identifier.
204: * @return the identifier.
205: */
206: public ProgramElementName getProgramElementName() {
207: if (name instanceof ProgramElementName) {
208: return (ProgramElementName) name;
209: } else if (name instanceof SortedSchemaVariable) {
210: return (((ProgramSV) name).getProgramElementName());
211: } else
212: return null;
213: }
214:
215: /**
216: * Get arguments.
217: * @return the expression array wrapper.
218: */
219: public ArrayOfExpression getArguments() {
220: return arguments;
221: }
222:
223: /**
224: * Gets index-th argument
225: * @return the expression
226: */
227: public Expression getArgumentAt(int index) {
228: if (arguments != null) {
229: return arguments.getExpression(index);
230: }
231: throw new ArrayIndexOutOfBoundsException();
232: }
233:
234: /**
235: * determines the arguments types and constructs a signature of the current
236: * method
237: */
238: public ListOfKeYJavaType getMethodSignature(Services services,
239: ExecutionContext ec) {
240: ListOfKeYJavaType signature = SLListOfKeYJavaType.EMPTY_LIST;
241: if (arguments != null) {
242: final TypeConverter typeConverter = services
243: .getTypeConverter();
244: for (int i = arguments.size() - 1; i >= 0; i--) {
245: signature = signature.prepend(typeConverter
246: .getKeYJavaType(getArgumentAt(i), ec));
247: }
248: }
249: return signature;
250: }
251:
252: /**
253: * returns the static KeYJavaType of the methods prefix
254: */
255: public KeYJavaType determineStaticPrefixType(Services services,
256: ExecutionContext ec) {
257: KeYJavaType prefixType;
258: if (prefix == null) {
259: prefixType = ec.getTypeReference().getKeYJavaType();
260: } else {
261: if (prefix instanceof Expression) {
262: prefixType = ((Expression) prefix).getKeYJavaType(
263: services, ec);
264: } else {
265: prefixType = ((TypeReference) prefix).getKeYJavaType();
266: }
267: }
268: return prefixType;
269: }
270:
271: public ProgramMethod method(Services services,
272: KeYJavaType refPrefixType, ExecutionContext ec) {
273:
274: return method(services, refPrefixType, getMethodSignature(
275: services, ec), ec.getTypeReference().getKeYJavaType());
276: }
277:
278: /**
279: *
280: * @param services the Services class offering access to metamodel
281: * information
282: * @param classType the KeYJavaType where to start looking for the
283: * declared method
284: * @param signature the ListOfKeYJavaType of the arguments types
285: * @param context the KeYJavaType from where the method is called
286: * @return the found program method
287: */
288: public ProgramMethod method(Services services,
289: KeYJavaType classType, ListOfKeYJavaType signature,
290: KeYJavaType context) {
291: final String methodName = name.toString();
292: ProgramMethod pm = services.getJavaInfo().getProgramMethod(
293: classType, methodName, signature, context);
294: if (pm == null) {
295: pm = services.getImplementation2SpecMap()
296: .lookupModelMethod(classType, new Name(methodName));
297: }
298: return pm;
299: }
300:
301: public boolean implicit() {
302: return getProgramElementName().toString().charAt(0) == '<';
303: }
304:
305: public MethodName getMethodName() {
306: return name;
307: }
308:
309: /** calls the corresponding method of a visitor in order to
310: * perform some action/transformation on this element
311: * @param v the Visitor
312: */
313: public void visit(Visitor v) {
314: v.performActionOnMethodReference(this );
315: }
316:
317: public void prettyPrint(PrettyPrinter p) throws java.io.IOException {
318: p.printMethodReference(this );
319: }
320:
321: public KeYJavaType getKeYJavaType(Services services,
322: ExecutionContext ec) {
323: return method(services,
324: determineStaticPrefixType(services, ec), ec)
325: .getKeYJavaType();
326:
327: }
328:
329: public KeYJavaType getKeYJavaType(Services javaServ) {
330: return getKeYJavaType();
331: }
332:
333: public KeYJavaType getKeYJavaType() {
334: Debug.fail("");
335: return null;
336: }
337:
338: }
|