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.java;
011:
012: import java.util.*;
013:
014: import de.uka.ilkd.key.java.abstraction.*;
015: import de.uka.ilkd.key.java.declaration.*;
016: import de.uka.ilkd.key.java.recoderext.KeYCrossReferenceServiceConfiguration;
017: import de.uka.ilkd.key.java.reference.TypeRef;
018: import de.uka.ilkd.key.java.reference.TypeReference;
019: import de.uka.ilkd.key.logic.JavaBlock;
020: import de.uka.ilkd.key.logic.NamespaceSet;
021: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
022: import de.uka.ilkd.key.logic.op.ProgramMethod;
023: import de.uka.ilkd.key.logic.op.SLListOfProgramMethod;
024: import de.uka.ilkd.key.logic.sort.ObjectSort;
025: import de.uka.ilkd.key.util.Debug;
026: import de.uka.ilkd.key.util.KeYExceptionHandler;
027:
028: public class KeYProgModelInfo {
029:
030: private KeYCrossReferenceServiceConfiguration sc = null;
031: private KeYRecoderMapping mapping;
032: private TypeConverter typeConverter;
033: private HashMap implicits = new HashMap();
034: private KeYExceptionHandler exceptionHandler = null;
035:
036: public KeYProgModelInfo(TypeConverter typeConverter,
037: KeYExceptionHandler keh) {
038: this (new KeYCrossReferenceServiceConfiguration(keh),
039: new KeYRecoderMapping(), typeConverter);
040: exceptionHandler = keh;
041: }
042:
043: KeYProgModelInfo(KeYCrossReferenceServiceConfiguration crsc,
044: KeYRecoderMapping krm, TypeConverter typeConverter) {
045: sc = crsc;
046: this .typeConverter = typeConverter;
047: this .mapping = krm;
048: }
049:
050: public KeYRecoderMapping rec2key() {
051: return mapping;
052: }
053:
054: public KeYCrossReferenceServiceConfiguration getServConf() {
055: return sc;
056: }
057:
058: public KeYExceptionHandler getExceptionHandler() {
059: return exceptionHandler;
060: }
061:
062: /**
063: * Returns all KeY-elements mapped by Recoder2KeY object of this
064: * KeYProgModelInfo.
065: * @return a Set object containing the KeY-elements.
066: */
067:
068: public Set allElements() {
069: return rec2key().elemsKeY();
070: }
071:
072: /**
073: * Returns all ObjectSorts mapped to java.Types in KeY.
074: * @return a Collection containing the ObjectSorts.
075: */
076: public Collection allObjectSorts() {
077: Set result = new HashSet();
078: Iterator it = allElements().iterator();
079: while (it.hasNext()) {
080: Object o = it.next();
081: if (o instanceof KeYJavaType
082: && (((KeYJavaType) o).getSort() instanceof ObjectSort)) {
083: result.add(((KeYJavaType) o).getSort());
084: }
085: }
086: return result;
087: }
088:
089: private recoder.list.MethodList getAllRecoderMethods(KeYJavaType kjt) {
090: if (kjt.getJavaType() instanceof TypeDeclaration) {
091: Object o = rec2key().toRecoder(kjt);
092: if (o instanceof recoder.abstraction.ClassType) {
093: recoder.abstraction.ClassType rtd = (recoder.abstraction.ClassType) o;
094: return rtd.getAllMethods();
095: }
096: }
097: return new recoder.list.MethodArrayList();
098:
099: }
100:
101: /**Returns all visible methods that are defined in this
102: * class type or any of its supertypes. The methods are
103: * in topological order with respect to the inheritance hierarchy.
104: * @return the list of visible methods of this type and its supertypes.
105: */
106:
107: public ListOfMethod getAllMethods(KeYJavaType kjt) {
108: recoder.list.MethodList rmethods = getAllRecoderMethods(kjt);
109: ListOfMethod result = SLListOfMethod.EMPTY_LIST;
110: for (int i = rmethods.size() - 1; i >= 0; i--) {
111: recoder.abstraction.Method rm = rmethods.getMethod(i);
112: Method m = ((ProgramMethod) rec2key().toKeY(rm))
113: .getMethodDeclaration();
114: result = result.prepend(m);
115: }
116: return result;
117: }
118:
119: /**Returns all visible methods that are defined in this
120: * class type or any of its supertypes. The methods are
121: * in topological order with respect to the inheritance hierarchy.
122: * @return the list of visible methods of this type and its supertypes.
123: */
124:
125: public ListOfProgramMethod getAllProgramMethods(KeYJavaType kjt) {
126: recoder.list.MethodList rmethods = getAllRecoderMethods(kjt);
127: ListOfProgramMethod result = SLListOfProgramMethod.EMPTY_LIST;
128: for (int i = rmethods.size() - 1; i >= 0; i--) {
129: recoder.abstraction.Method rm = rmethods.getMethod(i);
130: ProgramMethod m = (ProgramMethod) rec2key().toKeY(rm);
131: if (m != null) {
132: result = result.prepend(m);
133: }
134: }
135: return result;
136: }
137:
138: private recoder.list.TypeList getRecoderTypes(ListOfType types) {
139: if (types == null) {
140: return null;
141: }
142: IteratorOfType it = types.iterator();
143: recoder.list.TypeArrayList tl = new recoder.list.TypeArrayList(
144: types.size());
145: while (it.hasNext()) {
146: Type n = it.next();
147: tl.add((recoder.abstraction.Type) rec2key().toRecoder(n));
148: }
149: return tl;
150: }
151:
152: private recoder.list.TypeList getRecoderTypes(
153: ListOfKeYJavaType types) {
154: if (types == null) {
155: return null;
156: }
157: IteratorOfKeYJavaType it = types.iterator();
158: recoder.list.TypeArrayList tl = new recoder.list.TypeArrayList(
159: types.size());
160: while (it.hasNext()) {
161: final KeYJavaType kjt = it.next();
162: tl.add((recoder.abstraction.Type) rec2key().toRecoder(kjt));
163: }
164: return tl;
165: }
166:
167: /**
168: * Returns the full name of a KeYJavaType t.
169: * @return the full name of t as a String.
170: */
171:
172: public String getFullName(KeYJavaType t) {
173: recoder.abstraction.Type rt = (recoder.abstraction.Type) rec2key()
174: .toRecoder(t);
175: return rt.getFullName();
176: }
177:
178: public recoder.abstraction.Type getType(TypeReference tr) {
179: recoder.abstraction.Type result;
180: if (tr instanceof TypeRef) {
181: result = (recoder.abstraction.Type) rec2key().toRecoder(
182: ((TypeRef) tr).getKeYJavaType());
183: return result;
184: }
185: result = getServConf().getSourceInfo().getType(
186: (recoder.java.reference.TypeReference) rec2key()
187: .toRecoder(tr));
188: return result;
189: }
190:
191: /**
192: * Checks whether subType is a subtype of superType or not.
193: * @returns true if subType is subtype of superType,
194: * false in the other case.
195: */
196:
197: public boolean isSubtype(KeYJavaType subType, KeYJavaType super Type) {
198: return isSubtype((recoder.abstraction.Type) rec2key()
199: .toRecoder(subType),
200: (recoder.abstraction.Type) rec2key().toRecoder(
201: super Type));
202: }
203:
204: private boolean isSubtype(recoder.abstraction.Type subType,
205: recoder.abstraction.Type super Type) {
206: if (subType instanceof recoder.abstraction.ClassType
207: && super Type instanceof recoder.abstraction.ClassType) {
208: return isSubtype((recoder.abstraction.ClassType) subType,
209: (recoder.abstraction.ClassType) super Type);
210: } else if (super Type instanceof recoder.abstraction.ArrayType
211: && subType instanceof recoder.abstraction.ArrayType) {
212: return isAssignmentCompatible(
213: (recoder.abstraction.ArrayType) subType,
214: (recoder.abstraction.ArrayType) super Type);
215: } else if (subType instanceof recoder.abstraction.ArrayType
216: && super Type instanceof recoder.abstraction.ClassType) {
217: return "java.lang.Object".equals(super Type.getFullName())
218: || "Object".equals(super Type.getName());
219: }
220: // should not occur
221: throw new RuntimeException(
222: "Method isSubtype in class KeYProgModelInfo "
223: + "currently only supports two class types or two "
224: + "array type but no mixture!");
225: }
226:
227: private boolean isSubtype(
228: recoder.abstraction.ClassType classSubType,
229: recoder.abstraction.ClassType classType) {
230: boolean isSub = getServConf().getSourceInfo().isSubtype(
231: classSubType, classType);
232: if (!isSub) {
233: boolean result = getServConf().getByteCodeInfo().isSubtype(
234: classSubType, classType);
235: return result;
236: } else {
237: return true;
238: }
239: }
240:
241: /**
242: * create a recoder package reference out of a IDENT (DOT IDENT)+
243: * String
244: */
245: private recoder.java.reference.PackageReference createPackageReference(
246: String pkgName) {
247: final int lastDot = pkgName.lastIndexOf('.');
248: if (lastDot != -1) {
249: return new recoder.java.reference.PackageReference(
250: createPackageReference(pkgName
251: .substring(0, lastDot)),
252: new recoder.java.Identifier(pkgName
253: .substring(lastDot + 1)));
254: }
255: return new recoder.java.reference.PackageReference(
256: new recoder.java.Identifier(pkgName));
257: }
258:
259: /**
260: * checks if name refers to a package
261: * @param name a String with the name to be checked
262: * @return true iff name refers to a package
263: */
264: public boolean isPackage(String name) {
265: return ((recoder.service.DefaultNameInfo) sc.getNameInfo())
266: .isPackage(name);
267: }
268:
269: /**
270: * checls wheter subType is assignment compatible to type according
271: * to the rules defined in the java language specification
272: */
273: private boolean isAssignmentCompatible(
274: recoder.abstraction.ArrayType subType,
275: recoder.abstraction.ArrayType type) {
276: recoder.abstraction.Type bt1 = subType.getBaseType();
277: recoder.abstraction.Type bt2 = type.getBaseType();
278: if (bt1 instanceof recoder.abstraction.PrimitiveType
279: && bt2 instanceof recoder.abstraction.PrimitiveType) {
280: return bt1.getFullName().equals(bt2.getFullName());
281: }
282: if (bt1 instanceof recoder.abstraction.ClassType
283: && bt2 instanceof recoder.abstraction.ClassType)
284: return isSubtype((recoder.abstraction.ClassType) bt1,
285: (recoder.abstraction.ClassType) bt2);
286: if (bt1 instanceof recoder.abstraction.ArrayType
287: && bt2 instanceof recoder.abstraction.ArrayType)
288: return isAssignmentCompatible(
289: (recoder.abstraction.ArrayType) bt1,
290: (recoder.abstraction.ArrayType) bt2);
291: if (bt1 instanceof recoder.abstraction.ClassType
292: && bt2 instanceof recoder.abstraction.ArrayType)
293: return false;
294: if (bt1 instanceof recoder.abstraction.ArrayType
295: && bt2 instanceof recoder.abstraction.ClassType) {
296: if (((recoder.abstraction.ClassType) bt2).isInterface()) {
297: return ((recoder.abstraction.ClassType) bt2)
298: .getFullName().equals("java.lang.Cloneable")
299: || ((recoder.abstraction.ClassType) bt2)
300: .getFullName().equals(
301: "java.lang.Serializable");
302: } else {
303: return ((recoder.abstraction.ClassType) bt2)
304: .getFullName().equals("java.lang.Object");
305: }
306: }
307: return false;
308: }
309:
310: private recoder.list.MethodList getRecoderMethods(KeYJavaType ct) {
311: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
312: .toRecoder(ct);
313: return rct.getProgramModelInfo().getMethods(rct);
314: }
315:
316: private recoder.list.ConstructorList getRecoderConstructors(
317: KeYJavaType ct) {
318: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
319: .toRecoder(ct);
320: return rct.getProgramModelInfo().getConstructors(rct);
321: }
322:
323: private recoder.list.MethodList getRecoderMethods(KeYJavaType ct,
324: String m, ListOfType signature, KeYJavaType context) {
325: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
326: .toRecoder(ct);
327: recoder.abstraction.ClassType rcontext = (recoder.abstraction.ClassType) rec2key()
328: .toRecoder(context);
329: return rct.getProgramModelInfo().getMethods(rct, m,
330: getRecoderTypes(signature), rcontext);
331: }
332:
333: private recoder.list.MethodList getRecoderMethods(KeYJavaType ct,
334: String m, ListOfKeYJavaType signature, KeYJavaType context) {
335: final recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
336: .toRecoder(ct);
337: final recoder.abstraction.ClassType rcontext = (recoder.abstraction.ClassType) rec2key()
338: .toRecoder(context);
339: return rct.getProgramModelInfo().getMethods(rct, m,
340: getRecoderTypes(signature), rcontext);
341: }
342:
343: private recoder.list.ConstructorList getRecoderConstructors(
344: KeYJavaType ct, ListOfKeYJavaType signature) {
345: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
346: .toRecoder(ct);
347: recoder.list.ConstructorList res = rct.getProgramModelInfo()
348: .getConstructors(rct, getRecoderTypes(signature));
349: return res;
350: }
351:
352: /**
353: * Returns the list of most specific methods with the given
354: * name that are defined in the given type or in a supertype
355: * where they are visible for the given type, and have a signature
356: * that is compatible to the given one. If used to resolve a
357: * method call, the result should be defined and unambiguous.
358: * @param ct the class type to get methods from.
359: * @param m the name of the methods in question.
360: * @param signature the statical type signature of a callee.
361: */
362:
363: public ListOfMethod getMethods(KeYJavaType ct, String m,
364: ListOfType signature, KeYJavaType context) {
365: recoder.list.MethodList rml = getRecoderMethods(ct, m,
366: signature, context);
367: ListOfMethod result = SLListOfMethod.EMPTY_LIST;
368: for (int i = rml.size() - 1; i >= 0; i--) {
369: recoder.abstraction.Method rm = rml.getMethod(i);
370: Method method = (Method) rec2key().toKeY(rm);
371: result = result.prepend(method);
372: }
373: return result;
374: }
375:
376: /**
377: * Returns the methods locally defined within the given
378: * class type. If the type is represented in source code,
379: * the returned list matches the syntactic order.
380: * @param ct a class type.
381: */
382:
383: public ListOfMethod getMethods(KeYJavaType ct) {
384: recoder.list.MethodList rml = getRecoderMethods(ct);
385: ListOfMethod result = SLListOfMethod.EMPTY_LIST;
386: for (int i = rml.size() - 1; i >= 0; i--) {
387: recoder.abstraction.Method rm = rml.getMethod(i);
388: if (!(rm instanceof recoder.bytecode.MethodInfo)) {
389: Method m = ((ProgramMethod) rec2key().toKeY(rm))
390: .getMethodDeclaration();
391: result = result.prepend(m);
392: }
393: }
394: return result;
395: }
396:
397: /**
398: * Returns the ProgramMethods locally defined within the given
399: * class type. If the type is represented in source code,
400: * the returned list matches the syntactic order.
401: * @param ct a class type.
402: */
403: public ListOfProgramMethod getAllProgramMethodsLocallyDeclared(
404: KeYJavaType ct) {
405: recoder.list.MethodList rml = getRecoderMethods(ct);
406: ListOfProgramMethod result = SLListOfProgramMethod.EMPTY_LIST;
407: for (int i = rml.size() - 1; i >= 0; i--) {
408: recoder.abstraction.Method rm = rml.getMethod(i);
409: if (!(rm instanceof recoder.bytecode.MethodInfo)) {
410: result = result.prepend((ProgramMethod) rec2key()
411: .toKeY(rm));
412: }
413: }
414: return result;
415: }
416:
417: /**
418: * Returns the constructors locally defined within the given
419: * class type. If the type is represented in source code,
420: * the returned list matches the syntactic order.
421: * @param ct a class type.
422: */
423:
424: public ListOfProgramMethod getConstructors(KeYJavaType ct) {
425: recoder.list.ConstructorList rcl = getRecoderConstructors(ct);
426: ListOfProgramMethod result = SLListOfProgramMethod.EMPTY_LIST;
427: for (int i = rcl.size() - 1; i >= 0; i--) {
428: recoder.abstraction.Method rm = rcl.getConstructor(i);
429: ProgramMethod m = (ProgramMethod) rec2key().toKeY(rm);
430: if (m != null) {
431: result = result.prepend(m);
432: }
433: }
434: return result;
435: }
436:
437: /**
438: * retrieves the most specific constructor declared in the given type with
439: * respect to the given signature
440: * @param ct the KeYJavyType where to look for the constructor
441: * @param signature ListOfKeYJavaType representing the signature of the constructor
442: * @return the most specific constructor declared in the given type
443: */
444: public Constructor getConstructor(KeYJavaType ct,
445: ListOfKeYJavaType signature) {
446: recoder.list.ConstructorList constructors = getRecoderConstructors(
447: ct, signature);
448: if (constructors.size() == 1) {
449: Object o = rec2key().toKeY(constructors.getConstructor(0));
450: if (o instanceof Constructor) {
451: return (Constructor) o;
452: }
453: if (o instanceof ProgramMethod) {
454: return (Constructor) ((ProgramMethod) o)
455: .getMethodDeclaration();
456: }
457: }
458: if (constructors.size() == 0) {
459: Debug.out("javainfo: Constructor not found: ", ct);
460: return null;
461: }
462: Debug.fail();
463: return null;
464: }
465:
466: /**
467: * retrieves implicit methods
468: */
469: private ProgramMethod getImplicitMethod(KeYJavaType ct, String name) {
470: HashMap m = (HashMap) implicits.get(ct);
471: if (m != null) {
472: ProgramMethod pm = (ProgramMethod) m.get(name);
473: if (pm != null) {
474: return pm;
475: }
476: }
477: TypeDeclaration cd = (TypeDeclaration) ct.getJavaType();
478: ArrayOfMemberDeclaration members = cd.getMembers();
479: for (int i = 0; i < members.size(); i++) {
480: MemberDeclaration member = members.getMemberDeclaration(i);
481: if (member instanceof ProgramMethod
482: && ((ProgramMethod) member).getMethodDeclaration()
483: .getName().equals(name)) {
484: return (ProgramMethod) member;
485: }
486: }
487: Debug
488: .out(
489: "keyprogmodelinfo: implicit method %1 not found in %2 (%1, %2) ",
490: name, ct);
491: return null;
492: }
493:
494: /**
495: * Returns the programmethods with the given name that is defined
496: * in the given type or in a supertype where it is visible for the
497: * given type, and has a signature that is compatible to the given one.
498: * In the case that no method has been found or that the method could not
499: * be resolved uniquely <code>null</code> is returned.
500: * @param ct the class type to get methods from.
501: * @param m the name of the methods in question.
502: * @param signature the statical type signature of a callee.
503: * @return the programmethod, if one is found,
504: * null if none or more than one programmethod is found (in this case
505: * a debug output is written to console).
506: */
507: public ProgramMethod getProgramMethod(KeYJavaType ct, String m,
508: ListOfType signature, KeYJavaType context) {
509: if (ct.getJavaType() instanceof ArrayType
510: || context.getJavaType() instanceof ArrayType) {
511: return getImplicitMethod(ct, m);
512: }
513:
514: recoder.list.MethodList methodlist = getRecoderMethods(ct, m,
515: signature, context);
516: if (methodlist.size() == 1) {
517: return (ProgramMethod) rec2key().toKeY(
518: methodlist.getMethod(0));
519: }
520:
521: Debug.out("Program Method not found: ", m);
522: return null;
523: }
524:
525: /**
526: * Returns the programmethods with the given name that is defined
527: * in the given type or in a supertype where it is visible for the
528: * given type, and has a signature that is compatible to the given one.
529: * @param ct the class type to get methods from.
530: * @param m the name of the methods in question.
531: * @param signature the statical type signature of a callee.
532: * @return the programmethod, if one is found,
533: * null if none or more than one programmethod is found (in this case
534: * a debug output is written to console).
535: */
536: public ProgramMethod getProgramMethod(KeYJavaType ct, String m,
537: ListOfKeYJavaType signature, KeYJavaType context) {
538: if (ct.getJavaType() instanceof ArrayType
539: || context.getJavaType() instanceof ArrayType) {
540: return getImplicitMethod(ct, m);
541: }
542:
543: recoder.list.MethodList methodlist = getRecoderMethods(ct, m,
544: signature, context);
545:
546: if (methodlist.size() == 1) {
547: return (ProgramMethod) rec2key().toKeY(
548: methodlist.getMethod(0));
549: } else if (methodlist.size() == 0) {
550: Debug.out("javainfo: Program Method not found: ", m);
551: return null;
552: } else {
553: Debug.fail();
554: return null;
555: }
556: }
557:
558: /**
559: * returns the same fields as given in <tt>rfl</tt> and returns
560: * their KeY representation
561: * @param rfl the ListOfField to be looked up
562: * @return list with the corresponding fields as KeY datastructures
563: */
564: private ListOfField asKeYFields(recoder.list.FieldList rfl) {
565: ListOfField result = SLListOfField.EMPTY_LIST;
566: if (rfl == null) {
567: // this occurs for the artificial Null object at the moment
568: // should it have implicit fields?
569: return result;
570: }
571: for (int i = rfl.size() - 1; i >= 0; i--) {
572: recoder.abstraction.Field rf = rfl.getField(i);
573: Field f = (Field) rec2key().toKeY(rf);
574: if (f != null) {
575: result = result.prepend(f);
576: } else {
577: Debug.out(
578: "Field has no KeY equivalent (recoder field):",
579: rf.getFullName());
580: Debug
581: .out("This happens currently as classes only available in byte code "
582: + "are only partially converted ");
583: }
584: }
585: return result;
586: }
587:
588: /**
589: * returns the fields defined within the given class type.
590: * If the type is represented in source code, the returned list
591: * matches the syntactic order.
592: * @param ct the class type whose fields are returned
593: * @return the list of field members of the given type.
594: */
595: public ListOfField getAllFieldsLocallyDeclaredIn(KeYJavaType ct) {
596: if (ct.getJavaType() instanceof ArrayType) {
597: return getVisibleArrayFields(ct);
598: }
599: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
600: .toRecoder(ct);
601:
602: return asKeYFields(rct.getProgramModelInfo().getFields(rct));
603: }
604:
605: /**
606: * returns all in <tt>ct</tt> visible fields
607: * declared in <tt>ct</tt> or one of its supertypes
608: * in topological order starting with the fields of
609: * the given type
610: * If the type is represented in source code, the returned list
611: * matches the syntactic order.
612: * @param ct the class type whose fields are returned
613: * @return the list of field members of the given type.
614: */
615: public ListOfField getAllVisibleFields(KeYJavaType ct) {
616: if (ct.getJavaType() instanceof ArrayDeclaration) {
617: return getVisibleArrayFields(ct);
618: }
619:
620: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
621: .toRecoder(ct);
622: recoder.list.FieldList rfl = rct.getProgramModelInfo()
623: .getAllFields(rct);
624: return asKeYFields(rfl);
625: }
626:
627: /**
628: * returns all fields of and visible in an array field
629: * @param arrayType the KeYJavaType of the array
630: * @return the list of visible fields
631: */
632: private ListOfField getVisibleArrayFields(KeYJavaType arrayType) {
633: ListOfField result = SLListOfField.EMPTY_LIST;
634:
635: final ArrayOfMemberDeclaration members = ((ArrayDeclaration) arrayType
636: .getJavaType()).getMembers();
637:
638: for (int i = members.size() - 1; i >= 0; i--) {
639: final MemberDeclaration member = members
640: .getMemberDeclaration(i);
641: if (member instanceof FieldDeclaration) {
642: final ArrayOfFieldSpecification specs = ((FieldDeclaration) member)
643: .getFieldSpecifications();
644: for (int j = specs.size() - 1; j >= 0; j--) {
645: result = result.prepend(specs
646: .getFieldSpecification(j));
647: }
648: }
649: }
650:
651: // fields of java.lang.Object visible in an array
652: final ListOfField javaLangObjectField = getAllVisibleFields((KeYJavaType) rec2key()
653: .toKeY(sc.getNameInfo().getJavaLangObject()));
654:
655: final IteratorOfField it = javaLangObjectField.iterator();
656: while (it.hasNext()) {
657: final Field f = it.next();
658:
659: if (!((recoder.abstraction.Field) rec2key().toRecoder(f))
660: .isPrivate()) {
661: result = result.append(f);
662: }
663: }
664: return result;
665: }
666:
667: /**
668: * returns all proper subtypes of class <code>ct</code> (i.e. without <code>ct</code> itself)
669: */
670: private recoder.list.ClassTypeList getAllRecoderSubtypes(
671: KeYJavaType ct) {
672: return sc.getCrossReferenceSourceInfo()
673: .getAllSubtypes(
674: (recoder.abstraction.ClassType) rec2key()
675: .toRecoder(ct));
676: }
677:
678: /**
679: * returns all supertypes of the given class type with the type itself as
680: * first element
681: */
682: private recoder.list.ClassTypeList getAllRecoderSupertypes(
683: KeYJavaType ct) {
684: return sc.getCrossReferenceSourceInfo()
685: .getAllSupertypes(
686: (recoder.abstraction.ClassType) rec2key()
687: .toRecoder(ct));
688: }
689:
690: /**
691: * returns a list of KeYJavaTypes representing the given recoder types in
692: * the same order
693: * @param rctl the ClassTypeList to be converted
694: * @return list of KeYJavaTypes representing the given recoder types in
695: * the same order
696: */
697: private ListOfKeYJavaType asKeYJavaTypes(
698: final recoder.list.ClassTypeList rctl) {
699: ListOfKeYJavaType result = SLListOfKeYJavaType.EMPTY_LIST;
700: for (int i = rctl.size() - 1; i >= 0; i--) {
701: final recoder.abstraction.ClassType rct = rctl
702: .getClassType(i);
703: final KeYJavaType kct = (KeYJavaType) rec2key().toKeY(rct);
704: result = result.prepend(kct);
705: }
706: return result;
707: }
708:
709: /**
710: * Returns all known subtypes of the given class type.
711: * @param ct a class type
712: * @return the list of the known subtypes of the given class type.
713: */
714: public ListOfKeYJavaType getAllSupertypes(KeYJavaType ct) {
715: return asKeYJavaTypes(getAllRecoderSupertypes(ct));
716: }
717:
718: /**
719: * Returns all proper subtypes of the given class type
720: * @param ct a class type
721: * @return the list of the known subtypes of the given class type.
722: */
723: public ListOfKeYJavaType getAllSubtypes(KeYJavaType ct) {
724: return asKeYJavaTypes(getAllRecoderSubtypes(ct));
725: }
726:
727: private Recoder2KeY createRecoder2KeY(NamespaceSet nss) {
728: return new Recoder2KeY(sc, rec2key(), nss, typeConverter);
729: }
730:
731: /**
732: * Parses a given JavaBlock using cd as context to determine the right
733: * references.
734: * @param block a String describing a java block
735: * @param cd ClassDeclaration representing the context in which the
736: * block has to be interpreted.
737: * @return the parsed and resolved JavaBlock
738: */
739: public JavaBlock readBlock(String block, ClassDeclaration cd,
740: NamespaceSet nss) {
741: return createRecoder2KeY(nss)
742: .readBlock(
743: block,
744: new Context(
745: sc,
746: (recoder.java.declaration.ClassDeclaration) rec2key()
747: .toRecoder(cd)));
748: }
749:
750: /**
751: * Parses a given JavaBlock using an empty context.
752: * @param block a String describing a java block
753: * @return the parsed and resolved JavaBlock
754: */
755: public JavaBlock readJavaBlock(String block, NamespaceSet nss) {
756: return createRecoder2KeY(nss).readBlockWithEmptyContext(block);
757: }
758:
759: public ListOfKeYJavaType findImplementations(Type ct, String name,
760: ListOfKeYJavaType signature) {
761:
762: // set up recoder inputs
763: recoder.abstraction.ClassType rct = (recoder.abstraction.ClassType) rec2key()
764: .toRecoder(ct);
765: // transform the signature up to recoder conventions
766: recoder.list.TypeArrayList rsignature = new recoder.list.TypeArrayList(
767: signature.size());
768: IteratorOfKeYJavaType i = signature.iterator();
769: int j = 0;
770: while (i.hasNext()) {
771: rsignature.insert(j, (recoder.abstraction.Type) rec2key()
772: .toRecoder(i.next()));
773: j++;
774: }
775:
776: // If ct is an interface, but does not declare the method, we
777: // need to start the search "upstairs"
778:
779: while (rct.isInterface()
780: && !isDeclaringInterface(rct, name, rsignature)) {
781: rct = rct.getAllSupertypes().getClassType(1);
782: }
783:
784: ListOfKeYJavaType classList = SLListOfKeYJavaType.EMPTY_LIST;
785: classList = recFindImplementations(rct, name, rsignature,
786: classList);
787:
788: if (!declaresApplicableMethods(rct, name, rsignature)) {
789: // ct has no implementation, go up
790: recoder.list.ClassTypeList super Types = rct
791: .getAllSupertypes();
792: int k = 0;
793: while (k < super Types.size()
794: && !declaresApplicableMethods(super Types
795: .getClassType(k), name, rsignature))
796: k++;
797: if (k < super Types.size()) {
798: rct = super Types.getClassType(k);
799: KeYJavaType r = (KeYJavaType) mapping.toKeY(rct);
800: if (r == null) {
801: System.out.println("Type " + rct.getName());
802: } else {
803: classList = classList.append(r);
804: }
805: } // no implementation is needed if classes above are abstract
806: }
807:
808: return classList;
809: }
810:
811: private ListOfKeYJavaType recFindImplementations(
812: recoder.abstraction.ClassType ct, String name,
813: recoder.list.TypeList signature, ListOfKeYJavaType result) {
814: recoder.service.CrossReferenceSourceInfo si = getServConf()
815: .getCrossReferenceSourceInfo();
816:
817: if (declaresApplicableMethods(ct, name, signature)) {
818: KeYJavaType r = (KeYJavaType) mapping.toKeY(ct);
819: if (r == null) {
820: System.out.println("Type " + ct.getFullName() + ":"
821: + name + " not found");
822: } else {
823: result = result.prepend(r);
824: }
825: }
826:
827: recoder.list.ClassTypeList classes = si.getSubtypes(ct);
828:
829: //alpha sorting to make order deterministic
830: recoder.abstraction.ClassType[] classesArray = classes
831: .toClassTypeArray();
832: java.util.Arrays.sort(classesArray, new java.util.Comparator() {
833: public int compare(Object o1, Object o2) {
834: recoder.abstraction.ClassType c1 = (recoder.abstraction.ClassType) o1;
835: recoder.abstraction.ClassType c2 = (recoder.abstraction.ClassType) o2;
836: return -c1.getFullName().compareTo(c2.getFullName());
837: }
838: });
839:
840: for (int i = 0; i < classesArray.length; i++) {
841: recoder.abstraction.ClassType c = classesArray[i];
842: result = recFindImplementations(c, name, signature, result);
843: }
844: return result;
845: }
846:
847: private boolean declaresApplicableMethods(
848: recoder.abstraction.ClassType ct, String name,
849: recoder.list.TypeList signature) {
850: recoder.service.CrossReferenceSourceInfo si = getServConf()
851: .getCrossReferenceSourceInfo();
852:
853: recoder.list.MethodList list = si.getMethods(ct);
854: int s = list.size();
855: int i = 0;
856: while (i < s) {
857: recoder.abstraction.Method m = list.getMethod(i);
858: if (name.equals(m.getName())
859: && si.isCompatibleSignature(signature, m
860: .getSignature()) && si.isVisibleFor(m, ct)
861: && !m.isAbstract())
862: return true;
863: else
864: i++;
865: }
866: return false;
867: }
868:
869: private boolean isDeclaringInterface(
870: recoder.abstraction.ClassType ct, String name,
871: recoder.list.TypeList signature) {
872: recoder.service.CrossReferenceSourceInfo si = getServConf()
873: .getCrossReferenceSourceInfo();
874:
875: Debug.assertTrue(ct.isInterface());
876:
877: recoder.list.MethodList list = si.getMethods(ct);
878: int s = list.size();
879: int i = 0;
880: while (i < s) {
881: recoder.abstraction.Method m = list.getMethod(i);
882: if (name.equals(m.getName())
883: && si.isCompatibleSignature(signature, m
884: .getSignature()) && si.isVisibleFor(m, ct))
885: return true;
886: else
887: i++;
888: }
889: return false;
890: }
891:
892: public void putImplicitMethod(ProgramMethod m, KeYJavaType t) {
893: HashMap map = (HashMap) implicits.get(t);
894: if (map == null) {
895: map = new HashMap();
896: implicits.put(t, map);
897: }
898: map.put(m.name().toString(), m);
899: }
900:
901: public KeYProgModelInfo copy() {
902: return new KeYProgModelInfo(getServConf(), rec2key().copy(),
903: typeConverter);
904: }
905:
906: }
|