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: package de.uka.ilkd.key.logic.op;
011:
012: import java.lang.ref.WeakReference;
013: import java.util.WeakHashMap;
014:
015: import de.uka.ilkd.key.logic.Term;
016:
017: /**
018: * this class is used to represent the reference operator '.'
019: * in the shadow form (for transactions)
020: */
021: public class ShadowAttributeOp extends AttributeOp implements
022: ShadowedOperator {
023:
024: /**
025: * The pool of already created attribute operators. Ensures
026: * 'singleton' property of attribute operators.
027: */
028: private static final WeakHashMap operatorPool = new WeakHashMap(50);
029:
030: /**
031: * returns and if neccessary creates the access operator of the
032: * given attribute
033: * @return the attribute operator for the given attribute
034: */
035: public static ShadowAttributeOp getShadowAttributeOp(
036: IProgramVariable attribute) {
037: WeakReference attributeOpReference = (WeakReference) operatorPool
038: .get(attribute);
039: if (attributeOpReference == null
040: || attributeOpReference.get() == null) {
041: // wrapping attributeOp in a weak reference is necessary as
042: // it contains a strong reference to its key
043: attributeOpReference = new WeakReference(
044: new ShadowAttributeOp(attribute));
045: operatorPool.put(attribute, attributeOpReference);
046: }
047: return (ShadowAttributeOp) attributeOpReference.get();
048: }
049:
050: /**
051: * creates a new shadow attribute operator.
052: */
053: private ShadowAttributeOp(IProgramVariable attribute) {
054: super (attribute);
055: }
056:
057: /**
058: * In contrast to the standard attribute access operator the arity
059: * of a shadowed attribute is two. The first term denotes the object
060: * whose field is accessed and second one stores a shadow marker.
061: * @return arity of the Operator as int
062: */
063: public int arity() {
064: return 2;
065: }
066:
067: /**
068: * @return true if the operator is a shadowed
069: */
070: public boolean isShadowed() {
071: return true;
072: }
073:
074: /**
075: * returns the transaction number (shadow marker) of the given term
076: * it assumes that the term's top operator is a ShadowedAttributeOp
077: */
078: public Term getTransactionNumber(Term t) {
079: return t.sub(1);
080: }
081:
082: /**
083: * returns true if the given loc may be aliased by the current location
084: */
085: public boolean mayBeAliasedBy(Location loc) {
086: if (loc == this ) {
087: return true;
088: }
089:
090: if (loc instanceof AttributeOp) {
091: return attributesAliased(((AttributeOp) loc).attribute());
092: }
093:
094: return false;
095: }
096:
097: /**
098: * @param variable
099: * @return
100: */
101: private boolean attributesAliased(IProgramVariable variable) {
102: boolean attributesAliased = (variable instanceof SortedSchemaVariable || attribute() instanceof SortedSchemaVariable);
103:
104: attributesAliased = attributesAliased
105: || variable == attribute();
106:
107: return attributesAliased;
108: }
109:
110: public String toString() {
111: return ".(shadowed)" + attribute();
112: }
113: }
|