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: package de.uka.ilkd.key.parser.jml;
009:
010: import java.util.LinkedHashMap;
011:
012: import de.uka.ilkd.key.gui.Main;
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
016: import de.uka.ilkd.key.java.declaration.InterfaceDeclaration;
017: import de.uka.ilkd.key.java.declaration.MethodDeclaration;
018: import de.uka.ilkd.key.java.declaration.TypeDeclaration;
019: import de.uka.ilkd.key.java.declaration.VariableDeclaration;
020: import de.uka.ilkd.key.java.declaration.modifier.Model;
021: import de.uka.ilkd.key.java.declaration.modifier.Public;
022: import de.uka.ilkd.key.java.declaration.modifier.Static;
023: import de.uka.ilkd.key.java.reference.ReferencePrefix;
024: import de.uka.ilkd.key.java.reference.TypeRef;
025: import de.uka.ilkd.key.java.visitor.ProgramVariableCollector;
026: import de.uka.ilkd.key.jml.JMLClassSpec;
027: import de.uka.ilkd.key.jml.JMLNormalMethodSpec;
028: import de.uka.ilkd.key.jml.JMLSpec;
029: import de.uka.ilkd.key.jml.UsefulTools;
030: import de.uka.ilkd.key.logic.*;
031: import de.uka.ilkd.key.logic.op.*;
032: import de.uka.ilkd.key.logic.sort.ArraySort;
033: import de.uka.ilkd.key.logic.sort.ArraySortImpl;
034: import de.uka.ilkd.key.logic.sort.ObjectSort;
035: import de.uka.ilkd.key.logic.sort.Sort;
036: import de.uka.ilkd.key.util.ExtList;
037:
038: /**
039: * This class is used to decouple JML parser and JMLDL translation
040: * (further refactoring needs to be done)
041: */
042: public class JMLTranslator extends TermBuilder {
043:
044: private static int oldVarCount = 0;
045:
046: private final ArithOpProvider aOP;
047:
048: private final TypeDeclaration cld;
049:
050: private KeYJMLParser parser;
051:
052: private final Services services;
053:
054: private final KeYJavaType cldKeYJavaType;
055:
056: private ReferencePrefix prefix;
057:
058: public JMLTranslator(TypeDeclaration cld, Services services,
059: KeYJMLParser parser, ArithOpProvider aOP) {
060: this .cld = cld;
061: this .services = services;
062: this .aOP = aOP;
063: this .parser = parser;
064: cldKeYJavaType = services.getJavaInfo().getKeYJavaType(cld);
065: //this.allInt = allInt;
066: }
067:
068: public ReferencePrefix prefix() {
069: return prefix;
070: }
071:
072: public void setPrefix(ReferencePrefix prefix) {
073: this .prefix = prefix;
074: }
075:
076: public boolean isInterface() {
077: return cld instanceof InterfaceDeclaration;
078: }
079:
080: public KeYJavaType getCLDKeYJavaType() {
081: return cldKeYJavaType;
082: }
083:
084: public KeYJavaType getArrayTypeAndEnsureExistence(Sort baseSort,
085: int dim) {
086: final JavaInfo ji = getJavaInfo();
087: Sort as = ArraySortImpl.getArraySortForDim(baseSort, dim, ji
088: .getJavaLangObjectAsSort(), ji
089: .getJavaLangCloneableAsSort(), ji
090: .getJavaIoSerializableAsSort());
091: KeYJavaType kjt = ji.getKeYJavaType(as);
092: if (kjt == null || baseSort.toString().equals("int")) {
093: JavaBlock jb = ji.readJavaBlock("{" + as + " v;}");
094: return ((VariableDeclaration) ((StatementBlock) jb
095: .program()).getChildAt(0)).getTypeReference()
096: .getKeYJavaType();
097: }
098: return kjt;
099: }
100:
101: public Term buildQuantifierTerm(String q, ListOfNamed l, Term a,
102: Term t, JMLSpec currentSpec)
103: throws NotSupportedExpressionException {
104:
105: checkSupportedQuantifier(q);
106:
107: Term body = t;
108:
109: if (q.equals("\\min") || q.equals("\\max")) {
110: boolean isLong = isLong(t);
111: Function comp;
112: Function minmax;
113: ProgramVariable mv;
114: String varName;
115:
116: if (q.equals("\\min")) {
117: varName = "_min";
118: minmax = aOP.getMax(isLong);
119: comp = (Function) functions().lookup(new Name("leq"));
120: } else {
121: varName = "_max";
122: minmax = aOP.getMin(isLong);
123: comp = (Function) functions().lookup(new Name("geq"));
124: }
125:
126: mv = new LocationVariable(new ProgramElementName(varName
127: + (KeYJMLParser.paramVarCount++)), services
128: .getJavaInfo().getKeYJavaType(
129: isLong ? "long" : "int"));
130: currentSpec.getProgramVariableNS().add(mv);
131: final Term mvTerm = var(mv);
132:
133: final Term ex1 = and(not(parser.buildQuantifierTerm(
134: "\\exists", l, null, a)), equals(func(minmax),
135: mvTerm));
136: final Term ex2 = parser.buildQuantifierTerm("\\exists", l,
137: a, equals(mvTerm, t));
138:
139: final Term allq = parser.buildQuantifierTerm("\\forall", l,
140: a, tf.createFunctionTerm(comp, new Term[] { mvTerm,
141: t }));
142:
143: return parser.createModelMethod(q.substring(1)
144: + (KeYJMLParser.mmCount++), mvTerm, null, or(ex1,
145: and(allq, ex2)));
146: }
147:
148: if (l == SLListOfNamed.EMPTY_LIST) {
149: if (a != null) {
150: if (q.equals("\\exists")) {
151: body = and(a, body);
152: } else {
153: body = imp(a, body);
154: }
155: }
156: return body;
157: } else {
158: Quantifier op = null;
159: if (q.equals("\\forall")) {
160: op = Op.ALL;
161: } else if (q.equals("\\exists")) {
162: op = Op.EX;
163: } else {
164: throw new IllegalArgumentException("Quantifier " + q
165: + " not supported");
166: }
167: body = parser.buildQuantifierTerm(q, l.tail(), a, t);
168: final LogicVariable lv = (LogicVariable) l.head();
169:
170: final Term vTerm = var(lv);
171: // if the quantified variables have an objecttype, we only quantify
172: // over objects that are already created (nevertheless the
173: // quantified variable may be null)
174: if (lv.sort() instanceof ObjectSort) {
175: final Term createdTerm = UsefulTools.isCreated(vTerm,
176: services);
177:
178: final Term nullComp = equals(vTerm, NULL(services));
179: final Term cnCond = or(and(createdTerm, not(nullComp)),
180: nullComp);
181: if (op == Op.ALL) {
182: body = imp(cnCond, body);
183: } else {
184: body = and(cnCond, body);
185: }
186: }
187: return tf.createQuantifierTerm(op, lv, body);
188: }
189: }
190:
191: private void checkSupportedQuantifier(String str)
192: throws NotSupportedExpressionException {
193: final String[] notSupported = { "\\sum", "\\product",
194: "\\num_of" };
195:
196: for (int i = 0; i < notSupported.length; i++) {
197: if (str.equals(notSupported[i])) {
198: throw new NotSupportedExpressionException("Quantifier "
199: + str);
200: }
201: }
202: }
203:
204: /**
205: * creates a model method and adds it to the class specification
206: */
207: public Term createModelMethod(String name, Term result, Term pre,
208: Term post, final JMLClassSpec cSpec,
209: final boolean staticMode) {
210: final ExtList el = new ExtList();
211:
212: ListOfTerm pvs = UsefulTools.getProgramVariablesFromTerm(
213: result, SLListOfTerm.EMPTY_LIST);
214: pvs = UsefulTools.getProgramVariablesFromTerm(pre, pvs);
215: pvs = UsefulTools.getProgramVariablesFromTerm(post, pvs);
216:
217: el.add(new Public());
218: if (staticMode) {
219: el.add(new Static());
220: } else {
221: pvs = pvs.removeAll(var((ProgramVariable) parser.prefix()));
222: }
223: IteratorOfTerm it = pvs.iterator();
224: while (it.hasNext()) {
225: el.add(UsefulTools.getParameterDeclForVar(it.next(),
226: services));
227: }
228: el.add(new ProgramElementName(name));
229: final KeYJavaType type = services.getJavaInfo().getKeYJavaType(
230: result.sort());
231: el.add(new TypeRef(type));
232: el.add(new Model());
233:
234: final MethodDeclaration meth = new MethodDeclaration(el, false);
235: final ProgramMethod pm = new ProgramMethod(meth,
236: getCLDKeYJavaType(), type, PositionInfo.UNDEFINED);
237: cSpec.addModelMethod(pm);
238: final JMLNormalMethodSpec spec = new JMLNormalMethodSpec(pm,
239: services, new Namespace(), new LinkedHashMap(), cSpec,
240: parser.namespaces(), parser.javaPath());
241:
242: result = equals(result, var(spec.getResultVar()));
243: if (pre != null) {
244: spec.addPre(pre);
245: }
246: spec.addPost(result);
247: if (post != null) {
248: spec.addPost(post);
249: }
250: spec.setAssignableMode("nothing");
251: services.getImplementation2SpecMap().addModifier(pm, "pure");
252: services.getImplementation2SpecMap().addModifier(pm, "helper");
253: return UsefulTools.createTermForQuery(pm, pvs, parser.prefix());
254: }
255:
256: public TypeDeclaration cld() {
257: return cld;
258: }
259:
260: private Namespace functions() {
261: return parser.functions();
262: }
263:
264: private JavaInfo getJavaInfo() {
265: return services.getJavaInfo();
266: }
267:
268: private String getNameForOld(Term t) {
269: if (t.op() instanceof ProgramVariable) {
270: return ("_old" + (oldVarCount++) + "_" + (t.toString()
271: .length() > 25 ? t.toString().substring(0, 25) : t
272: .toString())).replace('.', '_').replace(':', '_');
273: } else {
274: return ("_old" + (oldVarCount++));
275: }
276: }
277:
278: /**
279: * checks if term t contains the Named object o
280: * @return true if o occurs in the term and is instance of Term,
281: * ProgramVariable, QuantifiableVariable, SchemaVariable or Operator.
282: */
283: public boolean occurCheck(Term t, Named o) {
284: if (t.op().equals(o) || this .equals(o))
285: return true;
286: if (o instanceof ProgramVariable
287: && t.javaBlock().program() != null) {
288: ProgramVariableCollector collector = new ProgramVariableCollector(
289: t.javaBlock().program());
290: collector.start();
291: if (collector.result().contains(o))
292: return true;
293: }
294: if (o instanceof QuantifiableVariable) {
295: if (t.freeVars().contains((QuantifiableVariable) o))
296: return true;
297: for (int i = 0; i < t.arity(); i++) {
298: for (int j = 0; j < t.varsBoundHere(i).size(); j++) {
299: if (t.varsBoundHere(i).getQuantifiableVariable(j)
300: .equals(o))
301: return true;
302: }
303: }
304: }
305: for (int i = 0; i < t.arity(); i++) {
306: if (occurCheck(t.sub(i), o))
307: return true;
308: }
309: return false;
310: }
311:
312: public Term getOld(Term t, JMLSpec currentSpec) {
313: if (t.isRigid())
314: return t;
315: Term old = (Term) parser.term2old().get(t);
316: final TypeConverter typeConverter = services.getTypeConverter();
317: final Sort intSort = typeConverter.getIntegerLDT().targetSort();
318: final Sort jintSort = typeConverter.getIntLDT().targetSort();
319: boolean allInt = Main.testMode;
320: if (old == null) {
321: final Term TRUE = TRUE(services);
322: ListOfNamed freeVariables = parser.variables()
323: .allElements();
324: final IteratorOfNamed nit = freeVariables.iterator();
325:
326: while (nit.hasNext()) {
327: Named n = nit.next();
328: if (!occurCheck(t, n)) {
329: freeVariables = freeVariables.removeAll(n);
330: } else {
331: final Sort varSort = ((LogicVariable) n).sort();
332: allInt = allInt
333: && (varSort == intSort || varSort == jintSort);
334: }
335: }
336:
337: if (freeVariables.size() != 0) {
338: final Sort retSort;
339: if (t.sort() == Sort.FORMULA) {
340: retSort = getJavaInfo().getKeYJavaType(
341: PrimitiveType.JAVA_BOOLEAN).getSort();
342: } else {
343: retSort = t.sort();
344: }
345:
346: final Term[] args = new Term[freeVariables.size()];
347: final Sort[] argSorts = new Sort[freeVariables.size()];
348: final IteratorOfNamed it = freeVariables.iterator();
349: for (int i = 0; it.hasNext(); i++) {
350: args[i] = var((LogicVariable) it.next());
351: argSorts[i] = args[i].sort();
352: }
353: if (allInt) {
354: ProgramVariable oldV = new LocationVariable(
355: new ProgramElementName(getNameForOld(t)),
356: getArrayTypeAndEnsureExistence(t.sort(),
357: freeVariables.size()));
358: currentSpec.getProgramVariableNS().add(oldV);
359: old = tf
360: .createArrayTerm(ArrayOp.getArrayOp(oldV
361: .sort()), tf
362: .createVariableTerm(oldV), args);
363: } else {
364: final Function f = new RigidFunction(new Name(
365: getNameForOld(t)), retSort, argSorts);
366: currentSpec.getFunctionNS().add(f);
367: functions().add(f);
368:
369: old = func(f, args);
370: }
371: if (isLong(t) && aOP.getCastToLong() != null) {
372: old = func(aOP.getCastToLong(), old);
373: }
374: } else {
375: final ProgramVariable oldV = new LocationVariable(
376: new ProgramElementName(getNameForOld(t)),
377: getTypeForOld(t));
378:
379: currentSpec.getProgramVariableNS().add(oldV);
380: old = var(oldV);
381: }
382:
383: if (t.sort() == Sort.FORMULA) {
384: old = equals(old, TRUE);
385: }
386: parser.term2old().put(t, old);
387: }
388: return old;
389: }
390:
391: private KeYJavaType getTypeForOld(Term t) {
392: final KeYJavaType type4old;
393: if (t.sort() == Sort.FORMULA) {
394: type4old = getJavaInfo().getKeYJavaType(
395: PrimitiveType.JAVA_BOOLEAN);
396: } else {
397: if (isLong(t)) {
398: type4old = getJavaInfo().getKeYJavaType(
399: PrimitiveType.JAVA_LONG);
400: } else {
401: if (t.op() instanceof ProgramVariable) {
402: type4old = ((ProgramVariable) t.op())
403: .getKeYJavaType();
404: } else {
405: type4old = getJavaInfo().getKeYJavaType(t.sort());
406: }
407: }
408: }
409: return type4old;
410: }
411:
412: public boolean isLong(Term t) {
413: final TypeConverter typeConverter = services.getTypeConverter();
414: if (t.sort() == typeConverter.getLongLDT().targetSort()) {
415: return true;
416: }
417:
418: if (t.sort() == Sort.FORMULA) {
419: return false;
420: }
421:
422: if (t.op() instanceof ProgramVariable) {
423: return PrimitiveType.JAVA_LONG.equals(((ProgramVariable) t
424: .op()).getKeYJavaType().getJavaType());
425: }
426:
427: final Function modLong = typeConverter.getLongLDT()
428: .getModuloLong();
429:
430: if (t.op() == modLong) {
431: return true;
432: }
433:
434: for (int i = 0; i < t.arity(); i++) {
435: if (isLong(t.sub(i))) {
436: return true;
437: }
438: }
439: return false;
440: }
441:
442: /**
443: * returns the translation of \\nonnullelements(t).
444: */
445: protected Term nonNullElements(Term t, JMLSpec currentSpec) {
446: Term nne, body;
447:
448: Term eq1 = not(equals(t, NULL(services)));
449:
450: if (t.sort() instanceof ArraySort
451: && ((ArraySort) t.sort()).elementSort() instanceof ObjectSort) {
452: final ProgramVariable v = new LocationVariable(
453: new ProgramElementName("_idx"
454: + KeYJMLParser.paramVarCount), services
455: .getJavaInfo().getKeYJavaType("int"));
456: currentSpec.getProgramVariableNS().add(v);
457:
458: final Term vTerm = var(v);
459:
460: final LogicVariable lv = new LogicVariable(new Name(
461: "index_lv" + (KeYJMLParser.paramVarCount++)),
462: services.getTypeConverter().getIntegerLDT()
463: .targetSort());
464:
465: // eq2 = tf.createEqualityTerm(vTerm, tf.createVariableTerm(lv));
466: final ProgramVariable length = services.getJavaInfo()
467: .getAttribute("length", (ObjectSort) t.sort());
468:
469: body = and(leq(zero(services), vTerm, services), lt(vTerm,
470: dot(t, length), services));
471:
472: // body = tf.createJunctorTerm(Op.IMP, new Term[]{eq2, body});
473: nne = nonNullElements(array(t, vTerm), currentSpec);
474:
475: eq1 = and(eq1, all(lv, tf.createUpdateTerm(vTerm, var(lv),
476: imp(body, nne))));
477: }
478: return eq1;
479: }
480:
481: }
|