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: // This file is part of KeY - Integrated Deductive Software Design
009: // Copyright (C) 2001-2005 Universitaet Karlsruhe, Germany
010: // Universitaet Koblenz-Landau, Germany
011: // Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016: //
017:
018: package de.uka.ilkd.key.proof;
019:
020: import java.io.File;
021: import java.io.FileInputStream;
022: import java.io.FileNotFoundException;
023: import java.io.StringReader;
024: import java.util.Iterator;
025: import java.util.LinkedList;
026: import java.util.Stack;
027: import java.util.Vector;
028:
029: import de.uka.ilkd.key.gui.*;
030: import de.uka.ilkd.key.gui.configuration.ProofSettings;
031: import de.uka.ilkd.key.java.ProgramElement;
032: import de.uka.ilkd.key.java.Services;
033: import de.uka.ilkd.key.logic.*;
034: import de.uka.ilkd.key.logic.op.*;
035: import de.uka.ilkd.key.parser.*;
036: import de.uka.ilkd.key.pp.AbbrevMap;
037: import de.uka.ilkd.key.pp.PresentationFeatures;
038: import de.uka.ilkd.key.proof.init.*;
039: import de.uka.ilkd.key.proof.mgt.OldOperationContract;
040: import de.uka.ilkd.key.rule.*;
041: import de.uka.ilkd.key.util.ExceptionHandlerException;
042: import de.uka.ilkd.key.util.KeYExceptionHandler;
043: import de.uka.ilkd.key.proof.decproc.DecisionProcedureSmtAuflia;
044:
045: public class ProblemLoader implements Runnable {
046:
047: File file;
048: Main main;
049: KeYMediator mediator;
050:
051: Proof proof = null;
052: IteratorOfNode children = null;
053:
054: Node currNode = null;
055: KeYExceptionHandler exceptionHandler = null;
056: Goal currGoal = null;
057: String currTacletName = null;
058: int currFormula = 0;
059: PosInTerm currPosInTerm = PosInTerm.TOP_LEVEL;
060: OldOperationContract currContract = null;
061: Stack stack = new Stack();
062: LinkedList loadedInsts = null;
063: ListOfIfFormulaInstantiation ifSeqFormulaList = SLListOfIfFormulaInstantiation.EMPTY_LIST;
064:
065: ProblemInitializer init;
066: InitConfig iconfig;
067:
068: /** if set uses the current problem instance instead of a new one */
069: boolean keepProblem;
070:
071: /** the profile to be used */
072: private Profile profile;
073:
074: private SwingWorker worker;
075:
076: public ProblemLoader(File file, Main main, Profile profile) {
077: this (file, main, profile, false);
078: }
079:
080: public ProblemLoader(File file, Main main, Profile profile,
081: boolean keepProblem) {
082: this .main = main;
083: mediator = main.mediator();
084: this .file = file;
085: this .profile = profile;
086: this .exceptionHandler = mediator.getExceptionHandler();
087: this .keepProblem = keepProblem;
088: }
089:
090: public void run() {
091: /* Invoking start() on the SwingWorker causes a new Thread
092: * to be created that will call construct(), and then
093: * finished(). Note that finished() is called even if
094: * the worker is interrupted because we catch the
095: * InterruptedException in doWork().
096: */
097: worker = new SwingWorker() {
098: public Object construct() {
099: Object res = doWork();
100: return res;
101: }
102:
103: public void finished() {
104: mediator.startInterface(true);
105: String msg = (String) get();
106: if (!"".equals(msg)) {
107: if (Main.batchMode) {
108: System.exit(-1);
109: } else {
110: new ExceptionDialog(mediator.mainFrame(),
111: exceptionHandler.getExceptions());
112: exceptionHandler.clear();
113: }
114: } else {
115: PresentationFeatures.initialize(mediator.func_ns(),
116: mediator.getNotationInfo(), mediator
117: .getSelectedProof());
118: }
119: if (Main.batchMode) {
120: //System.out.println("Proof: " +proof.openGoals());
121: if (proof.openGoals().size() == 0) {
122: System.out.println("proof.openGoals.size="
123: + proof.openGoals().size());
124: System.exit(0);
125: }
126: mediator.startAutoMode();
127: }
128: }
129: };
130: mediator.stopInterface(true);
131: worker.start();
132: }
133:
134: /**
135: * @param file the file or directory the user has chosen in the Open dialog
136: * @return the corresponding input object for the selected file/directory
137: * @throws FileNotFoundException
138: * @throws IllegalArgumentException if the user has selected a file with an unsupported extension
139: * an exception is thrown to indicate this
140: */
141: protected KeYUserProblemFile createProblemFile(File file)
142: throws FileNotFoundException {
143:
144: final String filename = file.getName();
145:
146: if (filename.endsWith(".java")) {
147: // java file, probably enriched by JML specifications
148: return new KeYJMLInput(filename, file,
149: profile instanceof JavaTestGenerationProfile, main
150: .getProgressMonitor());
151:
152: } else if (filename.endsWith(".key")
153: || filename.endsWith(".proof")) {
154: // KeY problem specification or saved proof
155: return new KeYUserProblemFile(filename, file, main
156: .getProgressMonitor(), Main.jmlSpecs);
157:
158: } else if (file.isDirectory()) {
159: // directory containing JML-enriched java sources
160: // prompt the
161: return new JavaInputWithJMLSpecBrowser(file.getPath(),
162: file, profile instanceof JavaTestGenerationProfile,
163: main.getProgressMonitor());
164: } else {
165: if (filename.lastIndexOf('.') != -1) {
166: throw new IllegalArgumentException(
167: "Unsupported file extension \'"
168: + filename.substring(filename
169: .lastIndexOf('.'))
170: + "\' of read-in file "
171: + filename
172: + ". Allowed extensions are: .key, .proof, .java or "
173: + "complete directories.");
174: } else {
175: throw new FileNotFoundException(
176: "File or directory\n\t " + filename
177: + "\n not found.");
178: }
179: }
180: }
181:
182: private Object doWork() {
183: String status = "";
184: KeYUserProblemFile problemFile = null;
185: try {
186: try {
187: if (!keepProblem) {
188: problemFile = createProblemFile(file);
189: init = new ProblemInitializer(main);
190: init.startProver(problemFile, problemFile);
191: }
192: proof = mediator.getSelectedProof();
193: mediator.stopInterface(true); // first stop (above) is not enough
194: // as there is no problem at that time
195: main.setStatusLine("Loading proof");
196: currNode = proof.root(); // initialize loader
197: children = currNode.childrenIterator(); // --"--
198: iconfig = proof.env().getInitConfig();
199: if (!keepProblem) {
200: init.tryReadProof(this , problemFile);
201: } else {
202: main.setStatusLine("Loading proof", (int) file
203: .length());
204: CountingBufferedInputStream cinp = new CountingBufferedInputStream(
205: new FileInputStream(file), main
206: .getProgressMonitor(), (int) file
207: .length() / 100);
208: KeYLexer lexer = new KeYLexer(cinp, proof
209: .getServices().getExceptionHandler());
210: KeYParser parser = new KeYParser(
211: ParserMode.PROBLEM, lexer, proof
212: .getServices());
213: antlr.Token t;
214: do {
215: t = lexer.getSelector().nextToken();
216: } while (t.getType() != KeYLexer.PROOF);
217: parser.proofBody(this );
218: }
219: main.setStandardStatusLine();
220:
221: // Inform the decproc classes that a new problem has been loaded
222: // This is done here because all benchmarks resulting from one loaded problem should be
223: // stored in the same directory
224: DecisionProcedureSmtAuflia.fireNewProblemLoaded(file,
225: proof);
226:
227: } catch (ExceptionHandlerException e) {
228: throw e;
229: } catch (Throwable thr) {
230: exceptionHandler.reportException(thr);
231: status = thr.getMessage();
232: }
233: } catch (ExceptionHandlerException ex) {
234: main.setStatusLine("Failed to load problem/proof");
235: status = ex.toString();
236: } finally {
237: if (problemFile != null
238: && problemFile instanceof KeYUserProblemFile) {
239: ((KeYUserProblemFile) problemFile).close();
240: }
241: }
242: return status;
243: }
244:
245: public void loadPreferences(String preferences) {
246: final ProofSettings proofSettings = ProofSettings.DEFAULT_SETTINGS;
247: proofSettings.loadSettingsFromString(preferences);
248: }
249:
250: // note: Expressions without parameters only emit the endExpr signal
251: public void beginExpr(char id, String s) {
252: //System.out.println("start "+id+"="+s);
253: switch (id) {
254: case 'b':
255: stack.push(children);
256: if (children.hasNext())
257: currNode = children.next();
258: break;
259: case 'r':
260: if (currNode == null)
261: currNode = children.next();
262: // otherwise we already fetched the node at branch point
263: currGoal = proof.getGoal(currNode);
264: currTacletName = s;
265: // set default state
266: currFormula = 0;
267: currPosInTerm = PosInTerm.TOP_LEVEL;
268: loadedInsts = null;
269: ifSeqFormulaList = SLListOfIfFormulaInstantiation.EMPTY_LIST;
270: break;
271:
272: case 'f':
273: currFormula = Integer.parseInt(s);
274: break;
275:
276: case 't':
277: currPosInTerm = PosInTerm.parseReverseString(s);
278: break;
279:
280: case 'i':
281: if (loadedInsts == null)
282: loadedInsts = new LinkedList();
283: loadedInsts.add(s);
284: break;
285:
286: case 'h':
287: // Debug.fail("Detected use of heuristics!");
288: break;
289: case 'q': // ifseqformula
290: Sequent seq = currGoal.sequent();
291: ifSeqFormulaList = ifSeqFormulaList
292: .append(new IfFormulaInstSeq(seq, Integer
293: .parseInt(s)));
294: break;
295: case 'u': //UserLog
296: if (proof.userLog == null)
297: proof.userLog = new Vector();
298: proof.userLog.add(s);
299: break;
300: case 'v': //Version log
301: if (proof.keyVersionLog == null)
302: proof.keyVersionLog = new Vector();
303: proof.keyVersionLog.add(s);
304: break;
305: case 's': //ProofSettings
306: //System.out.println("---------------\n" + s + "------------\n");
307: //necessary for downward compatibility of the proof format
308: loadPreferences(s);
309: break;
310: case 'n': //BuiltIn rules
311: if (currNode == null)
312: currNode = children.next();
313: currGoal = proof.getGoal(currNode);
314:
315: currTacletName = s;
316: // set default state
317: currFormula = 0;
318: currPosInTerm = PosInTerm.TOP_LEVEL;
319: break;
320: case 'c': //contract
321: currContract = (OldOperationContract) proof.getServices()
322: .getSpecificationRepository().getContractByName(s);
323: break;
324: }
325: }
326:
327: public void endExpr(char id, int linenr) {
328: //System.out.println("end "+id);
329: switch (id) {
330: case 'b':
331: children = (IteratorOfNode) stack.pop();
332: break;
333: case 'a':
334: if (currNode != null) {
335: currNode.getNodeInfo().setInteractiveRuleApplication(
336: true);
337: }
338: break;
339: case 'r':
340: try {
341: currGoal.apply(constructApp());
342: children = currNode.childrenIterator();
343: currNode = null;
344: } catch (Exception e) {
345: throw new RuntimeException("Error loading proof. Line "
346: + linenr + " rule: " + currTacletName, e);
347: }
348: break;
349: case 'n':
350: try {
351: currGoal.apply(constructBuiltinApp());
352: children = currNode.childrenIterator();
353: currNode = null;
354: } catch (BuiltInConstructionException e) {
355: throw new RuntimeException("Error loading proof. Line "
356: + linenr + " rule: " + currTacletName, e);
357: }
358: break;
359: }
360:
361: }
362:
363: /**
364: * Constructs rule application for UpdateSimplification from
365: * current parser information
366: *
367: * @return current rule application for updateSimplification
368: */
369: private BuiltInRuleApp constructBuiltinApp()
370: throws BuiltInConstructionException {
371: BuiltInRuleApp ourApp = null;
372: //PosInSequent posInSeq = null;
373: PosInOccurrence pos = null;
374:
375: if (currFormula != 0) { // otherwise we have no pos
376: pos = PosInOccurrence.findInSequent(currGoal.sequent(),
377: currFormula, currPosInTerm);
378: } else {
379: }
380:
381: final Constraint userConstraint = mediator.getUserConstraint()
382: .getConstraint();
383:
384: if (currContract != null) {
385: ourApp = new MethodContractRuleApp(
386: UseMethodContractRule.INSTANCE, pos,
387: userConstraint, currContract);
388: currContract = null;
389: return ourApp;
390: }
391:
392: final SetOfRuleApp ruleApps = mediator
393: .getBuiltInRuleApplications(currTacletName, pos);
394:
395: if (ruleApps.size() != 1) {
396: if (ruleApps.size() < 1) {
397: throw new BuiltInConstructionException(
398: currTacletName
399: + " is missing. Most probably the binary "
400: + "for this built-in rule ist not in your path or "
401: + "you do not have the permission to execute it.");
402: } else {
403: throw new BuiltInConstructionException(currTacletName
404: + ": found " + ruleApps.size()
405: + " applications. Don't know what to do !\n"
406: + "@ " + pos);
407: }
408: }
409: ourApp = (BuiltInRuleApp) ruleApps.iterator().next();
410: return ourApp;
411: }
412:
413: private TacletApp constructApp() throws AppConstructionException {
414:
415: TacletApp ourApp = null;
416: PosInOccurrence pos = null;
417:
418: Taclet t = iconfig.lookupActiveTaclet(new Name(currTacletName));
419: if (t == null) {
420: ourApp = currGoal.indexOfTaclets().lookup(currTacletName);
421: } else {
422: ourApp = NoPosTacletApp.createNoPosTacletApp(t);
423: }
424:
425: Constraint userC = mediator.getUserConstraint().getConstraint();
426: Services services = mediator.getServices();
427:
428: if (currFormula != 0) { // otherwise we have no pos
429: pos = PosInOccurrence.findInSequent(currGoal.sequent(),
430: currFormula, currPosInTerm);
431: //System.err.print("Want to apply "+currTacletName+" at "+currGoal);
432: //this is copied from TermTacletAppIndex :-/
433:
434: Constraint c = pos.constrainedFormula().constraint();
435: if (pos.termBelowMetavariable() != null) {
436: c = c.unify(pos.constrainedFormula().formula().subAt(
437: pos.posInTerm()), pos.termBelowMetavariable(),
438: mediator.getServices());
439: if (!c.isSatisfiable())
440: return null;
441: }
442: ourApp = ((NoPosTacletApp) ourApp).matchFind(pos, c,
443: services, userC);
444: ourApp = ourApp.setPosInOccurrence(pos);
445: }
446:
447: ourApp = constructInsts(ourApp, services);
448:
449: ourApp = ourApp.setIfFormulaInstantiations(ifSeqFormulaList,
450: services, userC);
451:
452: if (!ourApp.sufficientlyComplete()) {
453: ourApp = ourApp.tryToInstantiate(currGoal, proof
454: .getServices());
455: }
456:
457: return ourApp;
458: }
459:
460: /** 1st pass: only VariableSV */
461: public static TacletApp parseSV1(TacletApp app, SchemaVariable sv,
462: String value, Services services) {
463: LogicVariable lv = new LogicVariable(new Name(value), app
464: .getRealSort(sv, services));
465: Term instance = TermFactory.DEFAULT.createVariableTerm(lv);
466: return app
467: .addCheckedInstantiation(sv, instance, services, true);
468: }
469:
470: /** 2nd pass: all other SV */
471: public static TacletApp parseSV2(TacletApp app, SchemaVariable sv,
472: String value, Goal targetGoal) {
473: final Proof p = targetGoal.proof();
474: final Services services = p.getServices();
475: TacletApp result;
476: if (sv.isVariableSV()) {
477: // ignore -- already done
478: result = app;
479: } else if (sv.isProgramSV()) {
480: final ProgramElement pe = TacletInstantiationsTableModel
481: .getProgramElement(app, value, sv, services);
482: result = app
483: .addCheckedInstantiation(sv, pe, services, true);
484: } else if (sv.isSkolemTermSV()) {
485: result = app
486: .createSkolemConstant(value, sv, true, services);
487: } else if (sv.isListSV()) {
488: SetOfLocationDescriptor s = parseLocationList(value,
489: targetGoal);
490: result = app.addInstantiation(sv, s.toArray(), true);
491: } else {
492: Namespace varNS = p.getNamespaces().variables();
493: varNS = app.extendVarNamespaceForSV(varNS, sv);
494: Term instance = parseTerm(value, p, varNS, targetGoal
495: .getVariableNamespace(varNS));
496: result = app.addCheckedInstantiation(sv, instance,
497: services, true);
498: }
499: return result;
500: }
501:
502: private TacletApp constructInsts(TacletApp app, Services services) {
503: if (loadedInsts == null)
504: return app;
505: SetOfSchemaVariable uninsts = app.uninstantiatedVars();
506:
507: // first pass: add variables
508: Iterator it = loadedInsts.iterator();
509: while (it.hasNext()) {
510: String s = (String) it.next();
511: int eq = s.indexOf('=');
512: String varname = s.substring(0, eq);
513: String value = s.substring(eq + 1, s.length());
514: if (varname.startsWith(NameSV.NAME_PREFIX)) {
515: app = app.addInstantiation(new NameSV(varname),
516: new Name(value));
517: continue;
518: }
519:
520: SchemaVariable sv = lookupName(uninsts, varname);
521: if (sv == null) {
522: // throw new IllegalStateException(
523: // varname+" from \n"+loadedInsts+"\n is not in\n"+uninsts);
524: System.err.println(varname + " from "
525: + app.rule().name() + " is not in uninsts");
526: continue;
527: }
528:
529: if (sv.isVariableSV()) {
530: app = parseSV1(app, sv, value, services);
531: }
532: }
533:
534: // second pass: add everything else
535: uninsts = app.uninstantiatedVars();
536: it = loadedInsts.iterator();
537: while (it.hasNext()) {
538: String s = (String) it.next();
539: int eq = s.indexOf('=');
540: String varname = s.substring(0, eq);
541: String value = s.substring(eq + 1, s.length());
542: SchemaVariable sv = lookupName(uninsts, varname);
543: if (sv == null)
544: continue;
545: app = parseSV2(app, sv, value, currGoal);
546: }
547:
548: return app;
549: }
550:
551: public static Term parseTerm(String value, Proof proof,
552: Namespace varNS, Namespace progVar_ns) {
553: try {
554: return TermParserFactory.createInstance().parse(
555: new StringReader(value), null, proof.getServices(),
556: varNS, proof.getNamespaces().functions(),
557: proof.getNamespaces().sorts(), progVar_ns,
558: new AbbrevMap());
559: } catch (ParserException e) {
560: throw new RuntimeException("Error while parsing value "
561: + value + "\nVar namespace is: " + varNS + "\n", e);
562: }
563: }
564:
565: public static SetOfLocationDescriptor parseLocationList(
566: String value, Goal targetGoal) {
567: SetOfLocationDescriptor result = null;
568: Proof p = targetGoal.proof();
569: Namespace varNS = p.getNamespaces().variables();
570: NamespaceSet nss = new NamespaceSet(varNS, p.getNamespaces()
571: .functions(), p.getNamespaces().sorts(),
572: new Namespace(), new Namespace(), targetGoal
573: .getVariableNamespace(varNS));
574: Services services = p.getServices();
575: try {
576: result = (new KeYParser(ParserMode.TERM, new KeYLexer(
577: new StringReader(value), services
578: .getExceptionHandler()), null,
579: TermFactory.DEFAULT, null, services, nss,
580: new AbbrevMap())).location_list();
581: } catch (antlr.RecognitionException re) {
582: throw new RuntimeException("Cannot parse location list "
583: + value, re);
584: } catch (antlr.TokenStreamException tse) {
585: throw new RuntimeException("Cannot parse location list "
586: + value, tse);
587: }
588: return result;
589: }
590:
591: public static Term parseTerm(String value, Proof proof) {
592: return parseTerm(value, proof, proof.getNamespaces()
593: .variables(), proof.getNamespaces().programVariables());
594: }
595:
596: private SchemaVariable lookupName(SetOfSchemaVariable set,
597: String name) {
598: IteratorOfSchemaVariable it = set.iterator();
599: while (it.hasNext()) {
600: SchemaVariable v = it.next();
601: if (v.name().toString().equals(name))
602: return v;
603: }
604: return null; // handle this better!
605: }
606:
607: private class AppConstructionException extends Exception {
608:
609: AppConstructionException(String s) {
610: super (s);
611: }
612:
613: AppConstructionException(Throwable t) {
614: super (t);
615: }
616:
617: AppConstructionException(String s, Throwable t) {
618: super (s, t);
619: }
620:
621: }
622:
623: private class BuiltInConstructionException extends Exception {
624:
625: BuiltInConstructionException(String s) {
626: super(s);
627: }
628: }
629:
630: }
|