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: /** This file represents a Java method in the logic. It is part of the
012: * AST of a java program
013: */package de.uka.ilkd.key.logic.op;
014:
015: import java.io.IOException;
016:
017: import de.uka.ilkd.key.java.*;
018: import de.uka.ilkd.key.java.abstraction.Constructor;
019: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
020: import de.uka.ilkd.key.java.annotation.Annotation;
021: import de.uka.ilkd.key.java.declaration.*;
022: import de.uka.ilkd.key.java.reference.MethodReference;
023: import de.uka.ilkd.key.java.reference.ReferencePrefix;
024: import de.uka.ilkd.key.java.reference.TypeRef;
025: import de.uka.ilkd.key.java.reference.TypeReference;
026: import de.uka.ilkd.key.java.visitor.Visitor;
027: import de.uka.ilkd.key.logic.ProgramElementName;
028: import de.uka.ilkd.key.logic.ProgramInLogic;
029: import de.uka.ilkd.key.logic.Term;
030: import de.uka.ilkd.key.logic.sort.Sort;
031: import de.uka.ilkd.key.proof.mgt.Contractable;
032: import de.uka.ilkd.key.rule.MatchConditions;
033: import de.uka.ilkd.key.util.Debug;
034: import de.uka.ilkd.key.util.ExtList;
035:
036: /**
037: * The program method represents a concrete method in the logic.
038: * In case of an instance method the first argument represents the
039: * object on which the method is invoked.
040: */
041: public class ProgramMethod extends NonRigidFunction implements
042: SourceElement, ProgramElement, MemberDeclaration,
043: ProgramInLogic, Contractable {
044:
045: private final MethodDeclaration method;
046: private final KeYJavaType kjt;
047: private final KeYJavaType contKJT;
048: private final PositionInfo pi;
049:
050: public ProgramMethod(MethodDeclaration method, KeYJavaType contKJT,
051: KeYJavaType kjt, PositionInfo pi) {
052: // for some reasons pm are created for void methods too. It's odd,
053: // but expand method body relies on a pm....
054: super (new ProgramElementName(method.getProgramElementName()
055: .toString(), contKJT.getSort().toString()),
056: kjt == null ? null : kjt.getSort(), getArgumentSorts(
057: method, contKJT));
058:
059: this .method = method;
060: this .contKJT = contKJT;
061: this .kjt = kjt;
062: this .pi = pi;
063:
064: }
065:
066: /**
067: * determines the argument sorts of the symbol to be created
068: * @param md the MethodDeclaration whose signature is used as blueprint
069: * @param container the KeYJavaType of the type where this method is declared
070: * @return the symbols argument sorts
071: */
072: private static Sort[] getArgumentSorts(MethodDeclaration md,
073: KeYJavaType container) {
074: final boolean instanceMethod = !md.isStatic()
075: && !(md instanceof Constructor);
076:
077: final int arity = instanceMethod ? md
078: .getParameterDeclarationCount() + 1 : md
079: .getParameterDeclarationCount();
080:
081: final Sort[] argSorts = new Sort[arity];
082:
083: final int offset;
084:
085: if (instanceMethod) {
086: argSorts[0] = container.getSort();
087: offset = 1;
088: } else {
089: offset = 0;
090: }
091:
092: for (int i = offset; i < argSorts.length; i++) {
093: argSorts[i] = md.getParameterDeclarationAt(i - offset)
094: .getTypeReference().getKeYJavaType().getSort();
095: }
096: return argSorts;
097: }
098:
099: /**
100: * BUG: remove this method bit first adopt the jml translation to take about the
101: * correct type of parameters and automatic type conversion
102: * @return true iff number of subterms of term is equal
103: * to its own arity
104: *
105: */
106: public boolean validTopLevel(Term term) {
107: return term.arity() == this .arity(); //%%% needs more checking!!!!
108: }
109:
110: // convienience methods to access methods of the corresponding MethodDeclaration
111: // in a direct way
112:
113: public MethodDeclaration getMethodDeclaration() {
114: return method;
115: }
116:
117: /**
118: * returns the KeYJavaType of the <tt>i</tt>-th paramter declaration. This method
119: * does not care about the invoker as argSort does.
120: * @param i the int specifying the parameter position
121: * @return the KeYJavaType of the <tt>i</tt>-th parameter
122: */
123: public KeYJavaType getParameterType(int i) {
124: return method.getParameterDeclarationAt(i).getTypeReference()
125: .getKeYJavaType();
126: }
127:
128: public StatementBlock getBody() {
129: return getMethodDeclaration().getBody();
130: }
131:
132: /** toString */
133: public String toString() {
134: return name().toString();
135: }
136:
137: public SourceElement getFirstElement() {
138: return method.getFirstElement();
139: }
140:
141: public SourceElement getLastElement() {
142: return method.getLastElement();
143: }
144:
145: public Comment[] getComments() {
146: return method.getComments();
147: }
148:
149: /**
150: *@return the annotations.
151: */
152: public Annotation[] getAnnotations() {
153: return new Annotation[0];
154: }
155:
156: public int getAnnotationCount() {
157: return 0;
158: }
159:
160: public void prettyPrint(PrettyPrinter w) throws IOException {
161: method.prettyPrint(w);
162: }
163:
164: /**
165: * calls the corresponding method of a visitor in order to
166: * perform some action/transformation on this element
167: * @param v the Visitor
168: */
169: public void visit(Visitor v) {
170: v.performActionOnProgramMethod(this );
171: }
172:
173: /**
174: * Returns the start position of the primary token of this element.
175: * To get the start position of the syntactical first token,
176: * call the corresponding method of <CODE>getFirstElement()</CODE>.
177: * @return the start position of the primary token.
178: */
179: public Position getStartPosition() {
180: return pi.getStartPosition();
181: }
182:
183: /**
184: * Returns the end position of the primary token of this element.
185: * To get the end position of the syntactical first token,
186: * call the corresponding method of <CODE>getLastElement()</CODE>.
187: * @return the end position of the primary token.
188: */
189: public Position getEndPosition() {
190: return pi.getEndPosition();
191: }
192:
193: /**
194: * Returns the relative position (number of blank heading lines and
195: * columns) of the primary token of this element.
196: * To get the relative position of the syntactical first token,
197: * call the corresponding method of <CODE>getFirstElement()</CODE>.
198: * @return the relative position of the primary token.
199: */
200: public Position getRelativePosition() {
201: return pi.getRelativePosition();
202: }
203:
204: public PositionInfo getPositionInfo() {
205: return pi;
206: }
207:
208: /**
209: * Test whether the declaration is private.
210: */
211: public boolean isPrivate() {
212: return method.isPrivate();
213: }
214:
215: /**
216: * Test whether the declaration is protected.
217: */
218: public boolean isProtected() {
219: return method.isProtected();
220: }
221:
222: /**
223: * Test whether the declaration is public.
224: */
225: public boolean isPublic() {
226: return method.isPublic();
227: }
228:
229: /**
230: * Test whether the declaration is static.
231: */
232: public boolean isStatic() {
233: return method.isStatic();
234: }
235:
236: /**
237: * Test whether the declaration is a constructor.
238: */
239: public boolean isConstructor() {
240: return method instanceof Constructor;
241: }
242:
243: /**
244: * Test whether the declaration is model.
245: */
246: public boolean isModel() {
247: return method.isModel();
248: }
249:
250: /**
251: * Test whether the declaration is strictfp.
252: */
253: public boolean isStrictFp() {
254: return method.isStrictFp();
255: }
256:
257: public ArrayOfModifier getModifiers() {
258: return method.getModifiers();
259: }
260:
261: public int getChildCount() {
262: return method.getChildCount();
263: }
264:
265: public ProgramElement getChildAt(int i) {
266: return method.getChildAt(i);
267: }
268:
269: /** equals modulo renaming is described in class
270: * SourceElement.
271: */
272: public boolean equalsModRenaming(SourceElement se,
273: NameAbstractionTable nat) {
274: if (se == null || !(se instanceof ProgramMethod)) {
275: return false;
276: }
277:
278: return method == ((ProgramMethod) se).getMethodDeclaration();
279: }
280:
281: public KeYJavaType getKeYJavaType() {
282: return kjt;
283: }
284:
285: public KeYJavaType getContainerType() {
286: return contKJT;
287: }
288:
289: public Expression convertToProgram(Term t, ExtList l) {
290: ProgramElement called;
291: if (isStatic()) {
292: called = new TypeRef(contKJT);
293: } else {
294: called = (ProgramElement) l.get(0);
295: l.remove(0);
296: }
297: return new MethodReference(l, getProgramElementName(),
298: (ReferencePrefix) called);
299: }
300:
301: public ProgramElementName getProgramElementName() {
302: return getMethodDeclaration().getProgramElementName();
303: }
304:
305: public String getFullName() {
306: return getMethodDeclaration().getFullName();
307: }
308:
309: public String getName() {
310: return getMethodDeclaration().getName();
311: }
312:
313: public boolean equalContractable(Contractable c) {
314: return equals(c)
315: && getContainerType().equals(
316: ((ProgramMethod) c).getContainerType());
317: }
318:
319: public boolean isAbstract() {
320: return getMethodDeclaration().isAbstract();
321: }
322:
323: public boolean isImplicit() {
324: return getName().startsWith("<");
325: }
326:
327: public boolean isNative() {
328: return getMethodDeclaration().isNative();
329: }
330:
331: public boolean isFinal() {
332: return getMethodDeclaration().isFinal();
333: }
334:
335: public boolean isSynchronized() {
336: return getMethodDeclaration().isSynchronized();
337: }
338:
339: public TypeReference getTypeReference() {
340: return getMethodDeclaration().getTypeReference();
341: }
342:
343: public Throws getThrown() {
344: return getMethodDeclaration().getThrown();
345: }
346:
347: public ParameterDeclaration getParameterDeclarationAt(int index) {
348: return getMethodDeclaration().getParameterDeclarationAt(index);
349: }
350:
351: /** returns the variablespecification of the i-th parameterdeclaration */
352: public VariableSpecification getVariableSpecification(int index) {
353: return method.getParameterDeclarationAt(index)
354: .getVariableSpecification();
355: }
356:
357: public int getParameterDeclarationCount() {
358: return getMethodDeclaration().getParameterDeclarationCount();
359: }
360:
361: public ArrayOfParameterDeclaration getParameters() {
362: return getMethodDeclaration().getParameters();
363: }
364:
365: public MatchConditions match(SourceData source,
366: MatchConditions matchCond) {
367: final ProgramElement src = source.getSource();
368: if (src == this ) {
369: source.next();
370: return matchCond;
371: } else {
372: Debug.out("Program match failed (pattern, source)", this,
373: src);
374: return null;
375: }
376: }
377: }
|