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: package de.uka.ilkd.key.rule.updatesimplifier;
009:
010: import java.util.Arrays;
011: import java.util.HashSet;
012:
013: import de.uka.ilkd.key.java.Services;
014: import de.uka.ilkd.key.logic.ProgramElementName;
015: import de.uka.ilkd.key.logic.Term;
016: import de.uka.ilkd.key.logic.TermFactory;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.rule.AbstractUpdateRule;
019: import de.uka.ilkd.key.rule.UpdateSimplifier;
020: import de.uka.ilkd.key.util.Debug;
021:
022: /**
023: * This rule implements the update rule to be used for application on non rigid
024: * functions with explicit dependency knowledge. The rule first sequentialzes
025: * the simultaneous update and then propagates the independant part of the
026: * update to the subterms. This rule may introduce <em>new</em> program
027: * variables.
028: */
029: public class ApplyOnNonRigidWithExplicitDependencies extends
030: AbstractUpdateRule {
031:
032: /**
033: * During update decomposition certain subterms <code>t</code>
034: * are replaced by a new introduced variable <code>var</code>.
035: * This inner class helps in particular to keep track
036: * of the pair <tt>(var, t)</tt> from which later new {@link AssignmentPair}s
037: * are created.
038: */
039: public class ReplacementResult {
040:
041: private ListOfAssignmentPair assignmentPairs = SLListOfAssignmentPair.EMPTY_LIST;
042: private Term result;
043:
044: /**
045: * creates a new instance
046: */
047: public ReplacementResult() {
048: super ();
049: }
050:
051: /**
052: * @return
053: */
054: public boolean hasChanged() {
055: return !assignmentPairs.isEmpty();
056: }
057:
058: /**
059: * returns a new {@link AssignmentPair}
060: * @return
061: */
062: public ListOfAssignmentPair getAssignmentPairs() {
063: return assignmentPairs;
064: }
065:
066: /**
067: * @return
068: */
069: public Term getTerm() {
070: return result;
071: }
072:
073: /**
074: * @param replacementVar
075: * @param term
076: */
077: public void addAssignmentPair(LocationVariable replacementVar,
078: Term term) {
079: assignmentPairs = assignmentPairs
080: .append(new AssignmentPairImpl(replacementVar,
081: new Term[0], term));
082: }
083:
084: /**
085: * @param term
086: */
087: public void setReplacementResultTerm(Term term) {
088: this .result = term;
089: }
090:
091: }
092:
093: private static final TermFactory BASIC_TERM_FACTORY = UpdateSimplifierTermFactory.DEFAULT
094: .getBasicTermFactory();
095:
096: /**
097: * Creates an instance of this rule for the given update simplifier
098: *
099: * @param updateSimplifier
100: * the UpdateSimplifier where the rule will be used
101: */
102: public ApplyOnNonRigidWithExplicitDependencies(
103: UpdateSimplifier updateSimplifier) {
104: super (updateSimplifier);
105: }
106:
107: /**
108: * This rule is applicable if the top operator of the target term is of kind
109: * {@link de.uka.ilkd.key.logic.op.NRFunctionWithExplicitDependencies}
110: *
111: * @param update
112: * the Update to be applied on the target term
113: * @param target
114: * the Term on which the update is applied
115: * @return true iff this rule is responsible for simplication of the given
116: * pair
117: */
118: public boolean isApplicable(Update update, Term target) {
119: return target.op() instanceof NRFunctionWithExplicitDependencies;
120: }
121:
122: /**
123: * applies the update on the given target and returns the result. It is
124: * assumed that
125: * {@link ApplyOnNonRigidWithExplicitDependencies#isApplicable(Update, Term)}
126: * has been called before and returned <tt>true</tt>
127: *
128: * @param update
129: * the Update to be applied on <code>target</code>
130: * @param target
131: * the Term with a top operator of kind
132: * {@link NRFunctionWithExplicitDependencies}on which the update
133: * is applied
134: * @param services
135: * the Services object
136: * @return the application result
137: */
138: public Term apply(Update update, Term target, Services services) {
139: logEnter(update, target);
140: final Update[] updates = sequentializeUpdate(update,
141: (NRFunctionWithExplicitDependencies) target.op());
142: Term result;
143: if (updates[1] != null) {
144: final PropagationResult pr = propagateUpdateToSubterms(
145: updates[1], target, services);
146: result = pr.hasChanged() ? BASIC_TERM_FACTORY.createTerm(
147: target.op(), pr.getSimplifiedSubterms(), pr
148: .getBoundVariables(), target.javaBlock())
149: : target;
150: } else {
151: result = target;
152: }
153:
154: result = (updates[0] != null ? UpdateSimplifierTermFactory.DEFAULT
155: .createUpdateTerm(updates[0].getAllAssignmentPairs(),
156: result)
157: : result);
158: logExit(result);
159: return result;
160: }
161:
162: /**
163: * @param update
164: * @return
165: */
166: private Update[] sequentializeUpdate(Update update,
167: NRFunctionWithExplicitDependencies nr) {
168:
169: final ArrayOfAssignmentPair pairs = update
170: .getAllAssignmentPairs();
171:
172: final Location[] nrLocs = new Location[nr.dependencies().size()];
173: nr.dependencies().arraycopy(0, nrLocs, 0, nrLocs.length);
174:
175: HashSet nrDependencies = new HashSet();
176: nrDependencies.addAll(Arrays.asList(nrLocs));
177:
178: ListOfAssignmentPair leftUpdate = SLListOfAssignmentPair.EMPTY_LIST;
179: ListOfAssignmentPair rightUpdate = SLListOfAssignmentPair.EMPTY_LIST;
180: // collect all assignment pairs with a location occuring in the
181: // dependency list
182: // as top operator on the left hand side
183: for (int i = 0; i < pairs.size(); i++) {
184: final AssignmentPair pair = pairs.getAssignmentPair(i);
185: Location pairLoc = pair.location();
186: if (pairLoc instanceof AttributeOp) {
187: pairLoc = (Location) ((AttributeOp) pairLoc)
188: .attribute();
189: }
190: if (nrDependencies.contains(pairLoc)
191: || pair.nontrivialGuard()
192: || pair.boundVars().size() > 0
193: || nrDependencies.contains(pair.value().op())) {
194: leftUpdate = leftUpdate.append(pair);
195: } else {
196: final Term[] locs = pair.locationSubs();
197: Term value = pair.value();
198: for (int j = 0, sz = locs.length; j < sz; j++) {
199: ReplacementResult res = replace(locs[j],
200: nrDependencies);
201: if (res.hasChanged()) {
202: locs[j] = res.getTerm();
203: leftUpdate.append(res.getAssignmentPairs());
204: }
205: }
206: ReplacementResult res = replace(value, nrDependencies);
207: if (res.hasChanged()) {
208: value = res.getTerm();
209: leftUpdate.append(res.getAssignmentPairs());
210: }
211: rightUpdate = rightUpdate
212: .append(new AssignmentPairImpl(pair.location(),
213: locs, value));
214:
215: }
216: }
217:
218: final Update[] updates = new Update[] {
219: leftUpdate.isEmpty() ? null : Update
220: .createUpdate(leftUpdate.toArray()),
221: rightUpdate.isEmpty() ? null : Update
222: .createUpdate(rightUpdate.toArray()) };
223:
224: return updates;
225: }
226:
227: private ReplacementResult replace(Term t, HashSet deps) {
228: ReplacementResult result = new ReplacementResult();
229:
230: result.setReplacementResultTerm(replaceOccurences(t, deps,
231: result));
232:
233: return result;
234: }
235:
236: /**
237: * it is assumed that t contains no variable binding terms TODO: full
238: * support of quantified variables
239: */
240: private Term replaceOccurences(Term t, HashSet deps,
241: ReplacementResult res) {
242: if (t.op() instanceof IUpdateOperator || deps.contains(t.op())) {
243: return getReplacement(t, res);
244: } else {
245: Term result = t;
246: final Term[] newSubs = new Term[t.arity()];
247: final ArrayOfQuantifiableVariable[] quantifiedVars = new ArrayOfQuantifiableVariable[t
248: .arity()];
249: boolean changed = false;
250: for (int i = 0; i < t.arity(); i++) {
251: newSubs[i] = replaceOccurences(t.sub(i), deps, res);
252: if (newSubs[i] != t.sub(i)) {
253: changed = true;
254: }
255: quantifiedVars[i] = t.varsBoundHere(i);
256: }
257: return changed ? BASIC_TERM_FACTORY.createTerm(t.op(),
258: newSubs, quantifiedVars, t.javaBlock()) : result;
259: }
260: }
261:
262: /**
263: * @param s
264: * @return
265: */
266: private static long COUNTER = 0;
267:
268: private Term getReplacement(Term s, ReplacementResult res) {
269: // TODO register new variables at namespace; use variablenameproposer;
270: // get KeYJavaType
271: final LocationVariable replacementVar = new LocationVariable(
272: new ProgramElementName("#pv" + COUNTER++), s.sort());
273: res.addAssignmentPair(replacementVar, s);
274: return BASIC_TERM_FACTORY.createVariableTerm(replacementVar);
275: }
276:
277: /**
278: * as currently a {@link NRFunctionWithExplicitDependencies}is not a
279: * location and can therefore not appear on the left hand side of an update
280: * this method must not be called. If this changes in future (e.g. the
281: * attribute operator becomes a subclass of this kind of operator) the
282: * method has to be implemented.
283: */
284: public Term matchingCondition(Update update, Term target,
285: Services services) {
286: Debug
287: .fail("matchingCondition(...) must not be called for target "
288: + target);
289: return null;
290: }
291:
292: }
|