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.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.logic.op.*;
015: import de.uka.ilkd.key.logic.sort.ProgramSVSort;
016: import de.uka.ilkd.key.util.ExtList;
017:
018: /**
019: * Class holding a complete partitioning of all PV- and expression
020: * schema variables in disjoint, non-empty classes (expression SV are
021: * treated like PVSV at this point to make type handling easier). This
022: * is used to cover all possible combinations of variables
023: * instantiated equally. This class is immutable.
024: */
025: public class SVPartitioning {
026: // Arrays of the partitions this object holds
027: private final SVPartition[] boundSVs; // Bound PVSV
028: private final SVPartition[] freeSVs; // Free PVSV
029: private final SVPartition[] expressionSVs; // Expression SV
030:
031: public static SVPartitioning[] findPartitionings(
032: ListOfSchemaVariable p_freeSVs,
033: ListOfSchemaVariable p_boundSVs,
034: ListOfSchemaVariable p_expressionSVs) {
035: return new SVPartitioner(p_freeSVs, p_boundSVs, p_expressionSVs)
036: .findPartitionings();
037: }
038:
039: private SVPartitioning(SVPartition[] p_freeSVs,
040: SVPartition[] p_boundSVs, SVPartition[] p_expressionSVs) {
041: boundSVs = p_boundSVs;
042: freeSVs = p_freeSVs;
043: expressionSVs = p_expressionSVs;
044: }
045:
046: SVPartitioning(SVPartition[] p_boundSVs,
047: SVPartition[] p_expressionSVs) {
048: this (null, cloneArray(p_boundSVs), cloneArray(p_expressionSVs));
049: }
050:
051: SVPartitioning setFreeSVPartitioning(SVPartition[] p_freeSVs) {
052: return new SVPartitioning(cloneArray(p_freeSVs), boundSVs,
053: expressionSVs);
054: }
055:
056: /**
057: * @return the number of partitions
058: */
059: public int size() {
060: return boundSVs.length + expressionSVs.length + freeSVs.length;
061: }
062:
063: /**
064: * @return true iff partition <code>p</code> does only exist of
065: * expression schema variables
066: */
067: public boolean isExpressionSV(int p) {
068: SchemaVariable sv = getPartition(p).head();
069: return sv.isProgramSV()
070: && ((SortedSchemaVariable) sv).sort() == ProgramSVSort.EXPRESSION;
071: }
072:
073: public boolean isNative(int p) {
074: return getPartitionHelp(p).isNative();
075: }
076:
077: /**
078: * @return the type of an arbitrary element of partition
079: * <code>p</code> for which the type is known; <code>null</code>
080: * if the type is unknown for all elements of partition
081: * <code>p</code>
082: */
083: public KeYJavaType getType(int p, SVTypeInfos p_svTypeInfos) {
084: return getType(getPartition(p), p_svTypeInfos);
085: }
086:
087: private KeYJavaType getType(ListOfSchemaVariable p_svs,
088: SVTypeInfos p_svTypeInfos) {
089: IteratorOfSchemaVariable it = p_svs.iterator();
090: SVTypeInfo res;
091: while (it.hasNext()) {
092: res = p_svTypeInfos.getInfo(it.next());
093: if (res != null)
094: return res.getType();
095: }
096: return null;
097: }
098:
099: /**
100: * @return partition <code>p</code> as a list
101: */
102: public ListOfSchemaVariable getPartition(int p) {
103: return getPartitionHelp(p).getVariables();
104: }
105:
106: private SVPartition getPartitionHelp(int p) {
107: if (p < boundSVs.length)
108: return boundSVs[p];
109: p -= boundSVs.length;
110: if (p < freeSVs.length)
111: return freeSVs[p];
112: p -= freeSVs.length;
113: return expressionSVs[p];
114: }
115:
116: private static SVPartition[] cloneArray(SVPartition[] p) {
117: SVPartition[] res = new SVPartition[p.length];
118: System.arraycopy(p, 0, res, 0, p.length);
119: return res;
120: }
121: }
122:
123: class SVPartition {
124: private final ListOfSchemaVariable variables;
125: private final boolean nativePV;
126:
127: SVPartition(ListOfSchemaVariable p_variables, boolean p_nativePV) {
128: variables = p_variables;
129: nativePV = p_nativePV;
130: }
131:
132: public ListOfSchemaVariable getVariables() {
133: return variables;
134: }
135:
136: public boolean isNative() {
137: return nativePV;
138: }
139: }
140:
141: /**
142: * <p>Construct all possible partitionings for a given set of schema
143: * variables, and all possibilities to instantiate each partition
144: * either with a new or a native program variable.</p>
145: *
146: * <p>Possible optimization: Test whether native program variables
147: * exist at all.</p>
148: */
149: class SVPartitioner {
150:
151: private final SchemaVariable[] freeSVs;
152: private final SVPartitioning emptyPart;
153: private final ExtList res = new ExtList();
154:
155: // Array that contains one entry for each element of
156: // <code>freeSVs</code>, and that tells to which partition each
157: // schema variable belongs
158: private final int[] partTable;
159:
160: SVPartitioner(ListOfSchemaVariable p_freeSVs,
161: ListOfSchemaVariable p_boundSVs,
162: ListOfSchemaVariable p_expressionSVs) {
163: freeSVs = toArray(p_freeSVs);
164: emptyPart = new SVPartitioning(
165: toSingletonPartitionArray(p_boundSVs),
166: toSingletonPartitionArray(p_expressionSVs));
167: partTable = new int[freeSVs.length];
168:
169: // initially <code>partTable</code> does only contain
170: // <code>0</code>
171: }
172:
173: SVPartitioning[] findPartitionings() {
174: findPartitioningsHelp(1);
175:
176: return (SVPartitioning[]) res.collect(SVPartitioning.class);
177: }
178:
179: /**
180: * Recursive method; each call creates a further partition of
181: * schema variables in all possible ways
182: */
183: private void findPartitioningsHelp(int p_depth) {
184: if (init(p_depth)) {
185: do {
186: findPartitioningsHelp(p_depth + 1);
187: } while (step(p_depth));
188: } else {
189: // all schema variables belong to exactly one partition
190: createPartitioning(p_depth - 1);
191: }
192: }
193:
194: private void createPartitioning(int p_partCount) {
195: SVPartition[] partitions = new SVPartition[p_partCount];
196: createPartitioningHelp(p_partCount, partitions);
197: }
198:
199: private void createPartitioningHelp(int p_code,
200: SVPartition[] p_partitions) {
201: if (p_code == 0) {
202: res.add(emptyPart.setFreeSVPartitioning(p_partitions));
203: return;
204: }
205:
206: final int index = p_code - 1;
207: final ListOfSchemaVariable variables = collectVariables(p_code);
208:
209: // For each partition the chosen program variable
210: // can be native or new
211:
212: p_partitions[index] = new SVPartition(variables, false);
213: createPartitioningHelp(index, p_partitions);
214:
215: p_partitions[index] = new SVPartition(variables, true);
216: createPartitioningHelp(index, p_partitions);
217: }
218:
219: private ListOfSchemaVariable collectVariables(int p_code) {
220: ListOfSchemaVariable variables = SLListOfSchemaVariable.EMPTY_LIST;
221:
222: for (int j = 0; j != partTable.length; ++j) {
223: if (partTable[j] == p_code)
224: variables = variables.prepend(freeSVs[j]);
225: }
226:
227: return variables;
228: }
229:
230: /**
231: * Set the first entry of <code>partTable</code> with value
232: * <code>0</code> to <code>p_code</code>
233: * @return true iff a zero-entry did exist
234: */
235: private boolean init(int p_code) {
236: int i;
237: for (i = 0; i != partTable.length; ++i) {
238: if (partTable[i] == 0) {
239: partTable[i] = p_code;
240: return true;
241: }
242: }
243:
244: return false;
245: }
246:
247: /**
248: * Iterate through all possible configurations of
249: * <code>partTable</code> that can be reached by assigning the
250: * values <code>0</code> and <code>p_code</code>; thereby entries
251: * having other values than <code>0</code> or <code>p_code</code>,
252: * as well as the first entry with value <code>p_code</code> are
253: * not modified
254: * @return false iff no further configuration exists, in this case
255: * <code>0</code> is assigned to all entries with value
256: * <code>p_code</code>
257: */
258: private boolean step(int p_code) {
259: int i;
260: boolean delay = true;
261: for (i = 0; i != partTable.length; ++i) {
262: if (partTable[i] == p_code) {
263: if (delay)
264: delay = false;
265: else
266: partTable[i] = 0;
267: } else if (partTable[i] == 0) {
268: partTable[i] = p_code;
269: return true;
270: }
271: }
272:
273: for (i = 0; i != partTable.length; ++i) {
274: if (partTable[i] == p_code)
275: partTable[i] = 0;
276: }
277:
278: return false;
279: }
280:
281: private SchemaVariable[] toArray(ListOfSchemaVariable p_list) {
282: SchemaVariable[] result = new SchemaVariable[p_list.size()];
283:
284: IteratorOfSchemaVariable it = p_list.iterator();
285: int i = 0;
286: while (it.hasNext())
287: result[i++] = it.next();
288:
289: return result;
290: }
291:
292: private static SVPartition[] toSingletonPartitionArray(
293: ListOfSchemaVariable p_svs) {
294:
295: SVPartition[] result = new SVPartition[p_svs.size()];
296:
297: IteratorOfSchemaVariable it = p_svs.iterator();
298: int i = 0;
299: while (it.hasNext()) {
300: final ListOfSchemaVariable singletonList = SLListOfSchemaVariable.EMPTY_LIST
301: .prepend(it.next());
302: result[i++] = new SVPartition(singletonList, false);
303: }
304:
305: return result;
306: }
307:
308: }
|