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.encapsulation;
012:
013: import java.util.Map;
014:
015: import de.uka.ilkd.key.logic.op.ArrayOp;
016: import de.uka.ilkd.key.logic.op.ProgramVariable;
017: import de.uka.ilkd.key.logic.sort.ObjectSort;
018: import de.uka.ilkd.key.logic.sort.Sort;
019: import de.uka.ilkd.key.util.Debug;
020:
021: class TypeSchemeChecker {
022:
023: private static final TypeSchemeTerm DEFAULT_FIELD_TERM = TypeSchemeUnion.ROOT;
024:
025: private final Map /*Location -> TypeSchemeTerm*/annotations;
026: private ListOfTypeSchemeConstraint constraints = SLListOfTypeSchemeConstraint.EMPTY_LIST;
027: private boolean failed = false;
028:
029: private int stringLitNameCounter = 0;
030: private int allocNameCounter = 0;
031: private int arrayAllocNameCounter = 0;
032: private int conditionalNameCounter = 0;
033:
034: public TypeSchemeChecker(Map /*Location -> TypeSchemeTerm*/
035: annotations) {
036: this .annotations = annotations;
037: }
038:
039: //-------------------------------------------------------------------------
040: //internal helper methods
041: //-------------------------------------------------------------------------
042:
043: private void verbose(Object o) {
044: //System.out.println(o);
045: }
046:
047: private void addConstraint(TypeSchemeConstraint constraint) {
048: verbose("Adding constraint: " + constraint);
049: constraints = constraints.prepend(constraint);
050: }
051:
052: private void addSubConstraint(TypeSchemeTerm term1,
053: TypeSchemeTerm term2) {
054: addConstraint(new TypeSchemeSubConstraint(term1, term2));
055: }
056:
057: private void addEqualConstraint(TypeSchemeTerm term1,
058: TypeSchemeTerm term2) {
059: addConstraint(new TypeSchemeEqualConstraint(term1, term2));
060: }
061:
062: private boolean hasPrimitiveType(ProgramVariable pv) {
063: return !(pv.sort() instanceof ObjectSort);
064: }
065:
066: private ListOfTypeSchemeConstraint dropTriviallyTrueConstraints(
067: ListOfTypeSchemeConstraint c) {
068: ListOfTypeSchemeConstraint result = SLListOfTypeSchemeConstraint.EMPTY_LIST;
069:
070: IteratorOfTypeSchemeConstraint it = c.iterator();
071: while (it.hasNext()) {
072: TypeSchemeConstraint constraint = it.next();
073: if (constraint.getFreeVars().size() > 0
074: || !constraint.evaluate()) {
075: result = result.prepend(constraint);
076: }
077: }
078:
079: return result;
080: }
081:
082: //-------------------------------------------------------------------------
083: //public interface
084: //-------------------------------------------------------------------------
085:
086: public void fail() {
087: failed = true;
088: }
089:
090: public ListOfTypeSchemeConstraint getConstraints() {
091: if (failed) {
092: TypeSchemeConstraint fc = new TypeSchemeFalseConstraint();
093: return SLListOfTypeSchemeConstraint.EMPTY_LIST.append(fc);
094: } else {
095: return dropTriviallyTrueConstraints(constraints);
096: }
097: }
098:
099: public TypeSchemeTerm checkNull() {
100: return TypeSchemeUnion.NULL;
101: }
102:
103: public TypeSchemeTerm checkThis() {
104: return TypeSchemeUnion.THIS;
105: }
106:
107: public TypeSchemeTerm checkSuper() {
108: return TypeSchemeUnion.THIS;
109: }
110:
111: public TypeSchemeTerm checkStringLiteral() {
112: return new TypeSchemeVariable("TS(stringliteral"
113: + stringLitNameCounter++ + ")",
114: TypeSchemeUnion.REP_PEER_ROOT);
115: }
116:
117: public TypeSchemeTerm checkPrimitiveLiteral() {
118: return TypeSchemeUnion.PRIMITIVE;
119: }
120:
121: public TypeSchemeTerm checkPrimitiveUnary(TypeSchemeTerm operandTerm) {
122: return TypeSchemeUnion.PRIMITIVE;
123: }
124:
125: public TypeSchemeTerm checkPrimitiveBinary(
126: TypeSchemeTerm operandTerm1, TypeSchemeTerm operandTerm2) {
127: return TypeSchemeUnion.PRIMITIVE;
128: }
129:
130: public TypeSchemeTerm checkInstanceLocalVariable(ProgramVariable var) {
131: TypeSchemeTerm varTerm;
132:
133: if (hasPrimitiveType(var)) {
134: varTerm = TypeSchemeUnion.PRIMITIVE;
135: } else {
136: varTerm = (TypeSchemeTerm) annotations.get(var);
137:
138: if (varTerm == null) {
139: varTerm = new TypeSchemeVariable("TS(" + var + ")",
140: TypeSchemeUnion.REP_PEER_READONLY_ROOT);
141: annotations.put(var, varTerm);
142: } else {
143: Debug
144: .assertTrue(((TypeSchemeVariable) varTerm)
145: .getDefaultValue() == TypeSchemeUnion.REP_PEER_READONLY_ROOT);
146: }
147: }
148:
149: return varTerm;
150: }
151:
152: public TypeSchemeTerm checkStaticLocalVariable(ProgramVariable var) {
153: TypeSchemeTerm varTerm;
154:
155: if (hasPrimitiveType(var)) {
156: varTerm = TypeSchemeUnion.PRIMITIVE;
157: } else {
158: varTerm = (TypeSchemeTerm) annotations.get(var);
159:
160: if (varTerm == null) {
161: varTerm = new TypeSchemeVariable("TS(" + var + ")",
162: TypeSchemeUnion.READONLY_ROOT);
163: annotations.put(var, varTerm);
164: } else {
165: Debug
166: .assertTrue(((TypeSchemeVariable) varTerm)
167: .getDefaultValue() == TypeSchemeUnion.READONLY_ROOT);
168:
169: }
170: }
171:
172: return varTerm;
173: }
174:
175: public TypeSchemeTerm checkInstanceField(ProgramVariable field) {
176: TypeSchemeTerm fieldTerm;
177:
178: if (hasPrimitiveType(field)) {
179: fieldTerm = TypeSchemeUnion.PRIMITIVE;
180: } else {
181: fieldTerm = (TypeSchemeTerm) annotations.get(field);
182:
183: if (fieldTerm == null) {
184: fieldTerm = DEFAULT_FIELD_TERM;
185: }
186: }
187:
188: return fieldTerm;
189: }
190:
191: public TypeSchemeTerm checkStaticField(ProgramVariable field) {
192: TypeSchemeTerm fieldTerm;
193:
194: if (hasPrimitiveType(field)) {
195: fieldTerm = TypeSchemeUnion.PRIMITIVE;
196: } else {
197: fieldTerm = (TypeSchemeTerm) annotations.get(field);
198:
199: if (fieldTerm == null) {
200: fieldTerm = DEFAULT_FIELD_TERM;
201: }
202:
203: addEqualConstraint(fieldTerm, TypeSchemeUnion.READONLY_ROOT);
204: }
205:
206: return fieldTerm;
207: }
208:
209: public TypeSchemeTerm checkInstanceFieldAccess(
210: TypeSchemeTerm receiverTerm, TypeSchemeTerm fieldTerm) {
211: return new TypeSchemeCombineTerm(receiverTerm, fieldTerm);
212: }
213:
214: public TypeSchemeTerm checkStaticFieldAccess(
215: TypeSchemeTerm fieldTerm) {
216: return fieldTerm;
217: }
218:
219: public TypeSchemeTerm checkArrayAccess(Sort arraySort,
220: TypeSchemeTerm receiverTerm, TypeSchemeTerm positionTerm) {
221: ArrayOp arrayOp = ArrayOp.getArrayOp(arraySort);
222: Debug.assertTrue(arrayOp != null);
223: TypeSchemeTerm componentTerm = (TypeSchemeTerm) annotations
224: .get(arrayOp);
225:
226: if (componentTerm == null) {
227: componentTerm = DEFAULT_FIELD_TERM;
228: }
229:
230: return new TypeSchemeCombineTerm(receiverTerm, componentTerm);
231: }
232:
233: public TypeSchemeTerm checkInstanceMethodCall(
234: TypeSchemeTerm receiverTerm,
235: TypeSchemeTerm[] actualParTerms,
236: TypeSchemeTerm[] formalParTerms,
237: TypeSchemeTerm formalResultTerm) {
238: Debug
239: .assertTrue(actualParTerms.length == formalParTerms.length);
240:
241: for (int i = 0; i < formalParTerms.length; i++) {
242: TypeSchemeTerm recFormalParTerm = new TypeSchemeCombineTerm(
243: receiverTerm, formalParTerms[i]);
244: addSubConstraint(actualParTerms[i], recFormalParTerm);
245: }
246:
247: return (formalResultTerm == null ? null
248: : new TypeSchemeCombineTerm(receiverTerm,
249: formalResultTerm));
250:
251: }
252:
253: public TypeSchemeTerm checkStaticMethodCall(
254: TypeSchemeTerm[] actualParTerms,
255: TypeSchemeTerm[] formalParTerms,
256: TypeSchemeTerm formalResultTerm) {
257: Debug
258: .assertTrue(actualParTerms.length == formalParTerms.length);
259:
260: for (int i = 0; i < formalParTerms.length; i++) {
261: addSubConstraint(actualParTerms[i], formalParTerms[i]);
262: }
263:
264: return formalResultTerm;
265: }
266:
267: public TypeSchemeTerm checkAllocation(
268: TypeSchemeTerm[] actualParTerms,
269: TypeSchemeTerm[] formalParTerms) {
270: Debug
271: .assertTrue(actualParTerms.length == formalParTerms.length);
272:
273: TypeSchemeTerm newTerm = new TypeSchemeVariable("TS(allocation"
274: + allocNameCounter++ + ")",
275: TypeSchemeUnion.REP_PEER_ROOT);
276:
277: for (int i = 0; i < formalParTerms.length; i++) {
278: TypeSchemeTerm newFormalParTerm = new TypeSchemeCombineTerm(
279: newTerm, formalParTerms[i]);
280: addSubConstraint(actualParTerms[i], newFormalParTerm);
281: }
282:
283: return newTerm;
284: }
285:
286: public TypeSchemeTerm checkArrayAllocation(TypeSchemeTerm sizeTerm) {
287: return new TypeSchemeVariable("TS(arrayallocation"
288: + arrayAllocNameCounter++ + ")",
289: TypeSchemeUnion.REP_PEER_ROOT);
290: }
291:
292: public TypeSchemeTerm checkConditional(
293: TypeSchemeTerm conditionTerm, TypeSchemeTerm thenTerm,
294: TypeSchemeTerm elseTerm) {
295: TypeSchemeTerm conditionalTerm = new TypeSchemeVariable(
296: "TS(conditional" + conditionalNameCounter++ + ")",
297: TypeSchemeUnion.PRIMITIVE_REP_PEER_READONLY_ROOT);
298:
299: addSubConstraint(thenTerm, conditionalTerm);
300: addSubConstraint(elseTerm, conditionalTerm);
301:
302: return conditionalTerm;
303: }
304:
305: public TypeSchemeTerm checkAssignment(TypeSchemeTerm lhsTerm,
306: TypeSchemeTerm rhsTerm) {
307: addSubConstraint(rhsTerm, lhsTerm);
308: return lhsTerm;
309: }
310:
311: public void checkReturn(TypeSchemeTerm actualResultTerm,
312: TypeSchemeTerm formalResultTerm) {
313: Debug
314: .assertTrue((actualResultTerm == null) == (formalResultTerm == null));
315: if (actualResultTerm != null) {
316: addSubConstraint(actualResultTerm, formalResultTerm);
317: }
318: }
319:
320: public void checkCatch(TypeSchemeTerm excTerm) {
321: addEqualConstraint(excTerm, TypeSchemeUnion.READONLY);
322: }
323: }
|