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.util.Iterator;
015: import java.util.LinkedHashMap;
016: import java.util.LinkedHashSet;
017: import java.util.Set;
018:
019: import de.uka.ilkd.key.gui.Main;
020: import de.uka.ilkd.key.gui.UsedMethodContractsList;
021: import de.uka.ilkd.key.java.CompilationUnit;
022: import de.uka.ilkd.key.java.JavaInfo;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.java.abstraction.IteratorOfType;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.java.abstraction.ListOfType;
027: import de.uka.ilkd.key.java.abstraction.SLListOfType;
028: import de.uka.ilkd.key.java.declaration.ArrayOfTypeDeclaration;
029: import de.uka.ilkd.key.java.declaration.ClassDeclaration;
030: import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
031: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
032: import de.uka.ilkd.key.jml.IteratorOfJMLMethodSpec;
033: import de.uka.ilkd.key.jml.JMLMethodSpec;
034: import de.uka.ilkd.key.jml.SetOfJMLMethodSpec;
035: import de.uka.ilkd.key.logic.Choice;
036: import de.uka.ilkd.key.logic.NamespaceSet;
037: import de.uka.ilkd.key.logic.Term;
038: import de.uka.ilkd.key.logic.TermBuilder;
039: import de.uka.ilkd.key.logic.op.*;
040: import de.uka.ilkd.key.parser.*;
041: import de.uka.ilkd.key.parser.jml.JMLSpecBuilder;
042: import de.uka.ilkd.key.proof.CountingBufferedInputStream;
043: import de.uka.ilkd.key.proof.Proof;
044: import de.uka.ilkd.key.proof.ProofAggregate;
045: import de.uka.ilkd.key.proof.mgt.*;
046: import de.uka.ilkd.key.util.ProgressMonitor;
047:
048: /** represents an input from a .key user problem file producing environment
049: * as well as a proof obligation.
050: */
051: public class KeYUserProblemFile extends KeYFile implements
052: ProofOblInput {
053:
054: private Term problemTerm = null;
055: private String problemHeader = "";
056:
057: // if false only the specifications of Object and Datagroup are read.
058: // The parsing of javacode and specifications of nonlibrary classes
059: // is not affected by this flag.
060: public static boolean parseLibSpecs = false;
061: // for disabling the parsing of java classes and their
062: // jmlspecs when running tests
063: private boolean parseJMLSpecs;
064:
065: private boolean chooseDLContract = false;
066: protected boolean tacletFile = false;
067:
068: /** creates a new representation of a KeYUserFile with the given name,
069: * a rule source representing the physical source of the input, and
070: * a graphical representation to call back in order to report the progress
071: * while reading.
072: */
073: public KeYUserProblemFile(String name, File file,
074: ProgressMonitor monitor) {
075: this (name, file, monitor, true);
076: }
077:
078: public KeYUserProblemFile(String name, File file,
079: ProgressMonitor monitor, boolean parseJMLSpecs) {
080: super (name, file, monitor);
081: this .parseJMLSpecs = parseJMLSpecs;
082: }
083:
084: public void readHelp(ModStrategy mod, boolean problemOnly)
085: throws ProofInputException {
086: if (file == null)
087: return;
088: if (initConfig == null) {
089: throw new IllegalStateException(
090: "KeYFile: InitConfig not set.");
091: }
092: try {
093: final CountingBufferedInputStream cinp = new CountingBufferedInputStream(
094: getNewStream(), monitor, getNumberOfChars() / 100);
095: final DeclPicker lexer = new DeclPicker(new KeYLexer(cinp,
096: initConfig.getServices().getExceptionHandler()));
097:
098: /*
099: two namespace sets which share all namespace except the
100: variable namespace
101: */
102: final NamespaceSet normal = initConfig.namespaces().copy();
103: final NamespaceSet schema = setupSchemaNamespace(normal);
104: final ParserConfig normalConfig = new ParserConfig(
105: initConfig.getServices(), normal);
106:
107: final ParserConfig schemaConfig = new ParserConfig(
108: initConfig.getServices(), schema);
109: problemParser = new KeYParser(ParserMode.PROBLEM, lexer,
110: file.toString(), schemaConfig, normalConfig,
111: initConfig.getTaclet2Builder(), initConfig
112: .getTaclets(), initConfig
113: .getActivatedChoices());
114: if (problemOnly) {
115: problemTerm = problemParser.parseProblem();
116: } else {
117: problemTerm = problemParser.problem();
118: }
119: String searchS = "\\problem";
120:
121: if (problemTerm == null) {
122: chooseDLContract = problemParser.getChooseContract();
123: if (chooseDLContract)
124: searchS = "\\chooseContract";
125: else {
126: if (!tacletFile) {
127: throw new ProofInputException(
128: "No \\problem or \\chooseContract in the input file!");
129: }
130: }
131: }
132: problemHeader = lexer.getText();
133: if (problemHeader != null
134: && problemHeader.lastIndexOf(searchS) != -1) {
135: problemHeader = problemHeader.substring(0,
136: problemHeader.lastIndexOf(searchS));
137: }
138: initConfig.setTaclets(problemParser.getTaclets());
139: initConfig.add(normalConfig.namespaces(), mod);
140:
141: if (!problemOnly) {
142: initConfig.getProofEnv().addMethodContracts(
143: problemParser.getContracts(), problemHeader);
144: }
145: } catch (antlr.ANTLRException e) {
146: throw new ProofInputException(e);
147: } catch (FileNotFoundException fnfe) {
148: throw new ProofInputException(fnfe);
149: }
150: }
151:
152: /** reads the whole .key file and modifies the initial configuration
153: * assigned to this object according to the given modification strategy.
154: * Throws an exception if no initial configuration has been set yet.
155: */
156: public void read(ModStrategy mod) throws ProofInputException {
157: readHelp(mod, false);
158: }
159:
160: /** reads the the problem section of the .key file and modifies
161: * the initial configuration assigned to this object according to
162: * the given modification strategy. Throws an exception if no
163: * initial configuration has been set yet.
164: */
165: public void readProblem(ModStrategy mod) throws ProofInputException {
166: readHelp(mod, true);
167: }
168:
169: public ProofAggregate getPO() {
170:
171: String name = name();
172:
173: if (problemTerm == null && chooseDLContract) {
174: Iterator it = initConfig.getProofEnv()
175: .getSpecificationRepository().getSpecs();
176: ContractSet contracts = new ContractSet();
177: while (it.hasNext()) {
178: ContractSet c = (ContractSet) it.next();
179: contracts.addAll(c);
180: }
181: final ContractSet res = new ContractSet();
182: it = contracts.iterator();
183: while (it.hasNext()) {
184: Contract c = (Contract) it.next();
185: if (c instanceof DLMethodContract)
186: res.add(c);
187: }
188:
189: UsedMethodContractsList fr = UsedMethodContractsList
190: .getInstance(Main.getInstance(false).mediator(),
191: res);
192: fr.setVisible(true);
193: DLMethodContract c = (DLMethodContract) fr.getContract();
194: if (c == null)
195: return null;
196: // Transform the header
197: c.setHeader(problemHeader);
198: problemHeader = c.getHeader();
199: DLHoareTriplePO poi = (DLHoareTriplePO) c
200: .getProofOblInput(null);
201: initConfig.getServices().getNamespaces().programVariables()
202: .add(c.getProgramVariables());
203: if (poi != null) {
204: problemTerm = poi.getTerm();
205: name = poi.name();
206: ProofAggregate po = ProofAggregate
207: .createProofAggregate(new Proof(name,
208: problemTerm, problemHeader, initConfig
209: .createTacletIndex(),
210: initConfig.createBuiltInRuleIndex(),
211: initConfig.getServices(), settings),
212: name);
213: poi.setPO(po);
214: poi.initContract(c);
215: return po;
216: }
217: return null;
218: } else {
219: return ProofAggregate.createProofAggregate(new Proof(name,
220: problemTerm, problemHeader, initConfig
221: .createTacletIndex(), initConfig
222: .createBuiltInRuleIndex(), initConfig
223: .getServices(), settings), name);
224: }
225: }
226:
227: /** returns the <code>java.io.file</code> file encapsulated by
228: * the <code>KeYUserProblemFile</code>.
229: */
230: public File getFile() {
231: return file.file();
232: }
233:
234: /**
235: * @return Returns the problemHeader.
236: */
237: protected String getProblemHeader() {
238: return problemHeader;
239: }
240:
241: /** returns true, that is the input asks the user which
242: * environment he prefers if there are multiple possibilities
243: */
244: public boolean askUserForEnvironment() {
245: return true;
246: }
247:
248: public void readSpecs() {
249: Services serv = initConfig.getServices();
250: ProgramMethod meth;
251: Iterator it;
252: if (method2jmlspecs != null && !method2jmlspecs.isEmpty()) {
253: it = method2jmlspecs.keySet().iterator();
254: while (it.hasNext()) {
255: meth = (ProgramMethod) it.next();
256: if (method2jmlspecs.get(meth) != null) {
257: IteratorOfJMLMethodSpec sit = ((SetOfJMLMethodSpec) method2jmlspecs
258: .get(meth)).iterator();
259: while (sit.hasNext()) {
260: JMLMethodSpec jmlspec = sit.next();
261: createJMLMethodContract(meth, jmlspec);
262: }
263: }
264: }
265: }
266: if (parseJMLSpecs) {
267: final Set kjts = serv.getJavaInfo().getAllKeYJavaTypes();
268: it = kjts.iterator();
269: while (it.hasNext()) {
270: final KeYJavaType kjt = (KeYJavaType) it.next();
271: if (!(kjt.getJavaType() instanceof InterfaceDeclaration || kjt
272: .getJavaType() instanceof ClassDeclaration)) {
273: continue;
274: }
275: ListOfProgramMethod ml = serv.getJavaInfo()
276: .getAllProgramMethodsLocallyDeclared(kjt);
277: IteratorOfProgramMethod mit = ml.iterator();
278: IteratorOfJMLMethodSpec sit;
279: JMLMethodSpec jmlspec;
280: while (mit.hasNext()) {
281: meth = mit.next();
282: SetOfJMLMethodSpec specs = serv
283: .getImplementation2SpecMap()
284: .getSpecsForMethod(meth);
285: if (specs != null) {
286: sit = specs.iterator();
287: while (sit.hasNext()) {
288: jmlspec = sit.next();
289: createJMLMethodContract(meth, jmlspec);
290: }
291: }
292: sit = serv.getImplementation2SpecMap()
293: .getInheritedMethodSpecs(meth, kjt)
294: .iterator();
295: while (sit.hasNext()) {
296: jmlspec = sit.next();
297: createJMLMethodContract(meth, jmlspec);
298: }
299: }
300: }
301: }
302: }
303:
304: private void createJMLMethodContract(Object meth,
305: JMLMethodSpec jmlspec) {
306: Modality[] allMod = new Modality[] { Op.DIA, Op.BOX };
307: String jp = null;
308: if (!jmlspec.isValid())
309: return;
310: try {
311: jp = readJavaPath();
312: } catch (ProofInputException e) {
313: e.printStackTrace();
314: }
315: for (int i = 0; i < allMod.length; i++) {
316: OldOperationContract mct = null;
317: if (meth instanceof ProgramMethod) {
318: KeYJavaType returnType = ((ProgramMethod) meth)
319: .getKeYJavaType();
320: if (returnType == null) {
321: returnType = initConfig.getServices().getJavaInfo()
322: .getKeYJavaType("void");
323: }
324: mct = new JMLMethodContract(new JavaModelMethod(
325: (ProgramMethod) meth, jp, initConfig
326: .getServices()), jmlspec, allMod[i]);
327: initConfig.getProofEnv().addMethodContract(mct);
328: }
329: }
330: }
331:
332: public boolean equals(Object o) {
333: if (o instanceof KeYUserProblemFile) {
334: final KeYUserProblemFile kf = (KeYUserProblemFile) o;
335:
336: if (file != null && kf.file != null) {
337: return kf.file.file().getAbsolutePath().equals(
338: file.file().getAbsolutePath());
339: }
340: if (file == null && kf.file == null) {
341: try {
342: return readJavaPath().equals(kf.readJavaPath());
343: } catch (ProofInputException e) {
344: return kf == this ;
345: }
346: }
347: }
348: return false;
349: }
350:
351: public int hashCode() {
352: if (file == null) {
353: try {
354: return readJavaPath().hashCode();
355: } catch (ProofInputException e) {
356: return 0;
357: }
358: }
359: return file.file().getAbsolutePath().hashCode();
360: }
361:
362: protected ListOfType getTypesWithJMLSpecs(CompilationUnit[] cUnits) {
363: ListOfType result = SLListOfType.EMPTY_LIST;
364: final JavaInfo ji = initConfig.getServices().getJavaInfo();
365: if (parseLibSpecs) {
366: Set kjts = ji.getAllKeYJavaTypes();
367: Iterator it = kjts.iterator();
368: while (it.hasNext()) {
369: KeYJavaType kjt = (KeYJavaType) it.next();
370: if (kjt.getJavaType() instanceof InterfaceDeclaration
371: || kjt.getJavaType() instanceof ClassDeclaration) {
372: result = result.append(kjt.getJavaType());
373: }
374: }
375: } else {
376: for (int i = 0; i < cUnits.length; i++) {
377: final ArrayOfTypeDeclaration tds = cUnits[i]
378: .getDeclarations();
379: for (int j = 0; j < tds.size(); j++) {
380: final TypeDeclaration typeDecl = tds
381: .getTypeDeclaration(j);
382: if (typeDecl instanceof InterfaceDeclaration
383: || typeDecl instanceof ClassDeclaration) {
384: result = result.append(typeDecl);
385: }
386: }
387: }
388: result = result
389: .append(ji.getJavaLangObject().getJavaType());
390: result = result.append(ji.getKeYJavaType(
391: "org.jmlspecs.lang.JMLDataGroup").getJavaType());
392: result = result.append(ji.getKeYJavaType(
393: "java.lang.Exception").getJavaType());
394: result = result.append(ji.getKeYJavaType(
395: "java.lang.Throwable").getJavaType());
396:
397: }
398: return result;
399: }
400:
401: protected void parseJMLSpecs(ListOfType types)
402: throws ProofInputException {
403: method2jmlspecs = new LinkedHashMap();
404: Set builders = new LinkedHashSet();
405: initConfig.createNamespacesForActivatedChoices();
406:
407: final IteratorOfType itt = types.iterator();
408: while (itt.hasNext()) {
409: TypeDeclaration t = (TypeDeclaration) itt.next();
410: JMLSpecBuilder builder = new JMLSpecBuilder(t, initConfig
411: .getServices(), initConfig.namespaces(),
412: TermBuilder.DF, readJavaPath(), initConfig
413: .getActivatedChoices().contains(
414: new Choice("javaSemantics",
415: "intRules")));
416: builders.add(builder);
417: }
418:
419: Iterator it = builders.iterator();
420: while (it.hasNext()) {
421: JMLSpecBuilder b = (JMLSpecBuilder) it.next();
422: b.parseModelMethodDecls();
423: }
424: it = builders.iterator();
425: while (it.hasNext()) {
426: JMLSpecBuilder b = (JMLSpecBuilder) it.next();
427: b.parseModelFieldDecls();
428: }
429: it = builders.iterator();
430: while (it.hasNext()) {
431: JMLSpecBuilder b = (JMLSpecBuilder) it.next();
432: b.parseJMLClassSpec();
433: }
434: it = builders.iterator();
435: while (it.hasNext()) {
436: JMLSpecBuilder b = (JMLSpecBuilder) it.next();
437: b.parseJMLMethodSpecs();
438: method2jmlspecs.putAll(b.getModelMethod2Specs());
439: }
440: initConfig.getServices().getImplementation2SpecMap()
441: .createLoopAnnotations();
442: }
443:
444: /**
445: * @deprecated temporary hack
446: */
447: public void readJML(CompilationUnit[] compUnits)
448: throws ProofInputException {
449: if (parseJMLSpecs) {
450: parseJMLSpecs(getTypesWithJMLSpecs(compUnits));
451: }
452: }
453:
454: public void readActivatedChoices() throws ProofInputException {
455: if (initConfig == null) {
456: throw new IllegalStateException(
457: "KeYFile: InitConfig not set.");
458: }
459: try {
460: if (settings == null)
461: getPreferences();
462:
463: ParserConfig pc = new ParserConfig(
464: initConfig.getServices(), initConfig.namespaces());
465: problemParser = new KeYParser(ParserMode.PROBLEM,
466: new KeYLexer(getNewStream(), initConfig
467: .getServices().getExceptionHandler()), file
468: .toString(), pc, pc, null, null, null);
469: problemParser.parseWith();
470:
471: settings.getChoiceSettings().updateWith(
472: problemParser.getActivatedChoices());
473:
474: initConfig.setActivatedChoices(settings.getChoiceSettings()
475: .getDefaultChoicesAsSet());
476:
477: } catch (antlr.ANTLRException e) {
478: throw new ProofInputException(e);
479: } catch (FileNotFoundException fnfe) {
480: throw new ProofInputException(fnfe);
481: }
482: }
483:
484: }
|