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.jml;
011:
012: import java.util.*;
013:
014: import de.uka.ilkd.key.collection.SetAsListOfString;
015: import de.uka.ilkd.key.collection.SetOfString;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
020: import de.uka.ilkd.key.java.abstraction.SLListOfKeYJavaType;
021: import de.uka.ilkd.key.java.annotation.LoopInvariantAnnotation;
022: import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
023: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
024: import de.uka.ilkd.key.java.statement.LoopStatement;
025: import de.uka.ilkd.key.logic.*;
026: import de.uka.ilkd.key.logic.op.IteratorOfProgramMethod;
027: import de.uka.ilkd.key.logic.op.ListOfProgramMethod;
028: import de.uka.ilkd.key.logic.op.ProgramMethod;
029: import de.uka.ilkd.key.logic.op.ProgramVariable;
030:
031: public class Implementation2SpecMap {
032:
033: //maps method declarations to a set of method specifications.
034: private HashMap method2specs;
035: //maps class or interface declarations to a class specification.
036: private TreeMap class2spec;
037: private HashMap loop2spec;
038: private HashMap method2JMLModifiers;
039: private Services services;
040: //used for caching inherited methodspecs
041: private HashMap inheritedSpecCache;
042:
043: private Term allInv = null;
044: // Namespace containing all program variables occuring in allInv
045: private Namespace allInvNS = null;
046:
047: public Implementation2SpecMap(Services services) {
048: method2specs = new HashMap();
049: class2spec = new TreeMap(new TypeComparator());
050: method2JMLModifiers = new HashMap();
051: this .services = services;
052: inheritedSpecCache = new HashMap();
053: loop2spec = new HashMap();
054: }
055:
056: private Implementation2SpecMap(HashMap method2specs,
057: TreeMap class2spec, HashMap method2JMLModifiers,
058: HashMap inheritedSpecCache, HashMap loop2spec,
059: Services services) {
060: this .method2specs = method2specs;
061: this .class2spec = class2spec;
062: this .method2JMLModifiers = method2JMLModifiers;
063: this .inheritedSpecCache = inheritedSpecCache;
064: this .loop2spec = loop2spec;
065: this .services = services;
066: }
067:
068: public void addMethodSpec(JMLMethodSpec ms) {
069: if (method2specs.get(ms.getProgramMethod()) == null) {
070: ms.setId(0);
071: method2specs.put(ms.getProgramMethod(),
072: SetAsListOfJMLMethodSpec.EMPTY_SET.add(ms));
073: } else {
074: SetOfJMLMethodSpec specs = (SetOfJMLMethodSpec) method2specs
075: .get(ms.getProgramMethod());
076: ms.setId(specs.size());
077: method2specs.put(ms.getProgramMethod(), specs.add(ms));
078: }
079: }
080:
081: public void addAllMethodSpecs(Set set) {
082: Iterator it = set.iterator();
083: while (it.hasNext()) {
084: addMethodSpec((JMLMethodSpec) it.next());
085: }
086: }
087:
088: public void setAllInvariants(Term inv) {
089: allInv = inv;
090: }
091:
092: /**
093: * returns the conjunction of all existing class invariants.
094: */
095: public Term allInvariants() {
096: return allInv;
097: }
098:
099: public void setAllInvPVNS(Namespace ns) {
100: allInvNS = ns;
101: }
102:
103: public Namespace getAllInvPVNS() {
104: return allInvNS;
105: }
106:
107: public SetOfJMLMethodSpec getSpecsForMethod(ProgramMethod md) {
108: return (SetOfJMLMethodSpec) method2specs.get(md);
109: }
110:
111: /**
112: * Removes the specifications for <code>md</code>.
113: */
114: public void clearSpecsForMethod(ProgramMethod md) {
115: method2specs.remove(md);
116: }
117:
118: public void addModifier(ProgramMethod md, String modifier) {
119: if (method2JMLModifiers.get(md) == null) {
120: method2JMLModifiers.put(md, SetAsListOfString.EMPTY_SET
121: .add(modifier));
122: } else {
123: method2JMLModifiers.put(md,
124: ((SetAsListOfString) method2JMLModifiers.get(md))
125: .add(modifier));
126: }
127: }
128:
129: public void addLoopSpec(LoopInvariant l) {
130: loop2spec.put(l.getLoop(), l);
131: }
132:
133: public void clearSpecsForLoop(LoopStatement ls) {
134: loop2spec.remove(ls);
135: }
136:
137: public LoopInvariant getSpecForLoop(LoopStatement ls) {
138: return (LoopInvariant) loop2spec.get(ls);
139: }
140:
141: /**
142: * Creates LoopInvariantAnnotations from the parsed loop specifications and
143: * adds them to the correcponding loop statements.
144: */
145: public void createLoopAnnotations() {
146: Iterator it = loop2spec.keySet().iterator();
147: while (it.hasNext()) {
148: LoopStatement loop = (LoopStatement) it.next();
149: LoopInvariant li = (LoopInvariant) loop2spec.get(loop);
150: SetOfLocationDescriptor assignable;
151: if ("nothing".equals(li.getAssignableMode())) {
152: assignable = SetAsListOfLocationDescriptor.EMPTY_SET;
153: } else if ("everything".equals(li.getAssignableMode())) {
154: assignable = SetAsListOfLocationDescriptor.EMPTY_SET
155: .add(EverythingLocationDescriptor.INSTANCE);
156: } else {
157: assignable = li.getAssignable();
158: }
159: Term[] olds = new Term[2 * li.getTerm2Old().size()];
160: Iterator kit = li.getTerm2Old().keySet().iterator();
161: int i = 0;
162: while (kit.hasNext()) {
163: Term t = (Term) kit.next();
164: olds[i++] = t;
165: olds[i++] = (Term) li.getTerm2Old().get(t);
166: }
167: loop.addLoopInvariant(new LoopInvariantAnnotation(li
168: .getInvariant(), assignable, new ArrayOfTerm(olds),
169: li.getVariant(), li.getPost(), li.getSelfVar()));
170: }
171: }
172:
173: /**
174: * adds the pure-modifier to every constructor and instance method declared
175: * in <code>kjt</code>
176: */
177: public void setPure(KeYJavaType kjt, NamespaceSet nss,
178: String javaPath) {
179: ListOfProgramMethod l = services.getJavaInfo()
180: .getAllProgramMethods(kjt);
181: IteratorOfProgramMethod it = l.iterator();
182: ProgramMethod md;
183: while (it.hasNext()) {
184: md = it.next();
185: if (!md.isStatic()) {
186: new JMLPuritySpec(md, services,
187: UsefulTools.buildParamNamespace(md
188: .getMethodDeclaration()),
189: new LinkedHashMap(), getSpecForClass(kjt), nss,
190: javaPath);
191: //%% How get the java path here???
192: addModifier(md, "pure");
193: }
194: }
195: }
196:
197: /**
198: * returns a list of KeYJavaTypes, that contain a specification for the
199: * method with the name <code>name</code>, in depth first order.
200: */
201: public ListOfKeYJavaType findSpecifications(String name,
202: KeYJavaType classType) {
203: ListOfKeYJavaType types = findSpecificationsInSubT(name,
204: classType);
205: types = types
206: .append(findSpecificationsInSuperT(name, classType));
207: return types;
208: }
209:
210: private ListOfKeYJavaType findSpecificationsInSubT(String name,
211: KeYJavaType classType) {
212: ListOfKeYJavaType types = SLListOfKeYJavaType.EMPTY_LIST;
213: JMLClassSpec cSpec = getSpecForClass(classType);
214: // TypeDeclaration td = cSpec.getClassDeclaration();
215: // %%RB are here all subtypes needed or only the direct ones
216: ListOfKeYJavaType subtypes = services.getJavaInfo()
217: .getAllSubtypes(classType);
218: if (cSpec != null
219: && cSpec.lookupModelMethodLocally(name) != null) {
220: types = types.prepend(classType);
221: }
222: IteratorOfKeYJavaType it = subtypes.iterator();
223: while (it.hasNext()) {
224: types = types.prepend(findSpecificationsInSubT(name, it
225: .next()));
226: }
227: return types;
228: }
229:
230: private ListOfKeYJavaType findSpecificationsInSuperT(String name,
231: KeYJavaType classType) {
232: ListOfKeYJavaType result = SLListOfKeYJavaType.EMPTY_LIST;
233: ListOfKeYJavaType sts = ((TypeDeclaration) classType
234: .getJavaType()).getSupertypes();
235: IteratorOfKeYJavaType it = sts.iterator();
236: while (it.hasNext()) {
237: KeYJavaType current = it.next();
238: JMLClassSpec cSpec = getSpecForClass(current);
239: if (cSpec != null
240: && cSpec.lookupModelMethodLocally(name) != null) {
241: return result.append(current);
242: } else {
243: result = findSpecificationsInSuperT(name, current);
244: if (result != SLListOfKeYJavaType.EMPTY_LIST) {
245: return result;
246: }
247: }
248: }
249: return SLListOfKeYJavaType.EMPTY_LIST;
250: }
251:
252: /**
253: * returns the method <code>methodName</code> if such a method is declared
254: * in <code>classType</code>, null otherwise.
255: */
256: public ProgramMethod lookupModelMethod(KeYJavaType classType,
257: Name methodName) {
258: JMLClassSpec spec = getSpecForClass(classType);
259: ProgramMethod pm = null;
260: if (spec != null) {
261: try {
262: pm = spec.lookupModelMethod(methodName);
263: } catch (AmbigiousModelElementException e) {
264: System.err.println(e.toString());
265: }
266: }
267: return pm;
268: }
269:
270: /**
271: * returns the field <code>fieldName</code> if such an attribute is
272: * declared in <code>classType</code>, null otherwise.
273: */
274: public ProgramVariable lookupModelField(KeYJavaType classType,
275: String fieldName) {
276: JMLClassSpec spec = getSpecForClass(classType);
277: ProgramVariable v = null;
278: if (spec != null) {
279: try {
280: v = spec.lookupModelField(new Name(fieldName));
281: } catch (AmbigiousModelElementException e) {
282: System.err.println(e.toString());
283: }
284: }
285: return v;
286: }
287:
288: public SetOfString getModifiers(ProgramMethod md) {
289: if (method2JMLModifiers.get(md) != null) {
290: return (SetOfString) method2JMLModifiers.get(md);
291: } else {
292: return SetAsListOfString.EMPTY_SET;
293: }
294: }
295:
296: /** checks whether the methods annotated with the pureModifier really
297: * have no side effect. This is done by allowing only normal_behavior
298: * specs with \nothing as assignable clause which is slightly different
299: * to jml definition of purity which allows the possibility of throwing
300: * exceptions.
301: */
302: /* public void checkPurity(){
303: Iterator it = method2JMLModifiers.keySet().iterator();
304: while(it.hasNext()){
305: MethodDeclaration md = (MethodDeclaration) it.next();
306: SetOfString set = (SetOfString) method2JMLModifiers.get(md);
307: if(set.contains("pure")){
308: SetOfJMLMethodSpec specs = getSpecsForMethod(md);
309: if(specs != null){
310: IteratorOfJMLMethodSpec spit = specs.iterator();
311: while(spit.hasNext()){
312: JMLMethodSpec spec = spit.next();
313: if(!(spec instanceof JMLNormalMethodSpec)){
314: JOptionPane.showConfirmDialog
315: (null,
316: "One of your specification cases for the "+
317: "pure method\n"+md.getName()+
318: "\nis not a normal_behavior specification case",
319: "Warning",
320: JOptionPane.DEFAULT_OPTION,
321: JOptionPane.WARNING_MESSAGE);
322: }
323: if(!spec.terminates()){
324: JOptionPane.showConfirmDialog
325: (null,
326: "Your specification for the pure method\n"+
327: md.getName()+
328: "\nallows nontermination",
329: "Warning",
330: JOptionPane.DEFAULT_OPTION,
331: JOptionPane.WARNING_MESSAGE);
332: }
333: if(!(md instanceof ConstructorDeclaration)){
334: if(!"nothing".equals(spec.getAssignableMode())){
335: JOptionPane.showConfirmDialog
336: (null,
337: "Pure Methods may not"+
338: " assign to any fields. "+
339: "\nplease check your specifications for "+
340: md.getName(),
341: "Inconsistent Specification",
342: JOptionPane.DEFAULT_OPTION,
343: JOptionPane.WARNING_MESSAGE);
344: }
345: }else{
346: IteratorOfTerm itt =
347: spec.getAssignable().iterator();
348: while(itt.hasNext()){
349: checkStatic(itt.next(), md);
350: }
351: }
352: }
353: }
354: }
355: }
356: }
357:
358: private void checkStatic(Term t, MethodDeclaration md){
359: if(t.op() instanceof ProgramVariable &&
360: !((ProgramVariable) t.op()).isStatic()){
361: JOptionPane.showConfirmDialog
362: (null,
363: "Pure Constructors may only"+
364: " assign to static fields. "+
365: "\nthat's why "+
366: md.getName()+" can't be declared pure",
367: "Inconsistent Specification",
368: JOptionPane.DEFAULT_OPTION,
369: JOptionPane.WARNING_MESSAGE);
370: }
371: if(t.op() instanceof AttributeOp){
372: checkStatic(t.sub(0), md);
373: }
374: if(t.op() instanceof ArrayOp){
375: checkStatic(t.sub(0), md);
376: checkStatic(t.sub(1), md);
377: }
378: }
379: */
380:
381: public void addClassSpec(JMLClassSpec cs) {
382: class2spec.put(services.getJavaInfo().getKeYJavaType(
383: cs.getClassDeclaration()), cs);
384: }
385:
386: public JMLClassSpec getSpecForClass(KeYJavaType classType) {
387: return (JMLClassSpec) class2spec.get(classType);
388: }
389:
390: public void removeMethodSpec(JMLMethodSpec ms) {
391: if (method2specs.get(ms.getProgramMethod()) != null) {
392: method2specs.put(ms.getProgramMethod(),
393: ((SetOfJMLMethodSpec) method2specs.get(ms
394: .getProgramMethod())).remove(ms));
395: }
396: }
397:
398: public void removeClassSpec(JMLClassSpec cs) {
399: class2spec.remove(services.getJavaInfo().getKeYJavaType(
400: cs.getClassDeclaration()));
401: }
402:
403: public Implementation2SpecMap copy(Services serv) {
404: Implementation2SpecMap ism = new Implementation2SpecMap(
405: (HashMap) method2specs.clone(), (TreeMap) class2spec
406: .clone(),
407: (HashMap) method2JMLModifiers.clone(),
408: (HashMap) inheritedSpecCache.clone(),
409: (HashMap) loop2spec.clone(), serv);
410: // ism.setProgVarNS(getProgVarNS());
411: return ism;
412: }
413:
414: public boolean equals(Object o) {
415: if (!(o instanceof Implementation2SpecMap)) {
416: return false;
417: }
418: Implementation2SpecMap ism = (Implementation2SpecMap) o;
419: return ism.method2specs.equals(method2specs)
420: && ism.class2spec.equals(class2spec)
421: && ism.loop2spec.equals(loop2spec);
422: }
423:
424: public int hashCode() {
425: return method2specs.hashCode() + 5 * class2spec.hashCode() + 17
426: * loop2spec.hashCode();
427: }
428:
429: /**
430: * returns all methoddeclarations in this map.
431: */
432: public Set getAllMethods() {
433: return method2specs.keySet();
434: }
435:
436: /**
437: * returns all classtypes in this map.
438: */
439: public Set getAllClasses() {
440: return class2spec.keySet();
441: }
442:
443: public SetOfJMLMethodSpec getInheritedMethodSpecs(ProgramMethod md,
444: KeYJavaType classType) {
445: InhKey key = new InhKey(md, classType);
446: if (inheritedSpecCache.get(key) != null) {
447: return (SetOfJMLMethodSpec) inheritedSpecCache.get(key);
448: }
449: SetOfJMLMethodSpec inh = SetAsListOfJMLMethodSpec.EMPTY_SET;
450: if (classType.getJavaType() instanceof InterfaceDeclaration
451: ||
452: /*"equals".equals(md.getName()) ||*/"finalize"
453: .equals(md.getName())
454: || "wait".equals(md.getName())
455: || "getClass".equals(md.getName())) {
456: return inh;
457: }
458: ListOfKeYJavaType st = services.getJavaInfo().getAllSupertypes(
459: classType);
460: IteratorOfKeYJavaType it = st.iterator();
461: ListOfKeYJavaType alreadyVisited = SLListOfKeYJavaType.EMPTY_LIST;
462: alreadyVisited = alreadyVisited.append(classType);
463: while (it.hasNext()) {
464: KeYJavaType current = it.next();
465: if (alreadyVisited.contains(current)) {
466: continue;
467: } else {
468: alreadyVisited = alreadyVisited.append(current);
469: }
470: ListOfProgramMethod l = services.getJavaInfo()
471: .getAllProgramMethods(current);
472: IteratorOfProgramMethod pmIt = l.iterator();
473: while (pmIt.hasNext()) {
474: SetOfJMLMethodSpec specs = getSpecsForMethod(pmIt
475: .next());
476: if (specs != null) {
477: IteratorOfJMLMethodSpec sIt = specs.iterator();
478: while (sIt.hasNext()) {
479: JMLMethodSpec spec = sIt.next();
480: if (!(spec instanceof JMLPuritySpec)
481: && spec.isCloneableFor(md)
482: && getSpecForClass(classType) != null
483: && spec.getInheritedPrefix() == null) {
484: inh = inh.add(spec.cloneFor(md,
485: getSpecForClass(classType)));
486: } else if (!spec.isCloneableFor(md)) {
487: break;
488: }
489: }
490: }
491: }
492: }
493: inheritedSpecCache.put(key, inh);
494: return inh;
495: }
496:
497: final static class TypeComparator implements Comparator {
498:
499: public int compare(Object o1, Object o2) {
500: final KeYJavaType type1 = (KeYJavaType) o1;
501: final KeYJavaType type2 = (KeYJavaType) o2;
502: // attention this is only sane as long as types
503: // are uniquely identified by their name
504: return type1.getFullName().compareTo(type2.getFullName());
505: }
506: }
507:
508: private static class InhKey {
509:
510: protected ProgramMethod md;
511: protected KeYJavaType ct;
512:
513: public InhKey(ProgramMethod md, KeYJavaType ct) {
514: this .md = md;
515: this .ct = ct;
516: }
517:
518: public boolean equals(Object o) {
519: if (!(o instanceof InhKey))
520: return false;
521: return ((InhKey) o).md == md && ((InhKey) o).ct == ct;
522: }
523:
524: public int hashCode() {
525: return md.hashCode() + 31 * ct.hashCode();
526: }
527: }
528: }
|