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: * Created on 18.12.2004
011: */
012: package de.uka.ilkd.key.rule.updatesimplifier;
013:
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.logic.ArrayOfTerm;
016: import de.uka.ilkd.key.logic.Term;
017: import de.uka.ilkd.key.logic.TermFactory;
018: import de.uka.ilkd.key.logic.op.*;
019: import de.uka.ilkd.key.rule.UpdateSimplifier;
020:
021: /**
022: * An abstract update simplification rule for update application on attribute
023: * access terms. This class is inherited by the concrete ruels for shadowed
024: * and unshadowed attribute accesses.
025: *
026: * @author bubel
027: */
028: public class ApplyOnAttributeAccess extends ApplyOnAccessTerm {
029:
030: /**
031: *
032: * @param updateSimplifier
033: */
034: public ApplyOnAttributeAccess(UpdateSimplifier updateSimplifier) {
035: super (updateSimplifier);
036: }
037:
038: /**
039: * determines whether this rule is applicable for the
040: * update x target (the term on which the update will be
041: * applied) pair
042: * @param update the Update to be applied on target
043: * @param target the Term on which the update is applied
044: * @return true if the top level operator of target is an
045: * attribute operator
046: */
047: public boolean isApplicable(Update update, Term target) {
048: return (target.op() instanceof AttributeOp)
049: || (target.op() instanceof NonRigidFunctionLocation);
050: }
051:
052: /**
053: * applies an update on a term representing an instance attribute
054: *
055: * @param update
056: * the Update to be applied on target
057: * @param target
058: * the Term representing an instance attribute
059: * @param services
060: * the Services object
061: * @return the simplified term describing the value of target under the
062: * given update
063: * @requires update != null && target!=null && target.op() instanceof
064: * AttributeOp && !(target.op() instanceof ShadowedOperator)
065: */
066: public Term apply(Update update, Term target, Services services) {
067: logEnter(update, target);
068:
069: // the field reference part (and if shadowed the transaction number)
070: // of target evaluated in the state described by the update
071: final PropagationResult pr = propagateUpdateToSubterms(update,
072: target, services);
073:
074: final Term result = UpdateSimplifierTermFactory.DEFAULT
075: .createIfExCascade(createCascade(pr, update, target),
076: updateSubterms(pr, target));
077:
078: logExit(result);
079:
080: return result;
081: }
082:
083: private AttrIfExCascade createCascade(PropagationResult pr,
084: Update update, Term target) {
085: return new AttrIfExCascade(update
086: .getAssignmentPairs((Location) target.op()),
087: new ArrayOfTerm(pr.getSimplifiedSubterms()),
088: (Location) target.op());
089: }
090:
091: private Term updateSubterms(PropagationResult pr, Term target) {
092: if (!pr.hasChanged())
093: return target;
094:
095: final TermFactory tf = UpdateSimplifierTermFactory.DEFAULT
096: .getBasicTermFactory();
097: return target.op() instanceof AttributeOp ? tf
098: .createAttributeTerm((AttributeOp) target.op(), pr
099: .getSimplifiedSubterms()) : tf
100: .createFunctionTerm((Function) target.op(), pr
101: .getSimplifiedSubterms());
102: }
103:
104: private static class AttrIfExCascade extends
105: IterateAssignmentPairsIfExCascade {
106:
107: private final Location targetLoc;
108: private final ArrayOfTerm targetSubs;
109: private final SetOfQuantifiableVariable criticalVars;
110:
111: public AttrIfExCascade(ArrayOfAssignmentPair pairs,
112: ArrayOfTerm targetSubs, Location targetLoc) {
113: super (pairs);
114: this .targetSubs = targetSubs;
115: this .targetLoc = targetLoc;
116: this .criticalVars = freeVars(targetSubs);
117: }
118:
119: public Term getCondition() {
120: final TermFactory tf = UpdateSimplifierTermFactory.DEFAULT
121: .getBasicTermFactory();
122:
123: Term res = getCurrentPair().guard();
124: final Term eqObjects = compareObjects(
125: targetSubs.getTerm(0), getCurrentPair()
126: .locationSubs()[0]);
127: res = tf.createJunctorTermAndSimplify(Op.AND, res,
128: eqObjects);
129:
130: // attention we need not to take care of
131: // the case {o.a':=t}o.a --> o.a as in this case this method must not
132: // be called (hint:update.getAssignmentPairs ( (Location)target.op () )
133: // returns only possible aliased assignement pairs)
134: if (targetLoc instanceof ShadowedOperator
135: && getCurrentPair().location() instanceof ShadowedOperator) {
136: // in this case a conjunction of conditions has to be used
137: // as the transaction number needs to be checked as well
138: final Term eqTrans = tf
139: .createEqualityTerm(targetSubs.getTerm(1),
140: getCurrentPair().locationSubs()[1]);
141: res = tf.createJunctorTermAndSimplify(Op.AND, res,
142: eqTrans);
143: }
144:
145: return res;
146: }
147:
148: protected SetOfQuantifiableVariable criticalVars() {
149: return criticalVars;
150: }
151: }
152:
153: public Term matchingCondition(Update update, Term target,
154: Services services) {
155: // the field reference part (and if shadowed the transaction number)
156: // of target evaluated in the state described by the update
157: final PropagationResult pr = propagateUpdateToSubterms(update,
158: target, services);
159:
160: return UpdateSimplifierTermFactory.DEFAULT
161: .matchingCondition(createCascade(pr, update, target));
162: }
163: }
|