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.java;
011:
012: import java.util.HashMap;
013:
014: import recoder.service.ConstantEvaluator;
015: import de.uka.ilkd.key.java.abstraction.*;
016: import de.uka.ilkd.key.java.expression.Literal;
017: import de.uka.ilkd.key.java.expression.ParenthesizedExpression;
018: import de.uka.ilkd.key.java.expression.literal.*;
019: import de.uka.ilkd.key.java.expression.operator.*;
020: import de.uka.ilkd.key.java.reference.*;
021: import de.uka.ilkd.key.logic.*;
022: import de.uka.ilkd.key.logic.ldt.*;
023: import de.uka.ilkd.key.logic.op.*;
024: import de.uka.ilkd.key.logic.sort.ArrayOfSort;
025: import de.uka.ilkd.key.logic.sort.ObjectSort;
026: import de.uka.ilkd.key.logic.sort.Sort;
027: import de.uka.ilkd.key.logic.sort.SortDefiningSymbols;
028: import de.uka.ilkd.key.util.Debug;
029: import de.uka.ilkd.key.util.ExtList;
030:
031: public class TypeConverter extends TermBuilder {
032:
033: private Services services;
034:
035: private ByteLDT byteLDT;
036: private ShortLDT shortLDT;
037: private IntLDT intLDT;
038: private LongLDT longLDT;
039: private CharLDT charLDT;
040: private BooleanLDT booleanLDT;
041: private IntegerLDT integerLDT;
042: private IntegerDomainLDT absIntegerLDT;
043: private ListOfLDT models = SLListOfLDT.EMPTY_LIST;
044:
045: /** required for this handling */
046: private final ThisReference this Reference = new ThisReference();
047:
048: public static StringConverter stringConverter = new StringConverter();
049:
050: TypeConverter(Services s) {
051: services = s;
052: }
053:
054: /**
055: * initializes the type converter with the integer and boolean
056: * language datatype definition to be used
057: * @param ldt the LDT
058: */
059: public void init(LDT ldt) {
060: if (ldt instanceof BooleanLDT) {
061: this .booleanLDT = (BooleanLDT) ldt;
062: } else if (ldt instanceof ByteLDT) {
063: this .byteLDT = (ByteLDT) ldt;
064: } else if (ldt instanceof ShortLDT) {
065: this .shortLDT = (ShortLDT) ldt;
066: } else if (ldt instanceof IntLDT) {
067: this .intLDT = (IntLDT) ldt;
068: } else if (ldt instanceof LongLDT) {
069: this .longLDT = (LongLDT) ldt;
070: } else if (ldt instanceof CharLDT) {
071: this .charLDT = (CharLDT) ldt;
072: } else if (ldt instanceof IntegerLDT) {
073: this .integerLDT = (IntegerLDT) ldt;
074: } else if (ldt instanceof IntegerDomainLDT) {
075: this .absIntegerLDT = (IntegerDomainLDT) ldt;
076: }
077: this .models = this .models.prepend(ldt);
078: Debug.out("Initialize LDTs: ", ldt);
079: }
080:
081: public void init(ListOfLDT ldts) {
082: IteratorOfLDT it = ldts.iterator();
083: while (it.hasNext()) {
084: init(it.next());
085: }
086: }
087:
088: public ListOfLDT getModels() {
089: return models;
090: }
091:
092: public Services getServices() {
093: return services;
094: }
095:
096: public LDT getModelFor(Type t) {
097: if (t == null || booleanLDT == null || byteLDT == null
098: || shortLDT == null || intLDT == null
099: || longLDT == null || charLDT == null) {
100: return null;
101: }
102: if (byteLDT.javaType().equals(t)) {
103: return byteLDT;
104: } else if (shortLDT.javaType().equals(t)) {
105: return shortLDT;
106: } else if (intLDT.javaType().equals(t)) {
107: return intLDT;
108: } else if (longLDT.javaType().equals(t)) {
109: return longLDT;
110: } else if (charLDT.javaType().equals(t)) {
111: return charLDT;
112: } else if (booleanLDT.javaType().equals(t)) {
113: return booleanLDT;
114: }
115: Debug.out("typeconverter: No LDT found for ", t);
116: return null;
117: }
118:
119: public LDT getModelFor(Sort s) {
120: if (s == null || booleanLDT == null || byteLDT == null
121: || shortLDT == null || intLDT == null
122: || longLDT == null || charLDT == null) {
123: return null;
124: }
125: if (byteLDT.targetSort() == s) {
126: return byteLDT;
127: } else if (shortLDT.targetSort() == s) {
128: return shortLDT;
129: } else if (intLDT.targetSort() == s) {
130: return intLDT;
131: } else if (longLDT.targetSort() == s) {
132: return longLDT;
133: } else if (charLDT.targetSort() == s) {
134: return charLDT;
135: } else if (booleanLDT.targetSort() == s) {
136: return booleanLDT;
137: }
138: Debug.out("No LDT found for ", s);
139: return null;
140: }
141:
142: public IntegerLDT getIntegerLDT() {
143: return integerLDT;
144: }
145:
146: public IntegerDomainLDT getIntegerDomainLDT() {
147: return absIntegerLDT;
148: }
149:
150: public ByteLDT getByteLDT() {
151: return byteLDT;
152: }
153:
154: public ShortLDT getShortLDT() {
155: return shortLDT;
156: }
157:
158: public IntLDT getIntLDT() {
159: return intLDT;
160: }
161:
162: public LongLDT getLongLDT() {
163: return longLDT;
164: }
165:
166: public CharLDT getCharLDT() {
167: return charLDT;
168: }
169:
170: public BooleanLDT getBooleanLDT() {
171: return booleanLDT;
172: }
173:
174: HashMap mcrMap = new HashMap(10);
175:
176: private Term translateMetaClassReference(MetaClassReference mcr) {
177: // throw new IllegalArgumentException("Convert MCR to a constant");
178: // return intLDT.translateLiteral( new CharLiteral('X'));
179: String name = mcr.getTypeReference().getName().intern();
180:
181: if (mcrMap.containsKey(name))
182: return (Term) mcrMap.get(name);
183:
184: final Sort dummySort = services.getJavaInfo()
185: .getJavaLangObjectAsSort();
186: final Term tMCR = func(new RigidFunction(new Name(name),
187: dummySort, new ArrayOfSort()));
188: mcrMap.put(name, tMCR);
189: return tMCR;
190: }
191:
192: private Term translateOperator(
193: de.uka.ilkd.key.java.expression.Operator op, LDT intLDT,
194: LDT booleanLDT, ExecutionContext ec) {
195:
196: final Term[] subs = new Term[op.getArity()];
197: if (op.getArity() >= 1) {
198: subs[0] = convertToLogicElement(op.getExpressionAt(0), ec);
199: }
200: if (op.getArity() == 2) {
201: subs[1] = convertToLogicElement(op.getExpressionAt(1), ec);
202: }
203:
204: LDT responsibleLDT = null;
205: if (intLDT.isResponsible(op, subs, services, ec)) {
206: responsibleLDT = intLDT;
207: } else if (booleanLDT.isResponsible(op, subs, services, ec)) {
208: responsibleLDT = booleanLDT;
209: } else {
210: Debug.out("typeconverter: no data type model "
211: + "available to convert:", op, op.getClass());
212: throw new IllegalArgumentException(
213: "TypeConverter could not handle" + " this");
214: }
215: return func(responsibleLDT.getFunctionFor(op, services, ec),
216: subs);
217: }
218:
219: private Term convertReferencePrefix(ReferencePrefix prefix,
220: ExecutionContext ec) {
221: Debug.out("typeconverter: (prefix, class)", prefix,
222: (prefix != null ? prefix.getClass() : null));
223: if (prefix instanceof FieldReference) {
224: return convertVariableReference((FieldReference) prefix, ec);
225: } else if (prefix instanceof MetaClassReference) {
226: Debug
227: .out("typeconverter: "
228: + "WARNING: metaclass-references not supported yet");
229: throw new IllegalArgumentException(
230: "TypeConverter could not handle" + " this");
231: } else if (prefix instanceof ProgramVariable) {
232: // the base case: the leftmost item is a local variable
233: return var((ProgramVariable) prefix);
234: } else if (prefix instanceof VariableReference) {
235: Debug
236: .out("typeconverter: " + "variablereference:",
237: (((VariableReference) prefix)
238: .getProgramVariable()));
239: return var(((VariableReference) prefix)
240: .getProgramVariable());
241: } else if (prefix instanceof ArrayReference) {
242: return convertArrayReference((ArrayReference) prefix, ec);
243: } else if (prefix instanceof ThisReference) {
244: return convertToLogicElement(ec.getRuntimeInstance());
245: } else {
246: Debug
247: .out(
248: "typeconverter: WARNING: unknown reference prefix:",
249: prefix, prefix == null ? null : prefix
250: .getClass());
251: throw new IllegalArgumentException(
252: "TypeConverter failed to convert " + prefix);
253: }
254: }
255:
256: public Term convertVariableReference(VariableReference fr,
257: ExecutionContext ec) {
258: Debug.out("TypeConverter: FieldReference: ", fr);
259: final ReferencePrefix prefix = fr.getReferencePrefix();
260: final ProgramVariable var = fr.getProgramVariable();
261: if (var.isStatic()) {
262: return var(var);
263: } else if (prefix == null) {
264: if (var.isMember()) {
265: return dot(convertReferencePrefix(this Reference, ec),
266: var);
267: }
268: return var(var);
269: } else if (!(prefix instanceof PackageReference)) {
270: return dot(convertReferencePrefix(prefix, ec), var);
271: }
272: Debug
273: .out(
274: "typeconverter: Not supported reference type (fr, class):",
275: fr, fr.getClass());
276: throw new IllegalArgumentException(
277: "TypeConverter could not handle this");
278: }
279:
280: public Term convertArrayReference(ArrayReference ar,
281: ExecutionContext ec) {
282: final Term[] index = new Term[ar.getDimensionExpressions()
283: .size()];
284: final Term t = convertToLogicElement(ar.getReferencePrefix(),
285: ec);
286: for (int i = 0; i < index.length; i++) {
287: index[i] = convertToLogicElement(ar
288: .getDimensionExpressions().getExpression(i), ec);
289: }
290: return tf.createArrayTerm(ArrayOp.getArrayOp(t.sort()), t,
291: index);
292: }
293:
294: private Term convertToInstanceofTerm(Instanceof io,
295: ExecutionContext ec) {
296: final KeYJavaType type = ((TypeReference) io.getChildAt(1))
297: .getKeYJavaType();
298: final Term obj = convertToLogicElement(io.getChildAt(0), ec);
299: final SortDefiningSymbols s = (SortDefiningSymbols) type
300: .getSort();
301: final InstanceofSymbol instanceOfSymbol = (InstanceofSymbol) s
302: .lookupSymbol(InstanceofSymbol.NAME);
303:
304: // in JavaDL S::instance(o) is also true if o (for reference types S)
305: // is null in opposite to Java
306: // we create here if (obj = null) then FALSE else S::instance(obj)
307: return ife(equals(obj, NULL(services)), FALSE(services), func(
308: instanceOfSymbol, obj));
309: }
310:
311: public Term convertToLogicElement(ProgramElement pe) {
312: return convertToLogicElement(pe, null);
313: }
314:
315: public Term convertToLogicElement(ProgramElement pe,
316: ExecutionContext ec) {
317: Debug.out("typeconverter: called for:", pe, pe.getClass());
318: if (pe instanceof ProgramVariable) {
319: return var((ProgramVariable) pe);
320: } else if (pe instanceof FieldReference) {
321: return convertVariableReference((FieldReference) pe, ec);
322: } else if (pe instanceof VariableReference) {
323: return convertVariableReference((VariableReference) pe, ec);
324: } else if (pe instanceof ArrayReference) {
325: return convertArrayReference((ArrayReference) pe, ec);
326: } else if (pe instanceof Literal) {
327: return convertLiteralExpression((Literal) pe);
328: } else if (pe instanceof Negative
329: && ((Negative) pe).getChildAt(0) instanceof IntLiteral) {
330: String val = ((IntLiteral) ((Negative) pe).getChildAt(0))
331: .getValue();
332: if (val.charAt(0) == '-') {
333: return integerLDT.translateLiteral(new IntLiteral(val
334: .substring(1)));
335: } else {
336: return integerLDT.translateLiteral(new IntLiteral("-"
337: + val));
338: }
339: } else if (pe instanceof Negative
340: && ((Negative) pe).getChildAt(0) instanceof LongLiteral) {
341: String val = ((LongLiteral) ((Negative) pe).getChildAt(0))
342: .getValue();
343: if (val.charAt(0) == '-') {
344: return integerLDT.translateLiteral(new LongLiteral(val
345: .substring(1)));
346: } else {
347: return integerLDT.translateLiteral(new LongLiteral("-"
348: + val));
349: }
350: } else if (pe instanceof ThisReference) {
351: return convertReferencePrefix((ThisReference) pe, ec);
352: } else if (pe instanceof ParenthesizedExpression) {
353: return convertToLogicElement(((ParenthesizedExpression) pe)
354: .getChildAt(0), ec);
355: } else if (pe instanceof Instanceof) {
356: return convertToInstanceofTerm((Instanceof) pe, ec);
357: } else if (pe instanceof de.uka.ilkd.key.java.expression.Operator) {
358: return translateOperator(
359: (de.uka.ilkd.key.java.expression.Operator) pe,
360: integerLDT, booleanLDT, ec);
361: } else if (pe instanceof PrimitiveType) {
362: throw new IllegalArgumentException(
363: "TypeConverter could not handle"
364: + " this primitive type");
365: } else if (pe instanceof MetaClassReference) {
366: return translateMetaClassReference((MetaClassReference) pe);
367: }
368: throw new IllegalArgumentException(
369: "TypeConverter: Unknown or not convertable ProgramElement "
370: + pe + " of type " + pe.getClass());
371: }
372:
373: /**
374: * dispatches the given literal and converts it
375: * @param lit the Literal to be converted
376: * @return the Term representing <tt>lit</tt> in the logic
377: */
378: private Term convertLiteralExpression(Literal lit) {
379: if (lit instanceof BooleanLiteral) {
380: return booleanLDT.translateLiteral(lit);
381: } else if (lit instanceof NullLiteral) {
382: return services.getJavaInfo().getNullConst();
383: } else if (lit instanceof IntLiteral) {
384: return integerLDT.translateLiteral(lit);
385: } else if (lit instanceof CharLiteral) {
386: return integerLDT.translateLiteral(lit);
387: } else if (lit instanceof LongLiteral) {
388: return integerLDT.translateLiteral(lit);
389: } else if (lit instanceof StringLiteral) {
390: return stringConverter.translateLiteral(lit, integerLDT,
391: services);
392: } else {
393: Debug.fail("Unknown literal type", lit);
394: return null;
395: }
396: }
397:
398: public static boolean isArithmeticOperator(
399: de.uka.ilkd.key.java.expression.Operator op) {
400: if (op instanceof Divide || op instanceof Times
401: || op instanceof Plus || op instanceof Minus
402: || op instanceof Modulo || op instanceof ShiftLeft
403: || op instanceof ShiftRight || op instanceof BinaryAnd
404: || op instanceof BinaryNot || op instanceof BinaryOr
405: || op instanceof BinaryXOr || op instanceof Negative
406: || op instanceof PreIncrement
407: || op instanceof PostIncrement
408: || op instanceof PreDecrement
409: || op instanceof PostDecrement) {
410: return true;
411: }
412: return false;
413: }
414:
415: /**
416: * performs binary numeric promotion on the argument types
417: */
418: public KeYJavaType getPromotedType(KeYJavaType type1,
419: KeYJavaType type2) {
420: final Type t1 = type1.getJavaType();
421: final Type t2 = type1.getJavaType();
422: if ((t1 == PrimitiveType.JAVA_BOOLEAN && t2 == PrimitiveType.JAVA_BOOLEAN))
423: return services.getJavaInfo().getKeYJavaType(
424: PrimitiveType.JAVA_BOOLEAN);
425: if ((t1 == PrimitiveType.JAVA_BYTE
426: || t1 == PrimitiveType.JAVA_SHORT
427: || t1 == PrimitiveType.JAVA_CHAR || t1 == PrimitiveType.JAVA_INT)
428: && (t2 == PrimitiveType.JAVA_BYTE
429: || t2 == PrimitiveType.JAVA_SHORT
430: || t2 == PrimitiveType.JAVA_CHAR || t2 == PrimitiveType.JAVA_INT))
431: return services.getJavaInfo().getKeYJavaType(
432: PrimitiveType.JAVA_INT);
433: if ((t2 == PrimitiveType.JAVA_LONG)
434: && (t1 == PrimitiveType.JAVA_BYTE
435: || t1 == PrimitiveType.JAVA_SHORT
436: || t1 == PrimitiveType.JAVA_INT
437: || t1 == PrimitiveType.JAVA_CHAR || t1 == PrimitiveType.JAVA_LONG))
438: return services.getJavaInfo().getKeYJavaType(
439: PrimitiveType.JAVA_LONG);
440: if ((t1 == PrimitiveType.JAVA_LONG)
441: && (t2 == PrimitiveType.JAVA_BYTE
442: || t2 == PrimitiveType.JAVA_SHORT
443: || t2 == PrimitiveType.JAVA_INT
444: || t2 == PrimitiveType.JAVA_CHAR || t2 == PrimitiveType.JAVA_LONG))
445: return services.getJavaInfo().getKeYJavaType(
446: PrimitiveType.JAVA_LONG);
447: throw new RuntimeException("Could not determine promoted type "
448: + "of " + t1 + " and " + t2);
449: }
450:
451: // this method performs unary numeric promotion on the arguments
452: public KeYJavaType getPromotedType(KeYJavaType type1) {
453: final Type t1 = type1.getJavaType();
454: if (t1 == PrimitiveType.JAVA_BOOLEAN)
455: // not really numeric ...
456: return services.getJavaInfo().getKeYJavaType(
457: PrimitiveType.JAVA_BOOLEAN);
458: if (t1 == PrimitiveType.JAVA_BYTE
459: || t1 == PrimitiveType.JAVA_SHORT
460: || t1 == PrimitiveType.JAVA_CHAR
461: || t1 == PrimitiveType.JAVA_INT)
462: return services.getJavaInfo().getKeYJavaType(
463: PrimitiveType.JAVA_INT);
464: if (t1 == PrimitiveType.JAVA_LONG)
465: return services.getJavaInfo().getKeYJavaType(
466: PrimitiveType.JAVA_LONG);
467: throw new RuntimeException("Could not determine promoted type "
468: + "of " + type1);
469: }
470:
471: public KeYJavaType getBooleanType() {
472: return booleanLDT.getKeYJavaType(PrimitiveType.JAVA_BOOLEAN);
473: }
474:
475: public Sort getPrimitiveSort(Type t) {
476: LDT result = getModelFor(t);
477: Debug.out("LDT found", t, result);
478: return (result == null ? null : result.targetSort());
479: }
480:
481: /**
482: * Retrieves the static type of the expression. This method may only be called
483: * if the expressions type can be determined without knowledge of context
484: * information, i.e. it must not be a expression with an ex-/or implicit this
485: * reference like this.a or a methodcall whose value can only be determined
486: * when one knows the exact invocation context.
487: *
488: * For these cases please use @link #getKeYJavaType(Expression, ExecutionContext)
489: *
490: * This method behaves same as invoking <code>getKeYJavaType(e, null)</code>
491: */
492: public KeYJavaType getKeYJavaType(Expression e) {
493: return getKeYJavaType(e, null);
494: }
495:
496: /**
497: * retrieves the type of the expression <tt>e</tt> with respect to
498: * the context in which it is evaluated
499: * @param e the Expression whose type has to be retrieved
500: * @param ec the ExecutionContext of expression <tt>e</tt>
501: * @return the KeYJavaType of expression <tt>e</tt>
502: */
503: public KeYJavaType getKeYJavaType(Expression e, ExecutionContext ec) {
504: if (e instanceof ThisReference) {
505: return ec.getTypeReference().getKeYJavaType();
506: }
507: return e.getKeYJavaType(services, ec);
508: }
509:
510: /**
511: * converts a logical term to an AST node if possible. If this fails
512: * it throws a runtime exception.
513: * @param term the Term to be converted
514: * @return the Term as an program AST node of type expression
515: * @throws RuntimeException iff a conversion is not possible
516: */
517: public Expression convertToProgramElement(Term term) {
518: if (term.op() == Op.NULL) {
519: return NullLiteral.NULL;
520: } else if (term.op() instanceof Function) {
521: final IteratorOfLDT it = models.iterator();
522: while (it.hasNext()) {
523: final LDT model = it.next();
524: if (model.hasLiteralFunction((Function) term.op())) {
525: return model.translateTerm(term, null);
526: }
527: }
528: }
529:
530: final ExtList children = new ExtList();
531: for (int i = 0; i < term.arity(); i++) {
532: children.add(convertToProgramElement(term.sub(i)));
533: }
534: if (term.op() instanceof ProgramInLogic) {
535: return ((ProgramInLogic) term.op()).convertToProgram(term,
536: children);
537: } else if (term.op() instanceof Function) {
538: final IteratorOfLDT it = models.iterator();
539: while (it.hasNext()) {
540: final LDT model = it.next();
541: if (model.containsFunction((Function) term.op())) {
542: return model.translateTerm(term, children);
543: }
544: }
545: }
546: throw new RuntimeException("Cannot convert term to program: "
547: + term + " " + term.op().getClass());
548: }
549:
550: public KeYJavaType getKeYJavaType(Term t) {
551: if (t.sort() instanceof ObjectSort) {
552: return services.getJavaInfo().getKeYJavaType(t.sort());
553: }
554:
555: KeYJavaType result = services.getJavaInfo().getKeYJavaType(
556: t.sort());
557: if (result == null) {
558: result = getKeYJavaType(convertToProgramElement(t));
559: }
560:
561: return result;
562: }
563:
564: public KeYJavaType getKeYJavaType(Type t) {
565: if (t instanceof KeYJavaType)
566: return (KeYJavaType) t;
567: final LDT model = getModelFor(t);
568: if (model != null) {
569: return model.getKeYJavaType(t);
570: } else {
571: Debug.out("javainfo: no predefined model for type ", t);
572: return null;
573: }
574: }
575:
576: /** These methods are taken from recoder (and modified) */
577:
578: public boolean isWidening(PrimitiveType from, PrimitiveType to) {
579: // we do not handle null's
580: if (from == null || to == null)
581: return false;
582: // equal types can be coerced
583: if (from == to)
584: return true;
585: // boolean types cannot be coerced into something else
586: if (from == PrimitiveType.JAVA_BOOLEAN
587: || to == PrimitiveType.JAVA_BOOLEAN)
588: return false;
589: // everything else can be coerced to a double
590: if (to == PrimitiveType.JAVA_DOUBLE)
591: return true;
592: // but a double cannot be coerced to anything else
593: if (from == PrimitiveType.JAVA_DOUBLE)
594: return false;
595: // everything except doubles can be coerced to a float
596: if (to == PrimitiveType.JAVA_FLOAT)
597: return true;
598: // but a float cannot be coerced to anything but float or double
599: if (from == PrimitiveType.JAVA_FLOAT)
600: return false;
601: // everything except float or double can be coerced to a long
602: if (to == PrimitiveType.JAVA_LONG)
603: return true;
604: // but a long cannot be coerced to anything but float, double or long
605: if (from == PrimitiveType.JAVA_LONG)
606: return false;
607: // everything except long, float or double can be coerced to an int
608: if (to == PrimitiveType.JAVA_INT)
609: return true;
610: // but an int cannot be coerced to the remaining byte, char, short
611: if (from == PrimitiveType.JAVA_INT)
612: return false;
613: // between byte, char, short, only one conversion is admissible
614: return (from == PrimitiveType.JAVA_BYTE && to == PrimitiveType.JAVA_SHORT);
615: }
616:
617: public boolean isWidening(ClassType from, ClassType to) {
618: return isWidening(getKeYJavaType(from), getKeYJavaType(to));
619: }
620:
621: public boolean isWidening(ArrayType from, ArrayType to) {
622: KeYJavaType toBase = to.getBaseType().getKeYJavaType();
623: if (toBase == services.getJavaInfo().getJavaLangObject()) { // seems incorrect
624: return true;
625: }
626: KeYJavaType fromBase = from.getBaseType().getKeYJavaType();
627: if (toBase.getJavaType() instanceof PrimitiveType) {
628: return toBase == fromBase;
629: }
630: return isWidening(fromBase, toBase);
631: }
632:
633: public boolean isWidening(Type from, Type to) {
634: if (from instanceof KeYJavaType)
635: return isWidening((KeYJavaType) from, getKeYJavaType(to));
636: if (to instanceof KeYJavaType)
637: return isWidening(getKeYJavaType(from), (KeYJavaType) to);
638:
639: if (from instanceof ClassType) {
640: return isWidening(getKeYJavaType(from), getKeYJavaType(to));
641: } else if (from instanceof PrimitiveType) {
642: if (to instanceof PrimitiveType) {
643: return isWidening((PrimitiveType) from,
644: (PrimitiveType) to);
645: }
646: } else if (from instanceof ArrayType) {
647: if (to instanceof ClassType) {
648: final Sort toSort = getKeYJavaType(to).getSort();
649: return services.getJavaInfo().isAJavaCommonSort(toSort);
650: } else if (to instanceof ArrayType) {
651: return isWidening((ArrayType) from, (ArrayType) to);
652: }
653: }
654: return false;
655: }
656:
657: // this also handles class types
658: public boolean isWidening(KeYJavaType from, KeYJavaType to) {
659: Type a = from.getJavaType();
660: Type b = to.getJavaType();
661:
662: if (a instanceof ClassType || a == null) {
663: return from.getSort().extendsTrans(to.getSort())
664: || (a == NullType.JAVA_NULL && b instanceof ArrayType);
665: } else {
666: if (b == null)
667: return to == services.getJavaInfo().getJavaLangObject()
668: && a instanceof ArrayType;
669: else
670: return isWidening(a, b);
671: }
672: }
673:
674: public boolean isImplicitNarrowing(Expression expr, PrimitiveType to) {
675:
676: int minValue, maxValue;
677: if (to == PrimitiveType.JAVA_BYTE) {
678: minValue = Byte.MIN_VALUE;
679: maxValue = Byte.MAX_VALUE;
680: } else if (to == PrimitiveType.JAVA_CHAR) {
681: minValue = Character.MIN_VALUE;
682: maxValue = Character.MAX_VALUE;
683: } else if (to == PrimitiveType.JAVA_SHORT) {
684: minValue = Short.MIN_VALUE;
685: maxValue = Short.MAX_VALUE;
686: } else {
687: return false;
688: }
689:
690: ConstantExpressionEvaluator cee = services
691: .getConstantExpressionEvaluator();
692:
693: ConstantEvaluator.EvaluationResult res = new ConstantEvaluator.EvaluationResult();
694:
695: if (!cee.isCompileTimeConstant(expr, res)
696: || res.getTypeCode() != ConstantEvaluator.INT_TYPE) {
697: return false;
698: }
699: int value = res.getInt();
700: return (minValue <= value) && (value <= maxValue);
701: }
702:
703: public boolean isIdentical(Type from, Type to) {
704: from = getKeYJavaType(from);
705: to = getKeYJavaType(to);
706: return from == to;
707: }
708:
709: public boolean isAssignableTo(Type from, Type to) {
710: return isIdentical(from, to) || isWidening(from, to);
711: }
712:
713: public boolean isAssignableTo(Expression expr, Type to,
714: ExecutionContext ec) {
715: return (to instanceof PrimitiveType && isImplicitNarrowing(
716: expr, (PrimitiveType) to))
717: || isIdentical(expr.getKeYJavaType(getServices(), ec),
718: to)
719: || isWidening(expr.getKeYJavaType(getServices(), ec),
720: to);
721: }
722:
723: // this also handles class types
724: public boolean isNarrowing(KeYJavaType from, KeYJavaType to) {
725: Type a = from.getJavaType();
726: Type b = to.getJavaType();
727:
728: if (a instanceof ClassType || a == null) {
729: return to.getSort().extendsTrans(from.getSort())
730: || (from == services.getJavaInfo()
731: .getJavaLangObject() && a instanceof ArrayType);
732: } else {
733: if (b == null)
734: return false;
735: else
736: return isNarrowing(a, b);
737: }
738: }
739:
740: public boolean isNarrowing(PrimitiveType from, PrimitiveType to) {
741: // we do not handle null's
742: if (from == null || to == null)
743: return false;
744:
745: if (from == PrimitiveType.JAVA_BYTE) {
746: return (to == PrimitiveType.JAVA_CHAR);
747: }
748: if (from == PrimitiveType.JAVA_SHORT) {
749: return (to == PrimitiveType.JAVA_BYTE || to == PrimitiveType.JAVA_CHAR);
750: }
751: if (from == PrimitiveType.JAVA_CHAR) {
752: return (to == PrimitiveType.JAVA_BYTE || to == PrimitiveType.JAVA_SHORT);
753: }
754: if (from == PrimitiveType.JAVA_INT) {
755: return (to == PrimitiveType.JAVA_BYTE
756: || to == PrimitiveType.JAVA_SHORT || to == PrimitiveType.JAVA_CHAR);
757: }
758: if (from == PrimitiveType.JAVA_LONG) {
759: return (to == PrimitiveType.JAVA_BYTE
760: || to == PrimitiveType.JAVA_SHORT
761: || to == PrimitiveType.JAVA_CHAR || to == PrimitiveType.JAVA_INT);
762: }
763: if (from == PrimitiveType.JAVA_FLOAT) {
764: return (to == PrimitiveType.JAVA_BYTE
765: || to == PrimitiveType.JAVA_SHORT
766: || to == PrimitiveType.JAVA_CHAR
767: || to == PrimitiveType.JAVA_INT || to == PrimitiveType.JAVA_LONG);
768: }
769: if (from == PrimitiveType.JAVA_DOUBLE) {
770: return (to == PrimitiveType.JAVA_BYTE
771: || to == PrimitiveType.JAVA_SHORT
772: || to == PrimitiveType.JAVA_CHAR
773: || to == PrimitiveType.JAVA_INT
774: || to == PrimitiveType.JAVA_LONG || to == PrimitiveType.JAVA_FLOAT);
775: }
776: return false;
777: }
778:
779: public boolean isNarrowing(ClassType from, ClassType to) {
780: return isNarrowing(getKeYJavaType(from), getKeYJavaType(to));
781: }
782:
783: public boolean isNarrowing(ArrayType from, ArrayType to) {
784: KeYJavaType toBase = to.getBaseType().getKeYJavaType();
785: KeYJavaType fromBase = from.getBaseType().getKeYJavaType();
786: return isReferenceType(toBase) && isReferenceType(fromBase)
787: && isNarrowing(fromBase, toBase);
788: }
789:
790: public boolean isNarrowing(Type from, Type to) {
791: if (from instanceof KeYJavaType)
792: return isNarrowing((KeYJavaType) from, getKeYJavaType(to));
793: if (to instanceof KeYJavaType)
794: return isNarrowing(getKeYJavaType(from), (KeYJavaType) to);
795:
796: if (from instanceof ClassType) {
797: return isNarrowing(getKeYJavaType(from), getKeYJavaType(to));
798: } else if (from instanceof PrimitiveType) {
799: if (to instanceof PrimitiveType) {
800: return isNarrowing((PrimitiveType) from,
801: (PrimitiveType) to);
802: }
803: } else if (from instanceof ArrayType) {
804: if (to instanceof ArrayType) {
805: return isNarrowing((ArrayType) from, (ArrayType) to);
806: }
807: }
808: return false;
809: }
810:
811: public boolean isCastingTo(Type from, Type to) {
812: // there is currently no interface handling
813:
814: // identity conversion
815: if (isIdentical(from, to))
816: return true;
817:
818: // conversions between numeric types are always possible
819: if (isArithmeticType(from) && isArithmeticType(to))
820: return true;
821:
822: // all widening conversions
823: if (isWidening(from, to))
824: return true;
825:
826: // narrowing
827: return isNarrowing(from, to);
828: }
829:
830: public boolean isArithmeticType(Type t) {
831: if (t instanceof KeYJavaType)
832: t = ((KeYJavaType) t).getJavaType();
833: return t == PrimitiveType.JAVA_BYTE
834: || t == PrimitiveType.JAVA_SHORT
835: || t == PrimitiveType.JAVA_INT
836: || t == PrimitiveType.JAVA_CHAR
837: || t == PrimitiveType.JAVA_LONG
838: || t == PrimitiveType.JAVA_FLOAT
839: || t == PrimitiveType.JAVA_DOUBLE;
840: }
841:
842: public boolean isIntegralType(Type t) {
843: if (t instanceof KeYJavaType)
844: t = ((KeYJavaType) t).getJavaType();
845: return t == PrimitiveType.JAVA_BYTE
846: || t == PrimitiveType.JAVA_SHORT
847: || t == PrimitiveType.JAVA_INT
848: || t == PrimitiveType.JAVA_CHAR
849: || t == PrimitiveType.JAVA_LONG;
850: }
851:
852: public boolean isReferenceType(Type t) {
853: if (t instanceof KeYJavaType)
854: t = ((KeYJavaType) t).getJavaType();
855: return
856: // there is currently no interface handling
857: t == null
858: || (t instanceof ClassType && !(t instanceof NullType))
859: || t instanceof ArrayType;
860: }
861:
862: public boolean isNullType(Type t) {
863: if (t instanceof KeYJavaType)
864: t = ((KeYJavaType) t).getJavaType();
865: return t == NullType.JAVA_NULL;
866: }
867:
868: public boolean isBooleanType(Type t) {
869: if (t instanceof KeYJavaType)
870: t = ((KeYJavaType) t).getJavaType();
871: return t == PrimitiveType.JAVA_BOOLEAN;
872: }
873:
874: public TypeConverter copy(Services services) {
875: final TypeConverter tc = new TypeConverter(services);
876: tc.init(models);
877: return tc;
878: }
879:
880: }
|