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.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.java.expression.operator.CopyAssignment;
017: import de.uka.ilkd.key.logic.JavaBlock;
018: import de.uka.ilkd.key.logic.ProgramElementName;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
021: import de.uka.ilkd.key.util.ExtList;
022:
023: public class ExpressionSkolemSymbolFactory extends
024: SkolemSymbolTacletFactory {
025:
026: public ExpressionSkolemSymbolFactory(Services p_services) {
027: super (p_services);
028: }
029:
030: /**
031: * Create a skolem symbol for expressions
032: * @param p_name name of the symbol
033: * @param p_type result type the symbol shall have
034: * @param p_influencingPVs program variable arguments the symbol is to
035: * be given. A result variable of type <code>p_type</code> and a
036: * selector variable of type int are added as the last two arguments
037: * implicitly
038: * @param jumpTable the jump table that symbol should have
039: */
040: public ProgramSVProxy createExpressionSymbol(
041: ProgramElementName p_name, KeYJavaType p_type,
042: ListOfIProgramVariable p_influencingPVs,
043: ArrayOfStatement p_jumpTable) {
044:
045: final ListOfIProgramVariable influencingPVs = p_influencingPVs
046: .append(createResultVariable(p_type)).append(
047: createSelectorVariable());
048:
049: final ProgramSVProxy pr = createExpressionSymbol(p_name,
050: p_type, getProgramVariableTypes(influencingPVs),
051: getProgramVariablesAsArray(influencingPVs), p_jumpTable);
052: createExpressionTaclets(pr);
053:
054: return pr;
055: }
056:
057: private ProgramSVProxy createExpressionSymbol(
058: ProgramElementName p_name, KeYJavaType p_type,
059: ArrayOfKeYJavaType p_influencingPVTypes,
060: ArrayOfIProgramVariable p_influencingPVs,
061: ArrayOfStatement p_jumpTable) {
062:
063: final ProgramSVSkolemExpression sk = new ProgramSVSkolemExpression(
064: p_name, p_type, p_influencingPVTypes, p_jumpTable
065: .size());
066:
067: final ProgramSVProxy pr = new ProgramSVProxy(sk,
068: p_influencingPVs, p_jumpTable);
069:
070: return pr;
071:
072: }
073:
074: private void createExpressionTaclets(ProgramSVProxy p) {
075: ExtList findProxy = new ExtList();
076: ExtList rwProxy = new ExtList();
077: createNormSymbols(p, findProxy, rwProxy);
078:
079: JavaBlock findJB = JavaBlock
080: .createJavaBlock(new ContextStatementBlock(findProxy));
081: JavaBlock replaceJB = JavaBlock
082: .createJavaBlock(new ContextStatementBlock(rwProxy));
083:
084: createTaclets(findJB, replaceJB, ""
085: + p.op().getProgramElementName() + "_expr");
086: }
087:
088: /**
089: * Create a statement symbol that is used for the expression
090: * normalization rule: An expression symbol is replaced with a statement
091: * symbol and an assignment
092: * @param p the primary symbol
093: * @param p_findStatement list to which the statement is added on which the
094: * normalization rule applies (assignment of the expression symbol to a
095: * program variable)
096: * @param p_rwStatement list to which the statements are added that replace
097: * the primary statement when applying the normalization rule
098: */
099: private void createNormSymbols(ProgramSVProxy p,
100: ExtList p_findStatement, ExtList p_rwStatement) {
101: SchemaVariable lhs = SchemaVariableFactory
102: .createProgramSV(createUniquePEName("pv"),
103: ProgramSVSort.VARIABLE, false);
104:
105: ArrayOfIProgramVariable pvs = createSVsForInfluencingPVs(p);
106: IProgramVariable retVal = pvs
107: .getIProgramVariable(pvs.size() - 2);
108:
109: ArrayOfStatement findJT = new ArrayOfStatement(
110: createSVsForJumpTable(p));
111:
112: ProgramSVProxy findProxy = new ProgramSVProxy(p.op(), pvs,
113: findJT);
114:
115: ProgramSVProxy rwProxy = createNormSymbol(p, pvs, findJT);
116:
117: p_findStatement.add(new CopyAssignment((Expression) lhs,
118: findProxy));
119:
120: p_rwStatement.add(rwProxy);
121: p_rwStatement.add(new CopyAssignment((Expression) lhs,
122: (Expression) retVal));
123: }
124:
125: private Statement[] createSVsForJumpTable(ProgramSVProxy p) {
126: final Statement[] findJT = new Statement[p.getJumpTable()
127: .size()];
128: int i = p.getJumpTable().size();
129:
130: while (i-- != 0)
131: findJT[i] = (Statement) SchemaVariableFactory
132: .createProgramSV(createUniquePEName("stmt"),
133: ProgramSVSort.STATEMENT, false);
134:
135: return findJT;
136: }
137:
138: private ProgramSVProxy createNormSymbol(ProgramSVProxy p,
139: ArrayOfIProgramVariable p_influencingPVs,
140: ArrayOfStatement p_jumpTable) {
141: final String baseName = "" + p.op().getProgramElementName()
142: + "_expr";
143:
144: final ListOfIProgramVariable pvArgs = getProgramVariablesAsList(p
145: .getInfluencingPVs());
146:
147: final ProgramSVProxy statement = createStatementSymbol(
148: baseName, pvArgs, p.getJumpTable());
149:
150: // Replace arguments and jump table with the given schema variables
151: final ArrayOfIProgramVariable svArgs = getProgramVariablesAsArray(getProgramVariablesAsList(p_influencingPVs));
152:
153: return new ProgramSVProxy(statement.op(), svArgs, p_jumpTable);
154: }
155:
156: /**
157: * Use the statement symbol factory to create the necessary statement symbol
158: * for the normalization rule
159: */
160: private ProgramSVProxy createStatementSymbol(String p_baseName,
161: ListOfIProgramVariable p_influencingPVs,
162: ArrayOfStatement p_jumpTable) {
163: final StatementSkolemSymbolFactory f = new StatementSkolemSymbolFactory(
164: getServices());
165:
166: final ProgramSVProxy proxy = f
167: .createStatementSymbolWithoutSelector(
168: createUniquePEName(p_baseName),
169: p_influencingPVs, p_jumpTable);
170:
171: addVocabulary(f);
172:
173: return proxy;
174: }
175:
176: private ProgramVariable createResultVariable(KeYJavaType retType) {
177: final ProgramVariable retVal = new LocationVariable(
178: createUniquePEName("ret"), retType);
179: addVariable(retVal);
180: return retVal;
181: }
182:
183: }
|