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: //
009: //
010:
011: package de.uka.ilkd.key.proof.init;
012:
013: import java.io.File;
014: import java.net.URL;
015: import java.util.HashMap;
016: import java.util.HashSet;
017: import java.util.Iterator;
018: import java.util.Vector;
019: import java.util.Map.Entry;
020:
021: import recoder.io.PathList;
022: import recoder.io.ProjectSettings;
023:
024: import org.apache.log4j.Logger;
025:
026: import de.uka.ilkd.key.gui.Main;
027: import de.uka.ilkd.key.gui.configuration.LibrariesSettings;
028: import de.uka.ilkd.key.gui.configuration.ProofSettings;
029: import de.uka.ilkd.key.java.CompilationUnit;
030: import de.uka.ilkd.key.java.Recoder2KeY;
031: import de.uka.ilkd.key.java.Services;
032: import de.uka.ilkd.key.logic.ConstrainedFormula;
033: import de.uka.ilkd.key.logic.IteratorOfConstrainedFormula;
034: import de.uka.ilkd.key.logic.IteratorOfNamed;
035: import de.uka.ilkd.key.logic.NamespaceSet;
036: import de.uka.ilkd.key.logic.Term;
037: import de.uka.ilkd.key.logic.op.Function;
038: import de.uka.ilkd.key.logic.op.ProgramVariable;
039: import de.uka.ilkd.key.logic.sort.Sort;
040: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
041: import de.uka.ilkd.key.proof.JavaModel;
042: import de.uka.ilkd.key.proof.ProblemLoader;
043: import de.uka.ilkd.key.proof.Proof;
044: import de.uka.ilkd.key.proof.ProofAggregate;
045: import de.uka.ilkd.key.proof.RuleSource;
046: import de.uka.ilkd.key.proof.mgt.AxiomJustification;
047: import de.uka.ilkd.key.proof.mgt.CvsException;
048: import de.uka.ilkd.key.proof.mgt.CvsRunner;
049: import de.uka.ilkd.key.proof.mgt.GlobalProofMgt;
050: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
051: import de.uka.ilkd.key.proof.mgt.RuleConfig;
052: import de.uka.ilkd.key.rule.IteratorOfBuiltInRule;
053: import de.uka.ilkd.key.rule.Rule;
054: import de.uka.ilkd.key.rule.UpdateSimplifier;
055: import de.uka.ilkd.key.util.KeYResourceManager;
056:
057: public class ProblemInitializer {
058:
059: private static JavaModel lastModel;
060: private static InitConfig lastBaseConfig;
061:
062: private final Main main;
063: private final Profile profile;
064: private final Services services;
065: private final UpdateSimplifier simplifier;
066:
067: private final HashSet alreadyParsed = new HashSet();
068:
069: //-------------------------------------------------------------------------
070: //constructors
071: //-------------------------------------------------------------------------
072:
073: public ProblemInitializer(Main main) {
074: this .main = main;
075: this .profile = main.mediator().getProfile();
076: this .services = new Services(main.mediator()
077: .getExceptionHandler());
078: this .simplifier = ProofSettings.DEFAULT_SETTINGS
079: .getSimultaneousUpdateSimplifierSettings()
080: .getSimplifier();
081: }
082:
083: /**
084: * For tests only
085: */
086: public ProblemInitializer(Profile profile) {
087: this .main = null;
088: this .profile = profile;
089: this .services = new Services();
090: this .simplifier = ProofSettings.DEFAULT_SETTINGS
091: .getSimultaneousUpdateSimplifierSettings()
092: .getSimplifier();
093: }
094:
095: //-------------------------------------------------------------------------
096: //internal methods
097: //-------------------------------------------------------------------------
098:
099: /**
100: * displays the status report in the status line
101: */
102: private void reportStatus(String status) {
103: if (main != null) {
104: main.setStatusLine(status);
105: }
106: }
107:
108: /**
109: * displays the status report in the status line
110: * and the maximum used by a progress bar
111: * @param status the String to be displayed in the status line
112: * @param progressMax an int describing what is 100 per cent
113: */
114: private void reportStatus(String status, int progressMax) {
115: if (main != null) {
116: main.setStatusLine(status, progressMax);
117: }
118: }
119:
120: /**
121: * displays the standard status line
122: */
123: private void reportReady() {
124: if (main != null) {
125: main.setStandardStatusLine();
126: }
127: }
128:
129: private void stopInterface() {
130: if (main != null) {
131: main.mediator().stopInterface(true);
132: }
133: }
134:
135: private void startInterface() {
136: if (main != null) {
137: main.mediator().startInterface(true);
138: }
139: }
140:
141: /**
142: * Delayed setup of symbols defined by sorts (e.g. functions for
143: * collection sorts). This may not have been done for previously
144: * defined sorts, as the integer sort was not available.
145: */
146: public void setUpSorts(InitConfig initConfig) {
147: IteratorOfNamed it = initConfig.sortNS().allElements()
148: .iterator();
149: while (it.hasNext()) {
150: Sort sort = (Sort) it.next();
151: if (sort instanceof SortDefiningSymbols) {
152: ((SortDefiningSymbols) sort).addDefinedSymbols(
153: initConfig.funcNS(), initConfig.sortNS());
154: }
155: }
156: }
157:
158: /**
159: * Helper for readIncludes().
160: */
161: private void readLDTIncludes(Includes in, InitConfig initConfig,
162: boolean readLibraries) throws ProofInputException {
163: //avoid infinite recursion
164: if (in.getLDTIncludes().isEmpty()) {
165: return;
166: }
167:
168: //collect all ldt includes into a single LDTInput
169: KeYFile[] keyFile = new KeYFile[in.getLDTIncludes().size()];
170: Iterator it = in.getLDTIncludes().iterator();
171: int i = 0;
172: while (it.hasNext()) {
173: String name = (String) it.next();
174: keyFile[i++] = new KeYFile(name, in.get(name),
175: (main == null) ? null : main.getProgressMonitor());
176: }
177: LDTInput ldtInp = new LDTInput(keyFile, main);
178:
179: //read the LDTInput
180: readEnvInput(ldtInp, initConfig, readLibraries);
181:
182: setUpSorts(initConfig);
183: }
184:
185: /**
186: * Helper for readEnvInput().
187: */
188: private void readIncludes(EnvInput envInput, InitConfig initConfig,
189: boolean readLibraries) throws ProofInputException {
190: envInput.setInitConfig(initConfig);
191: Includes in = envInput.readIncludes();
192:
193: //read LDT includes
194: readLDTIncludes(in, initConfig, readLibraries);
195:
196: //read normal includes
197: Iterator it = in.getIncludes().iterator();
198: while (it.hasNext()) {
199: String fileName = (String) it.next();
200: KeYFile keyFile = new KeYFile(fileName, in.get(fileName),
201: (main == null) ? null : main.getProgressMonitor());
202: readEnvInput(keyFile, initConfig, readLibraries);
203: }
204: }
205:
206: /**
207: * Helper for readEnvInput().
208: */
209: private void readLibraries(EnvInput envInput, InitConfig initConfig)
210: throws ProofInputException {
211: reportStatus("Loading Libraries");
212:
213: HashMap libraries = envInput.readLibrariesSettings()
214: .getLibraries();
215: if (libraries.size() == 0)
216: return;
217: String path = LibrariesSettings.getLibrariesPath();
218: Iterator it = libraries.entrySet().iterator();
219: while (it.hasNext()) {
220: final Entry entry = (Entry) it.next();
221: final String fileName = (String) entry.getKey();
222: final Boolean sel = (Boolean) entry.getValue();
223: if (sel.booleanValue()) {
224: RuleSource rs;
225: if (!fileName.startsWith(File.separator)) {
226: rs = RuleSource.initRuleFile(path + fileName);
227: } else {
228: rs = RuleSource.initRuleFile(fileName);
229: }
230: KeYFile keyFile = new KeYFile(fileName, rs,
231: (main == null) ? null : main
232: .getProgressMonitor());
233: readEnvInput(keyFile, initConfig);
234: }
235: }
236: reportReady();
237: }
238:
239: /**
240: * Helper for readJava().
241: */
242: private Vector getClasses(String f) throws ProofInputException {
243: File cfile = new File(f);
244: Vector v = new Vector();
245: if (cfile.isDirectory()) {
246: String[] list = cfile.list();
247: for (int i = 0; i < list.length; i++) {
248: String fullName = cfile.getPath() + File.separator
249: + list[i];
250: File n = new File(fullName);
251: if (n.isDirectory()) {
252: v.addAll(getClasses(fullName));
253: } else if (list[i].endsWith(".java")) {
254: v.add(fullName);
255: }
256: }
257: return v;
258: } else {
259: throw new ProofInputException("Java model path " + f
260: + " not found.");
261: }
262:
263: }
264:
265: /**
266: * Helper for readJava().
267: */
268: private JavaModel getJavaModel(String javaPath)
269: throws ProofInputException {
270: JavaModel jModel = JavaModel.NO_MODEL;
271: if (javaPath != null) {
272: String modelTag = "KeY_"
273: + new Long((new java.util.Date()).getTime());
274: jModel = new JavaModel(javaPath, modelTag);
275: if (javaPath.equals(System.getProperty("user.home"))) {
276: throw new ProofInputException(
277: "You do not want to have "
278: + "your home directory as the program model.");
279: }
280: CvsRunner cvs = new CvsRunner();
281: try {
282: boolean importOK = cvs.cvsImport(jModel.getCVSModule(),
283: javaPath, System.getProperty("user.name"),
284: modelTag);
285: if (importOK && lastModel != null
286: && lastModel != JavaModel.NO_MODEL
287: && javaPath.equals(lastModel.getModelDir())) {
288: String diff = cvs.cvsDiff(jModel.getCVSModule(),
289: lastModel.getModelTag(), modelTag);
290: if (diff.length() == 0) {
291: jModel = lastModel;
292: }
293: }
294: } catch (CvsException cvse) {
295: // leave already created new Java model
296: Logger.getLogger("key.proof.mgt").error(
297: "Dumping Model into CVS failed: " + cvse);
298: }
299: }
300: lastModel = jModel;
301: return jModel;
302: }
303:
304: /**
305: * Helper for readEnvInput().
306: */
307: private void readJava(EnvInput envInput, InitConfig initConfig)
308: throws ProofInputException {
309: envInput.setInitConfig(initConfig);
310: String javaPath = envInput.readJavaPath();
311: if (javaPath != null) {
312: //read Java
313: reportStatus("Reading Java model");
314: ProjectSettings settings = initConfig.getServices()
315: .getJavaInfo().getKeYProgModelInfo().getServConf()
316: .getProjectSettings();
317: PathList searchPathList = settings.getSearchPathList();
318:
319: if (searchPathList.find(javaPath) == null) {
320: searchPathList.add(javaPath);
321: }
322: Recoder2KeY r2k = new Recoder2KeY(initConfig.getServices(),
323: initConfig.namespaces());
324: if (javaPath == "") {
325: r2k.parseSpecialClasses();
326: initConfig.getProofEnv().setJavaModel(
327: JavaModel.NO_MODEL);
328: } else {
329: String[] cus = (String[]) getClasses(javaPath).toArray(
330: new String[] {});
331: CompilationUnit[] compUnits = r2k
332: .readCompilationUnitsAsFiles(cus);
333: //temporary hack
334: if (envInput instanceof KeYUserProblemFile) {
335: KeYUserProblemFile kupf = (KeYUserProblemFile) envInput;
336: kupf.readActivatedChoices();
337: kupf.readJML(compUnits);
338: }
339: initConfig.getServices().getJavaInfo()
340: .setJavaSourcePath(javaPath);
341:
342: //checkin Java model to CVS
343: reportStatus("Checking Java model");
344: JavaModel jmodel = getJavaModel(javaPath);
345: initConfig.getProofEnv().setJavaModel(jmodel);
346: }
347:
348: reportReady();
349:
350: setUpSorts(initConfig);
351: } else {
352: initConfig.getProofEnv().setJavaModel(JavaModel.NO_MODEL);
353: }
354: }
355:
356: private void readEnvInput(EnvInput envInput, InitConfig initConfig,
357: boolean readLibraries) throws ProofInputException {
358: if (alreadyParsed.add(envInput)) {
359: //read includes
360: readIncludes(envInput, initConfig, readLibraries);
361:
362: //read Java
363: // readJava(envInput, initConfig);
364:
365: //read libraries
366: if (readLibraries) {
367: readLibraries(envInput, initConfig);
368: }
369:
370: //read Java
371: readJava(envInput, initConfig);
372:
373: //read envInput itself
374: reportStatus("Reading " + envInput.name(), envInput
375: .getNumberOfChars());
376: // System.out.println("Reading envInput: " + envInput.name());
377: envInput.setInitConfig(initConfig);
378: envInput.read(ModStrategy.NO_VARS_GENSORTS);//envInput.read(ModStrategy.NO_VARS_FUNCS_GENSORTS);
379: reportReady();
380:
381: setUpSorts(initConfig);
382: }
383: }
384:
385: private void readEnvInput(EnvInput envInput, InitConfig initConfig)
386: throws ProofInputException {
387: readEnvInput(envInput, initConfig, true);
388: }
389:
390: private void populateNamespaces(Term term, NamespaceSet namespaces) {
391: for (int i = 0; i < term.arity(); i++) {
392: populateNamespaces(term.sub(i), namespaces);
393: }
394:
395: if (term.op() instanceof Function) {
396: namespaces.functions().add(term.op());
397: } else if (term.op() instanceof ProgramVariable) {
398: namespaces.programVariables().add(term.op());
399: }
400:
401: //TODO: consider Java blocks (should not be strictly necessary
402: //for the moment, though)
403: }
404:
405: /**
406: * Ensures that the passed proof's namespaces contain all functions
407: * and program variables used in its root sequent.
408: */
409: private void populateNamespaces(Proof proof) {
410: NamespaceSet namespaces = proof.getNamespaces();
411: IteratorOfConstrainedFormula it = proof.root().sequent()
412: .iterator();
413: while (it.hasNext()) {
414: ConstrainedFormula cf = it.next();
415: populateNamespaces(cf.formula(), namespaces);
416: }
417: }
418:
419: private InitConfig determineEnvironment(ProofOblInput po,
420: InitConfig initConfig) throws ProofInputException {
421: ProofEnvironment env = initConfig.getProofEnv();
422:
423: //read activated choices
424: po.setInitConfig(initConfig);
425: po.readActivatedChoices();
426: initConfig.createNamespacesForActivatedChoices();
427:
428: //TODO: what does this actually do?
429: ProofSettings.DEFAULT_SETTINGS.getChoiceSettings()
430: .updateChoices(initConfig.choiceNS(), false);
431:
432: //init ruleConfig
433: RuleConfig ruleConfig = new RuleConfig(initConfig
434: .getActivatedChoices());
435: env.setRuleConfig(ruleConfig);
436:
437: //possibly reuse an existing proof environment
438: if (main != null) {
439: ProofEnvironment envChosen = GlobalProofMgt.getInstance()
440: .getProofEnvironment(env.getJavaModel(),
441: env.getRuleConfig(),
442: po.askUserForEnvironment());
443:
444: if (envChosen != null) {
445: assert envChosen.getInitConfig().getProofEnv() == envChosen;
446: return envChosen.getInitConfig();
447: }
448: }
449:
450: //register the proof environment
451: if (main != null) {
452: GlobalProofMgt.getInstance().registerProofEnvironment(env);
453: }
454:
455: //read specs (TODO)
456: po.setInitConfig(initConfig);
457: po.readSpecs();
458:
459: return initConfig;
460: }
461:
462: private void setUpProofHelper(ProofOblInput problem,
463: InitConfig initConfig) throws ProofInputException {
464: ProofAggregate pl = problem.getPO();
465: if (pl == null) {
466: throw new ProofInputException("No proof");
467: }
468:
469: //register non-built-in rules
470: reportStatus("Registering rules");
471: initConfig.getProofEnv().registerRules(initConfig.getTaclets(),
472: AxiomJustification.INSTANCE);
473: reportReady();
474:
475: Proof[] proofs = pl.getProofs();
476: for (int i = 0; i < proofs.length; i++) {
477: proofs[i].setSimplifier(simplifier);
478: proofs[i].setNamespaces(proofs[i].getNamespaces());//TODO: refactor Proof.setNamespaces() so this becomes unnecessary
479: populateNamespaces(proofs[i]);
480: }
481: initConfig.getProofEnv().registerProof(problem, pl);
482: if (main != null) {
483: main.addProblem(pl);
484: }
485: GlobalProofMgt.getInstance().tryReuse(pl);
486: }
487:
488: //-------------------------------------------------------------------------
489: //public interface
490: //-------------------------------------------------------------------------
491:
492: /**
493: * Creates an initConfig / a proof environment and reads an EnvInput into it
494: */
495: public InitConfig prepare(EnvInput envInput)
496: throws ProofInputException {
497: stopInterface();
498: alreadyParsed.clear();
499:
500: //if the profile changed, read in standard rules
501: if (lastBaseConfig == null
502: || !lastBaseConfig.getProfile().equals(profile)) {
503: lastBaseConfig = new InitConfig(services, profile);
504: RuleSource tacletBase = profile.getStandardRules()
505: .getTacletBase();
506: if (tacletBase != null) {
507: KeYFile tacletBaseFile = new KeYFile("taclet base",
508: profile.getStandardRules().getTacletBase(),
509: (main == null) ? null : main
510: .getProgressMonitor());
511: readEnvInput(tacletBaseFile, lastBaseConfig, false);
512: }
513: }
514:
515: //create initConfig
516: InitConfig initConfig = lastBaseConfig.copy();
517:
518: //register built in rules
519: final IteratorOfBuiltInRule builtInRules = profile
520: .getStandardRules().getStandardBuiltInRules()
521: .iterator();
522: while (builtInRules.hasNext()) {
523: final Rule r = builtInRules.next();
524: initConfig.getProofEnv().registerRule(r,
525: profile.getJustification(r));
526: }
527:
528: //read envInput
529: readEnvInput(envInput, initConfig);
530:
531: startInterface();
532: return initConfig;
533: }
534:
535: public void startProver(InitConfig initConfig, ProofOblInput po)
536: throws ProofInputException {
537: assert initConfig != null;
538: stopInterface();
539:
540: try {
541: //determine environment
542: initConfig = determineEnvironment(po, initConfig);
543:
544: //read problem
545: reportStatus("Loading problem \"" + po.name() + "\"");
546: po.setInitConfig(initConfig);
547: po.readProblem(ModStrategy.NO_FUNCS);
548: reportReady();
549:
550: //final work
551: setUpProofHelper(po, initConfig);
552: } catch (ProofInputException e) {
553: reportStatus(po.name() + " failed");
554: throw e;
555: } finally {
556: startInterface();
557: }
558: }
559:
560: public void startProver(ProofEnvironment env, ProofOblInput po)
561: throws ProofInputException {
562: assert env.getInitConfig().getProofEnv() == env;
563: startProver(env.getInitConfig(), po);
564: }
565:
566: public void startProver(EnvInput envInput, ProofOblInput po)
567: throws ProofInputException {
568: try {
569: InitConfig initConfig = prepare(envInput);
570: startProver(initConfig, po);
571: } catch (ProofInputException e) {
572: reportStatus(envInput.name() + " failed");
573: throw e;
574: }
575: }
576:
577: public void tryReadProof(ProblemLoader prl, ProofOblInput problem)
578: throws ProofInputException {
579: if (problem instanceof KeYFile) {
580: KeYFile proof = (KeYFile) problem;
581: reportStatus("Loading proof", proof.getNumberOfChars());
582: proof.readProof(prl);
583: }
584: }
585: }
|