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.HashMap;
011: import java.util.HashSet;
012: import java.util.Iterator;
013: import java.util.LinkedList;
014:
015: import de.uka.ilkd.key.java.Expression;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.SourceElement;
018: import de.uka.ilkd.key.java.abstraction.ClassType;
019: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
021: import de.uka.ilkd.key.java.declaration.ArrayOfParameterDeclaration;
022: import de.uka.ilkd.key.java.expression.Assignment;
023: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
024: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
025: import de.uka.ilkd.key.java.reference.ExecutionContext;
026: import de.uka.ilkd.key.java.reference.MethodReference;
027: import de.uka.ilkd.key.java.reference.ReferencePrefix;
028: import de.uka.ilkd.key.java.reference.TypeRef;
029: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
030: import de.uka.ilkd.key.java.statement.MethodFrame;
031: import de.uka.ilkd.key.java.statement.Throw;
032: import de.uka.ilkd.key.logic.*;
033: import de.uka.ilkd.key.logic.op.*;
034: import de.uka.ilkd.key.proof.Node;
035: import de.uka.ilkd.key.proof.ProgVarReplacer;
036: import de.uka.ilkd.key.rule.ListOfRuleSet;
037: import de.uka.ilkd.key.rule.PosTacletApp;
038: import de.uka.ilkd.key.rule.RuleSet;
039: import de.uka.ilkd.key.rule.Taclet;
040: import de.uka.ilkd.key.rule.inst.ContextInstantiationEntry;
041: import de.uka.ilkd.key.visualdebugger.SourceElementId;
042: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
043:
044: public class ITNode {
045: private SourceElement activeStatement;
046:
047: ListOfTerm bc = SLListOfTerm.EMPTY_LIST;
048:
049: private LinkedList children = new LinkedList();
050:
051: private boolean exprEnd;
052:
053: private ProgramVariable expressionResultVar = null;
054:
055: private SourceElementId exprId = null;
056:
057: private final int id;
058:
059: private HashSet idsOfNonPVExpressions = new HashSet();
060:
061: private boolean isMethodInvokation = false;
062:
063: private ITNode lastExpressionId;
064:
065: private boolean methodInvocationForET;
066:
067: private ITNode methodNode;
068:
069: private Term methodReference;
070:
071: private boolean methodReturn;
072:
073: private Term methodReturnResult;
074:
075: private boolean nobc = false;
076:
077: private final Node node;
078:
079: private ListOfProgramVariable parameter;
080:
081: private final ITNode parent;
082:
083: ListOfTerm pc = SLListOfTerm.EMPTY_LIST;
084:
085: private ProgramMethod programMethod;
086:
087: private Services serv = VisualDebugger.getVisualDebugger()
088: .getMediator().getServices();
089:
090: private SourceElementId statementId = null;
091:
092: private ListOfTerm values = null;
093:
094: private VisualDebugger vd = VisualDebugger.getVisualDebugger();
095:
096: public ITNode(ListOfTerm bc, ListOfTerm pc, Node n, ITNode parent) {
097: this .bc = bc;
098: this .parent = parent;
099:
100: this .id = n.serialNr();
101: this .pc = pc;
102: this .node = n;
103: if (parent != null)
104: this .idsOfNonPVExpressions = (HashSet) parent.idsOfNonPVExpressions
105: .clone();
106: this .activeStatement = calcActStatement();
107: statementId = calcStatementId();
108: this .exprId = calcExprId();
109: this .exprEnd = calcExprEnd();
110: this .methodReturn = calcMethodReturn();
111: this .isMethodInvokation = this .calcIsMethodInvocation();
112: setMethodNode();
113: }
114:
115: public ITNode(Node n) {
116: this .parent = null;
117: this .id = n.serialNr();
118: this .node = n;
119: this .methodNode = null;
120: this .activeStatement = calcActStatement();
121: this .statementId = calcStatementId();
122: this .exprEnd = calcExprEnd();
123: this .exprId = calcExprId();
124: this .isMethodInvokation = this .calcIsMethodInvocation();
125: }
126:
127: public void addChild(ITNode n) {
128: children.add(n);
129: }
130:
131: private SourceElement calcActStatement() {
132: return vd.determineFirstAndActiveStatement(node);
133:
134: }
135:
136: private boolean calcExprEnd() {
137:
138: if (activeStatement instanceof MethodBodyStatement) {
139: final MethodBodyStatement mbs = (MethodBodyStatement) activeStatement;
140: // FIXME: do not lookup for method using Strings use the real AST
141: // objects instead
142: // This is likely to break as soon as a method ending with sep is
143: // present
144: if (mbs.getMethodReference().getMethodName().toString()
145: .endsWith("sep")) {
146: if (mbs.getArguments().size() > 1) { // is expression sep, no
147: // statment sep
148: this .expressionResultVar = (ProgramVariable) mbs
149: .getArguments().getExpression(1);
150:
151: return true;
152: }
153:
154: }
155: }
156:
157: // FIXME: What happens here?
158: if (true)
159: return false;
160:
161: if (activeStatement != null
162: && node.getAppliedRuleApp() instanceof PosTacletApp) {
163: PosTacletApp pta = (PosTacletApp) node.getAppliedRuleApp();
164:
165: MethodFrame mf = getMethodFrame(pta);
166: if (mf == null || mf.getProgramMethod() == null)
167: return false;
168:
169: if (mf.getProgramMethod().name().toString().endsWith("sep") // TODO
170: // remove
171: // taclet
172: // names...
173: // with
174: // special
175: // tacltes
176: // for
177: // sep,
178: // eg.
179: && node.getAppliedRuleApp().rule().displayName()
180: .toString().equals("method_call_return"))
181: return true;
182: }
183: return false;
184: }
185:
186: /**
187: * active statement of the form int b = sep(12,expr);
188: *
189: * @return
190: */
191: private SourceElementId calcExprId() {
192: if (parent != null && parent.getExprId() != null)
193: this .lastExpressionId = parent;
194: else if (isExprEnd())
195: lastExpressionId = parent.getLastExpressionId()
196: .getLastExpressionId();
197: else if (parent != null)
198: lastExpressionId = parent.getLastExpressionId();
199: else
200: this .lastExpressionId = null;
201:
202: final SourceElement statement = activeStatement;
203:
204: if (statement != null && statement instanceof CopyAssignment) {
205:
206: final SourceElement act = ((Assignment) statement)
207: .getChildAt(1);
208:
209: if (act != null && act instanceof MethodReference) {
210: MethodReference mr = (MethodReference) act;
211: // FIXME: do not lookup for method using Strings use the real
212: // AST objects instead
213: // This is likely to break.
214: if (mr.getMethodName().toString().equals("sep")
215: && mr.getArgumentAt(0) instanceof IntLiteral) {// TODO
216: // sep(11,expr)
217:
218: if (node.getAppliedRuleApp() instanceof PosTacletApp) {
219:
220: final ProgramVariable pv = (ProgramVariable) ((Assignment) statement)
221: .getChildAt(0);
222:
223: PosTacletApp pta = (PosTacletApp) node
224: .getAppliedRuleApp();
225: MethodFrame mf = getMethodFrame(pta);
226: ExecutionContext ec = (ExecutionContext) mf
227: .getExecutionContext();
228: final SourceElementId sid = new SourceElementId(
229: ec.getTypeReference().toString(),
230: ((IntLiteral) (mr.getArgumentAt(0)))
231: .getValue(),
232: false,
233: pv.getKeYJavaType().getJavaType() == PrimitiveType.JAVA_BOOLEAN);
234:
235: if (!isTempVar(mr.getArgumentAt(1), sid))
236:
237: return sid;
238: }
239:
240: }
241:
242: }
243: }
244: return null;
245: }
246:
247: private boolean calcIsMethodInvocation() {
248: if (node.getAppliedRuleApp() != null
249: && node.getAppliedRuleApp().rule().name().toString()
250: .equals("introduce_post_predicate"))
251: return false;
252:
253: if (activeStatement instanceof MethodBodyStatement) {
254: final MethodBodyStatement mbs = (MethodBodyStatement) activeStatement;
255: final String name = mbs.getMethodReference()
256: .getMethodName().toString();
257: // FIXME: do no use Strings to identify these methods
258: if (name.startsWith("<alloc") || name.endsWith("sep")) {
259: return false; // no element added to method stack
260: }
261: this .methodInvocationForET = true;
262:
263: if (this .inExecutionTree(mbs))
264: this .methodInvocationForET = true;
265: else
266: this .methodInvocationForET = false;
267:
268: ReferencePrefix refPre = mbs.getMethodReference()
269: .getReferencePrefix();
270:
271: if (refPre instanceof TypeRef) {
272: final KeYJavaType kjt = ((TypeRef) refPre)
273: .getKeYJavaType();
274: final ClassType type = (ClassType) kjt.getJavaType();
275: // so = getStaticObject(type, symbolicObjects);
276:
277: programMethod = (mbs.getProgramMethod(serv));
278:
279: } else {
280:
281: final Term t = serv.getTypeConverter()
282: .convertToLogicElement(refPre);
283: methodReference = t;
284: HashMap map = new HashMap();
285: Term baseVar = getPref(t);
286:
287: PosInOccurrence pio = vd.getProgramPIO(getNode()
288: .sequent());
289: HashSet set = new HashSet();
290: set.add(baseVar.op());
291: HashMap result = vd.getValuesForLocation(set, pio);
292: Term val = (Term) result.get(TermFactory.DEFAULT
293: .createVariableTerm((ProgramVariable) baseVar
294: .op()));
295: map.put(baseVar.op(), val);
296: ProgVarReplacer pvr = new ProgVarReplacer(map);
297: Term res = pvr.replace(t);
298: programMethod = mbs.getProgramMethod(serv);
299:
300: methodReference = res;
301: }
302:
303: HashSet set = vd.getParam(mbs);
304: ListOfProgramVariable inputPara = vd
305: .arrayOfExpression2ListOfProgVar(
306: mbs.getArguments(), 0);
307: ProgramVariable[] inputParaArray = inputPara.toArray();
308:
309: ArrayOfParameterDeclaration paraDecl = mbs
310: .getProgramMethod(serv).getParameters();
311: final HashMap loc2val = vd.getValuesForLocation(set, vd
312: .getProgramPIO(node.sequent()));
313:
314: ListOfProgramVariable paramDeclAsPVList = SLListOfProgramVariable.EMPTY_LIST;
315:
316: this .values = SLListOfTerm.EMPTY_LIST;
317:
318: for (int i = 0; i < paraDecl.size(); i++) {
319: ProgramVariable next = (ProgramVariable) paraDecl
320: .getParameterDeclaration(i)
321: .getVariableSpecification()
322: .getProgramVariable();
323: Term val = (Term) loc2val.get(TermFactory.DEFAULT
324: .createVariableTerm(inputParaArray[i]));// TODO
325: this .values = this .values.append(val);
326: paramDeclAsPVList = paramDeclAsPVList.append(next);
327:
328: }
329: parameter = (paramDeclAsPVList);
330:
331: return true;
332:
333: }
334:
335: return false;
336:
337: }
338:
339: /**
340: * The method computes if this node represents a method return node, i.e. if
341: * it describes a state exactly after a method has returned. This is the
342: * case iff. the parent's node method stack has at least a depth of
343: * <tt>1</tt> (it must be inside a method) and the difference between the
344: * method stack depths is exactly once and the reason for the decrease is
345: * not a thrown exception.
346: *
347: * @return true if this node represent the state after a normal method
348: * return
349: */
350: private boolean calcMethodReturn() {
351: if (parent == null) {
352: return false;
353: }
354:
355: final int stackSize1 = vd.getMethodStackSize(parent.node);
356: final int stackSize2 = vd.getMethodStackSize(node);
357:
358: if (stackSize1 <= 0) {
359: return false;
360: }
361:
362: if (this .activeStatement instanceof Throw) {
363: return false;
364: }
365:
366: return (stackSize1 - stackSize2) == 1;
367: }
368:
369: private synchronized SourceElementId calcStatementId() {
370: if (node.getAppliedRuleApp() != null
371: && node.getAppliedRuleApp().rule() != null
372: && node.getAppliedRuleApp().rule() instanceof Taclet) {
373: Taclet taclet = (Taclet) node.getAppliedRuleApp().rule();
374: if (!this .tacletIsInRuleSet(taclet, "statement_sep"))
375: return null;
376:
377: } else
378: return null;
379:
380: SourceElement act = this .activeStatement;
381: if (act != null && act instanceof MethodReference) {
382: MethodReference mr = (MethodReference) act;
383: if (mr.getMethodName().toString().equals(
384: VisualDebugger.sepName)
385: && mr.getArgumentAt(0) instanceof IntLiteral) {
386: if (node.getAppliedRuleApp() != null
387: && node.getAppliedRuleApp().rule() != null
388: && !node.getAppliedRuleApp().rule().name()
389: .toString().equals(
390: "introduce_post_predicate")) {
391: if (node.getAppliedRuleApp() instanceof PosTacletApp) {
392:
393: PosTacletApp pta = (PosTacletApp) node
394: .getAppliedRuleApp();
395: MethodFrame mf = getMethodFrame(pta);
396: ExecutionContext ec = (ExecutionContext) mf
397: .getExecutionContext();
398:
399: return new SourceElementId(ec
400: .getTypeReference().toString(),
401: ((IntLiteral) (mr.getArgumentAt(0)))
402: .getValue());
403: }
404: }
405: }
406:
407: }
408:
409: return null;
410: }
411:
412: public SourceElement getActStatement() {
413:
414: return activeStatement;
415: }
416:
417: public ListOfTerm getBc() {
418: return bc;
419: }
420:
421: public ITNode[] getChildren() {
422: return (ITNode[]) children.toArray(new ITNode[children.size()]);
423: }
424:
425: public ProgramVariable getExpressionResultVar() {
426: return expressionResultVar;
427: }
428:
429: public SourceElementId getExprId() {
430: return exprId;
431: }
432:
433: public int getId() {
434: return id;
435: }
436:
437: public ITNode getLastExpressionId() {
438: return lastExpressionId;
439: }
440:
441: private MethodFrame getMethodFrame(PosTacletApp pta) {
442: final ContextInstantiationEntry cie = pta.instantiations()
443: .getContextInstantiation();
444: if (cie == null)
445: return null;
446: else
447: return vd.getMethodFrame(cie.contextProgram());
448:
449: }
450:
451: public ITNode getMethodNode() {
452: return methodNode;
453: }
454:
455: public Term getMethodReference() {
456: return methodReference;
457: }
458:
459: public Term getMethodReturnResult() {
460: return methodReturnResult;
461: }
462:
463: public Node getNode() {
464: return node;
465: }
466:
467: public ListOfProgramVariable getParameter() {
468: return parameter;
469: }
470:
471: public ITNode getParent() {
472: return parent;
473: }
474:
475: public ListOfTerm getPc() {
476: // remove implicit
477: if (!VisualDebugger.showImpliciteAttr)
478: return vd.removeImplicite(pc);
479: return pc;
480: }
481:
482: public ListOfTerm getPc(boolean impl) {
483: // remove implicit
484: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
485:
486: for (IteratorOfTerm it = pc.iterator(); it.hasNext();) {
487: final Term n = it.next();
488: if (!VisualDebugger.containsImplicitAttr(n) || impl)
489: result = result.append(n);
490:
491: }
492:
493: return result;
494: }
495:
496: private Term getPref(Term t) {
497: while (t.op() instanceof AttributeOp) {
498: t = t.sub(0);
499:
500: }
501:
502: // TODO Auto-generated method stub
503: return t;
504: }
505:
506: public ProgramMethod getProgramMethod() {
507: return programMethod;
508: }
509:
510: public SourceElementId getStatementId() {
511: return statementId;
512: }
513:
514: public ListOfTerm getValues() {
515: return values;
516: }
517:
518: public boolean inExecutionTree(MethodBodyStatement mbs) {
519: final String name = mbs.getMethodReference().getMethodName()
520: .toString();
521: String className = mbs.getProgramMethod(serv)
522: .getContainerType().getSort().toString();
523: if (className.startsWith("java")
524: || className.startsWith("System"))
525: return false;
526:
527: if (!name.startsWith("<") || name.startsWith("<init>"))
528: return true;
529:
530: return false;
531: }
532:
533: public boolean isExprEnd() {
534: return this .exprEnd;
535: }
536:
537: public boolean isMethodInvocation() {
538: return isMethodInvokation;
539: }
540:
541: public boolean isMethodInvocationForET() {
542: return methodInvocationForET;
543: }
544:
545: public boolean isMethodReturn() {
546: return methodReturn;
547: }
548:
549: public boolean isNobc() {
550: return nobc;
551: }
552:
553: private boolean isTempVar(Expression e, SourceElementId id) {
554: if (e instanceof ProgramVariable) {
555: if (this .idsOfNonPVExpressions.contains(id))
556: return true;
557: } else {
558: this .idsOfNonPVExpressions.add(id);
559: }
560:
561: return false;
562: }
563:
564: public void removeAllChildren() {
565: this .children = new LinkedList();
566: }
567:
568: private void setMethodNode() {
569: if (parent.isMethodInvocation()) {
570: this .methodNode = parent;
571: } else if (methodReturn) {
572: if (parent.getMethodNode() != null) {
573: // compute return value
574: methodNode = parent.getMethodNode().getMethodNode();
575: MethodBodyStatement mbs = (MethodBodyStatement) parent
576: .getMethodNode().getActStatement();
577: IProgramVariable resultVar = mbs.getResultVariable();
578: if (resultVar != null) {
579: final PosInOccurrence pio = vd
580: .getProgramPIO(getNode().sequent());
581: HashSet set = new HashSet();
582: set.add(resultVar);
583: final HashMap result = vd.getValuesForLocation(set,
584: pio);
585: // TODO
586: this .methodReturnResult = (Term) result
587: .get(TermFactory.DEFAULT
588: .createVariableTerm((ProgramVariable) resultVar));
589: }
590: }
591: } else {
592: this .methodNode = parent.getMethodNode();
593: }
594: }
595:
596: public void setNobc(boolean nobc) {
597: this .nobc = nobc;
598: }
599:
600: private boolean tacletIsInRuleSet(Taclet t, String ruleSet) {
601: ListOfRuleSet list = t.getRuleSets();
602: RuleSet rs;
603: while (!list.isEmpty()) {
604: rs = list.head();
605: Name name = rs.name();
606: if (name.toString().equals(ruleSet))
607: return true;
608: list = list.tail();
609: }
610: return false;
611: }
612:
613: public String toString() {
614: String result = "";
615: result = result + " (( " + bc + " Node " + id + " ";
616: Iterator it = children.iterator();
617: while (it.hasNext()) {
618: result = result + it.next();
619: }
620:
621: result = result + " ))";
622:
623: return result;
624: }
625:
626: }
|