001: package visualdebugger.actions;
002:
003: import java.io.File;
004: import java.io.FileWriter;
005: import java.io.IOException;
006: import java.util.*;
007:
008: import org.eclipse.core.resources.IProject;
009: import org.eclipse.core.runtime.CoreException;
010: import org.eclipse.jdt.core.*;
011: import org.eclipse.jdt.core.dom.*;
012: import org.eclipse.jface.action.IAction;
013: import org.eclipse.jface.dialogs.MessageDialog;
014: import org.eclipse.jface.text.BadLocationException;
015: import org.eclipse.jface.text.Document;
016: import org.eclipse.jface.viewers.ISelection;
017: import org.eclipse.jface.viewers.StructuredSelection;
018: import org.eclipse.jface.window.Window;
019: import org.eclipse.text.edits.MalformedTreeException;
020: import org.eclipse.text.edits.TextEdit;
021: import org.eclipse.text.edits.UndoEdit;
022: import org.eclipse.ui.IActionDelegate;
023: import org.eclipse.ui.IObjectActionDelegate;
024: import org.eclipse.ui.IWorkbenchPart;
025: import org.eclipse.ui.PlatformUI;
026:
027: import visualdebugger.views.InsertSepVisitor;
028: import de.uka.ilkd.key.casetool.eclipse.EclipseSignaturesHelper;
029: import de.uka.ilkd.key.casetool.eclipse.MethodPOSelectionDialog;
030: import de.uka.ilkd.key.collection.ListOfString;
031: import de.uka.ilkd.key.collection.SLListOfString;
032: import de.uka.ilkd.key.gui.JMLEclipseAdapter;
033: import de.uka.ilkd.key.gui.JMLPOAndSpecProvider;
034: import de.uka.ilkd.key.gui.Main;
035: import de.uka.ilkd.key.jml.JMLMethodSpec;
036: import de.uka.ilkd.key.jml.JMLSpec;
037: import de.uka.ilkd.key.proof.init.*;
038: import de.uka.ilkd.key.util.ExceptionHandlerException;
039: import de.uka.ilkd.key.visualdebugger.DebuggerEvent;
040: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
041:
042: public class StartVisualDebuggerAction implements IObjectActionDelegate {
043:
044: public static boolean allInvariants = false;
045:
046: // public static boolean allInvariants=false;
047:
048: protected static final int PROJECT_ALREADY_OPEN = 1;
049:
050: protected static final int PROJECT_LOAD_CANCELED = 3;
051:
052: protected static final int PROJECT_LOAD_FAILED = 4;
053:
054: protected static final int PROJECT_LOAD_SUCESSFUL = 2;
055:
056: public static void deleteTree(File path) {
057:
058: final File[] files = path.listFiles();
059: for (int i = 0; i < files.length; i++) {
060: if (files[i].isDirectory())
061: deleteTree(files[i]);
062: files[i].delete();
063: }
064: path.delete();
065: }
066:
067: public static void delTemporaryDirectory() {
068: File dir = new File(VisualDebugger.tempDir);
069: StartVisualDebuggerAction.deleteTree(dir);
070: if (!dir.exists())
071: dir.mkdirs();
072:
073: }
074:
075: private CompilationUnit debugCU;
076:
077: // quick-and-dirty for syncExec(dialog.open()) in swt thread
078: MethodPOSelectionDialog dialog;
079:
080: boolean nokey = false;
081:
082: ISelection selection;
083:
084: int state;
085:
086: HashSet types = new HashSet();
087:
088: /**
089: * Constructor for Action1.
090: */
091: public StartVisualDebuggerAction() {
092: super ();
093: }
094:
095: protected synchronized int assertProjectParsed(IProject project,
096: boolean jmlBrowserIntended) {
097:
098: // project's java model has not been loaded into KeY yet, do this
099: // now
100:
101: final String inputName = "visualDebugger-project_"
102: + project.getName();
103: final File location = new File(VisualDebugger.tempDir);
104:
105: if (!location.exists()) {
106: location.mkdirs();
107: }
108:
109: Main main = Main.getInstance(false);
110:
111: JavaInput input;
112:
113: if (jmlBrowserIntended) {
114:
115: input = new JavaInputWithJMLSpecBrowser(inputName,
116: location, false, main.getProgressMonitor());
117:
118: } else {
119: input = new JavaInput(inputName, location, main
120: .getProgressMonitor());
121: }
122:
123: ProblemInitializer problemInit = new ProblemInitializer(main);
124:
125: String error = "Prover init for " + location + " failed.";
126: try {
127: problemInit.startProver(input, input);
128: error = "";
129: } catch (ProofInputException pie) {
130: error = pie.getMessage();
131: } catch (ExceptionHandlerException ehe) {
132: error = ehe.getCause() == null ? ehe.getMessage() : ehe
133: .getCause().getMessage();
134: }
135:
136: if (error.length() == 0) {
137: return PROJECT_LOAD_SUCESSFUL;
138: } else {
139: MessageDialog.openError(PlatformUI.getWorkbench()
140: .getActiveWorkbenchWindow().getShell(),
141: "Error loading java model into KeY prover",
142: "While loading this project, the following error"
143: + " occured:\n" + error);
144: return PROJECT_LOAD_FAILED;
145: }
146:
147: }
148:
149: /**
150: * creates class <tt>Debug</tt> implementing the <tt>sep</tt> methods
151: * representing breakpoints.
152: *
153: * @param ast
154: * the AST with the environment where to insert the class
155: * @return the compilation unit containing the created class
156: */
157: private CompilationUnit createDebuggerClass(AST ast) {
158: CompilationUnit unit = ast.newCompilationUnit();
159:
160: PackageDeclaration packageDeclaration = ast
161: .newPackageDeclaration();
162: packageDeclaration.setName(ast
163: .newSimpleName(VisualDebugger.debugPackage));
164: unit.setPackage(packageDeclaration);
165: ImportDeclaration importDeclaration = ast
166: .newImportDeclaration();
167: TypeDeclaration type = ast.newTypeDeclaration();
168: type.setInterface(false);
169: Modifier mf = ast
170: .newModifier(Modifier.ModifierKeyword.PUBLIC_KEYWORD);
171:
172: type.modifiers().add(mf);
173:
174: type.setName(ast.newSimpleName(VisualDebugger.debugClass));
175:
176: unit.types().add(type);
177:
178: return unit;
179: }
180:
181: private JMLMethodSpec getMethodSpec(Vector methodSpecs) {
182: for (Iterator it = methodSpecs.iterator(); it.hasNext();) {
183: Object next = it.next();
184: if (next instanceof JMLMethodSpec) {
185: return (JMLMethodSpec) next;
186: }
187:
188: }
189: // TODO Auto-generated method stub
190: return null;
191: }
192:
193: private MethodDeclaration getSepMethodDeclaration(AST ast) {
194:
195: MethodDeclaration methodDeclaration = ast
196: .newMethodDeclaration();
197: methodDeclaration.setConstructor(false);
198: Modifier mf = ast
199: .newModifier(Modifier.ModifierKeyword.STATIC_KEYWORD);
200: methodDeclaration.modifiers().add(mf);
201:
202: mf = ast.newModifier(Modifier.ModifierKeyword.PUBLIC_KEYWORD);
203: methodDeclaration.modifiers().add(mf);
204:
205: methodDeclaration.setName(ast.newSimpleName("sep"));
206: methodDeclaration.setReturnType2(ast
207: .newPrimitiveType(PrimitiveType.VOID));
208: SingleVariableDeclaration variableDeclaration = ast
209: .newSingleVariableDeclaration();
210:
211: variableDeclaration.setType(ast
212: .newPrimitiveType(PrimitiveType.INT));
213: variableDeclaration.setName(ast.newSimpleName("id"));
214: methodDeclaration.parameters().add(variableDeclaration);
215: org.eclipse.jdt.core.dom.Block block = ast.newBlock();
216: methodDeclaration.setBody(block);
217: return methodDeclaration;
218: }
219:
220: private MethodDeclaration getSepMethodDeclaration(AST ast, Type type) {
221:
222: MethodDeclaration methodDeclaration = ast
223: .newMethodDeclaration();
224: methodDeclaration.setConstructor(false);
225: Modifier mf = ast
226: .newModifier(Modifier.ModifierKeyword.STATIC_KEYWORD);
227: methodDeclaration.modifiers().add(mf);
228:
229: mf = ast.newModifier(Modifier.ModifierKeyword.PUBLIC_KEYWORD);
230: methodDeclaration.modifiers().add(mf);
231:
232: methodDeclaration.setName(ast
233: .newSimpleName(VisualDebugger.sepName));
234:
235: methodDeclaration.setReturnType2(type);
236:
237: SingleVariableDeclaration variableDeclaration = ast
238: .newSingleVariableDeclaration();
239:
240: variableDeclaration.setType(ast
241: .newPrimitiveType(PrimitiveType.INT));
242: variableDeclaration.setName(ast.newSimpleName("id"));
243:
244: SingleVariableDeclaration variableDeclaration2 = ast
245: .newSingleVariableDeclaration();
246:
247: variableDeclaration2.setType((Type) ASTNode.copySubtree(ast,
248: type));
249: variableDeclaration2.setName(ast.newSimpleName("expr"));
250:
251: methodDeclaration.parameters().add(variableDeclaration);
252: methodDeclaration.parameters().add(variableDeclaration2);
253:
254: org.eclipse.jdt.core.dom.Block block = ast.newBlock();
255: ReturnStatement ret = ast.newReturnStatement();
256: ret.setExpression(ast.newSimpleName("expr"));
257: block.statements().add(ret);
258:
259: methodDeclaration.setBody(block);
260: // System.out.println(methodDeclaration);
261: return methodDeclaration;
262: }
263:
264: private MethodDeclaration getSepMethodDeclarationDEPRECATED(
265: AST ast, ITypeBinding type) {
266:
267: MethodDeclaration methodDeclaration = ast
268: .newMethodDeclaration();
269: methodDeclaration.setConstructor(false);
270: Modifier mf = ast
271: .newModifier(Modifier.ModifierKeyword.STATIC_KEYWORD);
272: methodDeclaration.modifiers().add(mf);
273:
274: mf = ast.newModifier(Modifier.ModifierKeyword.PUBLIC_KEYWORD);
275: methodDeclaration.modifiers().add(mf);
276:
277: methodDeclaration.setName(ast.newSimpleName("sep"));
278:
279: SimpleType loggerType = ast.newSimpleType(ast.newName(type
280: .getQualifiedName()));
281:
282: methodDeclaration.setReturnType2(loggerType);
283:
284: SingleVariableDeclaration variableDeclaration = ast
285: .newSingleVariableDeclaration();
286:
287: variableDeclaration.setType(ast
288: .newPrimitiveType(PrimitiveType.INT));
289: variableDeclaration.setName(ast.newSimpleName("id"));
290:
291: SingleVariableDeclaration variableDeclaration2 = ast
292: .newSingleVariableDeclaration();
293:
294: variableDeclaration2.setType((Type) ASTNode.copySubtree(ast,
295: loggerType));
296: variableDeclaration2.setName(ast.newSimpleName("expr"));
297:
298: methodDeclaration.parameters().add(variableDeclaration);
299: methodDeclaration.parameters().add(variableDeclaration2);
300:
301: org.eclipse.jdt.core.dom.Block block = ast.newBlock();
302: ReturnStatement ret = ast.newReturnStatement();
303: ret.setExpression(ast.newSimpleName("expr"));
304: block.statements().add(ret);
305:
306: methodDeclaration.setBody(block);
307: // System.out.println(methodDeclaration);
308: return methodDeclaration;
309: }
310:
311: private Type getType(AST ast, ITypeBinding bind) {// TODO !!!!!!!!!
312: return ast.newSimpleType(ast.newName(bind.getQualifiedName()));
313: }
314:
315: public final ICompilationUnit[] getTypes(IJavaProject javaproject) {
316: ArrayList typeList = new ArrayList();
317: try {
318: IPackageFragmentRoot[] roots = javaproject
319: .getPackageFragmentRoots();
320: // System.out.println("package roots "+roots);
321: for (int i = 0; i < roots.length; i++) {
322: IPackageFragmentRoot root = roots[i];
323: if (root.getKind() == IPackageFragmentRoot.K_SOURCE) {
324: IJavaElement[] javaElements = root.getChildren();
325: for (int j = 0; j < javaElements.length; j++) {
326: IJavaElement javaElement = javaElements[j];
327: if (javaElement.getElementType() == IJavaElement.PACKAGE_FRAGMENT) {
328: IPackageFragment pf = (IPackageFragment) javaElement;
329: // System.out.println("pf "+pf);
330: ICompilationUnit[] compilationUnits = pf
331: .getCompilationUnits();
332: typeList.addAll(Arrays
333: .asList(compilationUnits));
334:
335: }
336: }
337: }
338: }
339: } catch (CoreException e) {
340: e.printStackTrace();
341: }
342: ICompilationUnit[] types = new ICompilationUnit[typeList.size()];
343: return (ICompilationUnit[]) typeList.toArray(types);
344: }
345:
346: public void insertSeps(ICompilationUnit unit) {
347: String source = "";
348:
349: try {
350: source = unit.getBuffer().getContents();
351: } catch (JavaModelException e) {
352: // TODO Auto-generated catch block
353: e.printStackTrace();
354: }
355: Document document = new Document(source);
356:
357: // creation of DOM/AST from a ICompilationUnit
358: ASTParser parser = ASTParser.newParser(AST.JLS3);
359: parser.setResolveBindings(true);
360:
361: parser.setSource(unit);
362:
363: CompilationUnit astRoot = (CompilationUnit) parser
364: .createAST(null);
365:
366: InsertSepVisitor visitor = new InsertSepVisitor();
367: astRoot.recordModifications();
368:
369: TypeDeclaration td = (TypeDeclaration) astRoot.types().get(0);
370:
371: ImportDeclaration importDeclaration = astRoot.getAST()
372: .newImportDeclaration();
373:
374: importDeclaration.setName(astRoot.getAST().newSimpleName(
375: VisualDebugger.debugPackage));
376: importDeclaration.setOnDemand(true);
377: astRoot.imports().add(importDeclaration);
378:
379: astRoot.accept(visitor);
380: // creation of ASTRewrite
381: types.addAll(visitor.getTypes());
382:
383: TextEdit edits = astRoot.rewrite(document, null);
384: try {
385: UndoEdit undo = edits.apply(document);
386: } catch (MalformedTreeException e) {
387: e.printStackTrace();
388: } catch (BadLocationException e) {
389: if (VisualDebugger.vdInDebugMode)
390: e.printStackTrace();
391: }
392:
393: // computation of the new source code
394: try {
395: edits.apply(document);
396: } catch (MalformedTreeException e) {
397:
398: e.printStackTrace();
399: } catch (BadLocationException e) {
400: if (VisualDebugger.vdInDebugMode) {
401: System.out.println(e.getLocalizedMessage());
402: System.out.println(e.getMessage());
403: e.printStackTrace();
404: }
405: }
406: String newSource = document.get();
407:
408: String s = null;
409:
410: s = newSource;
411: // s = astRoot.toString();
412: String fn = unit.getPath().toString();
413: String d = VisualDebugger.tempDir
414: + fn.substring(1, fn.lastIndexOf(File.separator));
415: File fil = new File(d);
416: if (!fil.exists())
417: fil.mkdirs();
418:
419: fn = fn.substring(fn.lastIndexOf(File.separator) + 1);
420:
421: File pcFile = new File(fil, fn);
422:
423: try {
424: FileWriter fw = new FileWriter(pcFile);
425: fw.write(s);
426: fw.flush();
427: fw.close();
428: } catch (IOException e) {
429: e.printStackTrace();
430: }
431:
432: }
433:
434: public void insertSeps(IJavaProject project) {
435: ICompilationUnit[] units = getTypes(project);
436: types = new HashSet();
437: debugCU = createDebuggerClass(AST.newAST(AST.JLS3));
438:
439: for (int i = 0; i < units.length; i++) {
440: insertSeps(units[i]);
441: }
442:
443: TypeDeclaration td = (TypeDeclaration) debugCU.types().get(0);
444:
445: for (Iterator it = types.iterator(); it.hasNext();) {
446: ITypeBinding next = (ITypeBinding) it.next();
447: td.bodyDeclarations().add(
448: getSepMethodDeclaration(debugCU.getAST(), this
449: .getType(debugCU.getAST(), next)));
450:
451: }
452:
453: td.bodyDeclarations().add(
454: getSepMethodDeclaration(debugCU.getAST(), debugCU
455: .getAST().newPrimitiveType(PrimitiveType.INT)));
456: td.bodyDeclarations()
457: .add(
458: getSepMethodDeclaration(debugCU.getAST(),
459: debugCU.getAST().newPrimitiveType(
460: PrimitiveType.BYTE)));
461: td.bodyDeclarations().add(
462: getSepMethodDeclaration(debugCU.getAST(), debugCU
463: .getAST().newPrimitiveType(
464: PrimitiveType.BOOLEAN)));
465: td.bodyDeclarations().add(
466: getSepMethodDeclaration(debugCU.getAST()));
467:
468: String projectPath = project.getPath().toOSString()
469: .substring(1);
470:
471: final String pathToDebugPackage = VisualDebugger.tempDir
472: + projectPath + File.separator
473: + VisualDebugger.debugPackage + File.separator;
474:
475: final String pathToDebugClass = pathToDebugPackage
476: + VisualDebugger.debugClass + ".java";
477:
478: new File(pathToDebugPackage).mkdirs();
479:
480: File pcFile = new File(pathToDebugClass);
481: try {
482: pcFile.createNewFile();
483: } catch (IOException e1) {
484: e1.printStackTrace();
485: }
486:
487: try {
488: final FileWriter fw = new FileWriter(pcFile);
489: // FIXME: toString is only for debugging purpose, no warranty that it will
490: // always generate a compilable output
491: fw.write(debugCU.toString());
492: fw.flush();
493: fw.close();
494: } catch (IOException e) {
495: e.printStackTrace();
496: }
497:
498: }
499:
500: /**
501: * @see IActionDelegate#rune(IAction)
502: */
503: public void run(IAction action) {
504:
505: if (selection == null) {
506: return;
507: }
508:
509: VisualDebugger.setDebuggingMode(true);
510:
511: final Main keyProver = Main.getInstance(false);
512:
513: // remove old environments
514: while (VisualDebugger.getVisualDebugger().getMediator()
515: .getProof() != null) {
516: keyProver.closeTaskWithoutIntercation();
517: }
518:
519: VisualDebugger.getVisualDebugger();// .prepareKeY();
520:
521: if (selection != null
522: && selection instanceof StructuredSelection) {
523: IMethod selectedMethod = (IMethod) ((StructuredSelection) selection)
524: .getFirstElement();
525: ICompilationUnit srcFile = selectedMethod
526: .getCompilationUnit();
527:
528: if (srcFile == null) {
529: MessageDialog.openError(PlatformUI.getWorkbench()
530: .getActiveWorkbenchWindow().getShell(),
531: "No Source Found.",
532: "The method you selected does not exist in source form. "
533: + "It cannot be used for a proof.");
534: return;
535: }
536:
537: File location = new File(VisualDebugger.tempDir);
538:
539: if (location.exists()) {
540: delTemporaryDirectory();
541: } else {
542: location.mkdirs();
543: }
544:
545: insertSeps(srcFile.getJavaProject());
546:
547: // TODO generalize to consider packageFragmentRoots (needed to
548: // support
549: // special source locations like folders only linked into the
550: // eclipse
551: // project
552: IProject project = srcFile.getJavaProject().getProject();
553:
554: visualdebugger.Activator.getDefault().setProject(
555: srcFile.getJavaProject());
556:
557: visualdebugger.Activator.getDefault().setIProject(project);
558: // assure the sources are parsed
559: int status = assertProjectParsed(project, false);
560:
561: if (status == PROJECT_ALREADY_OPEN
562: || status == PROJECT_LOAD_SUCESSFUL) {
563: // determine the encapsulating class of the selected method
564: IType declaringType = selectedMethod.getDeclaringType();
565:
566: // extract signature of method
567: // int paramCount = selectedMethod.getNumberOfParameters();
568: try {
569: // selectedMethod.get
570: String[] parameterNames = selectedMethod
571: .getParameterNames();
572: String[] parameterTypes = selectedMethod
573: .getParameterTypes();
574: ListOfString sigStrings = SLListOfString.EMPTY_LIST;
575:
576: for (int i = 0; i < parameterNames.length; i++) {
577: String javaType = EclipseSignaturesHelper
578: .determineJavaType(parameterTypes[i],
579: declaringType);
580: if (javaType != null) {
581: sigStrings = sigStrings.append(javaType);
582: } else {
583: MessageDialog
584: .openError(
585: PlatformUI
586: .getWorkbench()
587: .getActiveWorkbenchWindow()
588: .getShell(),
589: "Error determining signature types !",
590: "Could not resolve type "
591: + parameterTypes[i]
592: + " of the method's parameter "
593: + parameterNames[i]
594: + " !"
595: + " This is probably a syntax problem, check your import statements.");
596: return;
597: }
598: }
599:
600: keyProver.toBack();
601: Main.setStandalone(false);
602:
603: final JMLPOAndSpecProvider provider = keyProver
604: .getJMLPOAndSpecProvider();
605:
606: ((JMLEclipseAdapter) provider)
607: .setMainVisible(false);
608:
609: Vector methodSpecs = provider
610: .getMethodSpecs(declaringType
611: .getFullyQualifiedName(),
612: selectedMethod.getElementName(),
613: sigStrings);
614: final JMLMethodSpec spec = getMethodSpec(methodSpecs);
615: if (spec != null) {
616: startProver("Debugging "
617: + selectedMethod.getElementName(),
618: provider, spec, allInvariants, false,
619: false);
620: } else {
621: dialog = new MethodPOSelectionDialog(PlatformUI
622: .getWorkbench()
623: .getActiveWorkbenchWindow().getShell(),
624: methodSpecs);
625: state = dialog.open();
626:
627: boolean allInvariants = dialog
628: .isAllInvariantsSelected();
629: boolean addInvariantsToPostCondition = dialog
630: .isAddInvariantsToPostConditionSelected();
631:
632: if (state == Window.OK) {
633: Object selectedPO = dialog
634: .getSelectionOnOK()
635: .getFirstElement();
636:
637: // TODO complete this step-by-step
638: // assignable: see JML Specification browser
639: // boolean assignablePO = (selectedPO instanceof
640: // AssignableCheckProofOblInput);
641: if (selectedPO instanceof AssignableCheckProofOblInput) {
642: AssignableCheckProofOblInput assignableCheckPO = (AssignableCheckProofOblInput) selectedPO;
643: startProver("Debugging "
644: + selectedMethod
645: .getElementName(),
646: provider, assignableCheckPO
647: .getSpec(),
648: allInvariants,
649: addInvariantsToPostCondition,
650: true);
651: } else if (selectedPO instanceof JMLSpec) {
652: startProver("Debugging "
653: + selectedMethod
654: .getElementName(),
655: provider, (JMLSpec) selectedPO,
656: allInvariants,
657: addInvariantsToPostCondition,
658: false);
659: } else {
660: // TODO handle error case
661: }
662: }
663: }
664: } catch (JavaModelException e) {
665: // TODO Auto-generated catch block
666: e.printStackTrace();
667: }
668: }
669: }
670:
671: VisualDebugger.getVisualDebugger().initialize();
672: }
673:
674: /**
675: * @see IActionDelegate#selectionChanged(IAction, ISelection)
676: */
677: public void selectionChanged(IAction action, ISelection selection) {
678: this .selection = selection;
679: }
680:
681: /**
682: * @see IObjectActionDelegate#setActivePart(IAction, IWorkbenchPart)
683: */
684: public void setActivePart(IAction action, IWorkbenchPart targetPart) {
685: if (selection == null) {
686: action.setEnabled(false);
687: }
688: action.setEnabled(true);
689: }
690:
691: private void startProver(String debuggerEventMsg,
692: final JMLPOAndSpecProvider provider, final JMLSpec spec,
693: final boolean allInvariants, final boolean invPost,
694: final boolean assignable) {
695: VisualDebugger.getVisualDebugger().fireDebuggerEvent(
696: new DebuggerEvent(
697: DebuggerEvent.PROJECT_LOADED_SUCCESSFUL,
698: debuggerEventMsg));
699: provider.createPOandStartProver(spec, allInvariants, invPost,
700: assignable);
701: }
702: }
|