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.parser.jml;
011:
012: import java.io.StringReader;
013: import java.util.*;
014:
015: import antlr.RecognitionException;
016:
017: import de.uka.ilkd.key.java.Comment;
018: import de.uka.ilkd.key.java.IteratorOfProgramElement;
019: import de.uka.ilkd.key.java.ListOfProgramElement;
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
022: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
023: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
024: import de.uka.ilkd.key.java.recoderext.ClassInitializeMethodBuilder;
025: import de.uka.ilkd.key.java.statement.LoopStatement;
026: import de.uka.ilkd.key.java.visitor.JavaASTCollector;
027: import de.uka.ilkd.key.jml.*;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.IteratorOfProgramMethod;
030: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
031: import de.uka.ilkd.key.logic.op.Op;
032: import de.uka.ilkd.key.logic.op.ProgramMethod;
033: import de.uka.ilkd.key.proof.init.ProofInputException;
034: import de.uka.ilkd.key.util.ExceptionHandlerException;
035:
036: /**
037: * provides methods for parsing the specifications of a single class/interface.
038: */
039: public class JMLSpecBuilder {
040:
041: private TypeDeclaration cd;
042: private Services services;
043: private NamespaceSet nss;
044: private TermBuilder tb;
045: private boolean parsedMethods = false;
046: private boolean parsedClass = false;
047: private LinkedHashMap method2specs = new LinkedHashMap();
048: private LinkedHashMap method2term = null;
049: private JMLClassSpec classSpec = null;
050: private ArithOpProvider aOP = null;
051: //contains jml-comments in cd
052: private LinkedHashSet jmlComments = null;
053: //contains jml-comments without model method declarations.
054: private LinkedHashSet jmlCommentsWithoutMM = null;
055: //contains jml-comments without model method and model field declarations.
056: private LinkedHashSet jmlCommentsWithoutMFMM = null;
057: //where the sources for the input are below
058: private String javaPath;
059:
060: public JMLSpecBuilder(TypeDeclaration cd, Services services,
061: NamespaceSet nss, TermBuilder tb, String javaPath,
062: boolean javaSemantics) {
063: this .cd = cd;
064: this .services = services;
065: this .nss = nss;
066: this .tb = tb;
067: aOP = new DefaultArithOpProvider(nss.functions(), javaSemantics);
068: Comment[] comments = cd.getComments();
069: if (comments != null) {
070: jmlComments = new LinkedHashSet();
071: for (int i = 0; i < comments.length; i++) {
072: if (comments[i].containsJMLSpec()) {
073: jmlComments.add(comments[i].getJMLSpec());
074: }
075: }
076: }
077: this .javaPath = javaPath;
078: }
079:
080: public TypeDeclaration getTypeDeclaration() {
081: return cd;
082: }
083:
084: /**
085: * returns a term containing the proofobligations for the methodspecs
086: * of <code>pm</code> and the invariant and constraint proofobligation
087: * for the containing class.
088: */
089: public Term buildProofObligation(ProgramMethod pm) {
090: Implementation2SpecMap ism = services
091: .getImplementation2SpecMap();
092: SetOfJMLMethodSpec specs = ism.getSpecsForMethod(pm);
093: classSpec = ism.getSpecForClass(pm.getContainerType());
094: return makeConjunction(specs, pm);
095: }
096:
097: /**
098: * parses jml model fields declared in <code>cd</code>.
099: * Can't be called before parseModelMethodDecls() has been called
100: */
101: public void parseModelFieldDecls() throws ProofInputException {
102: if (jmlCommentsWithoutMFMM == null
103: && jmlCommentsWithoutMM != null) {
104: jmlCommentsWithoutMFMM = new LinkedHashSet();
105: Iterator it = jmlCommentsWithoutMM.iterator();
106: while (it.hasNext()) {
107: String s = (String) it.next();
108: parseFieldDecl(s, jmlCommentsWithoutMFMM, classSpec);
109: }
110: } else {
111: throw new ProofInputException(
112: jmlCommentsWithoutMFMM == null ? "Tried to parse model field "
113: + "declarations before parsing "
114: + "model method declarations"
115: : "already parsed model field "
116: + "declarations for class/interface "
117: + cd);
118: }
119: }
120:
121: /**
122: * parses jml model methods declared in <code>cd</code>.
123: */
124: public void parseModelMethodDecls() throws ProofInputException {
125: if (jmlCommentsWithoutMM == null) {
126: classSpec = new JMLClassSpec(services, cd, nss, javaPath);
127: jmlCommentsWithoutMM = new LinkedHashSet();
128: Iterator it = jmlComments.iterator();
129: while (it.hasNext()) {
130: String s = (String) it.next();
131: parseMethodDecl(s, jmlCommentsWithoutMM, classSpec);
132: }
133: } else {
134: throw new ProofInputException(
135: "already parsed model method "
136: + "declarations for class/interface " + cd);
137: }
138: }
139:
140: /**
141: * parses jml specification like invariants, constraints or represents
142: * in <code>cd</code>. parseModelMethodDecls() and parseModelFieldDecls()
143: * have to be called first.
144: */
145: public void parseJMLClassSpec() throws ProofInputException {
146: if (!parsedClass && jmlCommentsWithoutMFMM != null) {
147: Iterator it = jmlCommentsWithoutMFMM.iterator();
148: while (it.hasNext()) {
149: String s = (String) it.next();
150: if (s.trim().equals("") || s.matches("@?\\s*in \\w+;"))
151: continue;
152: StringReader stream = new StringReader(s);
153: KeYJMLParser parser = new KeYJMLParser(new KeYJMLLexer(
154: stream), "no file, parsing comment from "
155: + cd.getName(), services, nss,
156: TermFactory.DEFAULT, cd, null, classSpec, aOP,
157: javaPath);
158: try {
159: parser.parseClassSpec();
160: } catch (ExceptionHandlerException e1) {
161: if (!(e1.getCause() instanceof NotSupportedExpressionException)) {
162: if (e1.getCause() instanceof RecognitionException) {
163: reportRecognitionException((RecognitionException) e1
164: .getCause());
165: } else {
166: throw e1;
167: }
168: } else {
169: services.getExceptionHandler().clear();
170: }
171: } catch (antlr.RecognitionException e) {
172: reportRecognitionException(e);
173: } catch (antlr.ANTLRException e) {
174: throw new ProofInputException(e);
175: }
176: }
177: parsedClass = true;
178: } else {
179: if (jmlCommentsWithoutMFMM == null) {
180: throw new ProofInputException(
181: "tried to parse class spec "
182: + "without parsing model "
183: + "declarations for class " + cd
184: + " first");
185: }
186: }
187: }
188:
189: /**
190: * @param e1
191: * @throws ProofInputException
192: */
193: private void reportRecognitionException(RecognitionException e)
194: throws ProofInputException {
195: int line = e.getLine();
196: int column = e.getColumn();
197: throw new ProofInputException(e.getFilename() + "(" + line
198: + "," + column + "): " + e.getMessage());
199: }
200:
201: public NamespaceSet namespaces() {
202: return nss;
203: }
204:
205: private void parseMethodDecl(String s, Set otherSpecs,
206: JMLClassSpec cs) throws ProofInputException {
207: int mIndex = s.indexOf("model ");
208: if (mIndex == -1
209: || (s.indexOf("_behavior") == -1 && s
210: .indexOf("requires") == -1)) {
211: otherSpecs.add(s);
212: return;
213: }
214: int start = s.substring(0, mIndex + 1).lastIndexOf("\n") + 1;
215: int end = s.indexOf(";", mIndex);
216: int lbIndex = s.indexOf("{", mIndex);
217: if (end == -1 || (end > lbIndex && lbIndex != -1)) {
218: end = s.length() - 1;
219: }
220: int pIndex = s.indexOf("(", mIndex);
221: if (pIndex > end || pIndex == -1) {
222: if (end == s.length() - 1 || pIndex == -1) {
223: otherSpecs.add(s);
224: } else {
225: otherSpecs.add(s.substring(0, end));
226: parseMethodDecl(s.substring(end + 1), otherSpecs, cs);
227: }
228: return;
229: }
230: String methDecl = s.substring(start, end + 1);
231: StringReader stream = new StringReader(methDecl);
232: String nonMethSpec;
233: if (s.indexOf("_behavior") != -1) {
234: nonMethSpec = s.substring(0, start).split(
235: "public +[a-z]+_behavior", 2)[0];
236: } else {
237: nonMethSpec = s.substring(0, start).split("requires", 2)[0];
238: }
239: String methSpec = "/*@ "
240: + s.substring(0, start).substring(nonMethSpec.length())
241: + " @*/";
242: otherSpecs.add(nonMethSpec);
243:
244: KeYJMLParser parser = new KeYJMLParser(new KeYJMLLexer(stream),
245: "parsing comment from " + cd.getName(), services, nss,
246: TermFactory.DEFAULT, cd, null, cs, aOP, javaPath);
247: try {
248: parser.parseMethodDecl(methSpec);
249: } catch (ExceptionHandlerException e1) {
250: if (!(e1.getCause() instanceof NotSupportedExpressionException)) {
251: if (e1.getCause() instanceof RecognitionException) {
252: reportRecognitionException((RecognitionException) e1
253: .getCause());
254: } else {
255: throw e1;
256: }
257: } else {
258: services.getExceptionHandler().clear();
259: }
260: } catch (RecognitionException e) {
261: reportRecognitionException(e);
262: } catch (antlr.ANTLRException e) {
263: throw new ProofInputException(e);
264: }
265: parseMethodDecl(s.substring(end + 1), otherSpecs, cs);
266: }
267:
268: private void parseFieldDecl(String s, Set otherSpecs,
269: JMLClassSpec cs) throws ProofInputException {
270:
271: int mIndex = s.indexOf("model ");
272: if (mIndex == -1)
273: mIndex = s.indexOf("ghost");
274: if (mIndex != -1) {
275: int start = s.substring(0, mIndex + 1).lastIndexOf("\n");
276: int end = s.indexOf(";", mIndex);
277: int endNextLine = s.indexOf(";", end + 1);
278: if (s.indexOf("in", end) != -1
279: && s.indexOf("in", end) < endNextLine) {
280: end = endNextLine;
281: }
282: otherSpecs.add(s.substring(0, start + 1));
283: StringReader stream = new StringReader(s.substring(
284: start + 1, end + 1));
285: KeYJMLParser parser = new KeYJMLParser(new KeYJMLLexer(
286: stream), "parsing comment from " + cd.getName(),
287: services, nss, TermFactory.DEFAULT, cd, null, cs,
288: aOP, javaPath);
289: try {
290: parser.parseFieldDecl();
291:
292: } catch (ExceptionHandlerException e1) {
293: if (!(e1.getCause() instanceof NotSupportedExpressionException)) {
294: if (e1.getCause() instanceof RecognitionException) {
295: reportRecognitionException((RecognitionException) e1
296: .getCause());
297: } else {
298: throw e1;
299: }
300: } else {
301: services.getExceptionHandler().clear();
302: }
303: } catch (RecognitionException e) {
304: reportRecognitionException(e);
305: } catch (antlr.ANTLRException e) {
306: throw new ProofInputException(e);
307: }
308: parseFieldDecl(s.substring(end + 1), otherSpecs, cs);
309: } else {
310: otherSpecs.add(s);
311: }
312: }
313:
314: /**
315: * parses the specifications attached as comments to <code>m</code>.
316: */
317: protected SetOfJMLMethodSpec parseJMLMethodSpec(ProgramMethod m)
318: throws ProofInputException {
319: SetOfJMLMethodSpec result = SetAsListOfJMLMethodSpec.EMPTY_SET;
320: if (m.getMethodDeclaration() == null) {
321: return result;
322: }
323: MethodDeclaration md = m.getMethodDeclaration();
324: Comment[] comments = md.getComments();
325: if (comments != null) {
326: for (int i = 0; i < comments.length; i++) {
327: if (comments[i].containsJMLSpec()
328: && !UsefulTools.isClassSpec(comments[i])) {
329: String s = comments[i].getJMLSpec();
330: StringReader stream = new StringReader(s);
331: KeYJMLParser parser = new KeYJMLParser(
332: new KeYJMLLexer(stream),
333: "no file, parsing comment from "
334: + md.getName() + " in class "
335: + cd.getName(), services, nss,
336: TermFactory.DEFAULT, cd, m, classSpec, aOP,
337: javaPath);
338: try {
339: parser.methodspecification();
340: } catch (ExceptionHandlerException e1) {
341: if (!(e1.getCause() instanceof NotSupportedExpressionException)) {
342: throw e1;
343: } else {
344: services.getExceptionHandler().clear();
345: }
346: } catch (antlr.ANTLRException e) {
347: throw new ProofInputException(e);
348: }
349: result = result.union(parser.getSpecs());
350: }
351: }
352: }
353: parseLoopInvariants(m);
354: return result;
355: }
356:
357: private void parseLoopInvariants(ProgramMethod md)
358: throws ProofInputException {
359: JavaASTCollector coll = new JavaASTCollector(md,
360: de.uka.ilkd.key.java.statement.LoopStatement.class);
361: coll.start();
362: ListOfProgramElement l = coll.getNodes();
363: IteratorOfProgramElement it = l.iterator();
364: LoopStatement loop;
365: while (it.hasNext()) {
366: loop = (LoopStatement) it.next();
367: Comment[] comments = loop.getComments();
368: if (comments != null) {
369: for (int i = 0; i < comments.length; i++) {
370: if (comments[i].containsJMLSpec()) {
371: String s = comments[i].getJMLSpec();
372: StringReader stream = new StringReader(s);
373: KeYJMLParser parser = new KeYJMLParser(
374: new KeYJMLLexer(stream),
375: "no file, parsing comment from loop"
376: + " in method " + md.getName()
377: + " in class " + cd.getName(),
378: services, nss, TermFactory.DEFAULT, cd,
379: md, classSpec, aOP, javaPath);
380: try {
381: parser.parseLoopInvariant(loop);
382: } catch (ExceptionHandlerException e1) {
383: if (!(e1.getCause() instanceof NotSupportedExpressionException)) {
384: throw e1;
385: } else {
386: services.getExceptionHandler().clear();
387: }
388: } catch (antlr.ANTLRException e) {
389: throw new ProofInputException(e);
390: }
391: }
392: }
393: }
394: }
395: }
396:
397: /**
398: * returns a mapping from methods to terms that are conjunctions
399: * of the proofobligations generated from the methodspecs of these methods
400: * obsolete (but for testing reasons still there).
401: */
402: public HashMap buildProofObligations() throws ProofInputException {
403: if (!parsedMethods || !parsedClass) {
404: parseSpecs();
405: }
406: if (method2term != null) {
407: return method2term;
408: } else {
409: method2term = new LinkedHashMap();
410: Iterator it = method2specs.keySet().iterator();
411: while (it.hasNext()) {
412: Object m = it.next();
413: Term t = makeConjunction(
414: (SetOfJMLMethodSpec) method2specs.get(m),
415: (ProgramMethod) m);
416: if (t != null) {
417: method2term.put(m, t);
418: }
419: }
420: }
421: return method2term;
422: }
423:
424: /**
425: * returns a conjunction of the proofobligations for <code>md</code>
426: * generated from <code>specs</code>.
427: * obsolete (but for testing reasons still there).
428: */
429: private Term makeConjunction(SetOfJMLMethodSpec specs,
430: ProgramMethod md) {
431: Term result = null;
432: Term a, inv, invPre;
433: JMLMethodSpec spec;
434: if (specs != SetAsListOfJMLMethodSpec.EMPTY_SET) {
435: IteratorOfJMLMethodSpec it = specs.iterator();
436: spec = it.next();
437: result = spec.createDLFormula(false, false);
438: inv = classSpec.getPreservesInvariantBehavior(md, false);
439: invPre = spec.getCompletePre(false, false, false);
440: while (it.hasNext()) {
441: spec = it.next();
442: a = spec.createDLFormula(false, false);
443: invPre = tb.or(
444: spec.getCompletePre(false, false, false),
445: invPre);
446: if (a != null) {
447: if (result.op() != Op.TRUE) {
448: result = tb.and(result, a);
449: } else {
450: result = a;
451: }
452: }
453: }
454: if (inv != null) {
455: inv = tb.imp(invPre, inv);
456: }
457: if (result != null && result.op() != Op.TRUE) {
458: if (inv != null) {
459: result = tb.and(result, inv);
460: }
461: } else {
462: result = inv;
463: }
464: // the method has no specification, but maybe it has to preserve
465: // invariants, etc.
466: // implicit methods need a special treatment.
467: } else if (!md.getName().startsWith("<")
468: && (!md.isStatic()
469: && (classSpec.getInstanceInvariants() != null || classSpec
470: .getInstanceConstraints() != null) || classSpec
471: .getStaticConstraints() != null)
472: || classSpec.getStaticInvariants() != null
473: && (!md.getName().startsWith("<") || md
474: .getName()
475: .equals(
476: ClassInitializeMethodBuilder.CLASS_INITIALIZE_IDENTIFIER))) {
477: result = classSpec.getPreservesInvariantBehavior(md, false);
478: }
479: return result;
480: }
481:
482: /**
483: * returns a map from methods to the specs which have been parsed by this
484: * JMLSpecBuilder.
485: */
486: public HashMap getMethod2Specs() {
487: try {
488: parseSpecs();
489: } catch (ProofInputException e) {
490: e.printStackTrace();
491: }
492: return method2specs;
493: }
494:
495: /**
496: * returns a map with the model methods and their specs
497: * parsed by this JMLSpecBuilder.
498: */
499: public HashMap getModelMethod2Specs() {
500: try {
501: parseSpecs();
502: } catch (ProofInputException e) {
503: e.printStackTrace();
504: }
505: return classSpec.buildModelMethod2Specs();
506: }
507:
508: /**
509: * Parses the specs of the methods declared in <code>cd</code>
510: */
511: public void parseJMLMethodSpecs() throws ProofInputException {
512: if (parsedMethods) {
513: return;
514: }
515: if (cd.getFullName().indexOf("jmlspecs.models") == -1) {
516: KeYJavaType kjt = services.getJavaInfo().getKeYJavaType(cd);
517: ListOfProgramMethod ms = services.getJavaInfo()
518: .getKeYProgModelInfo()
519: .getAllProgramMethodsLocallyDeclared(kjt).append(
520: services.getJavaInfo()
521: .getKeYProgModelInfo()
522: .getConstructors(kjt));
523: IteratorOfProgramMethod it = ms.iterator();
524: while (it.hasNext()) {
525: ProgramMethod m = it.next();
526: if (m != null) {
527: method2specs.put(m, parseJMLMethodSpec(m));
528: }
529: }
530:
531: }
532: IteratorOfNamed mmit = classSpec.getModelMethods()
533: .allElements().iterator();
534: while (mmit.hasNext()) {
535: ProgramMethod m = (ProgramMethod) mmit.next();
536: parseJMLMethodSpec(m);
537: }
538: parsedMethods = true;
539: }
540:
541: private void parseSpecs() throws ProofInputException {
542: parseJMLClassSpec();
543: parseJMLMethodSpecs();
544: }
545: }
|