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: // This file is part of KeY - Integrated Deductive Software Design
010: // Copyright (C) 2001-2004 Universitaet Karlsruhe, Germany
011: // Universitaet Koblenz-Landau, Germany
012: // Chalmers University of Technology, Sweden
013: //
014: // The KeY system is protected by the GNU General Public License.
015: // See LICENSE.TXT for details.
016: //
017: //
018:
019: package de.uka.ilkd.key.proof;
020:
021: import java.util.Map;
022:
023: import de.uka.ilkd.key.java.ArrayOfProgramElement;
024: import de.uka.ilkd.key.java.ProgramElement;
025: import de.uka.ilkd.key.java.Statement;
026: import de.uka.ilkd.key.java.StatementBlock;
027: import de.uka.ilkd.key.java.visitor.ProgVarReplaceVisitor;
028: import de.uka.ilkd.key.logic.*;
029: import de.uka.ilkd.key.logic.op.*;
030: import de.uka.ilkd.key.rule.*;
031: import de.uka.ilkd.key.rule.inst.*;
032: import de.uka.ilkd.key.util.Debug;
033:
034: /**
035: * Replaces program variables.
036: */
037: public class ProgVarReplacer {
038:
039: /**
040: * map specifying the replacements to be done
041: */
042: protected final Map map;
043:
044: /**
045: * creates a ProgVarReplacer that replaces program variables as specified
046: * by the map parameter
047: */
048: public ProgVarReplacer(Map m) {
049: map = m;
050: }
051:
052: /**
053: * merges "next" into "base"
054: * precondition:
055: * "next" is the result of replacing in "base" the formula at position
056: * "idx" by calling Semisequent.replace()
057: * (this implies that "next" contains exactly one removed and one added
058: * formula)
059: */
060: private void mergeSemiCIs(SemisequentChangeInfo base,
061: SemisequentChangeInfo next, int idx) {
062: Debug.assertTrue(next.modifiedFormulas().isEmpty());
063:
064: IteratorOfConstrainedFormula remIt = next.removedFormulas()
065: .iterator();
066: Debug.assertTrue(remIt.hasNext());
067: ConstrainedFormula remCf = remIt.next();
068: Debug.assertFalse(remIt.hasNext());
069: base.removedFormula(idx, remCf);
070:
071: IteratorOfConstrainedFormula addIt = next.addedFormulas()
072: .iterator();
073: Debug.assertTrue(addIt.hasNext());
074: ConstrainedFormula addCf = addIt.next();
075: Debug.assertFalse(addIt.hasNext());
076: base.addedFormula(idx, addCf);
077:
078: base.setFormulaList(next.getFormulaList());
079: base.setSemisequent(next.semisequent());
080: }
081:
082: /**
083: * replaces in a goal
084: */
085: public void replace(Goal goal) {
086: //globals
087: SetOfProgramVariable set = replace(goal.getGlobalProgVars());
088: goal.setGlobalProgVars(set);
089:
090: //taclet apps
091: replace(goal.ruleAppIndex().tacletIndex());
092:
093: //sequent
094: SequentChangeInfo sci = replace(goal.sequent());
095: goal.setSequent(sci);
096: }
097:
098: /**
099: * replaces in a set
100: */
101: public SetOfProgramVariable replace(SetOfProgramVariable vars) {
102: SetOfProgramVariable result = vars;
103:
104: IteratorOfProgramVariable it = vars.iterator();
105: while (it.hasNext()) {
106: ProgramVariable var = it.next();
107: ProgramVariable newVar = (ProgramVariable) map.get(var);
108: if (newVar != null) {
109: result = result.remove(var);
110: result = result.add(newVar);
111: }
112: }
113:
114: return result;
115: }
116:
117: /**
118: * replaces in the partially instantiated apps of a taclet index
119: */
120: public void replace(TacletIndex tacletIndex) {
121: ListOfNoPosTacletApp noPosTacletApps = tacletIndex
122: .getPartialInstantiatedApps();
123: SetOfNoPosTacletApp appsToBeRemoved, appsToBeAdded;
124: appsToBeRemoved = SetAsListOfNoPosTacletApp.EMPTY_SET;
125: appsToBeAdded = SetAsListOfNoPosTacletApp.EMPTY_SET;
126:
127: IteratorOfNoPosTacletApp it = noPosTacletApps.iterator();
128: while (it.hasNext()) {
129: NoPosTacletApp noPosTacletApp = it.next();
130: SVInstantiations insts = noPosTacletApp.instantiations();
131:
132: SVInstantiations newInsts = replace(insts);
133:
134: if (newInsts != insts) {
135: NoPosTacletApp newNoPosTacletApp = NoPosTacletApp
136: .createNoPosTacletApp(noPosTacletApp.taclet(),
137: newInsts, noPosTacletApp.constraint(),
138: noPosTacletApp.newMetavariables(),
139: noPosTacletApp
140: .ifFormulaInstantiations());
141: appsToBeRemoved = appsToBeRemoved.add(noPosTacletApp);
142: appsToBeAdded = appsToBeAdded.add(newNoPosTacletApp);
143: }
144: }
145:
146: tacletIndex.removeTaclets(appsToBeRemoved);
147: tacletIndex.addTaclets(appsToBeAdded);
148: }
149:
150: /**
151: * replaces in an SVInstantiations
152: */
153: public SVInstantiations replace(SVInstantiations insts) {
154: SVInstantiations result = insts;
155:
156: IteratorOfEntryOfSchemaVariableAndInstantiationEntry it;
157: it = insts.pairIterator();
158: while (it.hasNext()) {
159: EntryOfSchemaVariableAndInstantiationEntry e = it.next();
160: SchemaVariable sv = e.key();
161: InstantiationEntry ie = e.value();
162: Object inst = ie.getInstantiation();
163:
164: if (ie instanceof ContextInstantiationEntry) {
165: ProgramElement pe = (ProgramElement) inst;
166: ProgramElement newPe = replace(pe);
167: if (newPe != pe) {
168: ContextInstantiationEntry cie = (ContextInstantiationEntry) ie;
169: result = result.replace(cie.prefix(), cie.suffix(),
170: cie.activeStatementContext(), newPe);
171: }
172: } else if (ie instanceof OperatorInstantiation) {
173: /*nothing to be done (currently)*/
174: } else if (ie instanceof ProgramInstantiation) {
175: ProgramElement pe = (ProgramElement) inst;
176: ProgramElement newPe = replace(pe);
177: if (newPe != pe) {
178: result = result.replace(sv, newPe);
179: }
180: } else if (ie instanceof ProgramListInstantiation) {
181: ArrayOfProgramElement a = (ArrayOfProgramElement) inst;
182: int size = a.size();
183: ProgramElement[] array = new ProgramElement[size];
184:
185: boolean changedSomething = false;
186: for (int i = 0; i < size; i++) {
187: ProgramElement pe = a.getProgramElement(i);
188: array[i] = replace(pe);
189: if (array[i] != pe) {
190: changedSomething = true;
191: }
192: }
193:
194: if (changedSomething) {
195: ArrayOfProgramElement newA = new ArrayOfProgramElement(
196: array);
197: result = result.replace(sv, newA);
198: }
199: } else if (ie instanceof TermInstantiation) {
200: Term t = (Term) inst;
201: Term newT = replace(t);
202: if (newT != t) {
203: result = result.replace(sv, newT);
204: }
205: } else {
206: Debug.fail("unexpected subtype of InstantiationEntry");
207: }
208: }
209:
210: return result;
211: }
212:
213: /**
214: * replaces in a sequent
215: */
216: public SequentChangeInfo replace(Sequent s) {
217: SemisequentChangeInfo anteCI = replace(s.antecedent());
218: SemisequentChangeInfo succCI = replace(s.succedent());
219:
220: Semisequent newAntecedent = anteCI.semisequent();
221: Semisequent newSuccedent = succCI.semisequent();
222:
223: Sequent newSequent = Sequent.createSequent(newAntecedent,
224: newSuccedent);
225:
226: SequentChangeInfo result = SequentChangeInfo
227: .createSequentChangeInfo(anteCI, succCI, newSequent, s);
228: return result;
229: }
230:
231: /**
232: * replaces in a semisequent
233: */
234: public SemisequentChangeInfo replace(Semisequent s) {
235: SemisequentChangeInfo result = new SemisequentChangeInfo();
236: result.setFormulaList(s.toList());
237: result.setSemisequent(s);
238:
239: final IteratorOfConstrainedFormula it = s.iterator();
240:
241: for (int formulaNumber = 0; it.hasNext(); formulaNumber++) {
242: final ConstrainedFormula oldcf = it.next();
243: final ConstrainedFormula newcf = replace(oldcf);
244:
245: if (newcf != oldcf) {
246: SemisequentChangeInfo semiCI = result.semisequent()
247: .replace(formulaNumber, newcf);
248: mergeSemiCIs(result, semiCI, formulaNumber);
249: }
250: }
251:
252: return result;
253: }
254:
255: /**
256: * replaces in a constrained formula
257: */
258: public ConstrainedFormula replace(ConstrainedFormula cf) {
259: ConstrainedFormula result = cf;
260:
261: final Term newFormula = replace(cf.formula());
262:
263: if (newFormula != cf.formula()) {
264: result = new ConstrainedFormula(newFormula, cf.constraint());
265: }
266: return result;
267: }
268:
269: public Term replaceProgramVariable(Term t) {
270: final ProgramVariable pv = (ProgramVariable) t.op();
271: Object o = map.get(pv);
272: if (o instanceof ProgramVariable) {
273: return TermFactory.DEFAULT
274: .createVariableTerm((ProgramVariable) o);
275: } else if (o instanceof Term) {
276: return (Term) o;
277: }
278: return t;
279: }
280:
281: protected Term replaceQuanUpdateTerm(Term t) {
282: assert t.op() instanceof QuanUpdateOperator;
283:
284: Term result = t;
285: boolean changed = false;
286:
287: final QuanUpdateOperator iuop = (QuanUpdateOperator) t.op();
288:
289: final Term locs[] = new Term[iuop.locationCount()];
290: final Term vals[] = new Term[iuop.locationCount()];
291: final Term guards[] = new Term[iuop.locationCount()];
292: final ArrayOfQuantifiableVariable[] qvars = new ArrayOfQuantifiableVariable[iuop
293: .locationCount()];
294:
295: for (int i = 0; i < iuop.locationCount(); i++) {
296: final Term location = iuop.location(t, i);
297: locs[i] = replace(location);
298: changed = changed || (locs[i] != location);
299: final Term value = iuop.value(t, i);
300: vals[i] = replace(value);
301: changed = changed || vals[i] != value;
302: final Term guard = iuop.guard(t, i);
303: guards[i] = replace(guard);
304: changed = changed || guards[i] != guard;
305: final ArrayOfQuantifiableVariable boundVars = iuop
306: .boundVars(t, i);
307: qvars[i] = boundVars;
308: changed = changed || qvars[i] != boundVars;
309: }
310: final Term target = replace(iuop.target(t));
311: changed = changed || target != iuop.target(t);
312:
313: if (changed) {
314: result = TermFactory.DEFAULT.createQuanUpdateTerm(qvars,
315: guards, locs, vals, target);
316: }
317:
318: return result;
319: }
320:
321: /**
322: * replaces in a term
323: */
324: public Term replace(Term t) {
325: final Operator op = t.op();
326: if (op instanceof QuanUpdateOperator) {
327: return replaceQuanUpdateTerm(t);
328: } else if (op instanceof ProgramVariable) {
329: return replaceProgramVariable(t);
330: } else {
331: return standardReplace(t);
332: }
333: }
334:
335: /**
336: * @param t
337: * @param result
338: * @return
339: */
340: protected Term standardReplace(Term t) {
341: Term result = t;
342:
343: final Term newSubTerms[] = new Term[t.arity()];
344: final ArrayOfQuantifiableVariable[] boundVars = new ArrayOfQuantifiableVariable[t
345: .arity()];
346:
347: boolean changedSubTerm = false;
348:
349: for (int i = 0, ar = t.arity(); i < ar; i++) {
350: final Term subTerm = t.sub(i);
351: newSubTerms[i] = replace(subTerm);
352: if (newSubTerms[i] != subTerm) {
353: changedSubTerm = true;
354: }
355: boundVars[i] = t.varsBoundHere(i);
356: }
357:
358: final JavaBlock jb = t.javaBlock();
359: JavaBlock newJb = jb;
360: if (!jb.isEmpty()) {
361: Statement s = (Statement) jb.program();
362: Statement newS = (Statement) replace(s);
363: if (newS != s) {
364: newJb = JavaBlock
365: .createJavaBlock((StatementBlock) newS);
366: }
367: }
368:
369: if (changedSubTerm || newJb != jb) {
370: result = TermFactory.DEFAULT.createTerm(t.op(),
371: newSubTerms, boundVars, newJb);
372: }
373: return result;
374: }
375:
376: public LocationDescriptor replace(LocationDescriptor loc) {
377: if (loc instanceof BasicLocationDescriptor) {
378: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
379: return new BasicLocationDescriptor(replace(bloc
380: .getFormula()), replace(bloc.getLocTerm()));
381: } else {
382: return loc;
383: }
384: }
385:
386: /**
387: * replaces in a statement
388: */
389: public ProgramElement replace(ProgramElement pe) {
390: ProgVarReplaceVisitor pvrv = new ProgVarReplaceVisitor(pe, map,
391: false);
392: pvrv.start();
393: return pvrv.result();
394: }
395: }
|