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: * Created on Apr 14, 2005
010: */
011: package de.uka.ilkd.key.rule.metaconstruct;
012:
013: import de.uka.ilkd.key.java.JavaInfo;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
016: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
017: import de.uka.ilkd.key.java.abstraction.ListOfKeYJavaType;
018: import de.uka.ilkd.key.logic.Name;
019: import de.uka.ilkd.key.logic.Term;
020: import de.uka.ilkd.key.logic.TermBuilder;
021: import de.uka.ilkd.key.logic.TermFactory;
022: import de.uka.ilkd.key.logic.op.AbstractMetaOperator;
023: import de.uka.ilkd.key.logic.op.Op;
024: import de.uka.ilkd.key.logic.sort.ArraySort;
025: import de.uka.ilkd.key.logic.sort.ClassInstanceSortImpl;
026: import de.uka.ilkd.key.logic.sort.PrimitiveSort;
027: import de.uka.ilkd.key.logic.sort.Sort;
028: import de.uka.ilkd.key.rule.inst.SVInstantiations;
029:
030: /**
031: * This metaconstruct tries to statically determine whether an array component
032: * assignment is safe, i.e. does not lead to an <code>ArrayStoreException</code>
033: * Currently it makes use of a strong closed world assumption which could be relaxed
034: * (of course by loss of power) to a version wo closed world asssumptions making
035: * use of the final modifier of classes.
036: * TODO: add features for multi-dimensional arrays
037: */
038: public class ArrayStoreStaticAnalyse extends AbstractMetaOperator {
039:
040: /**
041: * creates this metaconstruct
042: */
043: public ArrayStoreStaticAnalyse() {
044: super (new Name("#arrayStoreStaticAnalyse"), 1);
045: }
046:
047: private ListOfKeYJavaType determineDynamicTypes(
048: ClassInstanceSortImpl s, Services serv) {
049: final KeYJavaType keYJavaType = serv.getJavaInfo()
050: .getKeYJavaType(s);
051: final ListOfKeYJavaType result = serv.getJavaInfo()
052: .getAllSubtypes(keYJavaType);
053:
054: return result.prepend(keYJavaType);
055: }
056:
057: /**
058: *
059: * tests if the given sorts and all their subsorts are assignment
060: * compatible or not.
061: * <tt> null </tt> is returned if some are and others are not
062: */
063: private Term assignmentCompatible(
064: ClassInstanceSortImpl arrayElementSort,
065: ClassInstanceSortImpl elementSort, Services serv) {
066: final IteratorOfKeYJavaType elementDynamicTypesIt = determineDynamicTypes(
067: elementSort, serv).iterator();
068: final ListOfKeYJavaType arrayElementDynamicTypes = determineDynamicTypes(
069: arrayElementSort, serv);
070:
071: boolean assignmentCompatible = true;
072: boolean assignmentCompatibleSet = false;
073:
074: while (elementDynamicTypesIt.hasNext()) {
075: final IteratorOfKeYJavaType arrayElementDynamicTypesIt = arrayElementDynamicTypes
076: .iterator();
077: final Sort dynamicElementSort = elementDynamicTypesIt
078: .next().getSort();
079: boolean extTrans = false;
080: while (arrayElementDynamicTypesIt.hasNext()) {
081: final Sort arrayElementDynamicSort = arrayElementDynamicTypesIt
082: .next().getSort();
083: extTrans = dynamicElementSort
084: .extendsTrans(arrayElementDynamicSort);
085:
086: if (assignmentCompatibleSet
087: && extTrans != assignmentCompatible) {
088: // in this case we cannot say anything
089: // at least not true or false
090: // may be return later a formula
091: return null;
092: }
093: assignmentCompatible = assignmentCompatible && extTrans;
094: assignmentCompatibleSet = true;
095: }
096: }
097:
098: final TermFactory tf = TermFactory.DEFAULT;
099: return assignmentCompatible ? tf.createJunctorTerm(Op.TRUE)
100: : tf.createJunctorTerm(Op.FALSE);
101: }
102:
103: /**
104: * tries to determine whether the predicate "arrayStoreValid" is true or
105: * false using type analysis. It makes some strong closed world assumptions.
106: * A weaker version without closed world assumption is possible making use of
107: * the final modifier of classes.
108: * It assumes that teh first argumnet of <tt>arrayStoreValid</tt> is not
109: * equal to <tt>null</tt>
110: */
111: public Term calculate(Term term, SVInstantiations svInst,
112: Services services) {
113: // term.sub(0) is predicate arrayStoreCondition
114: final Term array = term.sub(0).sub(0);
115: final Term element = term.sub(0).sub(1);
116:
117: final JavaInfo ji = services.getJavaInfo();
118:
119: if (!(array.sort() instanceof ArraySort)
120: || ji.isAJavaCommonSort(array.sort())
121: || ji.isAJavaCommonSort(element.sort())) {
122: return term.sub(0);
123: }
124:
125: final ArraySort arraySort = (ArraySort) array.sort();
126: final Sort arrayElementSort = arraySort.elementSort();
127: final Sort elementSort = element.sort();
128: if (arrayElementSort instanceof ClassInstanceSortImpl
129: && elementSort instanceof ClassInstanceSortImpl) {
130: final Term result = assignmentCompatible(
131: (ClassInstanceSortImpl) arrayElementSort,
132: (ClassInstanceSortImpl) elementSort, services);
133: return result == null ? term.sub(0) : result;
134: } else if (arrayElementSort instanceof PrimitiveSort) {
135: if (!(elementSort instanceof PrimitiveSort)) {
136: return TermBuilder.DF.ff();
137: } else {
138: final Sort abstractInt = services.getTypeConverter()
139: .getIntegerLDT().targetSort();
140: if (arrayElementSort.extendsTrans(abstractInt)
141: && elementSort.extendsTrans(abstractInt)) {
142: return TermBuilder.DF.tt();
143: }
144: return TermBuilder.DF.ff();
145: }
146: }
147:
148: return term.sub(0);
149: }
150:
151: }
|