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.sort;
012:
013: import java.lang.ref.WeakReference;
014: import java.util.WeakHashMap;
015:
016: public class ArraySortImpl extends AbstractCollectionSort implements
017: ArraySort {
018:
019: private static WeakHashMap aSH = new WeakHashMap();
020:
021: private final ArrayOfSort commonJavaSorts;
022:
023: private SetOfSort extendsSorts;
024:
025: /** keeping this key is important to prevent for too early hasmap removal*/
026: private final SortKey sk;
027:
028: private ArraySortImpl(SetOfSort extendsSorts, SortKey sk) {
029: super (sk.elemSort.name() + "[]", sk.elemSort);
030:
031: this .sk = sk;
032:
033: final Sort[] commons = new Sort[3];
034: commons[0] = this .sk.javaLangObjectSort;
035: commons[1] = this .sk.javaLangCloneable;
036: commons[2] = this .sk.javaLangSerializable;
037: commonJavaSorts = new ArrayOfSort(commons);
038: // uncommented because of ASMKeY:
039: // Debug.assertTrue(extendsSorts!=SetAsListOfSort.EMPTY_SET);
040: this .extendsSorts = extendsSorts;
041: }
042:
043: /**
044: * @return an object of this class with elementSort().equals(p),
045: * or null if such an object cannot be constructed (as p is an
046: * incompatible sort).
047: */
048: public Sort cloneFor(Sort p) {
049: return getArraySort(p, commonJavaSorts.getSort(0),
050: commonJavaSorts.getSort(1), commonJavaSorts.getSort(2));
051: }
052:
053: /**
054: * @return the sorts of the predecessors of this sort
055: */
056: public SetOfSort extendsSorts() {
057: return extendsSorts;
058: }
059:
060: /**
061: * returns elemSort([])^n.
062: */
063: public static Sort getArraySortForDim(Sort elemSort, int n,
064: Sort objectSort, Sort cloneableSort, Sort serializableSort) {
065: Sort result = elemSort;
066: while (n > 0) {
067: result = getArraySort(result, objectSort, cloneableSort,
068: serializableSort);
069: n--;
070: }
071: return result;
072: }
073:
074: /**
075: * returns the ArraySort to the given elementsort. This method ensures that
076: * only one ArraySort-object exists for each Arraysort.
077: */
078: public static ArraySort getArraySort(Sort elemSort,
079: Sort objectSort, Sort cloneableSort, Sort serializableSort) {
080: // this wrapper is required as some element sorts are shared among
081: // several environments (int, boolean)
082: final SortKey sk = new SortKey(elemSort, objectSort,
083: cloneableSort, serializableSort);
084: ArraySort as = aSH.containsKey(sk) ? (ArraySort) ((WeakReference) aSH
085: .get(sk)).get()
086: : null;
087:
088: if (as == null) {
089: // HACK: this simple handling of sort creation does not treat
090: // depending symbols (i.e. ArrayOfS::instance)
091: SetOfSort localExtendsSorts = getArraySuperSorts(elemSort,
092: objectSort, cloneableSort, serializableSort);
093: as = new ArraySortImpl(localExtendsSorts, sk);
094: aSH.put(sk, new WeakReference(as));
095:
096: }
097: return as;
098: }
099:
100: private static SetOfSort getArraySuperSorts(Sort elem,
101: Sort objectSort, Sort cloneableSort, Sort serializableSort) {
102: int i = 1;
103: while (elem instanceof ArraySort) {
104: elem = ((ArraySort) elem).elementSort();
105: i++;
106: }
107: SetOfSort super Sorts = elem.extendsSorts();
108:
109: if (elem instanceof PrimitiveSort || elem == objectSort) {
110: i--;
111: super Sorts = super Sorts.add(objectSort).add(cloneableSort)
112: .add(serializableSort);
113: }
114:
115: if (i > 0) {
116: final IteratorOfSort it = super Sorts.iterator();
117: super Sorts = SetAsListOfSort.EMPTY_SET;
118: while (it.hasNext()) {
119: Sort s = it.next();
120: super Sorts = super Sorts.add(getArraySortForDim(s, i,
121: objectSort, cloneableSort, serializableSort));
122: }
123: }
124:
125: return super Sorts;
126: }
127:
128: static class SortKey {
129: final Sort elemSort;
130: final Sort javaLangObjectSort;
131: final Sort javaLangSerializable;
132: final Sort javaLangCloneable;
133:
134: public SortKey(Sort elemSort, Sort javaLangObjectSort,
135: Sort javaLangCloneable, Sort javaLangSerializable) {
136: this .elemSort = elemSort;
137: this .javaLangObjectSort = javaLangObjectSort;
138: this .javaLangCloneable = javaLangCloneable;
139: this .javaLangSerializable = javaLangSerializable;
140: }
141:
142: public boolean equals(Object o) {
143: if (!(o instanceof SortKey)) {
144: return false;
145: }
146: final SortKey sk = (SortKey) o;
147: return elemSort == sk.elemSort
148: && javaLangObjectSort == sk.javaLangObjectSort
149: && javaLangSerializable == sk.javaLangSerializable
150: && javaLangCloneable == sk.javaLangCloneable;
151: }
152:
153: public int hashCode() {
154: return elemSort.hashCode()
155: + (javaLangCloneable == null ? 0
156: : 31 * javaLangCloneable.hashCode())
157: + (javaLangObjectSort == null ? 0
158: : 17 * javaLangObjectSort.hashCode())
159: + (javaLangSerializable == null ? 0
160: : 3 * javaLangSerializable.hashCode());
161: }
162:
163: }
164: }
|