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: package de.uka.ilkd.key.visualization;
009:
010: import java.util.HashSet;
011: import java.util.LinkedList;
012: import java.util.Set;
013:
014: import de.uka.ilkd.key.java.*;
015: import de.uka.ilkd.key.java.reference.ExecutionContext;
016: import de.uka.ilkd.key.java.reference.TypeReference;
017: import de.uka.ilkd.key.java.statement.MethodFrame;
018: import de.uka.ilkd.key.java.statement.Throw;
019: import de.uka.ilkd.key.java.visitor.JavaASTCollector;
020: import de.uka.ilkd.key.logic.op.SetAsListOfProgramMethod;
021: import de.uka.ilkd.key.logic.op.SetOfProgramMethod;
022: import de.uka.ilkd.key.proof.Node;
023:
024: public class ExecutionTraceModel {
025:
026: public final static Integer TYPE1 = new Integer(1);
027: public final static Integer TYPE2 = new Integer(2);
028: public final static Integer TYPE3 = new Integer(3);
029:
030: private TraceElement start = null;
031: private TraceElement end = null;
032: private ContextTraceElement she = null;
033: private Node startNode, endNode;
034: private long rating = 0;
035: private boolean uncaughtException = false;
036: private TraceElement exception = null;
037: private Integer type;
038: private SimpleVisualizationStrategy.Occ startOcc;
039: // indicates that the symbolic execution on this trace has terminated
040: // (either normally or by an uncaught exception)
041: private boolean terminated = false;
042:
043: public ExecutionTraceModel(TraceElement start, TraceElement end,
044: ContextTraceElement she, Node startN, Node endN) {
045: this .startNode = startN;
046: this .endNode = endN;
047: this .start = start;
048: this .end = end;
049: this .she = she;
050: findUncaughtExeption();
051: }
052:
053: public ExecutionTraceModel(TraceElement start, TraceElement end,
054: ContextTraceElement she, long rating, Node startN,
055: Node endN, Integer type,
056: SimpleVisualizationStrategy.Occ startOcc) {
057: this .startNode = startN;
058: this .startOcc = startOcc;
059: this .endNode = endN;
060: this .start = start;
061: this .end = end;
062: this .she = she;
063: this .rating = rating;
064: this .type = type;
065: findUncaughtExeption();
066: }
067:
068: public Node getFirstNode() {
069: return startNode;
070: }
071:
072: public Node getLastNode() {
073: return endNode;
074: }
075:
076: public TraceElement getFirstTraceElement() {
077: return start;
078: }
079:
080: public TraceElement getLastTraceElement() {
081: return end;
082: }
083:
084: public ContextTraceElement getLastContextTraceElement() {
085: return she;
086: }
087:
088: public void setLastContextTraceElement(ContextTraceElement she) {
089: this .she = she;
090: }
091:
092: public long getRating() {
093: return rating;
094: }
095:
096: public void setTerminated(boolean terminated) {
097: this .terminated = terminated;
098: }
099:
100: public boolean blockCompletelyExecuted() {
101: return terminated;
102: }
103:
104: private boolean noExecutableStatement(ProgramElement block) {
105: if (block instanceof StatementBlock) {
106: StatementBlock sb = (StatementBlock) block;
107: return sb.isEmpty()
108: || sb.getBody().size() == 1
109: && noExecutableStatement(sb.getBody().getStatement(
110: 0));
111: }
112: if (block instanceof MethodFrame) {
113: return noExecutableStatement(((MethodFrame) block)
114: .getBody());
115: }
116: return false;
117: }
118:
119: /**
120: * Returns all ProgramMethods occuring in this trace.
121: */
122: public SetOfProgramMethod getProgramMethods(Services serv) {
123: SetOfProgramMethod result = SetAsListOfProgramMethod.EMPTY_SET;
124: TraceElement current = start;
125: while (current != end) {
126: JavaASTCollector coll = new JavaASTCollector(current
127: .getProgram(), MethodFrame.class);
128: coll.start();
129: ListOfProgramElement l = coll.getNodes();
130: IteratorOfProgramElement it = l.iterator();
131: while (it.hasNext()) {
132: MethodFrame mf = (MethodFrame) it.next();
133: if (mf.getProgramMethod() != null) {
134: result = result.add(mf.getProgramMethod());
135: }
136: }
137: current = current.getNextInProof();
138: // current = current.getNextExecuted();
139: }
140: return result;
141: }
142:
143: public Set getExecutedStatementPositions() {
144: HashSet result = new HashSet();
145: TraceElement current = start;
146: while (current != end) {
147: if (current.getSrcElement() != null) {
148: result.add(current.getSrcElement().getPositionInfo()
149: .getStartPosition());
150: }
151: current = current.getNextInProof();
152: }
153: return result;
154: }
155:
156: /**
157: * Returns the first ExecutionContext occuring in this trace.
158: */
159: public TypeReference getOuterExecutionContext() {
160: TraceElement current = start;
161: while (current != end) {
162: if (current.getExecutionContext() != null) {
163: return ((ExecutionContext) current
164: .getExecutionContext()).getTypeReference();
165: }
166: current = current.getNextExecuted();
167: }
168: return null;
169: }
170:
171: /**
172: *
173: * @param cte a ContextTraceElement in the Execution Trace Model
174: * @return the path to cte
175: */
176: public ContextTraceElement[] getPath(ContextTraceElement cte) {
177: LinkedList parents = new LinkedList();
178: ContextTraceElement parent;
179: parent = cte.getParent();
180: parents.add(cte);
181: while (parent != TraceElement.PARENTROOT) {
182: parents.addFirst(parent);
183: parent = parent.getParent();
184: }
185: ContextTraceElement[] array = new ContextTraceElement[parents
186: .size()];
187: parents.toArray(array);
188: return array;
189: }
190:
191: private void findUncaughtExeption() {
192: TraceElement che = getLastContextTraceElement();
193: if (che != null) {
194: while (che != TraceElement.END) {
195: if (che.getSrcElement() instanceof Throw) {
196: exception = che;
197: uncaughtException = true;
198: return;
199: }
200: che = che.getNextInProof();
201: }
202: }
203: }
204:
205: public boolean uncaughtException() {
206: return uncaughtException;
207: }
208:
209: public TraceElement getUncaughtException() {
210: return exception;
211: }
212:
213: public ContextTraceElement getFirstContextTraceElement() {
214: if (start instanceof ContextTraceElement) {
215: return (ContextTraceElement) start;
216: }
217: return start.getNextExecuted();
218: }
219:
220: public Integer getType() {
221: return type;
222: }
223:
224: public SimpleVisualizationStrategy.Occ getStartOcc() {
225: return startOcc;
226: }
227:
228: public String toString() {
229: String result = "";
230: ContextTraceElement cte = getFirstContextTraceElement();
231: while (cte != null) {
232: result += toStringTree(cte, " ");
233: if (cte instanceof ParentContextTraceElement) {
234: cte = ((ParentContextTraceElement) cte).stepOver();
235: } else {
236: cte = cte.getNextExecuted();
237: }
238: }
239: return result;
240: }
241:
242: public String toStringTree(ContextTraceElement cte, String indention) {
243: String result = toStringElement(cte, indention);
244: if ("".equals(result)) {
245: return "";
246: }
247: if (cte instanceof ParentContextTraceElement) {
248: ParentContextTraceElement pcte = (ParentContextTraceElement) cte;
249: ContextTraceElement[] children = pcte.getChildren();
250: for (int j = 0; j < children.length; j++) {
251: result += toStringTree(children[j], indention + " ");
252: }
253: }
254: return result;
255: }
256:
257: public String toStringElement(ContextTraceElement cte,
258: String indention) {
259: String result;
260: if (cte == null)
261: return "";
262: if (cte.getContextStatement() != null) {
263: result = indention + cte.getContextStatement();
264: } else if (cte.getSrcElement() != null) {
265: result = indention + cte.getSrcElement();
266: } else {
267: return "";
268: }
269: int i = result.indexOf("\n");
270: if (i > -1) {
271: result = result.substring(0, i) + "\n";
272: } else {
273: result += "\n";
274: }
275: return result;
276: }
277:
278: }
|