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: package de.uka.ilkd.key.rule.updatesimplifier;
010:
011: import de.uka.ilkd.key.java.Services;
012: import de.uka.ilkd.key.logic.ArrayOfTerm;
013: import de.uka.ilkd.key.logic.Term;
014: import de.uka.ilkd.key.logic.TermFactory;
015: import de.uka.ilkd.key.logic.op.*;
016: import de.uka.ilkd.key.logic.sort.AbstractSort;
017: import de.uka.ilkd.key.rule.UpdateSimplifier;
018:
019: /**
020: * An abstract update simplification rule for application on array access
021: * operators.
022: *
023: * @author bubel
024: */
025: public class ApplyOnArrayAccess extends ApplyOnAccessTerm {
026:
027: /**
028: * @param updateSimplifier
029: */
030: public ApplyOnArrayAccess(UpdateSimplifier updateSimplifier) {
031: super (updateSimplifier);
032: }
033:
034: /**
035: * determines whether this rule is applicable for the
036: * update x target (the term on which the update will be
037: * applied) pair
038: * @param update the Update to be applied on target
039: * @param target the Term on which the update is applied
040: * @return true if the top level operator of target is an
041: * attribute operator
042: */
043: public boolean isApplicable(Update update, Term target) {
044: return target.op() instanceof ArrayOp;
045: }
046:
047: /**
048: * determines whether this rule is applicable for the pair of update and
049: * target (the term on which the update will be applied) term
050: *
051: * @param update
052: * the Update to be applied on the given term
053: * @param target
054: * the Term on which the update is applied
055: * @param services
056: * the Services object
057: * @return true if the rule can be applied on the update, target pair
058: */
059: public Term apply(Update update, Term target, Services services) {
060:
061: logEnter(update, target);
062:
063: // the field reference part (and if shadowed the transaction number)
064: // of target evaluated in the state described by the update
065: final PropagationResult pr = propagateUpdateToSubterms(update,
066: target, services);
067:
068: final Term result = UpdateSimplifierTermFactory.DEFAULT
069: .createIfExCascade(createCascade(pr, update, target),
070: updateSubterms(pr, target));
071:
072: logExit(result);
073:
074: if (!(result.sort().extendsTrans(target.sort()))) {
075: return UpdateSimplifierTermFactory.DEFAULT
076: .getBasicTermFactory().createCastTerm(
077: (AbstractSort) target.sort(), result);
078: }
079: return result;
080:
081: }
082:
083: private ArrayIfExCascade createCascade(PropagationResult pr,
084: Update update, Term target) {
085: return new ArrayIfExCascade(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:
098: return tf.createArrayTerm((ArrayOp) target.op(), pr
099: .getSimplifiedSubterms());
100: }
101:
102: private static class ArrayIfExCascade extends
103: IterateAssignmentPairsIfExCascade {
104:
105: private final Location targetLoc;
106: private final ArrayOfTerm targetSubs;
107: private final SetOfQuantifiableVariable criticalVars;
108:
109: public ArrayIfExCascade(ArrayOfAssignmentPair pairs,
110: ArrayOfTerm targetSubs, Location targetLoc) {
111: super (pairs);
112: this .targetSubs = targetSubs;
113: this .targetLoc = targetLoc;
114: this .criticalVars = freeVars(targetSubs);
115: }
116:
117: public Term getCondition() {
118: final TermFactory tf = UpdateSimplifierTermFactory.DEFAULT
119: .getBasicTermFactory();
120:
121: Term res = getCurrentPair().guard();
122: final Term eqObjects = compareObjects(
123: targetSubs.getTerm(0), getCurrentPair()
124: .locationSubs()[0]);
125: final Term eqIndex = tf.createEqualityTerm(targetSubs
126: .getTerm(1), getCurrentPair().locationSubs()[1]);
127: res = tf.createJunctorTermAndSimplify(Op.AND, res,
128: eqObjects);
129: res = tf.createJunctorTermAndSimplify(Op.AND, res, eqIndex);
130:
131: if (targetLoc instanceof ShadowedOperator
132: && getCurrentPair().location() instanceof ShadowedOperator) {
133: // in this case a conjunction of conditions has to be used
134: // as the transaction number needs to be checked as well
135: final Term eqTrans = tf
136: .createEqualityTerm(targetSubs.getTerm(2),
137: getCurrentPair().locationSubs()[2]);
138: res = tf.createJunctorTermAndSimplify(Op.AND, res,
139: eqTrans);
140: }
141:
142: return res;
143: }
144:
145: protected SetOfQuantifiableVariable criticalVars() {
146: return criticalVars;
147: }
148: }
149:
150: public Term matchingCondition(Update update, Term target,
151: Services services) {
152: // the field reference part (and if shadowed the transaction number)
153: // of target evaluated in the state described by the update
154: final PropagationResult pr = propagateUpdateToSubterms(update,
155: target, services);
156:
157: return UpdateSimplifierTermFactory.DEFAULT
158: .matchingCondition(createCascade(pr, update, target));
159: }
160: }
|