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.java.visitor;
011:
012: import java.util.ArrayList;
013: import java.util.HashMap;
014: import java.util.Map;
015:
016: import de.uka.ilkd.key.java.ProgramElement;
017: import de.uka.ilkd.key.java.annotation.Annotation;
018: import de.uka.ilkd.key.java.annotation.LoopInvariantAnnotation;
019: import de.uka.ilkd.key.java.declaration.ArrayOfVariableSpecification;
020: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
021: import de.uka.ilkd.key.logic.*;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.util.Debug;
024: import de.uka.ilkd.key.util.ExtList;
025:
026: /**
027: * Walks through a java AST in depth-left-first-order. This visitor
028: * replaces a number of program variables by others or new ones.
029: */
030: public class ProgVarReplaceVisitor extends CreatingASTVisitor {
031:
032: private ProgramElement result = null;
033:
034: // indicates if ALL program variables are to be replace by new
035: // variables with the same name
036: protected boolean replaceallbynew = true;
037:
038: /**
039: * stores the program variables to be replaced as keys and the new
040: * program variables as values
041: */
042: protected Map replaceMap;
043:
044: /**
045: * creates a visitor that replaces the program variables in the given
046: * statement by new ones with the same name
047: * @param st the statement where the prog vars are replaced
048: * @param oldPVs the program variables that are replaced
049: */
050: public ProgVarReplaceVisitor(ProgramElement st,
051: ProgramVariable[] oldPVs) {
052: super (st, true);
053: replaceMap = new HashMap();
054: for (int i = 0; i < oldPVs.length; i++) {
055: replaceMap.put(oldPVs[i], copy(oldPVs[i]));
056: }
057: }
058:
059: /**
060: * creates a visitor that replaces the program variables in the given
061: * statement by new ones with the same name
062: * @param st the statement where the prog vars are replaced
063: * @param map the HashMap with the replacements
064: */
065: public ProgVarReplaceVisitor(ProgramElement st, Map map) {
066: super (st, true);
067: replaceMap = map;
068: }
069:
070: /**
071: * creates a visitor that replaces the program variables in the given
072: * statement
073: * @param st the statement where the prog vars are replaced
074: * @param map the HashMap with the replacements
075: * @param replaceall decides if all variables are to be replaced
076: */
077: public ProgVarReplaceVisitor(ProgramElement st, Map map,
078: boolean replaceall) {
079: this (st, map);
080: replaceallbynew = replaceall;
081: }
082:
083: /**
084: * creates a visitor that replaces the program variables in the given
085: * statement by new ones with the same name
086: * @param st the statement where the prog vars are replaced
087: */
088: public ProgVarReplaceVisitor(ProgramElement st) {
089: this (st, new HashMap());
090: }
091:
092: //%%% HACK: there should be a central facility for introducing new program
093: // variables; this method is also used in <code>MethodCall</code> to
094: // create copies of parameter variables
095: public static ProgramVariable copy(ProgramVariable pv) {
096: return copy(pv, "");
097: }
098:
099: //%%% HACK: there should be a central facility for introducing new program
100: // variables; this method is also used in <code>MethodCall</code> to
101: // create copies of parameter variables
102: public static ProgramVariable copy(ProgramVariable pv,
103: String postFix) {
104: ProgramElementName name = pv.getProgramElementName();
105: return new LocationVariable(VariableNamer.parseName(name
106: .toString()
107: + postFix, name.getCreationInfo()), pv.getKeYJavaType());
108: }
109:
110: protected void walk(ProgramElement node) {
111: if (node instanceof LocalVariableDeclaration && replaceallbynew) {
112: LocalVariableDeclaration vd = (LocalVariableDeclaration) node;
113: ArrayOfVariableSpecification vspecs = vd
114: .getVariableSpecifications();
115: for (int i = 0; i < vspecs.size(); i++) {
116: ProgramVariable pv = (ProgramVariable) vspecs
117: .getVariableSpecification(i)
118: .getProgramVariable();
119: if (!replaceMap.containsKey(pv)) {
120: replaceMap.put(pv, copy(pv));
121: }
122: }
123: }
124: super .walk(node);
125: }
126:
127: /** the action that is performed just before leaving the node the
128: * last time
129: */
130: protected void doAction(ProgramElement node) {
131: node.visit(this );
132: }
133:
134: /** starts the walker*/
135: public void start() {
136: stack.push(new ExtList());
137: walk(root());
138: ExtList el = stack.peek();
139: int i = 0;
140: while (!(el.get(i) instanceof ProgramElement)) {
141: i++;
142: }
143: result = (ProgramElement) stack.peek().get(i);
144: }
145:
146: public ProgramElement result() {
147: return result;
148: }
149:
150: public void performActionOnProgramVariable(ProgramVariable pv) {
151: ProgramElement newPV = (ProgramElement) replaceMap.get(pv);
152: if (newPV != null) {
153: addChild(newPV);
154: changed();
155: } else {
156: doDefaultAction(pv);
157: }
158: }
159:
160: /**
161: * Performs action on the annotations <code>a</code>.
162: */
163: protected void performActionOnAnnotationArray(Annotation[] a) {
164: for (int i = 0; i < a.length; i++) {
165: if (a[i] instanceof LoopInvariantAnnotation) {
166: LoopInvariantAnnotation lia = (LoopInvariantAnnotation) a[i];
167: Term newInvariant = lia.invariant() == null ? null
168: : replaceVariablesInTerm(lia.invariant());
169: SetOfLocationDescriptor newAssignable = lia
170: .assignable() == null ? null
171: : replaceVariablesInLocs(lia.assignable());
172: ArrayOfTerm newOlds = lia.olds() == null ? null
173: : replaceVariablesInTerms(lia.olds());
174: Term newVariant = lia.variant() == null ? null
175: : replaceVariablesInTerm(lia.variant());
176: Term newPost = lia.variant() == null ? null
177: : replaceVariablesInTerm(lia.post());
178: ProgramVariable newSelfVar = (ProgramVariable) replaceMap
179: .get(lia.getSelfVar());
180: if (newSelfVar == null) {
181: newSelfVar = lia.getSelfVar();
182: }
183: LoopInvariantAnnotation newLia = new LoopInvariantAnnotation(
184: newInvariant, newAssignable, newOlds,
185: newVariant, newPost, newSelfVar);
186:
187: addToTopOfStack(newLia);
188: } else {
189: addToTopOfStack(a[i]);
190: }
191: }
192: if (a.length > 0) {
193: changed();
194: }
195: }
196:
197: private Term replaceVariablesInTerm(Term t) {
198: if (t == null)
199: return null;
200: if (t.op() instanceof ProgramVariable) {
201: if (replaceMap.containsKey(t.op())) {
202: Object o = replaceMap.get(t.op());
203: if (o instanceof ProgramVariable) {
204: return TermFactory.DEFAULT
205: .createVariableTerm((ProgramVariable) replaceMap
206: .get(t.op()));
207: } else {
208: return TermFactory.DEFAULT
209: .createVariableTerm((SchemaVariable) replaceMap
210: .get(t.op()));
211: }
212: } else {
213: return t;
214: }
215: } else {
216: Term subTerms[] = new Term[t.arity()];
217: ArrayList vars = new ArrayList();
218: for (int i = 0; i < t.arity(); i++) {
219: ArrayOfQuantifiableVariable vbh = t.varsBoundHere(i);
220: for (int j = 0; j < vbh.size(); j++) {
221: vars.add(vbh.getQuantifiableVariable(j));
222: }
223: subTerms[i] = replaceVariablesInTerm(t.sub(i));
224: }
225: Operator op;
226: if (t.op() instanceof IUpdateOperator) {
227: IUpdateOperator uo = (IUpdateOperator) t.op();
228: ListOfLocation locs = SLListOfLocation.EMPTY_LIST;
229: for (int i = 0; i < uo.locationCount(); i++) {
230: if (replaceMap.containsKey(uo.location(i))) {
231: locs = locs.append((Location) replaceMap.get(uo
232: .location(i)));
233: } else {
234: locs = locs.append(uo.location(i));
235: }
236: }
237: op = uo.replaceLocations(locs.toArray());
238: } else {
239: op = t.op();
240: }
241: QuantifiableVariable v1[] = new QuantifiableVariable[0];
242: v1 = (QuantifiableVariable[]) (vars.toArray(v1));
243: JavaBlock jb = t.javaBlock();
244: return TermFactory.DEFAULT.createTerm(op, subTerms, v1, jb);
245: }
246: }
247:
248: private SetOfLocationDescriptor replaceVariablesInLocs(
249: SetOfLocationDescriptor locs) {
250: SetOfLocationDescriptor res = SetAsListOfLocationDescriptor.EMPTY_SET;
251:
252: IteratorOfLocationDescriptor it = locs.iterator();
253: while (it.hasNext()) {
254: LocationDescriptor loc = it.next();
255: LocationDescriptor newLoc;
256:
257: if (loc instanceof BasicLocationDescriptor) {
258: BasicLocationDescriptor bloc = (BasicLocationDescriptor) loc;
259: Term newFormula = replaceVariablesInTerm(bloc
260: .getFormula());
261: Term newLocTerm = replaceVariablesInTerm(bloc
262: .getLocTerm());
263: newLoc = new BasicLocationDescriptor(newFormula,
264: newLocTerm);
265: } else {
266: Debug
267: .assertTrue(loc instanceof EverythingLocationDescriptor);
268: newLoc = loc;
269: }
270:
271: res = res.add(newLoc);
272: }
273:
274: return res;
275: }
276:
277: private ArrayOfTerm replaceVariablesInTerms(ArrayOfTerm terms) {
278: Term[] res = new Term[terms.size()];
279:
280: for (int i = 0; i < res.length; i++) {
281: res[i] = replaceVariablesInTerm(terms.getTerm(i));
282: }
283:
284: return new ArrayOfTerm(res);
285: }
286:
287: public void performActionOnLocationVariable(LocationVariable x) {
288: performActionOnProgramVariable(x);
289: }
290:
291: public void performActionOnProgramConstant(ProgramConstant x) {
292: performActionOnProgramVariable(x);
293: }
294: }
|