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.logic.op;
012:
013: import java.lang.ref.WeakReference;
014: import java.util.WeakHashMap;
015:
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.reference.ArrayReference;
018: import de.uka.ilkd.key.java.reference.ReferencePrefix;
019: import de.uka.ilkd.key.logic.Name;
020: import de.uka.ilkd.key.logic.Term;
021: import de.uka.ilkd.key.logic.sort.*;
022: import de.uka.ilkd.key.rule.MatchConditions;
023: import de.uka.ilkd.key.rule.inst.GenericSortCondition;
024: import de.uka.ilkd.key.rule.inst.GenericSortInstantiations;
025: import de.uka.ilkd.key.rule.inst.SortException;
026: import de.uka.ilkd.key.util.Debug;
027: import de.uka.ilkd.key.util.ExtList;
028:
029: public class ArrayOp extends AccessOp implements SortDependingSymbol {
030:
031: /**
032: * The pool of already created array operators. Ensures
033: * 'singleton' property of array operators.
034: */
035: private static final WeakHashMap operatorPool = new WeakHashMap(50);
036:
037: /** Sort of the array this operator addresses */
038: protected final Sort sort;
039:
040: private final Sort dependingOnSort;
041:
042: private static final Name kind = new Name("arrayaccess");
043:
044: /**
045: * returns and if neccessary creates the shadowed array access operator for
046: * the given array sort
047: *
048: * @param arraySort the Sort to which this operator is applicable
049: * must be of kind {@link ArraySort} or {@link ProgramSVSort}
050: * @return the array access operator for the given array sort
051: */
052: public static ArrayOp getArrayOp(Sort arraySort) {
053: Debug.assertTrue(arraySort instanceof ArraySort
054: || arraySort instanceof ProgramSVSort
055: || arraySort instanceof GenericSort
056: || arraySort == AbstractMetaOperator.METASORT,
057: arraySort + " is no allowed array sort.");
058: WeakReference arrayAccessOpReference = (WeakReference) operatorPool
059: .get(arraySort);
060: if (arrayAccessOpReference == null
061: || arrayAccessOpReference.get() == null) {
062: // wrapping attributeOp in a weak reference is necessary as
063: // it contains a strong reference to its key
064: arrayAccessOpReference = new WeakReference(new ArrayOp(
065: arraySort));
066: operatorPool.put(arraySort, arrayAccessOpReference);
067: }
068: return (ArrayOp) arrayAccessOpReference.get();
069: }
070:
071: protected ArrayOp(Name name, Sort arraySort) {
072: super (name);
073: this .sort = arraySort;
074: if (arraySort instanceof ProgramSVSort
075: || arraySort == AbstractMetaOperator.METASORT) {
076: this .dependingOnSort = null;
077: } else {
078: this .dependingOnSort = arraySort;
079: }
080: }
081:
082: /**
083: * creates an ArrayOp
084: */
085: private ArrayOp(Sort arraySort) {
086: this (new Name("arrayAccess(" + arraySort + ")"), arraySort);
087: }
088:
089: /**
090: * determines the sort of the {@link Term} if it would be created using this
091: * Operator as top level operator and the given terms as sub terms. The
092: * assumption that the constructed term would be allowed is not checked.
093: * @param term an array of Term containing the subterms of a (potential)
094: * term with this operator as top level operator
095: * @return sort of the term with this operator as top level operator of the
096: * given substerms
097: */
098: public Sort sort(Term[] term) {
099: if (sort instanceof ProgramSVSort
100: || sort instanceof GenericSort
101: || sort == AbstractMetaOperator.METASORT) {
102: return ProgramSVSort.NONSIMPLEEXPRESSION;
103: }
104: return ((ArraySort) sort).elementSort();
105: }
106:
107: /** checks whether the top level structure of the given @link Term
108: * is syntactically valid, given the assumption that the top level
109: * operator of the term is the same as this Operator. The
110: * assumption that the top level operator and the term are equal
111: * is NOT checked.
112: * @return true iff the top level structure of
113: * the @link Term is valid.
114: */
115: public boolean validTopLevel(Term term) {
116: Sort s = term.sub(0).sort();
117: if (sort instanceof ArraySort
118: && (s instanceof ArraySort || s == Sort.NULL)) {
119: // missing check if term.sub(1) has integer sort
120: return s.extendsTrans(sort);
121: } else if (sort instanceof ProgramSVSort
122: || sort instanceof GenericSort
123: || sort == AbstractMetaOperator.METASORT) {
124: return true;
125: }
126: return false;
127: }
128:
129: /**
130: * the arity of an array access operator is <code>2</code> where the
131: * first sub term denotes the array object itself and the second one
132: * the accessed index
133: * @return arity of the Operator as int
134: */
135: public int arity() {
136: return 2;
137: }
138:
139: /**
140: * @return true if the operator is a shadowed
141: */
142: public boolean isShadowed() {
143: return false;
144: }
145:
146: /**
147: * @return the array sort on which this operator is applied
148: */
149: public Sort arraySort() {
150: return sort;
151: }
152:
153: /**
154: * @return the sort of this operator
155: */
156: public Sort sort() {
157: return ((ArraySort) sort).elementSort();
158: }
159:
160: /**
161: * the top level operator of t must be <tt>this</tt>
162: * returns the reference prefix of this array access for the given term
163: */
164: public Term referencePrefix(Term t) {
165: Debug.assertTrue(t.op() == this );
166: return t.sub(0);
167: }
168:
169: /**
170: * the top level operator of t must be <tt>this</tt>
171: * returns the index of this array access for the given term
172: */
173: public Term index(Term t) {
174: Debug.assertTrue(t.op() == this );
175: return t.sub(1);
176: }
177:
178: public de.uka.ilkd.key.java.Expression convertToProgram(Term t,
179: ExtList el) {
180: ReferencePrefix accessPath = (ReferencePrefix) el.get(0);
181: el.remove(accessPath);
182: return new ArrayReference(el, accessPath);
183: }
184:
185: /**
186: * tests if the location <code>loc</code> may be an alias of this array
187: * location
188: * @param loc the Location to check
189: * @return true iff <code>loc</code> may be an alias of the current (this)
190: * location
191: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliasedBy
192: * (de.uka.ilkd.key.logic.op.Location)
193: */
194: public boolean mayBeAliasedBy(Location loc) {
195: if (!(loc instanceof ArrayOp)
196: || (loc instanceof ShadowedOperator))
197: return false;
198:
199: final ArrayOp aOp = (ArrayOp) loc;
200: return arraySortAliased(aOp.arraySort(), arraySort())
201: || sort instanceof ProgramSVSort
202: || aOp.sort instanceof ProgramSVSort;
203: }
204:
205: protected boolean arraySortAliased(Sort as1, Sort as2) {
206: assert as1 instanceof ArraySort && as2 instanceof ArraySort;
207: return true;
208: }
209:
210: /**
211: * implements the default operator matching rule which means
212: * that the compared object have to be equal otherwise
213: * matching fails
214: */
215: public MatchConditions match(SVSubstitute subst,
216: MatchConditions mc, Services services) {
217: if (subst.getClass() == this .getClass()) {
218: if (getSortDependingOn() instanceof ProgramSVSort) {
219: return mc;
220: } else if (getSortDependingOn() instanceof GenericSort) {
221: final GenericSortInstantiations genSortInst = mc
222: .getInstantiations()
223: .getGenericSortInstantiations();
224: final GenericSort gs = (GenericSort) getSortDependingOn();
225: if (genSortInst.isInstantiated(gs)) {
226: final Sort s = genSortInst.getRealSort(
227: getSortDependingOn(), services);
228: assert s instanceof ArraySort;
229: return getArrayOp(s).match(subst, mc, services);
230: } else {
231: final GenericSortCondition c = GenericSortCondition
232: .createIdentityCondition(gs,
233: ((ArrayOp) subst)
234: .getSortDependingOn());
235: if (c == null) {
236: Debug.out("FAILED. Generic sort condition");
237: return null; //FAILED;
238: } else {
239: try {
240: mc = mc.setInstantiations(mc
241: .getInstantiations().add(c));
242: } catch (SortException e) {
243: Debug.out("FAILED. Sort mismatch.", gs,
244: ((ArrayOp) subst)
245: .getSortDependingOn());
246: return null; //FAILED;
247: }
248: }
249: return mc;
250: }
251: } else if (getSortDependingOn() == null) {
252: // array operators occuring in find expressions must be
253: // qualified
254: assert false;
255: }
256: }
257: return super .match(subst, mc, services);
258:
259: }
260:
261: public String toString() {
262: return "[](" + arraySort() + ")";
263: }
264:
265: public SortDependingSymbol getInstanceFor(SortDefiningSymbols p_sort) {
266: return getArrayOp(p_sort);
267: }
268:
269: public Name getKind() {
270: return kind;
271: }
272:
273: public Sort getSortDependingOn() {
274: return dependingOnSort;
275: }
276:
277: public boolean isSimilar(SortDependingSymbol p) {
278:
279: return p != null && p.getKind().equals(this.getKind());
280: }
281:
282: }
|