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.logic.Name;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.sort.ArraySort;
019: import de.uka.ilkd.key.logic.sort.GenericSort;
020: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
021: import de.uka.ilkd.key.logic.sort.Sort;
022: import de.uka.ilkd.key.util.Debug;
023:
024: /**
025: * Shadow Array access operator used in transactions
026: */
027: public class ShadowArrayOp extends ArrayOp implements ShadowedOperator {
028:
029: /**
030: * The pool of already created array operators. Ensures
031: * 'singleton' property of array operators.
032: */
033: private static final WeakHashMap operatorPool = new WeakHashMap(50);
034:
035: /**
036: * returns and if neccessary creates the array access operator for the given
037: * array sort
038: *
039: * @param arraySort
040: * the ArraySort to which this operator is applicable
041: * @return the array access operator for the given array sort
042: */
043: public static ShadowArrayOp getShadowArrayOp(Sort arraySort) {
044: Debug.assertTrue(arraySort instanceof ArraySort
045: || arraySort instanceof ProgramSVSort
046: || arraySort instanceof GenericSort
047: || arraySort == AbstractMetaOperator.METASORT,
048: arraySort + " is no allowed array sort.");
049: WeakReference arrayAccessOpReference = (WeakReference) operatorPool
050: .get(arraySort);
051: if (arrayAccessOpReference == null
052: || arrayAccessOpReference.get() == null) {
053: // wrapping attributeOp in a weak reference is necessary as
054: // it contains a strong reference to its key
055: arrayAccessOpReference = new WeakReference(
056: new ShadowArrayOp(arraySort));
057: operatorPool.put(arraySort, arrayAccessOpReference);
058: }
059: return (ShadowArrayOp) arrayAccessOpReference.get();
060: }
061:
062: /**
063: * creates an ShadowArrayOp
064: */
065: ShadowArrayOp(Sort arraySort) {
066: super (new Name("shadowed-access(" + arraySort + ")"), arraySort);
067: }
068:
069: /** @return arity of the Operator as int */
070: public int arity() {
071: return 3;
072: }
073:
074: /**
075: * @return true if the operator is a shadowed
076: */
077: public boolean isShadowed() {
078: return true;
079: }
080:
081: public Term getTransactionNumber(Term t) {
082: return t.sub(2);
083: }
084:
085: public boolean mayBeAliasedBy(Location loc) {
086: if (loc == this )
087: return true;
088:
089: if (loc instanceof ArrayOp) {
090: ArrayOp locAsArray = (ArrayOp) loc;
091: if ((locAsArray.sort instanceof ProgramSVSort
092: || sort instanceof ProgramSVSort || sort == AbstractMetaOperator.METASORT)
093: || arraySortAliased(locAsArray.arraySort(),
094: arraySort())) {
095: return true;
096: }
097: }
098: return false;
099: }
100:
101: public String toString() {
102: return "[](shadowed, " + arraySort() + ")";
103: }
104: }
|