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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2003 Universitaet Karlsruhe, Germany
011: // and Chalmers University of Technology, Sweden
012: //
013: // The KeY system is protected by the GNU General Public License.
014: // See LICENSE.TXT for details.
015: //
016:
017: package de.uka.ilkd.key.jml;
018:
019: import java.util.HashMap;
020: import java.util.Iterator;
021:
022: import de.uka.ilkd.key.java.Comment;
023: import de.uka.ilkd.key.java.Services;
024: import de.uka.ilkd.key.java.StatementBlock;
025: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
026: import de.uka.ilkd.key.java.declaration.*;
027: import de.uka.ilkd.key.java.recoderext.ImplicitFieldAdder;
028: import de.uka.ilkd.key.java.reference.ReferencePrefix;
029: import de.uka.ilkd.key.java.reference.TypeRef;
030: import de.uka.ilkd.key.logic.*;
031: import de.uka.ilkd.key.logic.op.*;
032: import de.uka.ilkd.key.logic.sort.ObjectSort;
033: import de.uka.ilkd.key.logic.sort.Sort;
034: import de.uka.ilkd.key.rule.UpdateSimplifier;
035: import de.uka.ilkd.key.rule.updatesimplifier.Update;
036:
037: public class UsefulTools {
038:
039: private static final UpdateSimplifier simplifier = new UpdateSimplifier();
040:
041: private UsefulTools() {
042: }
043:
044: /**
045: * Checks whether <code>a</code> occurs in <code>b</code> or not. If
046: * <code>ignoreMod</code> is true, subterms with a modality as top operant
047: * are ignored.
048: */
049: public static boolean occursIn(Term a, Term b, boolean ignoreMod) {
050: if (a == null || b == null) {
051: return false;
052: }
053: if (a.equals(b)) {
054: return true;
055: } else if (b.op() instanceof Modality && ignoreMod) {
056: return false;
057: } else {
058: for (int i = 0; i < b.arity(); i++) {
059: if (occursIn(a, b.sub(i), ignoreMod))
060: return true;
061: }
062: }
063: return false;
064: }
065:
066: /**
067: * Checks whether <code>attr</code> occurs in <code>b</code> and
068: * returns the terms of the form t.attr that have been found in
069: * <code>b</code>. If <code>ignoreMod</code> is true,
070: * subterms with a modality as top operant are ignored.
071: */
072: public static ListOfTerm occursAsAttr(ProgramVariable attr, Term b,
073: boolean ignoreMod) {
074: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
075: if (b == null) {
076: return result;
077: }
078: if ((b.op() instanceof AttributeOp)
079: && ((AttributeOp) b.op()).attribute() == attr) {
080: return result.append(b);
081: }
082: if (b.op() instanceof Modality && ignoreMod) {
083: return result;
084: }
085: for (int i = 0; i < b.arity(); i++) {
086: result = result.append(occursAsAttr(attr, b.sub(i),
087: ignoreMod));
088: }
089: return result;
090: }
091:
092: /**
093: * Collects the model variables in <code>b</code>.
094: * If <code>ignoreMod</code> is true,
095: * subterms with a modality as top operant are ignored.
096: */
097: public static SetOfTerm collectModelVariables(Term b,
098: boolean ignoreMod) {
099: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
100: if (b == null) {
101: return result;
102: }
103: if ((b.op() instanceof AttributeOp)
104: && (((AttributeOp) b.op()).attribute() instanceof ProgramVariable)
105: && ((ProgramVariable) ((AttributeOp) b.op())
106: .attribute()).isModel()) {
107: return result.add(b);
108: }
109: if ((b.op() instanceof ProgramVariable)
110: && ((ProgramVariable) b.op()).isModel()) {
111: return result.add(b);
112: }
113: if (b.op() instanceof Modality && ignoreMod) {
114: return result;
115: }
116: for (int i = 0; i < b.arity(); i++) {
117: result = result.union(collectModelVariables(b.sub(i),
118: ignoreMod));
119: }
120: return result;
121: }
122:
123: /**
124: * adds updates for represents clauses if necessary. These Updates have the
125: * form {m := m()}t
126: * where m is a modelfield and m() is a query generated from the represents
127: * clause for m.
128: */
129: public static Term addRepresents(Term t, Services services,
130: ProgramVariable self) {
131: if (t == null)
132: return t;
133: SetOfTerm fields = collectModelVariables(t, false);
134: if (fields != SetAsListOfTerm.EMPTY_SET) {
135: IteratorOfTerm it = fields.iterator();
136: UpdateFactory uf = new UpdateFactory(services, simplifier);
137: Update update = null;
138: while (it.hasNext()) {
139: Term field = it.next();
140: Term value;
141: if (field.op() instanceof AttributeOp) {
142: KeYJavaType kjt = services.getJavaInfo()
143: .getKeYJavaType(field.sub(0).sort());
144: HashMap rep = services.getImplementation2SpecMap()
145: .getSpecForClass(kjt).getRepresents();
146: ProgramVariable v = (ProgramVariable) ((AttributeOp) field
147: .op()).attribute();
148: if (rep.get(v) != null) {
149: value = simplifyRepresentsMethod(
150: TermFactory.DEFAULT
151: .createFunctionTerm(
152: (TermSymbol) ((Term) rep
153: .get(v)).op(),
154: field.sub(0)),
155: services, self);
156: } else {
157: // This case can occur if the representsclause contains
158: // an unsupported JML feature (or if the specification
159: // is syntactically invalid).
160: value = field;
161: }
162: } else {
163: final ProgramVariable v = (ProgramVariable) field
164: .op();
165: HashMap rep;
166: // if(v.isStatic()){
167: rep = services.getImplementation2SpecMap()
168: .getSpecForClass(v.getContainerType())
169: .getRepresents();
170: value = simplifyRepresentsMethod((Term) rep.get(v),
171: services, self);
172: // }
173: }
174: if (update == null) {
175: update = uf.elementaryUpdate(field, value);
176: } else {
177: update = uf.parallel(update, uf.elementaryUpdate(
178: field, value));
179: }
180: }
181: if (update != null) {
182: t = uf.apply(update, t);
183: }
184: }
185: return t;
186: }
187:
188: public static Term createTermForQuery(ProgramMethod pm,
189: ListOfTerm args, ReferencePrefix prefix) {
190: Term[] sub;
191: TermFactory tf = TermFactory.DEFAULT;
192: int i = 0;
193: if (pm.isStatic()) {
194: sub = new Term[args.size()];
195: } else {
196: sub = new Term[args.size() + 1];
197: sub[i++] = tf.createVariableTerm((ProgramVariable) prefix);
198: }
199: IteratorOfTerm it = args.iterator();
200: while (it.hasNext()) {
201: sub[i++] = it.next();
202: }
203: return tf.createFunctionTerm(pm, sub);
204: }
205:
206: public static ListOfTerm getProgramVariablesFromTerm(Term t,
207: ListOfTerm result) {
208: if (t == null) {
209: return result;
210: }
211: if (t.op() instanceof ProgramVariable) {
212: if (!result.contains(t)) {
213: result = result.append(t);
214: }
215: }
216: for (int i = 0; i < t.arity(); i++) {
217: result = getProgramVariablesFromTerm(t.sub(i), result);
218: }
219: return result;
220: }
221:
222: public static ParameterDeclaration getParameterDeclForVar(Term var,
223: Services serv) {
224: ProgramVariable pv = (ProgramVariable) var.op();
225: KeYJavaType kjt = pv.getKeYJavaType();
226: if (kjt == null) {
227: kjt = serv.getJavaInfo().getKeYJavaType(var.sort());
228: }
229: return new ParameterDeclaration(new Modifier[0], new TypeRef(
230: kjt), new VariableSpecification(pv), false);
231: }
232:
233: /** <code>a</code> is a function term for a query. If the specification
234: * of this query has a postcondition of the form \result == b then
235: * b is returned otherwise a is returned.
236: *
237: */
238: private static Term simplifyRepresentsMethod(Term a,
239: Services services, ProgramVariable self) {
240: Implementation2SpecMap ism = services
241: .getImplementation2SpecMap();
242: if (a.arity() > 0 && a.sub(0).op() == self) {
243: TermFactory tf = TermFactory.DEFAULT;
244: ProgramMethod pm = (ProgramMethod) a.op();
245: if (ism.getSpecsForMethod(pm) == null)
246: return a;
247: JMLMethodSpec spec = ism.getSpecsForMethod(pm).iterator()
248: .next();
249: Term post = spec.getPost();
250: if (post.op() instanceof Equality
251: && collectModelVariables(post, false) == SetAsListOfTerm.EMPTY_SET) {
252: if (spec.getPrefix() instanceof ProgramVariable
253: && spec.getPrefix() != self) {
254: post = tf.createUpdateTerm(tf
255: .createVariableTerm((ProgramVariable) spec
256: .getPrefix()), tf
257: .createVariableTerm(self), post);
258: post = simplifier.simplify(post, services);
259:
260: }
261: if (post.sub(0).op() == spec.getResultVar()) {
262: return post.sub(1);
263: } else if (post.sub(1).op() == spec.getResultVar()) {
264: return post.sub(0);
265: }
266: }
267: }
268: return a;
269: }
270:
271: /**
272: * Checks whether only pure methods have been used in this specification or
273: * not.
274: * @return null iff every method used in this term is declared
275: * with the jml-modifier pure or a method that isn't declared
276: * with pure otherwise.
277: */
278: public static ProgramMethod purityCheck(JMLMethodSpec spec,
279: Implementation2SpecMap ism) {
280: Term t = spec.createDLFormula(true, false);
281: return purityCheck(t, ism);
282: }
283:
284: /**
285: * Checks whether only pure methods have been used in this term or
286: * not.
287: * @return null iff every method used in this term is declared
288: * with the jml-modifier pure or a method that isn't declared
289: * with pure otherwise.
290: */
291: public static ProgramMethod purityCheck(Term t,
292: Implementation2SpecMap ism) {
293: if (t.op() instanceof ProgramMethod) {
294: if (!ism.getModifiers((ProgramMethod) t.op()).contains(
295: "pure")) {
296: return (ProgramMethod) t.op();
297: }
298: }
299:
300: for (int i = 0; i < t.arity(); i++) {
301: if (purityCheck(t.sub(i), ism) != null) {
302: return purityCheck(t.sub(i), ism);
303: }
304: }
305: return null;
306: }
307:
308: /**
309: * Returns forall self_lv( {self:=self_lv} t ) if <code>t</code> is neither
310: * static nor a constructor or <code>t</code> otherwise.
311: */
312: public static Term quantifySelf(Term t, MethodDeclaration md,
313: ProgramVariable self) {
314: if (!md.isStatic() && !(md instanceof ConstructorDeclaration)) {
315: TermFactory tf = TermFactory.DEFAULT;
316: Term vTerm = tf.createVariableTerm(self);
317: LogicVariable lv = new LogicVariable(new Name(self.name()
318: + "_lv"), self.sort());
319: Term lvTerm = tf.createVariableTerm(lv);
320: t = tf.createUpdateTerm(vTerm, lvTerm, t);
321: t = TermBuilder.DF.all(lv, t);
322: }
323: return t;
324: }
325:
326: /** Creates a quantified LogicVariable lv_i for ProgramVariabes p_i in
327: * <code>t</code> that aren't contained in the Namespace <code>ns</code>.
328: * @return q lv_1...lv_n {p_1 := lv_1}..{p_n := lv_n} t.
329: */
330: public static Term quantifyProgramVariables(Term t, Namespace ns,
331: Quantifier q, Services serv) {
332: SetOfNamed pvs = helpQuantify(t, ns.allElements());
333: IteratorOfNamed it = pvs.iterator();
334: return quantifyProgramVariables(t, it, q, serv);
335: }
336:
337: public static Term quantifyProgramVariables(Term t,
338: IteratorOfNamed it, Quantifier q, Services serv) {
339: while (it.hasNext()) {
340: ProgramVariable v = (ProgramVariable) it.next();
341: t = quantifyProgramVariable(t, v, q, serv);
342: }
343: return t;
344: }
345:
346: /**
347: * Returns q lv . {v := lv}t
348: */
349: public static Term quantifyProgramVariable(Term t,
350: ProgramVariable v, Quantifier q, Services serv) {
351: final TermFactory tf = TermFactory.DEFAULT;
352: final TermBuilder df = TermBuilder.DF;
353: Term vTerm = tf.createVariableTerm(v);
354:
355: final Sort intSort = serv.getTypeConverter().getIntegerLDT()
356: .targetSort();
357: final Sort sort;
358:
359: if (v.sort().extendsTrans(intSort)) {
360: sort = intSort;
361: } else {
362: sort = v.sort();
363: }
364:
365: LogicVariable lv = new LogicVariable(
366: new Name(v.name() + "_lv"), sort);
367: if (v.getKeYJavaType().getSort() instanceof ObjectSort) {
368:
369: Term nullComp = df.equals(vTerm, df.NULL(serv));
370: Term cnCond = df.and(isCreated(vTerm, serv), df
371: .not(nullComp));
372: cnCond = df.or(cnCond, nullComp);
373:
374: if (q == Op.ALL) {
375: t = df.imp(cnCond, t);
376: } else {
377: t = df.and(cnCond, t);
378: }
379: }
380: Term lvTerm = tf.createVariableTerm(lv);
381: t = tf.createUpdateTerm(vTerm, lvTerm, t);
382: t = tf.createQuantifierTerm(q, lv, t);
383: return t;
384: }
385:
386: public static Term isCreated(Term objectToGuard, Services s) {
387: if (!(objectToGuard.sort() instanceof ObjectSort)) {
388: throw new IllegalArgumentException(
389: "Only reference objects can be guarded.");
390: }
391:
392: final TermBuilder df = TermBuilder.DF;
393:
394: final ProgramVariable created = s.getJavaInfo().getAttribute(
395: ImplicitFieldAdder.IMPLICIT_CREATED,
396: s.getJavaInfo().getJavaLangObject());
397:
398: if (created == null) {
399: throw new IllegalStateException(
400: "missing implict attribute for "
401: + objectToGuard.sort());
402: }
403:
404: return df.equals(df.dot(objectToGuard, created), df.TRUE(s));
405: }
406:
407: /**
408: * returns all program variables that occur in t and ns.
409: */
410: private static SetOfNamed helpQuantify(Term t, ListOfNamed ns) {
411: SetOfNamed pvs = SetAsListOfNamed.EMPTY_SET;
412: if (t.op() instanceof ProgramVariable && !ns.contains(t.op())) {
413: pvs = pvs.add(t.op());
414: }
415: for (int i = 0; i < t.arity(); i++) {
416: pvs = pvs.union(helpQuantify(t.sub(i), ns));
417: }
418: return pvs;
419: }
420:
421: public static ListOfNamed getParameters(MethodDeclaration md) {
422: ListOfNamed pl = SLListOfNamed.EMPTY_LIST;
423: if (md != null && md.getParameters().size() != 0) {
424: ArrayOfParameterDeclaration params = md.getParameters();
425: for (int i = 0; i < params.size(); i++) {
426: ProgramVariable p = (ProgramVariable) params
427: .getParameterDeclaration(i)
428: .getVariableSpecification()
429: .getProgramVariable();
430: pl = pl.append(p);
431: }
432: }
433: return pl;
434: }
435:
436: public static Namespace buildParamNamespace(MethodDeclaration md) {
437: Namespace param_ns = new Namespace();
438: if (md != null && md.getParameters().size() != 0) {
439: ArrayOfParameterDeclaration params = md.getParameters();
440: for (int i = 0; i < params.size(); i++) {
441: ProgramVariable p = (ProgramVariable) params
442: .getParameterDeclaration(i)
443: .getVariableSpecification()
444: .getProgramVariable();
445: param_ns.add(p);
446: }
447: }
448: return param_ns;
449: }
450:
451: /**
452: * creates <{typeof(vTerm) v;}> q lv ({vTerm := lv} body)
453: * where v = vTerm.op()
454: */
455: public static Term createQuantifierTermWithPV(Quantifier q,
456: Term vTerm, LogicVariable lv, Term body) {
457: TermFactory tf = TermFactory.DEFAULT;
458: Term result;
459: body = tf.createUpdateTerm(vTerm, tf.createVariableTerm(lv),
460: body);
461: result = tf.createQuantifierTerm(q, lv, body);
462: //adds a declaration for the programvariable if necessary
463: ProgramVariable v = (ProgramVariable) vTerm.op();
464: LocalVariableDeclaration vDecl = new LocalVariableDeclaration(
465: new TypeRef(v.getKeYJavaType()),
466: new VariableSpecification(v));
467: JavaBlock jb = JavaBlock.createJavaBlock(new StatementBlock(
468: vDecl));
469: result = tf.createDiamondTerm(jb, result);
470: return result;
471: }
472:
473: /**
474: * Returns a conjunction of the terms returned by getAllInvariants() for
475: * every <code>JMLClassSpec</code>.
476: */
477: public static Term allInvariants(Implementation2SpecMap ism) {
478: if (ism.allInvariants() != null)
479: return ism.allInvariants();
480: Term result = null;
481:
482: Iterator it = ism.getAllClasses().iterator();
483: Namespace ns = new Namespace();
484:
485: while (it.hasNext()) {
486: KeYJavaType kjt = (KeYJavaType) it.next();
487: JMLClassSpec cs = ism.getSpecForClass(kjt);
488: Term inv = cs.getAllLocalInvariants();
489: ns.add(cs.getProgramVariableNS().allElements());
490: if (inv != null) {
491: if (result == null) {
492: result = inv;
493: } else {
494: result = TermBuilder.DF.and(result, inv);
495: }
496: }
497: }
498: ism.setAllInvPVNS(ns);
499: ism.setAllInvariants(result);
500: return result;
501: }
502:
503: private static boolean containsQuery(Term t) {
504: if (t.op() instanceof ProgramMethod) {
505: return true;
506: }
507: for (int i = 0; i < t.arity(); i++) {
508: if (containsQuery(t.sub(i))) {
509: return true;
510: }
511: }
512: return false;
513: }
514:
515: /**
516: * returns true if c contains a jml keyword that does not occur in
517: * methodspecs
518: */
519: public static boolean isClassSpec(Comment c) {
520: if (!c.containsJMLSpec()) {
521: return false;
522: }
523: String spec = c.getJMLSpec();
524: return (spec.indexOf(" invariant") != -1
525: || spec.indexOf(" constraint") != -1
526: || spec.indexOf(" invariant_redundantly") != -1
527: || spec.indexOf(" constraint_redundantly") != -1
528: || spec.indexOf(" model ") != -1
529: || spec.indexOf(" ghost ") != -1
530: || spec.indexOf(" represents") != -1
531: || spec.indexOf(" monitors_for") != -1
532: || spec.indexOf(" writable") != -1
533: || spec.indexOf(" readable") != -1
534: || spec.indexOf(" initially") != -1 || spec
535: .indexOf(" axiom") != -1);
536: }
537:
538: public static Term makeConjunction(Term t1, Term t2) {
539: if (t2 != null) {
540: if (t1 == null) {
541: return t2;
542: } else {
543: return TermBuilder.DF.and(t1, t2);
544: }
545: }
546: return t1;
547: }
548:
549: }
|