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.rule.metaconstruct;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.declaration.LocalVariableDeclaration;
015: import de.uka.ilkd.key.java.declaration.VariableSpecification;
016: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
017: import de.uka.ilkd.key.java.expression.operator.Equals;
018: import de.uka.ilkd.key.java.expression.operator.LogicalAnd;
019: import de.uka.ilkd.key.java.expression.operator.NotEquals;
020: import de.uka.ilkd.key.java.reference.ExecutionContext;
021: import de.uka.ilkd.key.java.reference.TypeRef;
022: import de.uka.ilkd.key.java.statement.*;
023: import de.uka.ilkd.key.logic.ProgramElementName;
024: import de.uka.ilkd.key.logic.VariableNamer;
025: import de.uka.ilkd.key.logic.op.LocationVariable;
026: import de.uka.ilkd.key.logic.op.ProgramSV;
027: import de.uka.ilkd.key.logic.op.ProgramVariable;
028: import de.uka.ilkd.key.logic.op.SchemaVariable;
029: import de.uka.ilkd.key.rule.inst.SVInstantiations;
030: import de.uka.ilkd.key.util.ExtList;
031:
032: /** This class is used to perform program transformations needed
033: * for the symbolic execution of a switch-case statement.
034: */
035: public class SwitchToIf extends ProgramMetaConstruct {
036:
037: public static int labelCount = 0;
038: private boolean noNewBreak = true;
039:
040: /** creates a switch-to-if ProgramMetaConstruct
041: * @param switch the Statement contained by the meta construct
042: */
043: public SwitchToIf(SchemaVariable _switch) {
044: super ("switch-to-if", (ProgramSV) _switch);
045: }
046:
047: /** performs the program transformation needed for symbolic
048: * program transformation
049: * @return the transformated program
050: */
051: public ProgramElement symbolicExecution(ProgramElement pe,
052: Services services, SVInstantiations insts) {
053: Switch sw = (Switch) pe;
054: int i = 0;
055: ExtList extL = new ExtList();
056: StatementBlock result;
057: Expression defCond = null;
058: Label l = new ProgramElementName("_l" + (labelCount++));
059: Break newBreak = new Break(l);
060:
061: VariableNamer varNamer = services.getVariableNamer();
062: ProgramElementName name = varNamer
063: .getTemporaryNameProposal("_var");
064:
065: Statement[] ifs = new Statement[sw.getBranchCount()];
066: final ExecutionContext ec = insts.getExecutionContext();
067: ProgramVariable exV = new LocationVariable(name, sw
068: .getExpression().getKeYJavaType(services, ec));
069: VariableSpecification exVSpec = new VariableSpecification(exV,
070: sw.getExpression().getKeYJavaType(services, ec));
071: Statement s = new LocalVariableDeclaration(new TypeRef(sw
072: .getExpression().getKeYJavaType(services, ec)), exVSpec);
073: result = new StatementBlock(new ArrayOfStatement(s));
074: result = insertStatementInBlock(result,
075: new Statement[] { new CopyAssignment(exV, sw
076: .getExpression()) });
077: extL.add(exV);
078: sw = changeBreaks(sw, newBreak);
079: while (i < sw.getBranchCount()) {
080: if (sw.getBranchAt(i) instanceof Case) {
081: extL.add(((Case) sw.getBranchAt(i)).getExpression());
082: ifs[i] = new If(new Equals(extL), new Then(
083: collectStatements(sw, i)));
084: extL.remove(((Case) sw.getBranchAt(i)).getExpression());
085: } else {
086: for (int j = 0; j < sw.getBranchCount(); j++) {
087: if (sw.getBranchAt(j) instanceof Case) {
088: extL.add(((Case) sw.getBranchAt(j))
089: .getExpression());
090: if (defCond != null) {
091: defCond = new LogicalAnd(defCond,
092: new NotEquals(extL));
093: } else {
094: defCond = new NotEquals(extL);
095: }
096: extL.remove(((Case) sw.getBranchAt(j))
097: .getExpression());
098: }
099: }
100: ifs[i] = new If(defCond, new Then(collectStatements(sw,
101: i)));
102: }
103: i++;
104: }
105: result = insertStatementInBlock(result, ifs);
106: if (noNewBreak) {
107: return result;
108: } else {
109: return new LabeledStatement(l, result);
110: }
111: }
112:
113: /** inserts the given statements at the end of the block
114: * @param b the Statementblock where to insert
115: * @param stmnt array of Statement those have to be inserted
116: */
117: private StatementBlock insertStatementInBlock(StatementBlock b,
118: Statement[] stmnt) {
119:
120: Statement[] block = new Statement[b.getStatementCount()
121: + stmnt.length];
122: for (int j = 0; j < b.getStatementCount(); j++) {
123: block[j] = b.getStatementAt(j);
124: }
125: for (int i = 0; i < stmnt.length; i++) {
126: block[i + b.getStatementCount()] = stmnt[i];
127: }
128: return new StatementBlock(new ArrayOfStatement(block));
129: }
130:
131: /**
132: * Replaces all breaks in <code>sw</code>, whose target is sw, with <code>b</code>
133: */
134: private Switch changeBreaks(Switch sw, Break b) {
135: int n = sw.getBranchCount();
136: Branch[] branches = new Branch[n];
137: for (int i = 0; i < n; i++) {
138: branches[i] = (Branch) recChangeBreaks(sw.getBranchAt(i), b);
139: }
140: return new Switch(sw.getExpression(), branches);
141: }
142:
143: private ProgramElement recChangeBreaks(ProgramElement p, Break b) {
144: if (p == null)
145: return null;
146: if (p instanceof Break && ((Break) p).getLabel() == null) {
147: noNewBreak = false;
148: return b;
149: }
150: if (p instanceof Branch) {
151: Statement[] s = new Statement[((Branch) p)
152: .getStatementCount()];
153: for (int i = 0; i < ((Branch) p).getStatementCount(); i++) {
154: s[i] = (Statement) recChangeBreaks(((Branch) p)
155: .getStatementAt(i), b);
156: }
157: if (p instanceof Case)
158: return new Case(((Case) p).getExpression(), s);
159: if (p instanceof Default)
160: return new Default(s);
161: if (p instanceof Catch)
162: return new Catch(((Catch) p).getParameterDeclaration(),
163: new StatementBlock(new ArrayOfStatement(s)));
164: if (p instanceof Finally)
165: return new Finally(new StatementBlock(
166: new ArrayOfStatement(s)));
167: if (p instanceof Then)
168: return new Then(new StatementBlock(
169: new ArrayOfStatement(s)));
170: if (p instanceof Else)
171: return new Else(new StatementBlock(
172: new ArrayOfStatement(s)));
173: }
174: if (p instanceof If) {
175: return new If(((If) p).getExpression(),
176: (Then) recChangeBreaks(((If) p).getThen(), b),
177: (Else) recChangeBreaks(((If) p).getElse(), b));
178: }
179: if (p instanceof StatementBlock) {
180: Statement[] s = new Statement[((StatementBlock) p)
181: .getStatementCount()];
182: for (int i = 0; i < ((StatementBlock) p)
183: .getStatementCount(); i++) {
184: s[i] = (Statement) recChangeBreaks(((StatementBlock) p)
185: .getStatementAt(i), b);
186: }
187: return new StatementBlock(new ArrayOfStatement(s));
188: }
189: if (p instanceof Try) {
190: int n = ((Try) p).getBranchCount();
191: Branch[] branches = new Branch[n];
192: for (int i = 0; i < n; i++) {
193: branches[i] = (Branch) recChangeBreaks(((Try) p)
194: .getBranchAt(i), b);
195: }
196: return new Try((StatementBlock) recChangeBreaks(((Try) p)
197: .getBody(), b), branches);
198: }
199: return p;
200: }
201:
202: /**
203: * Collects the Statements in a switch statement from branch <code>count</code>
204: * downward.
205: * @param s the switch statement.
206: * @param count the branch where the collecting of statements starts.
207: */
208: private StatementBlock collectStatements(Switch s, int count) {
209: int n = 0;
210: int k = 0;
211: Statement[] stats;
212: for (int i = count; i < s.getBranchCount(); i++) {
213: n += s.getBranchAt(i).getStatementCount();
214: }
215: stats = new Statement[n];
216: for (int i = count; i < s.getBranchCount(); i++) {
217: for (int j = 0; j < s.getBranchAt(i).getStatementCount(); j++) {
218: stats[k] = s.getBranchAt(i).getStatementAt(j);
219: k++;
220: }
221: }
222: return new StatementBlock(new ArrayOfStatement(stats));
223: }
224:
225: }
|