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: package de.uka.ilkd.key.proof.init;
011:
012: import java.io.File;
013: import java.io.FileNotFoundException;
014: import java.io.IOException;
015: import java.io.InputStream;
016: import java.util.LinkedHashMap;
017:
018: import de.uka.ilkd.key.collection.ListOfString;
019: import de.uka.ilkd.key.gui.configuration.LibrariesSettings;
020: import de.uka.ilkd.key.gui.configuration.ProofSettings;
021: import de.uka.ilkd.key.java.Services;
022: import de.uka.ilkd.key.logic.NamespaceSet;
023: import de.uka.ilkd.key.parser.KeYLexer;
024: import de.uka.ilkd.key.parser.KeYParser;
025: import de.uka.ilkd.key.parser.ParserConfig;
026: import de.uka.ilkd.key.parser.ParserMode;
027: import de.uka.ilkd.key.proof.CountingBufferedInputStream;
028: import de.uka.ilkd.key.proof.ProblemLoader;
029: import de.uka.ilkd.key.proof.RuleSource;
030: import de.uka.ilkd.key.proof.mgt.Contract;
031: import de.uka.ilkd.key.proof.mgt.Contractable;
032: import de.uka.ilkd.key.util.Debug;
033: import de.uka.ilkd.key.util.ProgressMonitor;
034:
035: /** represents an input from a .key file producing an environment.
036: */
037: public class KeYFile implements EnvInput {
038:
039: protected String javaPath;
040: private boolean javaPathAlreadyParsed = false;
041:
042: /** the RuleSource delivering the input stream for the file.
043: */
044: protected RuleSource file = null;
045:
046: /** maps methods to their jml specifications. */
047: protected LinkedHashMap method2jmlspecs = null;
048:
049: protected InputStream input = null;
050:
051: /** the initial configuration to be used (and modified) while reading.
052: */
053: protected InitConfig initConfig = null;
054:
055: private String name;
056:
057: protected KeYParser problemParser = null;
058:
059: protected ProofSettings settings;
060:
061: /** the graphical entity to notify on the state of reading.
062: */
063: protected ProgressMonitor monitor;
064:
065: /** creates a new representation for a given file by indicating a name
066: * and a file representing the physical source of the .key file.
067: */
068: public KeYFile(String name, File file) {
069: this (name, RuleSource.initRuleFile(file), null);
070: }
071:
072: /** creates a new representation for a given file by indicating a name
073: * and a file representing the physical source of the .key file.
074: * @param monitor the progress monitor to notify on the state of reading
075: */
076: public KeYFile(String name, File file, ProgressMonitor monitor) {
077: this (name, RuleSource.initRuleFile(file), monitor);
078: }
079:
080: /** creates a new representation for a given file by indicating a name
081: * and a RuleSource representing the physical source of the .key file.
082: * @param monitor the progress monitor to notify on the state of reading
083: */
084: public KeYFile(String name, RuleSource file, ProgressMonitor monitor) {
085: this .file = file;
086: this .name = name;
087: this .monitor = monitor;
088: }
089:
090: /** returns the initial configuration that is used to read and
091: * that may be modified by reading.
092: */
093: public InitConfig getInitConfig() {
094: return initConfig;
095: }
096:
097: /** returns the number of chars in the .key file.
098: */
099: public int getNumberOfChars() {
100: return file.getNumberOfChars();
101: }
102:
103: protected InputStream getNewStream() throws FileNotFoundException {
104: try {
105: if (input != null)
106: input.close();
107: } catch (IOException ioe) {
108: System.err.println("WARNING: Cannot close stream " + file
109: + "\n" + ioe);
110: }
111: if (!file.isAvailable()) {
112: throw new FileNotFoundException("File/Resource " + file
113: + " not found.");
114: }
115: input = file.getNewStream();
116: return input;
117: }
118:
119: /** reads the whole .key file and modifies the initial configuration
120: * assigned to this object according to the given modification strategy.
121: * Throws an exception if no initial configuration has been set yet.
122: */
123: public void read(ModStrategy mod) throws ProofInputException {
124: if (initConfig == null) {
125: throw new IllegalStateException(
126: "KeYFile: InitConfig not set.");
127: }
128: try {
129: Debug.out("Reading KeY file", file);
130: CountingBufferedInputStream cinp = new CountingBufferedInputStream(
131: getNewStream(), monitor, getNumberOfChars() / 100);
132:
133: final NamespaceSet normal = initConfig.namespaces().copy();
134: final NamespaceSet schema = setupSchemaNamespace(normal);
135:
136: final ParserConfig normalConfig = new ParserConfig(
137: initConfig.getServices(), normal);
138: final ParserConfig schemaConfig = new ParserConfig(
139: initConfig.getServices(), schema);
140:
141: problemParser = new KeYParser(ParserMode.PROBLEM,
142: new KeYLexer(cinp, initConfig.getServices()
143: .getExceptionHandler()), file.toString(),
144: schemaConfig, normalConfig, initConfig
145: .getTaclet2Builder(), initConfig
146: .getTaclets(), initConfig
147: .getActivatedChoices());
148: problemParser.problem();
149:
150: initConfig.addCategory2DefaultChoices(problemParser
151: .getCategory2Default());
152: initConfig.setTaclets(problemParser.getTaclets());
153: initConfig.add(normalConfig.namespaces(), mod);
154: if (initConfig.getProofEnv() != null) {
155: initConfig.getProofEnv().addMethodContracts(
156: problemParser.getContracts(), null);
157: }
158: Debug.out("Read KeY file ", file);
159: } catch (antlr.ANTLRException e) {
160: throw new ProofInputException(e);
161: } catch (FileNotFoundException fnfe) {
162: throw new ProofInputException(fnfe);
163: }
164: }
165:
166: /**
167: * when reading in rules modal schema operators and schemavariables are
168: * added to the namespace, but shall not occur in the normal function
169: * namespaces. Therefore we take the given namespaces and use copies of
170: * the normal function and variables namespace
171: * TODO: extend the normal namespace by a generic sort and schema function
172: * namespace and get rid of the schemaConfig...
173: * @param normal the Namespace containing the concrete symbols
174: * @return namespace for reading in rules etc.
175: */
176: protected NamespaceSet setupSchemaNamespace(
177: final NamespaceSet normal) {
178: return new NamespaceSet(normal.variables().copy(), normal
179: .functions().copy(), normal.sorts(), normal.ruleSets(),
180: normal.choices(), normal.programVariables());
181: }
182:
183: public Includes readIncludes() throws ProofInputException {
184: if (file == null)
185: return new Includes();
186: try {
187: final ParserConfig pc = new ParserConfig(new Services(),
188: new NamespaceSet());
189: // FIXME: there is no exception handler here, thus, when parsing errors are ecountered
190: // during collection of includes (it is enough to mispell \include) the error
191: // message is very uninformative - ProofInputException without filename, line and column
192: // numbers. Somebody please fix that. /Woj
193: problemParser = new KeYParser(ParserMode.PROBLEM,
194: new KeYLexer(getNewStream(), null),
195: file.toString(), pc, pc, null, null, null);
196: problemParser.parseIncludes();
197: return problemParser.getIncludes();
198: } catch (antlr.ANTLRException e) {
199: throw new ProofInputException(e);
200: } catch (FileNotFoundException fnfe) {
201: throw new ProofInputException(fnfe);
202: } catch (de.uka.ilkd.key.util.ExceptionHandlerException ehe) {
203: throw new ProofInputException(ehe);
204: }
205: }
206:
207: public LibrariesSettings readLibrariesSettings()
208: throws ProofInputException {
209: if (initConfig == null) {
210: throw new IllegalStateException(
211: "KeYFile: InitConfig not set.");
212: }
213:
214: if (settings == null) {
215: getPreferences();
216: }
217:
218: LibrariesSettings result;
219: if (settings == null
220: || settings.getLibrariesSettings().emptyProperties()) {
221: result = ProofSettings.DEFAULT_SETTINGS
222: .getLibrariesSettings();
223: } else {
224: result = settings.getLibrariesSettings();
225: }
226:
227: return result;
228: }
229:
230: private KeYParser createDeclParser() throws FileNotFoundException {
231: return new KeYParser(ParserMode.DECLARATION, new KeYLexer(
232: getNewStream(), initConfig.getServices()
233: .getExceptionHandler()), file.toString(),
234: initConfig.getServices().copy(), initConfig
235: .namespaces().copy());
236: }
237:
238: /** reads the sorts declaration of the .key file only,
239: * modifying the sort namespace
240: * of the initial configuration if allowed in the given
241: * modification strategy.
242: */
243: public void readSorts(ModStrategy mod) throws ProofInputException {
244: try {
245: KeYParser p = createDeclParser();
246: p.parseSorts();
247: initConfig.addCategory2DefaultChoices(p
248: .getCategory2Default());
249: initConfig.add(p.namespaces(), mod);
250: } catch (antlr.ANTLRException e) {
251: throw new ProofInputException(e);
252: } catch (FileNotFoundException fnfe) {
253: throw new ProofInputException(fnfe);
254: }
255: }
256:
257: /** reads the functions and predicates declared in the .key file only,
258: * modifying the function namespaces of the respective taclet options.
259: */
260: public void readFuncAndPred(ModStrategy mod)
261: throws ProofInputException {
262: if (file == null)
263: return;
264: try {
265: KeYParser p = createDeclParser();
266: p.parseFuncAndPred();
267: initConfig.add(p.namespaces(), mod);
268: } catch (antlr.ANTLRException e) {
269: throw new ProofInputException(e);
270: } catch (FileNotFoundException fnfe) {
271: throw new ProofInputException(fnfe);
272: }
273: }
274:
275: /** reads the rules and problems declared in the .key file only,
276: * modifying the set of rules
277: * of the initial configuration if allowed in the given
278: * modification strategy.
279: */
280: public void readRulesAndProblem(ModStrategy mod)
281: throws ProofInputException {
282:
283: /*
284: two namespace sets which share all namespace except the
285: variable and function namespace
286: */
287: final NamespaceSet normal = initConfig.namespaces().copy();
288: final NamespaceSet schema = setupSchemaNamespace(normal);
289:
290: final ParserConfig schemaConfig = new ParserConfig(initConfig
291: .getServices(), schema);
292:
293: final ParserConfig normalConfig = new ParserConfig(initConfig
294: .getServices(), normal);
295: try {
296: final CountingBufferedInputStream cinp = new CountingBufferedInputStream(
297: getNewStream(), monitor, getNumberOfChars() / 100);
298: problemParser = new KeYParser(ParserMode.PROBLEM,
299: new KeYLexer(cinp, initConfig.getServices()
300: .getExceptionHandler()), file.toString(),
301: schemaConfig, normalConfig, initConfig
302: .getTaclet2Builder(), initConfig
303: .getTaclets(), initConfig
304: .getActivatedChoices());
305: problemParser.parseTacletsAndProblem();
306: initConfig.add(normalConfig.namespaces(), mod);
307: initConfig.setTaclets(problemParser.getTaclets());
308: } catch (antlr.ANTLRException e) {
309: throw new ProofInputException(e);
310: } catch (FileNotFoundException fnfe) {
311: throw new ProofInputException(fnfe);
312: }
313: }
314:
315: public void readProblem(ModStrategy mod) throws ProofInputException {
316: readRulesAndProblem(mod);
317: }
318:
319: public void setInitConfig(InitConfig conf) {
320: this .initConfig = conf;
321: }
322:
323: /** reads a saved proof of a .key file
324: */
325: public void readProof(ProblemLoader prl) throws ProofInputException {
326: try {
327: problemParser.proof(prl);
328: } catch (antlr.ANTLRException e) {
329: throw new ProofInputException(e);
330: }
331: }
332:
333: public ProofSettings getPreferences() throws ProofInputException {
334: if (settings == null) {
335: if (file.isDirectory())
336: return null;
337: try {
338: problemParser = new KeYParser(ParserMode.PROBLEM,
339: new KeYLexer(getNewStream(), null), file
340: .toString());
341: settings = new ProofSettings(
342: ProofSettings.DEFAULT_SETTINGS);
343: settings.setProfile(ProofSettings.DEFAULT_SETTINGS
344: .getProfile());
345: settings.loadSettingsFromString(problemParser
346: .preferences());
347: } catch (antlr.ANTLRException e) {
348: throw new ProofInputException(e);
349: } catch (FileNotFoundException fnfe) {
350: throw new ProofInputException(fnfe);
351: } catch (de.uka.ilkd.key.util.ExceptionHandlerException ehe) {
352: throw new ProofInputException(ehe.getCause()
353: .getMessage());
354: }
355: }
356: return settings;
357: }
358:
359: /** returns the name of the .key file
360: */
361: public String name() {
362: return name;
363: }
364:
365: public void close() {
366: try {
367: if (input != null) {
368: input.close();
369: }
370: } catch (IOException ioe) {
371: System.err.println("WARNING: Cannot close stream " + file
372: + "\n" + ioe);
373: }
374: }
375:
376: public String toString() {
377: return name() + " " + file.toString();
378: }
379:
380: public boolean equals(Object o) {
381: if (!(o instanceof KeYFile))
382: return false;
383: KeYFile kf = (KeYFile) o;
384: if (file != null && kf.file != null) {
385: return kf.file.getExternalForm().equals(
386: file.getExternalForm());
387: }
388: return false;
389: }
390:
391: public int hashCode() {
392: final String externalForm = file.getExternalForm();
393: if (externalForm == null)
394: return -1;
395: return externalForm.hashCode();
396: }
397:
398: public Contractable[] getObjectOfContract() {
399: return new Contractable[0];
400: }
401:
402: public boolean initContract(Contract ct) {
403: return false;
404: }
405:
406: public String readJavaPath() throws ProofInputException {
407: if (javaPathAlreadyParsed)
408: return javaPath;
409: try {
410: problemParser = new KeYParser(ParserMode.PROBLEM,
411: new KeYLexer(getNewStream(), null), file.toString());
412:
413: problemParser.preferences(); // skip preferences
414:
415: ListOfString javaPaths = problemParser.javaSource();
416:
417: if (javaPaths == null) {
418: // no java model at all
419: javaPath = null;
420: javaPathAlreadyParsed = true;
421: return null;
422: }
423: javaPath = (javaPaths.size() == 0 ? "" : javaPaths.head());
424:
425: if (javaPaths.size() > 1)
426: Debug
427: .fail("Don't know what to do with multiple Java paths.");
428:
429: javaPathAlreadyParsed = true;
430:
431: if (javaPath.length() != 0) {
432: File cfile = new File(javaPath);
433: if (!cfile.isAbsolute()) { // test relative pathname
434: File parent = file.file().getParentFile();
435: cfile = new File(parent, javaPath)
436: .getCanonicalFile().getAbsoluteFile();
437: javaPath = cfile.getAbsolutePath();
438: }
439: if (!cfile.exists()) {
440: throw new ProofInputException(
441: "Declared Java source " + javaPath
442: + " not found.");
443: }
444: }
445: return javaPath;
446: } catch (antlr.ANTLRException e) {
447: throw new ProofInputException(e);
448: } catch (IOException ioe) {
449: throw new ProofInputException(ioe);
450: } catch (de.uka.ilkd.key.util.ExceptionHandlerException ehe) {
451: ehe.printStackTrace();
452: System.out.println(ehe.getCause().getMessage());
453: throw new ProofInputException(ehe.getCause().getMessage());
454: }
455: }
456: }
|