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.soundness;
012:
013: import de.uka.ilkd.key.java.*;
014: import de.uka.ilkd.key.java.abstraction.ArrayOfKeYJavaType;
015: import de.uka.ilkd.key.java.expression.literal.IntLiteral;
016: import de.uka.ilkd.key.java.expression.operator.Equals;
017: import de.uka.ilkd.key.java.statement.Else;
018: import de.uka.ilkd.key.java.statement.If;
019: import de.uka.ilkd.key.java.statement.Then;
020: import de.uka.ilkd.key.logic.JavaBlock;
021: import de.uka.ilkd.key.logic.ProgramElementName;
022: import de.uka.ilkd.key.logic.op.*;
023: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
024: import de.uka.ilkd.key.util.Debug;
025: import de.uka.ilkd.key.util.ExtList;
026:
027: /**
028: * Factory to create skolem symbols for statements
029: */
030: public class StatementSkolemSymbolFactory extends
031: SkolemSymbolTacletFactory {
032:
033: public StatementSkolemSymbolFactory(Services p_services) {
034: super (p_services);
035: }
036:
037: /**
038: * Create a skolem symbol for statements
039: * @param p_name name of the symbol
040: * @param p_influencingPVs program variable arguments the symbol is to
041: * be given. A selector variable of type int is added as the last argument
042: * implicitly
043: * @param jumpTable the jump table that symbol should have
044: */
045: public ProgramSVProxy createStatementSymbol(
046: ProgramElementName p_name,
047: ListOfIProgramVariable p_influencingPVs,
048: ArrayOfStatement p_jumpTable) {
049: return createStatementSymbolWithoutSelector(p_name,
050: p_influencingPVs.append(createSelectorVariable()),
051: p_jumpTable);
052: }
053:
054: /**
055: * Like <code>createStatementSymbol</code>, but assume that the last
056: * program variable argument already is a valid selector variable
057: * (of type int)
058: */
059: public ProgramSVProxy createStatementSymbolWithoutSelector(
060: ProgramElementName p_name,
061: ListOfIProgramVariable p_influencingPVs,
062: ArrayOfStatement p_jumpTable) {
063: Debug.assertTrue(checkSelectorVariable(p_influencingPVs),
064: "Last program variable argument is not an "
065: + "admissible selector variable");
066:
067: final ProgramSVProxy proxy = createStatementSymbol(p_name,
068: getProgramVariableTypes(p_influencingPVs),
069: getProgramVariablesAsArray(p_influencingPVs),
070: p_jumpTable);
071: createDecompositionTaclets(proxy);
072:
073: return proxy;
074: }
075:
076: private ProgramSVProxy createStatementSymbol(
077: ProgramElementName p_name,
078: ArrayOfKeYJavaType p_influencingPVTypes,
079: ArrayOfIProgramVariable p_influencingPVs,
080: ArrayOfStatement p_jumpTable) {
081:
082: final ProgramSVSkolemStatement sk = new ProgramSVSkolemStatement(
083: p_name, p_influencingPVTypes, p_jumpTable.size());
084:
085: final ProgramSVProxy pr = new ProgramSVProxy(sk,
086: p_influencingPVs, p_jumpTable);
087:
088: return pr;
089:
090: }
091:
092: private void createDecompositionTaclets(ProgramSVProxy p) {
093: ExtList ifJumpTable = new ExtList();
094: ExtList findProxy = new ExtList();
095: ExtList rwProxy = new ExtList();
096: createSepSymbol(p, findProxy, rwProxy, ifJumpTable);
097: JavaBlock findJB = JavaBlock
098: .createJavaBlock(new ContextStatementBlock(findProxy));
099: JavaBlock sepJB = JavaBlock.createJavaBlock(new StatementBlock(
100: rwProxy));
101: JavaBlock replaceJB = JavaBlock
102: .createJavaBlock(new ContextStatementBlock(ifJumpTable));
103:
104: createTaclets(findJB, replaceJB, sepJB, ""
105: + p.op().getProgramElementName() + "_sep");
106: }
107:
108: /**
109: * Create an additional skolem symbol that can be used for the program
110: * decomposition rule. Also create the statements necessary for the rule
111: * @param p the primary symbol
112: * @param p_findProxy list to which the statement is added on which the
113: * decomposition rule applies
114: * @param p_rwProxy list to which the statement is added that replaces the
115: * primary statement when applying the decomposition rule
116: * @param p_ifJumpTable list to which the if-cascade is added which is
117: * inserted by the decomposition rule
118: */
119: private void createSepSymbol(ProgramSVProxy p, ExtList p_findProxy,
120: ExtList p_rwProxy, ExtList p_jumpCascade) {
121: ProgramElementName name = new ProgramElementName(""
122: + p.op().getProgramElementName() + "_sep");
123:
124: ArrayOfIProgramVariable pvs = createSVsForInfluencingPVs(p);
125:
126: final IProgramVariable sel = pvs
127: .getIProgramVariable(pvs.size() - 1);
128:
129: Statement[] findJT = createJumpCascade(p.getJumpTable().size(),
130: p_jumpCascade, sel);
131:
132: p_findProxy.add(new ProgramSVProxy(p.op(), pvs,
133: new ArrayOfStatement(findJT)));
134: p_rwProxy.add(createStatementSymbol(name, p.op()
135: .getInfluencingPVTypes(), pvs, new ArrayOfStatement(
136: new Statement[0])));
137: }
138:
139: /**
140: * Create an if-cascade that dispatches the different abrupt exists given
141: * by the jump table of a skolem symbol occurrence. The jump statements
142: * are represented by schema variables for statements
143: * @param p_size the size of the if-cascade, i.e. the number of schema
144: * variables that should be inserted
145: * @param p_jumpCascade list to which the result is to be added
146: * @param p_sel the program variable that selects the chosen exit
147: * @return an array that holds the schema variables used to construct the
148: * if-cascade
149: */
150: private Statement[] createJumpCascade(int p_size,
151: ExtList p_jumpCascade, IProgramVariable p_sel) {
152: int i = p_size;
153: final Statement[] findJT = new Statement[p_size];
154: If cascade = null;
155:
156: while (i-- != 0)
157: cascade = addBranch(p_sel, findJT, i, cascade);
158:
159: if (cascade != null)
160: p_jumpCascade.add(cascade);
161:
162: return findJT;
163: }
164:
165: private If addBranch(IProgramVariable p_sel, Statement[] findJT,
166: int branchNum, If oldTop) {
167: final SchemaVariable stmtSV = SchemaVariableFactory
168: .createProgramSV(createUniquePEName("stmt"),
169: ProgramSVSort.STATEMENT, false);
170: findJT[branchNum] = (Statement) stmtSV;
171:
172: final Then thenLeg = new Then((Statement) stmtSV);
173:
174: final ExtList compOps = new ExtList();
175: compOps.add(p_sel);
176: compOps.add(new IntLiteral(branchNum));
177: final If newTop = new If(new Equals(compOps), thenLeg);
178:
179: if (oldTop != null)
180: newTop.addBranch(new Else(oldTop));
181:
182: return newTop;
183: }
184:
185: private boolean checkSelectorVariable(
186: ListOfIProgramVariable p_influencingPVs) {
187: while (p_influencingPVs.size() > 1)
188: p_influencingPVs = p_influencingPVs.tail();
189: return p_influencingPVs.size() != 0
190: && p_influencingPVs.head().getKeYJavaType() == getSelectorType();
191: }
192:
193: }
|