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: /**
012: * visitor for <t> execPostOrder </t> of
013: * {@link de.uka.ilkd.key.logic.Term}. Called with that method
014: * on a term, the visitor builds a new term replacing all AccessOp-s with
015: * ShadowAccessOp-s
016: */package de.uka.ilkd.key.logic;
017:
018: import java.util.Stack;
019:
020: import de.uka.ilkd.key.java.Services;
021: import de.uka.ilkd.key.java.recoderext.JVMIsTransientMethodBuilder;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.util.Debug;
024:
025: public class ShadowReplaceVisitor extends Visitor {
026:
027: private Term computedResult = null;
028: // private TypeConverter typeConverter = null;
029:
030: /**
031: * the stack contains the subterms that will be added in the next step of
032: * execPostOrder in Term in order to build the new term. A boolean value
033: * between or under the subterms on the stack indicate that a term using
034: * these subterms should build a new term instead of using the old one,
035: * because one of its subterms has been built, too.
036: */
037: private Stack subStack; //of Term (and Boolean)
038: private TermFactory tf = TermFactory.DEFAULT;
039: private Boolean newMarker = Boolean.TRUE;
040:
041: final Term transactionCounter;
042:
043: final static ProgramElementName transactionCounterName = new ProgramElementName(
044: JVMIsTransientMethodBuilder.IMPLICIT_TRANSACTION_COUNTER,
045: "de.uka.ilkd.key.javacard.KeYJCSystem");
046:
047: /**
048: * @param forceSVInst iff true instantiate uninstantiated SVs by
049: * creating new metavariables or new bound logicvariables
050: */
051: public ShadowReplaceVisitor(Services services) {
052: transactionCounter = tf.createVariableTerm(services
053: .getJavaInfo().getAttribute(
054: transactionCounterName.getProgramName(),
055: transactionCounterName.getQualifier()));
056: Debug.assertTrue(transactionCounter != null);
057: subStack = new Stack(); // of Term
058: }
059:
060: private Term[] neededSubs(int n) {
061: boolean newTerm = false;
062: Term[] result = new Term[n];
063: for (int i = n - 1; i >= 0; i--) {
064: Object top = subStack.pop();
065: if (top == newMarker) {
066: newTerm = true;
067: top = subStack.pop();
068: }
069: result[i] = (Term) top;
070: }
071: if (newTerm
072: && (subStack.empty() || subStack.peek() != newMarker)) {
073: subStack.push(newMarker);
074: }
075: return result;
076: }
077:
078: public void visit(Term visited) {
079: Operator op = visited.op();
080: boolean changed = false;
081:
082: if (op instanceof ShadowedOperator) {
083: Debug
084: .fail("You should not put #shadowed meta operator around already shadowed object access expressions!");
085: }
086:
087: if (op instanceof ArrayOp) {
088: op = ShadowArrayOp.getShadowArrayOp(((ArrayOp) op)
089: .arraySort());
090: changed = true;
091: } else if (op instanceof AttributeOp) {
092: op = ShadowAttributeOp
093: .getShadowAttributeOp(((AttributeOp) op)
094: .attribute());
095: changed = true;
096: }
097:
098: if (changed
099: && (subStack.empty() || subStack.peek() != newMarker)) {
100: subStack.push(newMarker);
101: }
102:
103: ArrayOfQuantifiableVariable boundVars = ((visited
104: .varsBoundHere(0).size() == 0) ? visited
105: .varsBoundHere(1) : visited.varsBoundHere(0));
106:
107: Term[] neededsubs = neededSubs(visited.arity());
108:
109: if (changed
110: || (!subStack.empty() && subStack.peek() == newMarker)) {
111:
112: Operator newOp;
113: if (changed) {
114: newOp = op;
115:
116: // FIXME - there is a problem with this:
117: // Java Card specs say, that after abortTransaction
118: // the references to all objects that were initialised during
119: // the (aborted) transaction are set to null.
120: // This is not solvable (I think) with the current
121: // shadowing mechanism
122: if (visited.op() instanceof AttributeOp) {
123: if (((AttributeOp) op).attribute().name()
124: .toString().startsWith("<")) {
125: // No change, it's a special attribute
126: // System.out.println(neededsubs[1].op().name());
127: newOp = visited.op();
128: }
129: }
130: // prepare extra subterm
131: if (newOp != visited.op()) {
132: final Term[] newsubs = new Term[neededsubs.length + 1];
133: System.arraycopy(neededsubs, 0, newsubs, 0,
134: neededsubs.length);
135: newsubs[neededsubs.length] = transactionCounter;
136: neededsubs = newsubs;
137: }
138:
139: } else {
140: newOp = visited.op();
141: }
142: pushNew(tf.createTerm(newOp, neededsubs, boundVars, visited
143: .javaBlock()));
144: } else {
145: subStack.push(visited);
146: }
147:
148: }
149:
150: private void pushNew(Object t) {
151: if (subStack.empty() || subStack.peek() != newMarker) {
152: subStack.push(newMarker);
153: }
154: subStack.push(t);
155: }
156:
157: /**
158: * delivers the new built term
159: */
160: public Term getTerm() {
161: if (computedResult == null) {
162: Object o = null;
163: do {
164: o = subStack.pop();
165: } while (o == newMarker);
166: Term t = (Term) o;
167: computedResult = t;
168: }
169: return computedResult;
170: }
171: }
|