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.visualdebugger.executiontree;
009:
010: import java.util.Iterator;
011: import java.util.LinkedList;
012:
013: import de.uka.ilkd.key.gui.KeYMediator;
014: import de.uka.ilkd.key.logic.ListOfTerm;
015: import de.uka.ilkd.key.logic.SLListOfTerm;
016: import de.uka.ilkd.key.proof.ListOfNode;
017: import de.uka.ilkd.key.proof.Node;
018: import de.uka.ilkd.key.proof.SLListOfNode;
019: import de.uka.ilkd.key.strategy.DebuggerStrategy;
020: import de.uka.ilkd.key.strategy.StrategyProperties;
021: import de.uka.ilkd.key.visualdebugger.DebuggerPO;
022: import de.uka.ilkd.key.visualdebugger.ProofStarter;
023: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
024:
025: /**
026: * A node of an execution tree representing the control flow of a program.
027: *
028: *
029: * FIXME: the copy method creates insane trees (I do currently no understand
030: * what ITNodes are, but most probably the copy method brings ETNodes and
031: * ITNodes out of sync), up to now I am not sure which behaviour of copy has
032: * been wanted. This bug applies to all subclasses as well.
033: */
034: public class ETNode {
035: private LinkedList children = new LinkedList();
036:
037: private ETMethodInvocationNode lastMethodInvocation = null;
038:
039: private ETStatementNode lastExpressionStart = null;
040:
041: private ETNode parent = null;
042:
043: private KeYMediator mediator = VisualDebugger.getVisualDebugger()
044: .getMediator();
045:
046: private ListOfTerm bc = SLListOfTerm.EMPTY_LIST;
047:
048: // ListOfTerm pc= SLListOfTerm.EMPTY_LIST;
049: private LinkedList itNodes = new LinkedList();
050:
051: private boolean nobc = false;
052:
053: private ListOfTerm simplifiedBC = null;
054:
055: public ETNode(ListOfTerm bc, ETNode parent) {
056: this .bc = bc;
057: this .parent = parent;
058: this .setMethodInvocation();
059: }
060:
061: public ETNode(ListOfTerm bc, LinkedList itNodes, ETNode parent) {
062: this .bc = bc;
063: this .itNodes = itNodes;
064: this .parent = parent;
065: this .setMethodInvocation();
066: }
067:
068: protected void setMethodInvocation() {
069: if (this instanceof ETMethodInvocationNode) {
070: this .lastMethodInvocation = (ETMethodInvocationNode) this ;
071: } else if (this instanceof ETMethodReturnNode) {
072: if (parent.getLastMethodInvocation().getParent() != null)
073: this .lastMethodInvocation = parent
074: .getLastMethodInvocation().getParent()
075: .getLastMethodInvocation();
076:
077: } else if (parent != null) {
078: this .lastMethodInvocation = parent
079: .getLastMethodInvocation();
080: }
081: }
082:
083: public void addChild(ETNode n) {
084: children.add(n);
085: }
086:
087: public void setChildren(LinkedList n) {
088: this .children = n;
089: }
090:
091: public ETNode[] getChildren() {
092: return (ETNode[]) children.toArray(new ETNode[children.size()]);
093: }
094:
095: public LinkedList getChildrenList() {
096: return children;
097: }
098:
099: public ITNode[] getITNodesArray() {
100: return (ITNode[]) itNodes.toArray(new ITNode[itNodes.size()]);
101: }
102:
103: public ListOfTerm getBC() {
104: if (!VisualDebugger.showImpliciteAttr && bc != null)
105: return VisualDebugger.getVisualDebugger().removeImplicite(
106: bc);
107: return bc;
108: }
109:
110: public void appendBC(ListOfTerm l) {
111: if (bc != null) // TODO ??????? remove this!
112: this .bc = bc.append(l);
113: else
114: bc = SLListOfTerm.EMPTY_LIST.append(l);
115: }
116:
117: /**
118: * itnode
119: *
120: * @param n
121: */
122: public void addITNode(ITNode n) {
123: itNodes.add(n);
124: }
125:
126: /**
127: * it nodes
128: *
129: * @param nodes
130: */
131: public void addITNodes(LinkedList nodes) {
132: this .itNodes.addAll(nodes);
133: }
134:
135: /**
136: * itnodes
137: *
138: * @return
139: */
140: public LinkedList getITNodes() {
141: return itNodes;
142: }
143:
144: /**
145: * creates a shallow copy of this node and attaches it to node <tt>p</tt>
146: * FIXME: FIX this method as it creates not well linked trees Problems: 1)
147: * the children of this node are not linked to their new parent -->
148: * malformed tree 2) the children are not copied themselves and linking
149: * would destroy the old tree
150: *
151: */
152: public ETNode copy(ETNode p) {
153: ETNode copy = new ETNode(bc, (LinkedList) itNodes.clone(), p);
154: copy.setChildren((LinkedList) children.clone());
155: return copy;
156: }
157:
158: public void computeSimplifiedBC() {
159: if (this .bc != null)
160: this .simplifiedBC = VisualDebugger.getVisualDebugger()
161: .simplify(this .bc);
162: else
163: simplifiedBC = null;
164: }
165:
166: public ListOfTerm getSimplifiedBc() {
167: if (this .simplifiedBC == null)
168: return bc;
169: else
170: return this .simplifiedBC;
171: }
172:
173: public String toString() {
174: return print();
175: }
176:
177: public String print() {
178: String result = "";// = "Node\n";
179: if (getITNodesArray().length > 0)
180: result = result + " ETNode " + getITNodesArray()[0].getId()
181: + " " + bc;
182: else
183: result = result + " ETNode " + " " + bc;
184: if (this .lastMethodInvocation != null)
185: result += "lmi "
186: + this .lastMethodInvocation.getMethodReference();
187: return result;
188: }
189:
190: public boolean isNobc() {
191: return nobc;
192: }
193:
194: public void setNobc(boolean nobc) {
195: this .nobc = nobc;
196: }
197:
198: public ETStatementNode getLastExpressionStart() {
199: return lastExpressionStart;
200: }
201:
202: public ETMethodInvocationNode getLastMethodInvocation() {
203: return lastMethodInvocation;
204: }
205:
206: public ETNode getParent() {
207: return parent;
208: }
209:
210: public ListOfNode getProofTreeNodes() {
211: ListOfNode result = SLListOfNode.EMPTY_LIST;
212: for (Iterator it = itNodes.iterator(); it.hasNext();) {
213: result = result.append(((ITNode) it.next()).getNode());
214:
215: }
216: return result;
217: }
218:
219: public boolean representsProofTreeNode(Node n) {
220: for (Iterator it = itNodes.iterator(); it.hasNext();) {
221: if (((ITNode) it.next()).getNode().equals(n))
222: return true;
223:
224: }
225: return false;
226:
227: }
228:
229: public void removeRedundandITNodes() {
230: ITNode[] nodes = getITNodesArray();
231: boolean[] a = new boolean[nodes.length];
232: for (int i = 0; i < a.length; i++) {
233: a[i] = false;
234: }
235:
236: int resultLenght = nodes.length;
237:
238: for (int i = 0; i < nodes.length; i++) {
239: for (int j = 0; j < nodes.length; j++) {
240: if (i != j && !a[j] && !a[i]) {
241: // System.out.println("Redundant? "+nodes[i].getPc()+" ->
242: // "+nodes[j].getPc());
243: if (redundant(nodes[i], nodes[j])) {
244: resultLenght--;
245: a[j] = true;
246: }
247: }
248:
249: }
250:
251: }
252:
253: ITNode[] result = new ITNode[resultLenght];
254: int resulti = 0;
255: for (int i = 0; i < nodes.length; i++) {
256: if (!a[i]) {
257: result[resulti] = nodes[i];
258: resulti++;
259: }
260:
261: }
262:
263: }
264:
265: private boolean redundant(ITNode n1, ITNode n2) {
266: DebuggerPO po = new DebuggerPO("DebuggerPO: redundant pc");
267:
268: po.setPCImpl(n1.getPc(), n2.getPc());
269:
270: po.setIndices(mediator.getProof().env().getInitConfig()
271: .createTacletIndex(), mediator.getProof().env()
272: .getInitConfig().createBuiltInRuleIndex());
273:
274: po.setProofSettings(mediator.getProof().getSettings());
275:
276: po.setConfig(mediator.getProof().env().getInitConfig());
277:
278: final ProofStarter ps = new ProofStarter();
279: ps.init(po);
280: ps.getProof().setActiveStrategy(
281: (DebuggerStrategy.Factory.create(ps.getProof(),
282: "DebuggerStrategy", new StrategyProperties())));
283: ps.run(mediator.getProof().env());
284: return ps.getProof().closed();
285: }
286: }
|