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.java.Expression;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
018: import de.uka.ilkd.key.java.reference.FieldReference;
019: import de.uka.ilkd.key.java.reference.ReferencePrefix;
020: import de.uka.ilkd.key.logic.Name;
021: import de.uka.ilkd.key.logic.Term;
022: import de.uka.ilkd.key.logic.sort.ArraySort;
023: import de.uka.ilkd.key.logic.sort.ObjectSort;
024: import de.uka.ilkd.key.logic.sort.Sort;
025: import de.uka.ilkd.key.rule.MatchConditions;
026: import de.uka.ilkd.key.util.Debug;
027:
028: /**
029: * this class is used to represent the reference operator '.' of
030: * Java, e.g.>> int[] a = new int[]{1,2,3}; int i = a.length; <<<
031: * where the '.' in a.length points to field called length
032: * ATTENTION: At this moment only variables are adressed to this may
033: * change in future
034: */
035: public class AttributeOp extends AccessOp {
036:
037: /**
038: * The pool of already created attribute operators. Ensures
039: * 'singleton' property of attribute operators.
040: */
041: private static final WeakHashMap operatorPool = new WeakHashMap(50);
042:
043: /** The attribute, which is accessed via this operator */
044: private final IProgramVariable attribute;
045:
046: /** Sort of the program variables */
047: private final Sort sort;
048:
049: /**
050: * returns and if neccessary creates the access operator of the
051: * given attribute
052: * @return the attribute operator for the given attribute
053: */
054: public static AttributeOp getAttributeOp(IProgramVariable attribute) {
055: WeakReference attributeOpReference = (WeakReference) operatorPool
056: .get(attribute);
057: if (attributeOpReference == null
058: || attributeOpReference.get() == null) {
059: // wrapping attributeOp in a weak reference is necessary as
060: // it contains a strong reference to its key
061: attributeOpReference = new WeakReference(new AttributeOp(
062: attribute));
063: operatorPool.put(attribute, attributeOpReference);
064: }
065: return (AttributeOp) attributeOpReference.get();
066: }
067:
068: /**
069: * creates a new access operator for the given attribute
070: * @param attribute the ProgramVariable representing a field
071: */
072: protected AttributeOp(IProgramVariable attribute) {
073: super (new Name("." + attribute.name().toString()));
074: this .attribute = attribute;
075: this .sort = attribute instanceof ProgramSV ? ((ProgramSV) attribute)
076: .sort()
077: : ((ProgramVariable) attribute).sort();
078: }
079:
080: /**
081: * checks whether the top level structure of the given {@link Term}
082: * is syntactically valid, given the assumption that the top level
083: * operator of the term is the same as this Operator. The
084: * assumption that the top level operator and the term are equal
085: * is NOT checked.
086: * @return true iff the top level structure of
087: * the @link Term is valid.
088: */
089: public boolean validTopLevel(Term term) {
090: if (((AttributeOp) term.op()).attribute() instanceof SchemaVariable
091: || term.sub(0).op() instanceof SchemaVariable) {
092: return true;
093: } else if (term.arity() != arity()) {
094: return false;
095: }
096: return term.sub(0).sort() instanceof ObjectSort
097: || term.sub(0).sort() instanceof ArraySort;
098: }
099:
100: /**
101: * The arity of an attribute operator is <code>1</code> and the
102: * corresponding subterm denotes the object whose attribute is
103: * accessed.
104: * @return arity of the Operator as int
105: */
106: public int arity() {
107: return 1;
108: }
109:
110: /** returns the attribute of the operator
111: * @return the attribute of the operator
112: */
113: public IProgramVariable attribute() {
114: return attribute;
115: }
116:
117: /**
118: * returns the KeYJavaType the attribute is declared in
119: */
120: public KeYJavaType getContainerType() {
121: return ((ProgramVariable) attribute()).getContainerType();
122: }
123:
124: /**
125: * the sort of the attribute
126: */
127: public Sort sort() {
128: return attribute.sort();
129: }
130:
131: /**
132: * returns the {@link KeYJavaType} of this access operator
133: * @return the KeYJavaType of this access operator
134: */
135: public KeYJavaType getKeYJavaType(Term t) {
136: return ((ProgramVariable) attribute).getKeYJavaType();
137: }
138:
139: /**
140: * the top level operator of t must be <tt>this</tt>
141: * returns the reference prefix of this attribute of the given term
142: */
143: public Term referencePrefix(Term t) {
144: Debug.assertTrue(t.op() == this );
145: return t.sub(0);
146: }
147:
148: /**
149: * converts the logical attribute access operator to its Java
150: * dependance
151: */
152: public Expression convertToProgram(Term t,
153: de.uka.ilkd.key.util.ExtList l) {
154: return new FieldReference((ProgramVariable) attribute,
155: (ReferencePrefix) l.get(0));
156: }
157:
158: /**
159: * determines the sort of the {@link Term} if it would be created using this
160: * Operator as top level operator and the given terms as sub terms. The
161: * assumption that the constructed term would be allowed is not checked.
162: * @param term an array of Term containing the subterms of a (potential)
163: * term with this operator as top level operator
164: * @return sort of the term with this operator as top level operator of the
165: * given substerms
166: */
167: public Sort sort(Term[] term) {
168: return sort;
169: }
170:
171: /**
172: * @return true if the operator is a shadowed
173: */
174: public boolean isShadowed() {
175: return false;
176: }
177:
178: public boolean equals(Object o) {
179: return o == this ;
180: }
181:
182: public int hashCode() {
183: return AttributeOp.class.hashCode() + 17 * attribute.hashCode();
184: }
185:
186: /** toString */
187: public String toString() {
188: return name().toString();
189: }
190:
191: /* (non-Javadoc)
192: * @see de.uka.ilkd.key.logic.op.Location#mayBeAliased(de.uka.ilkd.key.logic.op.Location)
193: */
194: public boolean mayBeAliasedBy(Location loc) {
195: return (loc == this || (loc instanceof AttributeOp
196: && !((AttributeOp) loc).isShadowed() && (attribute instanceof SortedSchemaVariable || (((AttributeOp) loc).attribute instanceof SortedSchemaVariable))));
197: }
198:
199: /**
200: * Tries to match the given operator <code>op</code> with this one.
201: */
202: public MatchConditions match(SVSubstitute subst,
203: MatchConditions mc, Services services) {
204: if (subst == this )
205: return mc;
206: if (subst.getClass() != this .getClass()) {
207: Debug.out("FAILED. Operator mismatch (template, orig)",
208: this , subst);
209: return null;
210: }
211: final AttributeOp attrOp = (AttributeOp) subst;
212: return attribute.match(attrOp.attribute, mc, services);
213: }
214: }
|