Source Code Cross Referenced for KeYProgModelInfo.java in  » Testing » KeY » de » uka » ilkd » key » java » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.java 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


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:        }
www.java2java.com | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.