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 de.uka.ilkd.key.java.ArrayOfProgramElement;
013: import de.uka.ilkd.key.java.ProgramElement;
014: import de.uka.ilkd.key.java.Services;
015: import de.uka.ilkd.key.java.SourceElement;
016: import de.uka.ilkd.key.logic.ProgramInLogic;
017: import de.uka.ilkd.key.logic.Term;
018: import de.uka.ilkd.key.logic.op.SchemaVariable;
019: import de.uka.ilkd.key.rule.AbstractProgramElement;
020: import de.uka.ilkd.key.rule.inst.SVInstantiations;
021: import de.uka.ilkd.key.rule.metaconstruct.ProgramMetaConstruct;
022: import de.uka.ilkd.key.util.Debug;
023: import de.uka.ilkd.key.util.ExtList;
024:
025: /**
026: * Walks through a java AST in depth-left-fist-order.
027: * This walker is used to transform a program according to the given
028: * SVInstantiations.
029: */
030: public class ProgramReplaceVisitor extends CreatingASTVisitor {
031:
032: private ProgramElement result = null;
033:
034: private Services services;
035: private SVInstantiations svinsts;
036:
037: private boolean allowPartialReplacement;
038:
039: /**
040: * create the ProgramReplaceVisitor
041: * @param root the ProgramElement where to begin
042: */
043: public ProgramReplaceVisitor(ProgramElement root,
044: Services services, SVInstantiations svi,
045: boolean allowPartialReplacement) {
046: super (root, false);
047: this .services = services;
048: svinsts = svi;
049: this .allowPartialReplacement = allowPartialReplacement;
050: }
051:
052: /** the action that is performed just before leaving the node the
053: * last time
054: */
055: protected void doAction(ProgramElement node) {
056: node.visit(this );
057: }
058:
059: /** starts the walker*/
060: public void start() {
061: stack.push(new ExtList());
062: walk(root());
063: final ExtList el = stack.peek();
064: int i = 0;
065: while (!(el.get(i) instanceof ProgramElement)) {
066: i++;
067: }
068: result = (ProgramElement) (stack.peek()).get(i);
069: }
070:
071: public ProgramElement result() {
072: return result;
073: }
074:
075: public String toString() {
076: return stack.peek().toString();
077: }
078:
079: /** the implemented default action is called if a program element is,
080: * and if it has children all its children too are left unchanged
081: */
082: protected void doDefaultAction(SourceElement x) {
083: addChild(x);
084: }
085:
086: public void performActionOnSchemaVariable(SchemaVariable sv) {
087: final Object inst = svinsts.getInstantiation(sv);
088: if (inst instanceof ProgramElement) {
089: Debug.out("ProgramReplace SV:", sv);
090: Debug.out("ProgramReplace:", inst);
091: addChild((ProgramElement) inst);
092: } else if (inst instanceof ArrayOfProgramElement) {
093: addChildren((ArrayOfProgramElement) inst);
094: } else if (inst instanceof Term
095: && ((Term) inst).op() instanceof ProgramInLogic) {
096: addChild(services.getTypeConverter()
097: .convertToProgramElement((Term) inst));
098: } else {
099: if (inst == null && allowPartialReplacement
100: && sv instanceof SourceElement) {
101: doDefaultAction((SourceElement) sv);
102: return;
103: }
104: Debug.fail("programreplacevisitor: Instantiation missing "
105: + "for schema variable ", sv);
106: }
107: changed();
108: }
109:
110: public void performActionOnProgramMetaConstruct(
111: ProgramMetaConstruct x) {
112: ProgramReplaceVisitor trans = new ProgramReplaceVisitor(x
113: .body(), services, svinsts, allowPartialReplacement);
114: trans.start();
115: ProgramElement localresult = trans.result();
116: localresult = x.symbolicExecution(localresult, services,
117: svinsts);
118: addChild(localresult);
119: changed();
120: }
121:
122: public void performActionOnAbstractProgramElement(
123: AbstractProgramElement x) {
124: result = x.getConcreteProgramElement(services);
125: addChild(result);
126: changed();
127: }
128: }
|