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.visitor;
011:
012: import java.util.HashSet;
013: import java.util.Iterator;
014: import java.util.Set;
015:
016: import de.uka.ilkd.key.java.Expression;
017: import de.uka.ilkd.key.java.ProgramElement;
018: import de.uka.ilkd.key.java.Services;
019: import de.uka.ilkd.key.java.SourceElement;
020: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
021: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
022: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
023: import de.uka.ilkd.key.java.reference.*;
024: import de.uka.ilkd.key.logic.ProgramElementName;
025: import de.uka.ilkd.key.logic.op.LocationVariable;
026: import de.uka.ilkd.key.logic.op.ProgramMethod;
027: import de.uka.ilkd.key.logic.op.ProgramVariable;
028: import de.uka.ilkd.key.util.Debug;
029:
030: /**
031: * Walks through a java AST in depth-left-fist-order.
032: * This walker is used to collect all Types in a program.
033: */
034: public class ProgramTypeCollector extends JavaASTVisitor {
035:
036: private HashSet result = new HashSet();
037: private HashSet programMethods = new HashSet();
038: private KeYJavaType type;
039: private Services services;
040: private ProgramVariable self;
041: private Set alreadyVisitedProgramMethods;
042:
043: public ProgramTypeCollector(ProgramElement root,
044: ProgramVariable self, KeYJavaType type, Services services,
045: Set alreadyVisitedProgramMethods) {
046: super (root);
047: this .type = type;
048: this .self = self;
049: this .services = services;
050: this .alreadyVisitedProgramMethods = alreadyVisitedProgramMethods;
051: }
052:
053: /** the action that is performed just before leaving the node the
054: * last time
055: */
056: protected void doAction(ProgramElement node) {
057: node.visit(this );
058: }
059:
060: /** starts the walker*/
061: public void start() {
062: walk(root());
063: }
064:
065: public HashSet getResult() {
066: return result;
067: }
068:
069: public HashSet getProgramMethods() {
070: return programMethods;
071: }
072:
073: public String toString() {
074: return result.toString();
075: }
076:
077: public void performActionOnTypeReference(TypeReference x) {
078: result.add(x.getKeYJavaType());
079: }
080:
081: public void performActionOnMethodReference(MethodReference x) {
082: MethodReference currentMR = x;
083: ProgramVariable currentSelf = self;
084: KeYJavaType currentType = type;
085: ReferencePrefix referencePre = currentMR.getReferencePrefix();
086:
087: if (referencePre != null) {
088: if (referencePre instanceof ProgramVariable) {
089: currentSelf = (ProgramVariable) referencePre;
090: currentType = currentSelf.getKeYJavaType();
091: }
092: if (referencePre instanceof TypeReference) {
093: currentType = ((TypeReference) referencePre)
094: .getKeYJavaType();
095: currentSelf = new LocationVariable(
096: new ProgramElementName("x_"
097: + referencePre.toString()), currentType);
098: }
099: if (referencePre instanceof Expression) {
100: currentType = services.getTypeConverter()
101: .getKeYJavaType(
102: (Expression) referencePre,
103: new ExecutionContext(new TypeRef(type),
104: self));
105: currentSelf = new LocationVariable(
106: new ProgramElementName("x_"
107: + referencePre.toString()), currentType);
108: }
109:
110: ListOfKeYJavaType imps = services
111: .getJavaInfo()
112: .getKeYProgModelInfo()
113: .findImplementations(
114: currentType,
115: currentMR.getMethodName().toString(),
116: currentMR.getMethodSignature(services,
117: new ExecutionContext(new TypeRef(
118: currentType), currentSelf)));
119:
120: IteratorOfKeYJavaType impsIt = imps.iterator();
121: while (impsIt.hasNext()) {
122: currentType = impsIt.next();
123:
124: ProgramMethod currentPM = services
125: .getJavaInfo()
126: .getProgramMethod(
127: currentType,
128: currentMR.getMethodName().toString(),
129: currentMR
130: .getMethodSignature(
131: services,
132: new ExecutionContext(
133: new TypeRef(
134: currentType),
135: currentSelf)),
136: currentSelf.getKeYJavaType());
137: //System.out.println("pm: " + currentPM);
138:
139: if (!alreadyVisitedProgramMethods.contains(currentPM)) {
140: alreadyVisitedProgramMethods.add(currentPM);
141: //System.out.println("pm building new ptc: " + currentPM);
142: if (services.getJavaInfo().getKeYJavaType(
143: currentPM.getContainerType()) != null) {
144: result.add(services.getJavaInfo()
145: .getKeYJavaType(
146: currentPM.getContainerType()));
147: }
148:
149: ProgramTypeCollector mCollector = new ProgramTypeCollector(
150: currentPM, currentSelf, currentType,
151: services, alreadyVisitedProgramMethods);
152:
153: mCollector.start();
154: Iterator it = mCollector.getResult().iterator();
155: while (it.hasNext()) {
156: result.add(it.next());
157: }
158: }
159:
160: // ACHTUNG: getProgramMethods ist unnoetig in der jetzigen Implementierung
161: // Allerdings ist keine Ueberpruefung ob ggf. eine programmethod mehrfach wiederholt wird
162:
163: /*
164: it = mCollector.getProgramMethods().iterator();
165:
166: Set addToMethodRefs = mCollector.getMethodRefs();
167: Iterator addToMethodRefsIt = addToMethodRefs.iterator();
168: while (addToMethodRefsIt.hasNext()) {
169: MethodReference mR = (MethodReference) addToMethodRefsIt.next();
170: // only add those methodReferences which have not been visited
171: // to the set of methodReferences which need to be visited
172: if (!visitedMethodRefs.contains(mR)) {
173: methodRefs.add(mR);
174: }
175: }
176: */
177: }
178: }
179: }
180:
181: protected void doDefaultAction(SourceElement x) {
182: if (x instanceof Expression) {
183: final KeYJavaType expressionType = services
184: .getTypeConverter().getKeYJavaType(
185: (Expression) x,
186: new ExecutionContext(new TypeRef(type),
187: self));
188: Debug.assertTrue(expressionType != null,
189: "Could not determine type of " + x);
190: result.add(expressionType);
191: }
192: }
193: }
|