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:
011: package de.uka.ilkd.key.rule.metaconstruct;
012:
013: import de.uka.ilkd.key.java.Expression;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.PrimitiveType;
016: import de.uka.ilkd.key.java.abstraction.Type;
017: import de.uka.ilkd.key.java.expression.Operator;
018: import de.uka.ilkd.key.java.reference.ExecutionContext;
019: import de.uka.ilkd.key.logic.Name;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.TermFactory;
022: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
023: import de.uka.ilkd.key.logic.op.ExpressionOperator;
024: import de.uka.ilkd.key.logic.op.Function;
025: import de.uka.ilkd.key.logic.op.NonRigidFunction;
026: import de.uka.ilkd.key.logic.op.SchemaVariable;
027: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
028: import de.uka.ilkd.key.logic.sort.Sort;
029: import de.uka.ilkd.key.rule.inst.SVInstantiations;
030:
031: public class InTypeOperator extends ExpressionOperator {
032:
033: private static final Name typeof_name = new Name("\\inType");
034:
035: public InTypeOperator(Sort sort, Expression expr) {
036: super (typeof_name, sort, expr);
037: }
038:
039: private long getUpperBound(String type) {
040: if (type.equals("byte"))
041: return Byte.MAX_VALUE;
042: else if (type.equals("short"))
043: return Short.MAX_VALUE;
044: else if (type.equals("int"))
045: return Integer.MAX_VALUE;
046: else if (type.equals("long"))
047: return Long.MAX_VALUE;
048: else if (type.equals("char"))
049: return Character.MAX_VALUE;
050: return 0;
051: }
052:
053: private long getLowerBound(String type) {
054: if (type.equals("byte"))
055: return Byte.MIN_VALUE;
056: else if (type.equals("short"))
057: return Short.MIN_VALUE;
058: else if (type.equals("int"))
059: return Integer.MIN_VALUE;
060: else if (type.equals("long"))
061: return Long.MIN_VALUE;
062: else if (type.equals("char"))
063: return Character.MIN_VALUE;
064: return 0;
065: }
066:
067: private Term createConstraintTerm(Expression expr, Type type,
068: ExecutionContext ec, Services services) {
069: IntegerLDT aiLDT = services.getTypeConverter().getIntegerLDT();
070: Function pred = null;
071: if (type == PrimitiveType.JAVA_BYTE) {
072: pred = (Function) aiLDT.functions().lookup(
073: new Name("inByte"));
074: } else if (type == PrimitiveType.JAVA_SHORT) {
075: pred = (Function) aiLDT.functions().lookup(
076: new Name("inShort"));
077: } else if (type == PrimitiveType.JAVA_INT) {
078: pred = (Function) aiLDT.functions().lookup(
079: new Name("inInt"));
080: } else if (type == PrimitiveType.JAVA_LONG) {
081: pred = (Function) aiLDT.functions().lookup(
082: new Name("inLong"));
083: } else if (type == PrimitiveType.JAVA_CHAR) {
084: pred = (Function) aiLDT.functions().lookup(
085: new Name("inChar"));
086: }
087: return TermFactory.DEFAULT.createFunctionTerm(pred, services
088: .getTypeConverter().convertToLogicElement(expr, ec));
089: }
090:
091: private Term createConstraintTerm(Expression expr,
092: ExecutionContext ec, Services services) {
093: Type type = services.getJavaInfo()
094: .getPrimitiveKeYJavaType(expr).getJavaType();
095: return createConstraintTerm(expr, type, ec, services);
096: }
097:
098: private Term createConstraintTerm(Operator op, Expression expr1,
099: ExecutionContext ec, Services services) {
100: Expression expr = null;
101: if (op instanceof de.uka.ilkd.key.java.expression.operator.Negative) {
102: expr = new de.uka.ilkd.key.java.expression.operator.Negative(
103: expr1);
104: }
105:
106: Type type = services.getJavaInfo()
107: .getPrimitiveKeYJavaType(expr).getJavaType();
108: return createConstraintTerm(expr, type, ec, services);
109: }
110:
111: private Term createConstraintTerm(Operator op, Expression expr1,
112: Expression expr2, ExecutionContext ec, Services services) {
113: Expression expr = null;
114: if (op instanceof de.uka.ilkd.key.java.expression.operator.Times) {
115: expr = new de.uka.ilkd.key.java.expression.operator.Times(
116: expr1, expr2);
117: } else if (op instanceof de.uka.ilkd.key.java.expression.operator.Divide) {
118: expr = new de.uka.ilkd.key.java.expression.operator.Divide(
119: expr1, expr2);
120: } else if (op instanceof de.uka.ilkd.key.java.expression.operator.Plus) {
121: expr = new de.uka.ilkd.key.java.expression.operator.Plus(
122: expr1, expr2);
123: } else if (op instanceof de.uka.ilkd.key.java.expression.operator.Minus) {
124: expr = new de.uka.ilkd.key.java.expression.operator.Minus(
125: expr1, expr2);
126: } else if (op instanceof de.uka.ilkd.key.java.expression.operator.Modulo) {
127: expr = new de.uka.ilkd.key.java.expression.operator.Modulo(
128: expr1, expr2);
129: }
130: Type type = services.getJavaInfo()
131: .getPrimitiveKeYJavaType(expr).getJavaType();
132: return createConstraintTerm(expr, type, ec, services);
133: }
134:
135: public Term resolveExpression(SVInstantiations svInst,
136: Services services) {
137:
138: // get expression instantiations
139: Expression exp = expression();
140: ExecutionContext ec = (svInst.getContextInstantiation() == null) ? null
141: : svInst.getContextInstantiation()
142: .activeStatementContext();
143:
144: if (exp instanceof de.uka.ilkd.key.java.expression.Operator) {
145: de.uka.ilkd.key.java.expression.Operator op = (de.uka.ilkd.key.java.expression.Operator) exp;
146: Expression[] children = new Expression[op
147: .getExpressionCount()];
148: for (int i = 0; i < op.getExpressionCount(); i++) {
149: children[i] = op.getExpressionAt(i);
150: }
151: // top level operator of the child was a unary operator
152: // at the moment the only unary op is a unary minus
153: if (op.getExpressionCount() == 1) {
154: Expression expr = (Expression) svInst
155: .getInstantiation((SchemaVariable) children[0]);
156: return createConstraintTerm(expr, ec, services);
157: } else
158: // top level operator of the child was a binary operator
159: if (op.getExpressionCount() == 2) {
160: Expression expr1 = (Expression) svInst
161: .getInstantiation((SchemaVariable) children[0]);
162: Expression expr2 = (Expression) svInst
163: .getInstantiation((SchemaVariable) children[1]);
164: return createConstraintTerm(op, expr1, expr2, ec,
165: services);
166: } else {
167: throw new RuntimeException("Method resolveExpression "
168: + "in Class InTypeOperator failed "
169: + "to resolve expression");
170: }
171: } else if (exp instanceof SchemaVariable) {
172: Expression expr = (Expression) svInst
173: .getInstantiation((SchemaVariable) exp);
174: return createConstraintTerm(expr, ec, services);
175: }
176:
177: return TermFactory.DEFAULT
178: .createFunctionTerm(new NonRigidFunction(new Name(
179: "ERROR"), new PrimitiveSort(new Name("ERROR")),
180: new PrimitiveSort[0]));
181:
182: }
183:
184: }
|