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:
011: package de.uka.ilkd.key.proof;
012:
013: import java.util.Map;
014:
015: import de.uka.ilkd.key.java.ProgramElement;
016: import de.uka.ilkd.key.java.Statement;
017: import de.uka.ilkd.key.java.StatementBlock;
018: import de.uka.ilkd.key.java.declaration.ArrayOfVariableSpecification;
019: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
020: import de.uka.ilkd.key.java.visitor.ProgVarReplaceVisitor;
021: import de.uka.ilkd.key.logic.JavaBlock;
022: import de.uka.ilkd.key.logic.ProgramElementName;
023: import de.uka.ilkd.key.logic.Term;
024: import de.uka.ilkd.key.logic.TermFactory;
025: import de.uka.ilkd.key.logic.op.*;
026: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
027:
028: public class TermSVReplacer {
029:
030: Map schemaVariables;
031: SetOfProgramVariable locallyDeclaredVars = SetAsListOfProgramVariable.EMPTY_SET;
032: SetOfProgramVariable pvsInProg = SetAsListOfProgramVariable.EMPTY_SET;
033: Term from, to;
034:
035: TermFactory fact;
036:
037: public TermSVReplacer(Map map) {
038: fact = TermFactory.DEFAULT;
039: schemaVariables = map;
040: }
041:
042: private void createSV(ProgramVariable pv) {
043:
044: SortedSchemaVariable ssv = (SortedSchemaVariable) SchemaVariableFactory
045: .createProgramSV(new ProgramElementName("#" + pv),
046: ProgramSVSort.VARIABLE, false);
047: schemaVariables.put(pv, ssv);
048: }
049:
050: public SetOfProgramVariable getLocallyDeclaredVars() {
051: return locallyDeclaredVars;
052: }
053:
054: public SetOfProgramVariable getPVsInProg() {
055: return pvsInProg;
056: }
057:
058: public Term inst(Term t) {
059: Term result = null;
060: if (t.op() instanceof ProgramVariable
061: && !((ProgramVariable) t.op()).isMember()) {
062: result = t;
063: if (!schemaVariables.containsKey(t.op())) {
064: createSV((ProgramVariable) t.op());
065: }
066: result = TermFactory.DEFAULT
067: .createVariableTerm((SchemaVariable) schemaVariables
068: .get(t.op()));
069:
070: } else {
071: Term subTerms[] = new Term[t.arity()];
072: ArrayOfQuantifiableVariable[] quantVars = new ArrayOfQuantifiableVariable[t
073: .arity()];
074: for (int i = 0; i < t.arity(); i++) {
075: quantVars[i] = t.varsBoundHere(i);
076: subTerms[i] = inst(t.sub(i));
077: }
078: Operator op;
079: if (t.op() instanceof IUpdateOperator) {
080: IUpdateOperator uo = (IUpdateOperator) t.op();
081: ListOfLocation locs = SLListOfLocation.EMPTY_LIST;
082: for (int i = 0; i < uo.locationCount(); i++) {
083: if (uo.location(i) instanceof ProgramVariable
084: && !((ProgramVariable) uo.location(i))
085: .isMember()) {
086: if (!schemaVariables
087: .containsKey(uo.location(i))) {
088: createSV((ProgramVariable) uo.location(i));
089: }
090: locs = locs.append((Location) schemaVariables
091: .get(uo.location(i)));
092: } else {
093: locs = locs.append(uo.location(i));
094: }
095: }
096: op = uo.replaceLocations(locs.toArray());
097: } else {
098: op = t.op();
099: }
100: JavaBlock jb = t.javaBlock();
101: if (!jb.isEmpty()) {
102: jb = JavaBlock
103: .createJavaBlock((StatementBlock) inst((Statement) t
104: .javaBlock().program()));
105: if (jb.equals(t.javaBlock()))
106: jb = t.javaBlock();
107: }
108: result = fact.createTerm(op, subTerms, quantVars, jb);
109: }
110: return result;
111: }
112:
113: public Statement inst(Statement sta) {
114: ProgVarReplaceVisitor pvrepl = new ProgVarReplaceVisitor(sta,
115: schemaVariables) {
116:
117: protected void walk(ProgramElement node) {
118: if (node instanceof LocalVariableDeclaration
119: && replaceallbynew) {
120: LocalVariableDeclaration vd = (LocalVariableDeclaration) node;
121: ArrayOfVariableSpecification vspecs = vd
122: .getVariableSpecifications();
123: for (int i = 0; i < vspecs.size(); i++) {
124: ProgramVariable pv = (ProgramVariable) vspecs
125: .getVariableSpecification(i)
126: .getProgramVariable();
127: if (!replaceMap.containsKey(pv)) {
128: createSV(pv);
129: }
130: locallyDeclaredVars = locallyDeclaredVars
131: .add(pv);
132: }
133: }
134: super .walk(node);
135: }
136:
137: public void performActionOnProgramVariable(
138: ProgramVariable pv) {
139: if (!pv.isMember() && !replaceMap.containsKey(pv)) {
140: createSV(pv);
141: }
142: pvsInProg = pvsInProg.add(pv);
143: super .performActionOnProgramVariable(pv);
144: }
145: };
146:
147: pvrepl.start();
148: return (Statement) pvrepl.result();
149: }
150:
151: }
|