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: package de.uka.ilkd.key.rule.metaconstruct;
011:
012: import de.uka.ilkd.key.java.*;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
016: import de.uka.ilkd.key.java.abstraction.Type;
017: import de.uka.ilkd.key.java.abstraction.ClassType;
018: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
019: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
020: import de.uka.ilkd.key.java.declaration.ParameterDeclaration;
021: import de.uka.ilkd.key.java.declaration.VariableSpecification;
022: import de.uka.ilkd.key.java.expression.operator.Instanceof;
023: import de.uka.ilkd.key.java.reference.*;
024: import de.uka.ilkd.key.java.statement.Else;
025: import de.uka.ilkd.key.java.statement.If;
026: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
027: import de.uka.ilkd.key.java.statement.Then;
028: import de.uka.ilkd.key.logic.Name;
029: import de.uka.ilkd.key.logic.ProgramElementName;
030: import de.uka.ilkd.key.logic.VariableNamer;
031: import de.uka.ilkd.key.logic.op.*;
032: import de.uka.ilkd.key.rule.inst.SVInstantiations;
033: import de.uka.ilkd.key.util.Debug;
034:
035: /**
036: * Symbolically executes a method invocation
037: */
038: public class MethodCall extends ProgramMetaConstruct {
039:
040: private final SchemaVariable resultVar;
041:
042: protected MethodReference methRef;
043: private ProgramMethod pm;
044: protected ReferencePrefix newContext;
045: private Services services;
046: protected ProgramVariable pvar;
047: private IExecutionContext execContextSV;
048: private ExecutionContext execContext;
049: protected ArrayOfExpression arguments;
050: protected KeYJavaType staticPrefixType;
051:
052: /** creates the methodcall-MetaConstruct
053: * @param body the ProgramElement contained by the meta construct
054: */
055: public MethodCall(ProgramElement body) {
056: this (null, null, body);
057: }
058:
059: /** creates the methodcall-MetaConstruct
060: * @param result the SchemaVariable that is used to keep the result
061: * @param body the ProgramElement contained by the meta construct
062: */
063: public MethodCall(SchemaVariable result, ProgramElement body) {
064: this (null, result, body);
065: }
066:
067: /** creates the methodcall-MetaConstruct
068: * @param result the SchemaVariable that is used to keep the result
069: * @param body the ProgramElement contained by the meta construct
070: */
071: public MethodCall(ProgramSV ec, SchemaVariable result,
072: ProgramElement body) {
073: this (new Name("method-call"), ec, result, body);
074: }
075:
076: /** creates the methodcall-MetaConstruct
077: * @param result the SchemaVariable that is used to keep the result
078: * @param body the ProgramElement contained by the meta construct
079: */
080: protected MethodCall(Name name, ProgramSV ec,
081: SchemaVariable result, ProgramElement body) {
082: super (name, body);
083: this .resultVar = result;
084: this .execContextSV = ec;
085: }
086:
087: /** gets an array of expression and returns a list of types */
088: private ListOfKeYJavaType getTypes(ArrayOfExpression args) {
089: ListOfKeYJavaType result = SLListOfKeYJavaType.EMPTY_LIST;
090: for (int i = args.size() - 1; i >= 0; i--) {
091: Expression argument = args.getExpression(i);
092: result = result.prepend(services.getTypeConverter()
093: .getKeYJavaType(argument, execContext));
094: }
095: return result;
096: }
097:
098: private ProgramMethod assertImplementationPresent(
099: ProgramMethod method, KeYJavaType t) {
100: if (method == null) {
101: Debug.fail("methodcall:No implementation available for ",
102: method);
103: }
104: return method;
105: }
106:
107: private KeYJavaType getStaticPrefixType(ReferencePrefix refPrefix) {
108: if (refPrefix == null || refPrefix instanceof ThisReference) {
109: return execContext.getTypeReference().getKeYJavaType();
110: } else if (refPrefix instanceof TypeRef) {
111: KeYJavaType t = ((TypeRef) refPrefix).getKeYJavaType();
112: if (t == null) { //%%%
113: Debug.fail();
114: }
115: return t;
116: } else if (refPrefix instanceof ProgramVariable) {
117: return ((ProgramVariable) refPrefix).getKeYJavaType();
118: } else if (refPrefix instanceof FieldReference) {
119: return ((FieldReference) refPrefix).getProgramVariable()
120: .getKeYJavaType();
121: } else if (refPrefix instanceof SuperReference) {
122: return services.getJavaInfo().getSuperclass(
123: execContext.getTypeReference().getKeYJavaType());
124: } else {
125: throw new de.uka.ilkd.key.util.NotSupported(
126: "Unsupported method invocation mode\n"
127: + refPrefix.getClass());
128: }
129: }
130:
131: protected ProgramMethod getMethod(KeYJavaType prefixType,
132: MethodReference mr) {
133: ProgramMethod result;
134: if (execContext != null) {
135: result = mr.method(services, prefixType, execContext);
136: if (result == null) {
137: // if a method is declared protected and prefix and
138: // execContext are in different packages we have to
139: // simulate visibility rules like being in prefixType
140: result = mr.method(services, prefixType, mr
141: .getMethodSignature(services, execContext),
142: prefixType);
143: }
144: } else {
145: result = mr.method(services, prefixType, mr
146: .getMethodSignature(services, execContext),
147: prefixType);
148: }
149: return result;
150: }
151:
152: private ProgramMethod getSuperMethod(ExecutionContext ex,
153: MethodReference mr) {
154: return mr.method(services, getSuperType(ex), ex);
155: }
156:
157: private KeYJavaType getSuperType(ExecutionContext ex) {
158: return services.getJavaInfo().getSuperclass(
159: ex.getTypeReference().getKeYJavaType());
160: }
161:
162: /** performs the program transformation needed for symbolic
163: * program execution
164: * @param services the Services with all necessary information
165: * about the java programs
166: * @param svInst the instantiations esp. of the inner and outer label
167: * @return the transformed program
168: */
169: public ProgramElement symbolicExecution(ProgramElement pe,
170: Services services, SVInstantiations svInst) {
171:
172: Debug.out("method-call: called for ", pe);
173: this .services = services;
174:
175: if (resultVar != null) {
176: pvar = (ProgramVariable) svInst.getInstantiation(resultVar);
177: }
178:
179: if (execContextSV != null) {
180: execContext = (ExecutionContext) svInst
181: .getInstantiation((SortedSchemaVariable) execContextSV);
182: } else {
183: execContext = svInst.getContextInstantiation()
184: .activeStatementContext();
185: }
186:
187: methRef = (MethodReference) pe;
188:
189: ReferencePrefix refPrefix = methRef.getReferencePrefix();
190: if (refPrefix == null) {
191: if (execContext.getRuntimeInstance() == null) {
192: refPrefix = execContext.getTypeReference();
193: } else {
194: refPrefix = execContext.getRuntimeInstance();
195: }
196: }
197:
198: staticPrefixType = getStaticPrefixType(methRef
199: .getReferencePrefix());
200: if (execContext != null) {
201: pm = assertImplementationPresent(methRef.method(services,
202: staticPrefixType, execContext), staticPrefixType);
203: } else {
204: pm = assertImplementationPresent(methRef.method(services,
205: staticPrefixType, methRef.getMethodSignature(
206: services, null), staticPrefixType),
207: staticPrefixType);
208: }
209: newContext = methRef.getReferencePrefix();
210: if (newContext == null || newContext instanceof ThisReference) {
211: newContext = execContext.getRuntimeInstance();
212: } else if (newContext instanceof FieldReference) {
213: final FieldReference fieldContext = (FieldReference) newContext;
214: if (fieldContext.referencesOwnInstanceField())
215: newContext = fieldContext
216: .setReferencePrefix(execContext
217: .getRuntimeInstance());
218: }
219:
220: VariableSpecification[] paramSpecs = createParamSpecs();
221: Statement[] paramDecl = createParamAssignments(paramSpecs);
222:
223: arguments = getVariables(paramSpecs);
224:
225: Statement result = null;
226:
227: if (pm.isStatic()) { // Static invocation mode
228: Debug
229: .out("method-call: invocation of static method detected");
230: newContext = null;
231: ProgramMethod staticMethod = getMethod(staticPrefixType,
232: methRef);
233: result = new MethodBodyStatement(staticMethod, newContext,
234: pvar, arguments);
235: } else if (refPrefix instanceof SuperReference) {
236: Debug
237: .out("method-call: super invocation of method detected."
238: + "Requires static resolving.");
239: ProgramMethod super Method = getSuperMethod(execContext,
240: methRef);
241: result = new MethodBodyStatement(super Method, execContext
242: .getRuntimeInstance(), pvar, arguments);
243: } else { // Instance invocation mode
244: if (pm.isPrivate()) { // private methods are bound statically
245: Debug
246: .out("method-call: invocation of private method detected."
247: + "Requires static resolving.");
248: result = makeMbs(staticPrefixType);
249: } else {
250: Debug.out("method-call: invocation of non-private"
251: + " instance method detected."
252: + "Requires dynamic resolving.");
253: ListOfKeYJavaType imps = services.getJavaInfo()
254: .getKeYProgModelInfo().findImplementations(
255: staticPrefixType, methRef.getName(),
256: getTypes(arguments));
257:
258: if (imps == SLListOfKeYJavaType.EMPTY_LIST) {
259: imps = services.getImplementation2SpecMap()
260: .findSpecifications(methRef.getName(),
261: staticPrefixType);
262: }
263: if (imps.isEmpty()) {
264: Type staticPrefix = staticPrefixType.getJavaType();
265: if (staticPrefix instanceof ClassType
266: && (((ClassType) staticPrefix)
267: .isInterface() || ((ClassType) staticPrefix)
268: .isAbstract())) {
269: // no implementing sub type found
270: // insert mbs with interface type so that contracts are applicable
271: result = makeMbs(staticPrefixType);
272: }
273: } else {
274: result = makeIfCascade(imps);
275: }
276: }
277: }
278: return KeYJavaASTFactory.insertStatementInBlock(paramDecl,
279: new StatementBlock(result));
280: }
281:
282: //***************** Dynamic Binding Construction Utilities ***************
283:
284: private Statement makeMbs(KeYJavaType t) {
285: ProgramMethod meth = getMethod(t, methRef);
286: return new MethodBodyStatement(meth, newContext, pvar,
287: arguments);
288: }
289:
290: public Expression makeIOf(Type t) {
291: Debug.assertTrue(newContext != null);
292: return new Instanceof((Expression) newContext, new TypeRef(
293: (KeYJavaType) t));
294: }
295:
296: protected Statement makeIfCascade(ListOfKeYJavaType imps) {
297: KeYJavaType currType = imps.head();
298: if (imps.size() == 1)
299: return makeMbs(currType);
300: else
301: return new If(makeIOf(currType),
302: new Then(makeMbs(currType)), new Else(
303: makeIfCascade(imps.tail())));
304: }
305:
306: public VariableSpecification[] createParamSpecs() {
307:
308: MethodDeclaration methDecl = pm.getMethodDeclaration();
309: int params = methDecl.getParameterDeclarationCount();
310: VariableSpecification[] varSpecs = new VariableSpecification[params];
311: for (int i = 0; i < params; i++) {
312: ParameterDeclaration parDecl = methDecl
313: .getParameterDeclarationAt(i);
314: VariableSpecification originalSpec = parDecl
315: .getVariableSpecification();
316: final ProgramVariable originalParamVar = (ProgramVariable) originalSpec
317: .getProgramVariable();
318:
319: VariableNamer varNamer = services.getVariableNamer();
320: ProgramElementName newName = varNamer
321: .getTemporaryNameProposal(originalParamVar
322: .getProgramElementName().toString());
323:
324: final IProgramVariable paramVar = new LocationVariable(
325: newName, originalParamVar.getKeYJavaType());
326:
327: varSpecs[i] = new VariableSpecification(paramVar,
328: originalSpec.getDimensions(), methRef
329: .getArgumentAt(i), originalSpec.getType());
330: }
331: return varSpecs;
332: }
333:
334: public Statement[] createParamAssignments(
335: VariableSpecification[] specs) {
336: MethodDeclaration methDecl = pm.getMethodDeclaration();
337: Statement[] paramDecl = new Statement[specs.length];
338: for (int i = 0; i < specs.length; i++) {
339: ParameterDeclaration parDecl = methDecl
340: .getParameterDeclarationAt(i);
341: paramDecl[i] = new LocalVariableDeclaration(parDecl
342: .getModifiers(), parDecl.getTypeReference(),
343: specs[i]);
344: }
345: return paramDecl;
346: }
347:
348: private ArrayOfExpression getVariables(
349: VariableSpecification[] varspecs) {
350: Expression[] vars = new Expression[varspecs.length];
351: for (int i = 0; i < varspecs.length; i++) {
352: vars[i] = (Expression) varspecs[i].getProgramVariable();
353: }
354: return new ArrayOfExpression(vars);
355: }
356:
357: }
|