0001: package visualdebugger.views;
0002:
0003: import java.util.HashMap;
0004: import java.util.HashSet;
0005: import java.util.Map;
0006:
0007: import org.eclipse.core.runtime.CoreException;
0008: import org.eclipse.draw2d.*;
0009: import org.eclipse.draw2d.Label;
0010: import org.eclipse.jdt.core.ICompilationUnit;
0011: import org.eclipse.jdt.core.JavaModelException;
0012: import org.eclipse.jdt.core.dom.Expression;
0013: import org.eclipse.jdt.ui.JavaUI;
0014: import org.eclipse.jface.action.Action;
0015: import org.eclipse.jface.action.IAction;
0016: import org.eclipse.jface.action.IToolBarManager;
0017: import org.eclipse.jface.action.Separator;
0018: import org.eclipse.jface.dialogs.MessageDialog;
0019: import org.eclipse.jface.text.ITextOperationTarget;
0020: import org.eclipse.jface.text.source.ISourceViewer;
0021: import org.eclipse.swt.SWT;
0022: import org.eclipse.swt.events.SelectionAdapter;
0023: import org.eclipse.swt.events.SelectionEvent;
0024: import org.eclipse.swt.events.SelectionListener;
0025: import org.eclipse.swt.graphics.Font;
0026: import org.eclipse.swt.graphics.FontData;
0027: import org.eclipse.swt.layout.GridData;
0028: import org.eclipse.swt.layout.GridLayout;
0029: import org.eclipse.swt.widgets.*;
0030: import org.eclipse.swt.widgets.Button;
0031: import org.eclipse.ui.IActionBars;
0032: import org.eclipse.ui.IEditorPart;
0033: import org.eclipse.ui.PartInitException;
0034: import org.eclipse.ui.PlatformUI;
0035: import org.eclipse.ui.part.ViewPart;
0036: import org.eclipse.ui.texteditor.MarkerUtilities;
0037:
0038: import visualdebugger.VBTBuilder;
0039: import visualdebugger.draw2d.*;
0040: import de.uka.ilkd.key.gui.Main;
0041: import de.uka.ilkd.key.logic.Term;
0042: import de.uka.ilkd.key.proof.*;
0043: import de.uka.ilkd.key.proof.decproc.DecProcRunner;
0044: import de.uka.ilkd.key.unittest.ModelGenerator;
0045: import de.uka.ilkd.key.visualdebugger.*;
0046: import de.uka.ilkd.key.visualdebugger.executiontree.*;
0047:
0048: public class ExecutionTreeView extends ViewPart implements
0049: DebuggerListener {
0050: private static final boolean debug = false;
0051:
0052: private boolean bcLabels = true;
0053:
0054: List bcListControl;
0055:
0056: Menu classMenu;
0057:
0058: ITNode currentRoot = null;
0059:
0060: private boolean cutTree = false;
0061:
0062: FigureCanvas figureCanvas;
0063:
0064: boolean hideInfeasible = true;
0065:
0066: HashSet labels = new HashSet();
0067:
0068: LightweightSystem lws;
0069:
0070: int maxmerge = 0;
0071:
0072: int merged = 0;
0073:
0074: private Action msletAction;
0075:
0076: Composite parent;
0077:
0078: TreeRoot root;
0079:
0080: private Figure selected;
0081:
0082: private MethodInvocationFigure selectedMIN = null;
0083:
0084: Shell shell;
0085:
0086: private Action sletAction;
0087:
0088: private Action testCaseAction, decisionProcedureAction;
0089:
0090: private ICompilationUnit unitOfLastExceptionMarker = null;
0091:
0092: private Action useBranchLabelsAction;
0093:
0094: final VisualDebugger vd;
0095:
0096: public ExecutionTreeView() {
0097: vd = VisualDebugger.getVisualDebugger();
0098: vd.addListener(this );
0099:
0100: }
0101:
0102: public synchronized TreeBranch buildRawTree(ITNode n) {
0103: SourceElementFigure statementNode = createNode("Node: "
0104: + n.getId() + "\n" + n.getActStatement(), true);
0105: TreeBranch branch = new TreeBranch(statementNode, null);
0106: ITNode[] children = n.getChildren();
0107: if (children != null && children.length > 0) {
0108: for (int i = 0; i < children.length; i++) {
0109: TreeBranch subTree = buildRawTree(children[i]);
0110: branch.addBranch(subTree, children[i].getBc() + "");
0111: root.addLabel(createConnection(statementNode, subTree
0112: .getNode(), children[i].getBc() != null ? vd
0113: .prettyPrint(children[i].getBc()) : "NULL",
0114: true));
0115: }
0116: }
0117: return branch;
0118: }
0119:
0120: public synchronized TreeBranch buildTreeBranch(ETNode n,
0121: TreeBranch parent) {
0122: try {
0123: IFigure statementNode = createNode(n);
0124: statementNode.addMouseListener(new MouseListener.Stub() {
0125: public void mousePressed(MouseEvent event) {
0126: if (event.button == 3) {
0127: classMenu.setVisible(true);
0128: }
0129: }
0130: });
0131:
0132: createRighClickContextMenu();
0133:
0134: TreeBranch branch = new TreeBranch(statementNode, parent);
0135: ETNode[] children = n.getChildren();
0136: if (children != null && children.length > 0) {
0137: for (int i = 0; i < children.length; i++) {
0138: TreeBranch subTree = buildTreeBranch(children[i],
0139: branch);
0140: branch.addBranch(subTree, children[i].getBC() + "");
0141: // subTree.getNode()
0142:
0143: // subTree.
0144:
0145: final Connection c = createConnection(
0146: statementNode, subTree.getNode(),
0147: children[i].getBC() != null ? vd
0148: .prettyPrint(children[i]
0149: .getSimplifiedBc())
0150: : "NO BC", (children.length > 1));
0151: subTree.setConnection(c);
0152:
0153: // c.setForegroundColor(ColorConstants.red);
0154: root.addLabel(c);
0155: // }
0156: }
0157: }
0158: return branch;
0159: } catch (Throwable t) {
0160: t.printStackTrace();
0161: }
0162: return null;
0163: }
0164:
0165: private void contributeToActionBars() {
0166: IActionBars bars = getViewSite().getActionBars();
0167: // fillLocalPullDown(bars.getMenuManager());
0168: fillLocalToolBar(bars.getToolBarManager());
0169: }
0170:
0171: private Connection createConnection(IFigure figFrom, IFigure figTo,
0172: String text, boolean withLabel) {
0173: PolylineConnection con = new PolylineConnection();
0174: con.setSourceAnchor(new ChopboxAnchor(figFrom));
0175: con.setTargetAnchor(new ChopboxAnchor(figTo));
0176: PolygonDecoration decoration = new PolygonDecoration();
0177: decoration.setTemplate(PolygonDecoration.TRIANGLE_TIP);
0178: con.setTargetDecoration(decoration);
0179:
0180: Ellipse e = new Ellipse();
0181:
0182: Label label;
0183: if (text.length() < 20)
0184: label = new Label(text);
0185: else
0186: label = new Label(text.substring(0, 19) + "...");
0187:
0188: Font font = new Font(shell.getDisplay(), "Arial", 8, SWT.NORMAL);
0189: ;
0190: label.setFont(font);
0191: label.setToolTip(new Label(text));
0192:
0193: label.setText("BC");
0194: label.setOpaque(true);
0195: e.setToolTip(new Label(text));
0196: e.add(label);
0197: e.setOpaque(false);
0198: e.setPreferredSize(15, 15);
0199: // e.setSize(15, 15);
0200: if (!text.equals("NO BC") && withLabel)
0201: con.add(label, new MidpointLocator(con, 0));
0202: labels.add(label);
0203: return con;
0204: }
0205:
0206: private Figure createNode(ETNode etNode) {
0207: if (etNode instanceof ETStatementNode) {
0208: final SourceElementFigure node = new SourceElementFigure(
0209: (ETStatementNode) etNode);
0210:
0211: node.addMouseListener(new MouseListener.Stub() {
0212: public void mouseDoubleClicked(MouseEvent me) {
0213: doubleClick(node);
0214: }
0215:
0216: public void mousePressed(MouseEvent me) {
0217: setSelected(node);
0218: }
0219: });
0220: return node;
0221:
0222: } else if (etNode instanceof ETLeafNode) {
0223: final ETLeafNode ln = (ETLeafNode) etNode;
0224: final LeafNode node = new LeafNode(ln);
0225: node.addMouseListener(new MouseListener.Stub() {
0226: public void mouseDoubleClicked(MouseEvent me) {
0227: // doubleClick(node);
0228: }
0229:
0230: public void mousePressed(MouseEvent me) {
0231: setLeafNodeSelected(node);
0232: }
0233: });
0234:
0235: return node;
0236: } else if (etNode instanceof ETMethodInvocationNode) {
0237:
0238: // if (true)
0239: // return new Label("TEST");
0240:
0241: final MethodInvocationFigure node = new MethodInvocationFigure(
0242: (ETMethodInvocationNode) etNode);
0243:
0244: node.addMouseListener(new MouseListener.Stub() {
0245: public void mouseDoubleClicked(MouseEvent me) {
0246: // doubleClick(node);
0247: }
0248:
0249: public void mousePressed(MouseEvent me) {
0250: // setSelected(node);
0251: }
0252: });
0253: return node;
0254:
0255: }
0256:
0257: else if (etNode instanceof ETMethodReturnNode) {
0258:
0259: // if (true)
0260: // return new Label("TEST");
0261:
0262: final MethodReturnFigure node = new MethodReturnFigure(
0263: (ETMethodReturnNode) etNode);
0264:
0265: node.addMouseListener(new MouseListener.Stub() {
0266: public void mouseDoubleClicked(MouseEvent me) {
0267: // doubleClick(node);
0268: }
0269:
0270: public void mousePressed(MouseEvent me) {
0271: setSelected(node);
0272: }
0273: });
0274: return node;
0275: }
0276:
0277: else {
0278: final Ellipse node = new Ellipse();
0279: node.setPreferredSize(10, 10);
0280: if (etNode.isNobc())
0281: node.setBackgroundColor(ColorConstants.yellow);
0282: else
0283: node.setBackgroundColor(ColorConstants.blue);
0284: // node.setMinimumSize(10, 10);
0285: return node;
0286:
0287: }
0288:
0289: }
0290:
0291: private SourceElementFigure createNode(String title,
0292: boolean listener) {
0293:
0294: final SourceElementFigure node = new SourceElementFigure(title);
0295: if (listener)
0296: node.addMouseListener(new MouseListener.Stub() {
0297: public void mouseDoubleClicked(MouseEvent me) {
0298: // doExpandCollapse();
0299: }
0300:
0301: public void mousePressed(MouseEvent me) {
0302: setSelected(node);
0303: }
0304: });
0305:
0306: if (!listener)
0307: node.setBackgroundColor(ColorConstants.white);
0308: return node;
0309: }
0310:
0311: /**
0312: * This is a callback that will allow us to create the viewer and initialize
0313: * it.
0314: */
0315: public void createPartControl(Composite parent) {
0316: shell = parent.getShell();
0317: this .parent = parent;
0318: // parent.setLayout(new GridLayout(2, false));
0319: parent.setLayout(new GridLayout(2, false));
0320: figureCanvas = new FigureCanvas(parent, SWT.NONE);
0321: figureCanvas.setScrollBarVisibility(FigureCanvas.AUTOMATIC);
0322:
0323: figureCanvas.getViewport().setContentsTracksHeight(true);
0324: figureCanvas.getViewport().setContentsTracksWidth(true);
0325: figureCanvas.getViewport().setContentsTracksHeight(true);
0326: figureCanvas.getViewport().setContentsTracksWidth(true);
0327: figureCanvas.setLayoutData(new GridData(GridData.FILL_BOTH));
0328:
0329: hookShell();
0330:
0331: // Put the LWS on the newly created Canvas.
0332: // lws = new LightweightSystem(canvas);
0333:
0334: root = new TreeRoot(createNode("Start", false));
0335: root.setMajorSpacing(40);
0336: root.setMinorSpacing(30);
0337:
0338: figureCanvas.setContents(root);
0339: shell.redraw();
0340:
0341: shell.open();
0342:
0343: makeActions();
0344: // hookContextMenu();
0345: // hookDoubleClickAction();
0346: contributeToActionBars();
0347:
0348: if (vd.getCurrentTree() != null) {
0349: this .currentRoot = vd.getCurrentTree();
0350: this .refresh();
0351: }
0352: }
0353:
0354: private void createRighClickContextMenu() {
0355: classMenu = new Menu(shell, SWT.POP_UP);
0356:
0357: MenuItem item = new MenuItem(classMenu, SWT.PUSH);
0358: item.setText("Run");
0359: item.addSelectionListener(new SelectionListener() {
0360: public void widgetDefaultSelected(SelectionEvent event) {
0361: }
0362:
0363: public void widgetSelected(SelectionEvent event) {
0364: final ListOfGoal goals = getSubtreeGoalsForETNode(((SourceElementFigure) ExecutionTreeView.this .selected)
0365: .getETNode());
0366: vd.run(goals);
0367: }
0368:
0369: });
0370:
0371: // create Step into button
0372: item = new MenuItem(classMenu, SWT.PUSH);
0373: item.setText("Step Into");
0374: item.addSelectionListener(new SelectionListener() {
0375: public void widgetDefaultSelected(SelectionEvent event) {
0376: }
0377:
0378: public void widgetSelected(SelectionEvent event) {
0379: ETNode node = ((SourceElementFigure) ExecutionTreeView.this .selected)
0380: .getETNode();
0381: final ListOfGoal goals = getSubtreeGoalsForETNode(node);
0382: vd.stepInto(goals);
0383: }
0384: });
0385:
0386: // create Step Over button
0387: item = new MenuItem(classMenu, SWT.PUSH);
0388: item.setText("Step Over");
0389: item.addSelectionListener(new SelectionListener() {
0390: public void widgetDefaultSelected(SelectionEvent event) {
0391: }
0392:
0393: public void widgetSelected(SelectionEvent event) {
0394: final ListOfGoal goals = getSubtreeGoalsForETNode(((SourceElementFigure) ExecutionTreeView.this .selected)
0395: .getETNode());
0396: vd.stepOver(goals);
0397:
0398: }
0399: });
0400:
0401: // create visualize button
0402: item = new MenuItem(classMenu, SWT.PUSH);
0403: item.setText("Visualize Node");
0404: item.addSelectionListener(new SelectionListener() {
0405: public void widgetDefaultSelected(SelectionEvent event) {
0406: }
0407:
0408: public void widgetSelected(SelectionEvent event) {
0409: vd
0410: .visualize(((SourceElementFigure) ExecutionTreeView.this .selected)
0411: .getETNode().getITNodesArray()[0]);
0412:
0413: }
0414:
0415: });
0416:
0417: // create test case button
0418: item = new MenuItem(classMenu, SWT.PUSH);
0419: item.setText("Create Test Cases For Path");
0420: item.addSelectionListener(new SelectionListener() {
0421: public void widgetDefaultSelected(SelectionEvent event) {
0422: }
0423:
0424: public void widgetSelected(SelectionEvent event) {
0425:
0426: if (ExecutionTreeView.this .selected instanceof LeafNode) {
0427: ETLeafNode leaf = ((LeafNode) ExecutionTreeView.this .selected)
0428: .getETLeafNode();
0429: VBTBuilder builder = new VBTBuilder(leaf
0430: .getProofTreeNodes(),
0431: ModelGenerator.SIMPLIFY);
0432:
0433: if (!builder.succesful())
0434: MessageDialog
0435: .openError(PlatformUI.getWorkbench()
0436: .getActiveWorkbenchWindow()
0437: .getShell(),
0438: "Test Case Generation",
0439: "An error occured during test case generation");
0440:
0441: else if (builder.newProjectCreated())
0442:
0443: MessageDialog
0444: .openInformation(
0445: PlatformUI
0446: .getWorkbench()
0447: .getActiveWorkbenchWindow()
0448: .getShell(),
0449: "Test Case Generation",
0450: "A test case for the selected execution path was generated.\n"
0451: + "It was written to "
0452: + builder.getFileName()
0453: + "\n"
0454: + "in the default package of the new created project "
0455: + builder
0456: .getTestGenProject()
0457: .getName());
0458: else
0459: MessageDialog
0460: .openInformation(
0461: PlatformUI
0462: .getWorkbench()
0463: .getActiveWorkbenchWindow()
0464: .getShell(),
0465: "Test Case Generation",
0466: "A test case for the selected execution path was generated.\n"
0467: + "It was written to "
0468: + builder.getFileName()
0469: + " \nin the default packege of project "
0470: + builder
0471: .getTestGenProject()
0472: .getName());
0473: }
0474:
0475: }
0476: });
0477:
0478: }
0479:
0480: void doubleClick(SourceElementFigure node) {
0481: ICompilationUnit cu = node.getUnit();
0482: try {
0483: IEditorPart ed = JavaUI.openInEditor(cu);
0484: ISourceViewer viewer = (ISourceViewer) ed
0485: .getAdapter(ITextOperationTarget.class);
0486:
0487: int s = node.getASTNode().getStartPosition();
0488: int o = node.getASTNode().getLength();
0489: viewer.setSelectedRange(s, o);
0490: viewer.revealRange(s, o);
0491: } catch (PartInitException e) {
0492: e.printStackTrace();
0493: } catch (JavaModelException e) {
0494: e.printStackTrace();
0495: }
0496:
0497: this .maxmerge++;
0498: this .merged = 0;
0499: }
0500:
0501: private void fillLocalToolBar(IToolBarManager manager) {
0502: // manager.add(sletAction);
0503: // manager.add(msletAction);
0504: // //manager.
0505: // manager.add(this.useBranchLabelsAction);
0506: manager.add(decisionProcedureAction);
0507: manager.add(new Separator());
0508: manager.add(this .testCaseAction);
0509: // manager.add(stepIntoAction);
0510: // manager.add(stepOverAction);
0511: }
0512:
0513: private TreeBranch findBranch(TreeBranch b,
0514: ETMethodInvocationNode etn) {
0515:
0516: while (b != null) {
0517:
0518: if (b.getNode() instanceof MethodInvocationFigure) {
0519: MethodInvocationFigure mif = (MethodInvocationFigure) b
0520: .getNode();
0521: if (mif.getETNode() == etn) {
0522: return b;
0523: }
0524: }
0525: b = b.getParentTB();
0526: }
0527: return null;
0528:
0529: }
0530:
0531: // TODO move to VisualDebugger
0532: private ListOfGoal getSubtreeGoalsForETNode(ETNode etNode) {
0533: final ITNode[] itNodes = etNode.getITNodesArray();
0534: ListOfGoal goals = SLListOfGoal.EMPTY_LIST;
0535: for (int i = 0; i < itNodes.length; i++) {
0536: final ListOfGoal g = vd.getMediator().getProof()
0537: .getSubtreeGoals((itNodes[i].getNode()));
0538: goals = goals.prepend(g);
0539: }
0540: return goals;
0541:
0542: }
0543:
0544: private void hookShell() {
0545: Composite localShell = new Composite(parent, 0);
0546: // localShell.set
0547: GridData gdata = new GridData(GridData.FILL_VERTICAL);
0548: // gdata.minimumWidth=30;
0549: // gdata.grabExcessHorizontalSpace=true;
0550: localShell.setLayoutData(gdata);
0551:
0552: localShell.setLayout(new GridLayout());
0553:
0554: Group rootGroup = new Group(localShell, 0);
0555: rootGroup.setText("Properties");
0556: FontData data = rootGroup.getFont().getFontData()[0];
0557: data.setStyle(SWT.BOLD);
0558: rootGroup.setLayout(new GridLayout());
0559: rootGroup.setLayoutData(new GridData(200, SWT.DEFAULT));
0560:
0561: if (debug) {
0562: final Button orientation = new Button(rootGroup, SWT.RADIO);
0563: orientation.setText("Raw Tree");
0564: orientation
0565: .setSelection(ExecutionTree.treeStyle == ExecutionTree.RAWTREE);
0566: orientation.addSelectionListener(new SelectionAdapter() {
0567: public void widgetSelected(SelectionEvent e) {
0568: ExecutionTree.treeStyle = ExecutionTree.RAWTREE;
0569: refresh();
0570: }
0571: });
0572:
0573: final Button orientation2 = new Button(rootGroup, SWT.RADIO);
0574: orientation2.setText("Statement Level Execution Tree");
0575: orientation2
0576: .setSelection(ExecutionTree.treeStyle == ExecutionTree.SLET);
0577: orientation2.addSelectionListener(new SelectionAdapter() {
0578: public void widgetSelected(SelectionEvent e) {
0579: ExecutionTree.treeStyle = ExecutionTree.SLET;
0580: refresh();
0581: }
0582: });
0583:
0584: final Button orientation3 = new Button(rootGroup, SWT.RADIO);
0585: orientation3.setText("Statement Level Execution Tree2");
0586: orientation3
0587: .setSelection(ExecutionTree.treeStyle == ExecutionTree.SLET2);
0588: orientation3.addSelectionListener(new SelectionAdapter() {
0589: public void widgetSelected(SelectionEvent e) {
0590: ExecutionTree.treeStyle = ExecutionTree.SLET2;
0591: refresh();
0592: }
0593: });
0594:
0595: final Button orientation6 = new Button(rootGroup, SWT.RADIO);
0596: orientation6.setText("Statement Level Execution Tree3");
0597: orientation6
0598: .setSelection(ExecutionTree.treeStyle == ExecutionTree.SLET3);
0599: orientation6.addSelectionListener(new SelectionAdapter() {
0600: public void widgetSelected(SelectionEvent e) {
0601: ExecutionTree.treeStyle = ExecutionTree.SLET3;
0602: refresh();
0603: }
0604: });
0605:
0606: }
0607:
0608: if (debug) {
0609: Group rootGroup2 = new Group(localShell, 0);
0610: rootGroup.setText("Properties");
0611: FontData data2 = rootGroup2.getFont().getFontData()[0];
0612: data2.setStyle(SWT.BOLD);
0613: rootGroup2.setLayout(new GridLayout());
0614: final Button hideInfButton = new Button(rootGroup2,
0615: SWT.CHECK);
0616: hideInfButton.setText("Hide Infeasible Paths");
0617: hideInfButton.setSelection(hideInfeasible);
0618: hideInfButton.addSelectionListener(new SelectionAdapter() {
0619: public void widgetSelected(SelectionEvent e) {
0620: hideInfeasible = hideInfButton.getSelection();
0621: refresh();
0622: }
0623: });
0624: }
0625:
0626: final org.eclipse.swt.widgets.Label majorLabel = new org.eclipse.swt.widgets.Label(
0627: rootGroup, 0);
0628: majorLabel.setText("Major Spacing: 10");
0629: final Scale major = new Scale(rootGroup, 0);
0630: major.setLayoutData(new GridLayout());
0631: major.setLayoutData(new GridData(100, SWT.DEFAULT));
0632:
0633: major.setSize(200, 200);
0634: major.setMinimum(10);
0635: major.setIncrement(10);
0636: major.setMaximum(200);
0637: major.setSelection(50);
0638: major.addSelectionListener(new SelectionAdapter() {
0639: public void widgetSelected(SelectionEvent e) {
0640: root.setMajorSpacing(major.getSelection());
0641: majorLabel.setText("Major Spacing: "
0642: + root.getMajorSpacing());
0643: }
0644: });
0645:
0646: final org.eclipse.swt.widgets.Label minorLabel = new org.eclipse.swt.widgets.Label(
0647: rootGroup, 0);
0648: minorLabel.setText("Minor Spacing: 10");
0649: final Scale minor = new Scale(rootGroup, 0);
0650: minor.setLayoutData(new GridLayout());
0651: minor.setLayoutData(new GridData(100, SWT.DEFAULT));
0652:
0653: minor.setMinimum(10);
0654: minor.setIncrement(5);
0655: minor.setMaximum(100);
0656: minor.setSelection(30);
0657: minor.addSelectionListener(new SelectionAdapter() {
0658: public void widgetSelected(SelectionEvent e) {
0659: root.setMinorSpacing(minor.getSelection());
0660: minorLabel.setText("Minor Spacing: "
0661: + root.getMinorSpacing());
0662: }
0663: });
0664:
0665: // text = new Text(localShell,SWT.BORDER | SWT.H_SCROLL | SWT.V_SCROLL
0666: // );
0667: // text.setEditable(false);
0668: // Color white = new Color(null,255,255,255);
0669: // text.setBackground(white);
0670:
0671: Group bcGroup = new Group(localShell, 0);
0672: bcGroup.setBackground(ColorConstants.white);
0673: bcGroup.setText("Branch Condition");
0674: bcGroup.setLayoutData(new GridData(GridData.FILL_BOTH));
0675: bcGroup.setLayout(new GridLayout());
0676:
0677: bcListControl = new List(bcGroup, SWT.READ_ONLY | SWT.MULTI
0678: | SWT.BORDER | SWT.WRAP | SWT.V_SCROLL | SWT.H_SCROLL);
0679: // bcListControl.set
0680: bcListControl.setLayoutData(new GridData(GridData.FILL_BOTH));
0681: // l = new org.eclipse.swt.widgets.Label(bcGroup, SWT.WRAP |
0682: // SWT.V_SCROLL);
0683: // l.setLayoutData(new GridData(GridData.FILL_BOTH));
0684: // l.setBackground(ColorConstants.white);
0685:
0686: // text.setLayoutData(recvData);
0687: // l.setText("TEST TEST TEST TEST TEST TESTTEST TEST TESTTEST TEST
0688: // TESTTEST TEST TESTTEST TEST TESTTEST TEST TESTTEST TEST \n TESTTEST
0689: // TEST TEST");
0690:
0691: // l.set
0692: // text.s
0693: // text.setSize(new Point(100,100));
0694: // text.setBounds(2, y, width, height)
0695: // text.
0696:
0697: }
0698:
0699: private void makeActions() {
0700: sletAction = new Action("SLET", IAction.AS_RADIO_BUTTON) {
0701: public void run() {
0702: // showMessage("Action 1 executed");
0703: }
0704: };
0705:
0706: sletAction.setToolTipText("Statement Level Execuion Tree");
0707:
0708: useBranchLabelsAction = new Action("BC Labels",
0709: IAction.AS_CHECK_BOX) {
0710: public void run() {
0711: bcLabels = useBranchLabelsAction.isChecked();
0712: if (currentRoot != null) {
0713: // setLabelsVisible(bcLabels);
0714: if (cutTree)
0715: cutTree = false;
0716: else
0717: cutTree = true;
0718:
0719: }
0720: }
0721: };
0722:
0723: useBranchLabelsAction
0724: .setToolTipText("Label the the branches of the tree with branch conditions");
0725:
0726: msletAction = new Action("MSLET", IAction.AS_RADIO_BUTTON) {
0727: public void run() {
0728: // showMessage("Action 1 executed");
0729: }
0730: };
0731:
0732: msletAction
0733: .setToolTipText("Minimal Statement Level Execuion Tree");
0734:
0735: testCaseAction = new Action() {
0736: public void run() {
0737: if (vd.getMediator().getProof() == null)
0738: return;
0739: ListOfNode nodes = toList(vd.getMediator().getProof()
0740: .root().leavesIterator());
0741: VBTBuilder builder = new VBTBuilder(nodes,
0742: ModelGenerator.SIMPLIFY);
0743:
0744: if (!builder.succesful())
0745: MessageDialog
0746: .openError(PlatformUI.getWorkbench()
0747: .getActiveWorkbenchWindow()
0748: .getShell(),
0749: "Test Case Generation",
0750: "An error occured during test case generation");
0751:
0752: else if (builder.newProjectCreated())
0753:
0754: MessageDialog
0755: .openInformation(
0756: PlatformUI.getWorkbench()
0757: .getActiveWorkbenchWindow()
0758: .getShell(),
0759: "Test Case Generation",
0760: "Test cases for the current execution tree were generated.\n"
0761: +
0762:
0763: "They were written to "
0764: + builder.getFileName()
0765: + "\n"
0766: + "in the default package of the new created project "
0767: + builder
0768: .getTestGenProject()
0769: .getName());
0770: else
0771: MessageDialog
0772: .openInformation(
0773: PlatformUI.getWorkbench()
0774: .getActiveWorkbenchWindow()
0775: .getShell(),
0776: "Test Case Generation",
0777: "Test cases for the current execution tree were generated.\n"
0778: + "They were written to "
0779: + builder.getFileName()
0780: + "\nin the default package of project "
0781: + builder
0782: .getTestGenProject()
0783: .getName());
0784: }
0785:
0786: };
0787: testCaseAction
0788: .setToolTipText("Create Test Cases for the Execution Tree");
0789: testCaseAction.setText("Create Test Cases");
0790:
0791: decisionProcedureAction = new Action() {
0792: public void run() {
0793: if (vd.getMediator().getProof() == null)
0794: return;
0795: if (!vd.getMediator().ensureProofLoaded())
0796: return;
0797: new DecProcRunner(Main.getInstance(false)).run();
0798: }
0799:
0800: };
0801: decisionProcedureAction
0802: .setToolTipText("Runs an external decision procedure \nin order to find infeasible execution paths");
0803: decisionProcedureAction.setText("Run Decision Procedure");
0804: }
0805:
0806: public synchronized void refresh() {
0807: try {
0808: if (currentRoot == null) {
0809: return;
0810: }
0811:
0812: IFigure contents = root.getContentsPane();
0813:
0814: labels = new HashSet();
0815: TreeBranch s = null;
0816: if (!contents.getChildren().isEmpty()) {
0817: ((Figure) contents).removeAll();
0818: this .root.removeLabels();
0819: }
0820:
0821: if (ExecutionTree.getETNode() == null) {
0822: return;
0823: }
0824:
0825: if (ExecutionTree.treeStyle == ExecutionTree.SLET2) {
0826: this .root.addBranch(s = buildTreeBranch(ExecutionTree
0827: .getEtTreeBeforeMerge(), null));
0828: } else
0829:
0830: if (ExecutionTree.treeStyle == ExecutionTree.SLET3) {
0831: this .root.addBranch(s = buildTreeBranch(ExecutionTree
0832: .getETNode(), null));
0833: } else if (ExecutionTree.treeStyle == ExecutionTree.RAWTREE)
0834: root.addBranch(s = buildRawTree(currentRoot));
0835: if (s != null)
0836: root.addLabel(createConnection(root.getNode(), s
0837: .getNode(), "", false));
0838: } catch (Throwable t) {
0839: t.printStackTrace();
0840: }
0841: }
0842:
0843: private void removeSelection() {
0844: // remove exception marker
0845: if (this .unitOfLastExceptionMarker != null) {
0846: try {
0847: this .unitOfLastExceptionMarker.getResource()
0848: .deleteMarkers(
0849: "VisualDebugger.exceptionmarker",
0850: false, 1);
0851: } catch (CoreException e1) {
0852: e1.printStackTrace();
0853: }
0854: this .unitOfLastExceptionMarker = null;
0855:
0856: }
0857:
0858: // remove selection of node
0859: if (selected != null) {
0860: if (selected instanceof LeafNode) {
0861: ((LeafNode) selected).setSelected(false);
0862: } else if (selected instanceof SourceElementFigure) {
0863: ((SourceElementFigure) selected).setSelected(false);
0864: } else if (selected instanceof MethodInvocationFigure) {
0865: ((MethodInvocationFigure) selected).setSelected(false);
0866: } else if (selected instanceof MethodReturnFigure) {
0867: ((MethodReturnFigure) selected).setSelected(false);
0868: }
0869: }
0870:
0871: if (this .selectedMIN != null) {
0872: selectedMIN.setSelected(false);
0873: }
0874:
0875: }
0876:
0877: private void repaintConnections() {
0878:
0879: IFigure contents = root.getContentsPane();
0880: labels = new HashSet();
0881:
0882: if (!contents.getChildren().isEmpty()) {
0883: this .root.removeLabels();
0884: }
0885:
0886: }
0887:
0888: private void setBranchConditionText(ETNode etn) {
0889:
0890: if (etn != null && etn.getSimplifiedBc() != null
0891: && etn.getParent() != null
0892: && etn.getParent().getChildrenList().size() > 1) {
0893:
0894: final Term[] bc = etn.getSimplifiedBc().toArray();
0895: final String[] termsString = new String[bc.length];
0896:
0897: // text.setItems();
0898: for (int i = 0; i < bc.length; i++) {
0899: termsString[i] = (vd.prettyPrint(bc[i]));
0900: }
0901:
0902: bcListControl.setItems(termsString);
0903: } else
0904: bcListControl.setItems(new String[0]);
0905:
0906: }
0907:
0908: /**
0909: * Passing the focus request to the viewer's control.
0910: */
0911: public void setFocus() {
0912:
0913: }
0914:
0915: private void setLeafNodeSelected(LeafNode node) {
0916: this .removeSelection();
0917:
0918: selected = node;
0919: node.setSelected(true);
0920: final ETLeafNode ln = node.getETLeafNode();
0921: this .setBranchConditionText(ln);
0922:
0923: if (ln.getExpression() != null) {
0924: SourceElementId id = ln.getExpression();
0925: Expression expr = visualdebugger.Activator.getDefault()
0926: .getExpression(id);
0927: ICompilationUnit unit = visualdebugger.Activator
0928: .getDefault().getCompilationUnit(id);
0929: try {
0930: IEditorPart ed = JavaUI.openInEditor(unit);
0931: ISourceViewer viewer = (ISourceViewer) ed
0932: .getAdapter(ITextOperationTarget.class);
0933: int s = expr.getStartPosition();
0934: int o = expr.getLength();
0935: viewer.setSelectedRange(s, o);
0936: viewer.revealRange(s, o);
0937: } catch (PartInitException e) {
0938: // TODO Auto-generated catch block
0939: e.printStackTrace();
0940: } catch (JavaModelException e) {
0941: // TODO Auto-generated catch block
0942: e.printStackTrace();
0943: }
0944: // ____
0945:
0946: try {
0947: Map map = new HashMap();
0948: int s = expr.getStartPosition();
0949: int o = expr.getLength();
0950:
0951: // map.put("StatementId", visitor.getStatementId());
0952: // MarkerUtilities.setLineNumber(map, 10);
0953: MarkerUtilities.setCharStart(map, s);
0954: MarkerUtilities.setCharEnd(map, s + o);
0955: MarkerUtilities.setMessage(map,
0956: "Possible Uncaught Exception: "
0957: + ln.getExceptionName());
0958:
0959: MarkerUtilities.createMarker(unit.getResource(), map,
0960: "VisualDebugger.exceptionmarker");
0961: unitOfLastExceptionMarker = unit;
0962:
0963: } catch (CoreException e) {
0964: // TODO Auto-generated catch block
0965: e.printStackTrace();
0966: }
0967:
0968: }
0969:
0970: vd.fireDebuggerEvent(new DebuggerEvent(
0971: DebuggerEvent.NODE_SELECTED, node.getETLeafNode()));
0972:
0973: }
0974:
0975: void setSelected(MethodReturnFigure node) {
0976: this .removeSelection();
0977: selected = node;
0978: node.setSelected(true);
0979:
0980: ETMethodReturnNode etn = (node).getETNode();
0981:
0982: this .setBranchConditionText(etn);
0983: TreeBranch min = this .findBranch((TreeBranch) node.getParent(),
0984: etn.getParent().getLastMethodInvocation());
0985: this .selectedMIN = ((MethodInvocationFigure) min.getNode());
0986: ((MethodInvocationFigure) min.getNode()).setSelected(true);
0987: vd.fireDebuggerEvent(new DebuggerEvent(
0988: DebuggerEvent.NODE_SELECTED, node.getETNode()));
0989: }
0990:
0991: void setSelected(SourceElementFigure node) {
0992: this .removeSelection();
0993: selected = node;
0994: node.setSelected(true);
0995:
0996: ETNode etn = (node).getETNode();
0997: this .setBranchConditionText(etn);
0998: vd.fireDebuggerEvent(new DebuggerEvent(
0999: DebuggerEvent.NODE_SELECTED, node.getETNode()));
1000: }
1001:
1002: public void startRefreshThread() {
1003: Display display = shell.getDisplay();
1004: final Thread barThread = new Thread("PBarThread") {
1005: public void run() {
1006: ExecutionTreeView.this .refresh();
1007: }
1008: };
1009: display.asyncExec(barThread);
1010: }
1011:
1012: private ListOfNode toList(IteratorOfNode it) {
1013: ListOfNode result = SLListOfNode.EMPTY_LIST;
1014: while (it.hasNext()) {
1015: result = result.append(it.next());
1016:
1017: }
1018: return result;
1019:
1020: }
1021:
1022: public synchronized void update(DebuggerEvent event) {
1023: if (event.getType() == DebuggerEvent.TREE_CHANGED) {
1024: this .currentRoot = (ITNode) event.getSubject();
1025: startRefreshThread();
1026: } else if (event.getType() == DebuggerEvent.TEST_RUN_FAILED) {
1027: final VisualDebugger.TestCaseIdentifier tci = (VisualDebugger.TestCaseIdentifier) event
1028: .getSubject();
1029: Display display = shell.getDisplay();
1030: final Thread barThread = new Thread("Failed Test C Thread") {
1031: public void run() {
1032: VisualDebugger
1033: .print("Execution Tree view: failed tc: "
1034: + tci);
1035: Node n = vd.getNodeForTC(tci.getFile(), tci
1036: .getMethod());
1037: VisualDebugger.print("Node found: " + n.serialNr());
1038: if (n != null) {
1039: TreeBranch tb = root.findNode(n);
1040: if (tb != null) {
1041:
1042: tb.markBranch();
1043: }
1044:
1045: }
1046:
1047: MessageDialog
1048: .openInformation(
1049: PlatformUI.getWorkbench()
1050: .getActiveWorkbenchWindow()
1051: .getShell(),
1052: "Test Case Generation",
1053: "Test run of method "
1054: + tci.getMethod()
1055: + " in file "
1056: + tci.getFile()
1057: + " failed.\n"
1058: + "The corresponding execution path in the execution tree is highlighted.");
1059:
1060: }
1061: };
1062: display.asyncExec(barThread);
1063:
1064: } else if (event.getType() == DebuggerEvent.PROJECT_LOADED_SUCCESSFUL) {
1065: this .setBranchConditionText(null);
1066: // this.root.removeAll();
1067:
1068: }
1069:
1070: }
1071:
1072: }
|