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.Services;
014: import de.uka.ilkd.key.java.abstraction.IteratorOfKeYJavaType;
015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
016: import de.uka.ilkd.key.logic.ProgramElementName;
017: import de.uka.ilkd.key.logic.op.*;
018: import de.uka.ilkd.key.rule.inst.ProgramSkolemInstantiation;
019: import de.uka.ilkd.key.rule.inst.SVInstantiations;
020: import de.uka.ilkd.key.util.ExtList;
021:
022: /**
023: * Choose types for the untyped schema variables for PV and
024: * expressions
025: */
026: public class TypeInfoBuilder extends AbstractSkolemBuilder {
027:
028: private final RawProgramVariablePrefixes rpvp;
029: private ListOfSkolemSet results = SLListOfSkolemSet.EMPTY_LIST;
030:
031: public TypeInfoBuilder(SkolemSet p_oriSkolemSet,
032: RawProgramVariablePrefixes p_rpvp, Services p_services) {
033: super (p_oriSkolemSet, p_services);
034: rpvp = p_rpvp;
035: }
036:
037: public IteratorOfSkolemSet build() {
038: build(0, getOriginalSkolemSet().getInstantiations(),
039: getOriginalSkolemSet().getSVTypeInfos());
040:
041: return handleSubsumption(results.iterator());
042: }
043:
044: private void addResult(SkolemSet p) {
045: results = results.prepend(p);
046: }
047:
048: private void build(int p_variableNumber,
049: SVInstantiations p_currentSVI, SVTypeInfos p_currentSVTI) {
050: if (p_variableNumber == getSVPartitioning().size()) {
051: addResult(getOriginalSkolemSet().setSVTypeInfos(
052: p_currentSVTI));
053: return;
054: }
055:
056: PVCandidate[] pvs = createPVCandidates(p_variableNumber,
057: p_currentSVI, p_currentSVTI);
058:
059: int i;
060: for (i = 0; i != pvs.length; ++i) {
061: build(p_variableNumber + 1, pvs[i].svi, pvs[i].svti);
062: }
063: }
064:
065: private PVCandidate[] createPVCandidates(int p_variableNumber,
066: SVInstantiations p_currentSVI, SVTypeInfos p_currentSVTI) {
067: final ExtList res = new ExtList();
068: final ListOfSchemaVariable svs = getSVPartitioning()
069: .getPartition(p_variableNumber);
070: final KeYJavaType type = getPartitionType(p_variableNumber);
071:
072: if (type == null) {
073: if (getSVPartitioning().isNative(p_variableNumber))
074: createNativePVCandidates(svs, p_currentSVI,
075: p_currentSVTI, res);
076: else
077: createNewPVCandidates(svs, p_currentSVI, p_currentSVTI,
078: res);
079: } else
080: createNewPVCandidate(svs, type, p_currentSVI,
081: p_currentSVTI, res,
082: ProgramSkolemInstantiation.NEW_BOUND_VARIABLE);
083:
084: return (PVCandidate[]) res.collect(PVCandidate.class);
085: }
086:
087: private void createNativePVCandidates(ListOfSchemaVariable p_svs,
088: SVInstantiations p_currentSVI, SVTypeInfos p_currentSVTI,
089: ExtList p_res) {
090: final IteratorOfIProgramVariable nativeIt = rpvp
091: .getFreeProgramVariables().iterator();
092:
093: while (nativeIt.hasNext()) {
094: final IProgramVariable pv = nativeIt.next();
095:
096: final PVCandidate pvc = isValidInstantiation(p_currentSVI,
097: p_currentSVTI, p_svs, pv,
098: ProgramSkolemInstantiation.OCCURRING_VARIABLE);
099: if (pvc != null)
100: p_res.add(pvc);
101: }
102: }
103:
104: private void createNewPVCandidates(ListOfSchemaVariable p_svs,
105: SVInstantiations p_currentSVI, SVTypeInfos p_currentSVTI,
106: ExtList p_res) {
107: final IteratorOfKeYJavaType typeIt = createTypeCandidates();
108:
109: while (typeIt.hasNext())
110: createNewPVCandidate(p_svs, typeIt.next(), p_currentSVI,
111: p_currentSVTI, p_res,
112: ProgramSkolemInstantiation.NEW_FREE_VARIABLE);
113: }
114:
115: private void createNewPVCandidate(ListOfSchemaVariable p_svs,
116: KeYJavaType p_type, SVInstantiations p_currentSVI,
117: SVTypeInfos p_currentSVTI, ExtList p_res,
118: int p_instantiationType) {
119: final IProgramVariable pv = new LocationVariable(
120: new ProgramElementName("x"), p_type);
121:
122: final PVCandidate pvc = isValidInstantiation(p_currentSVI,
123: p_currentSVTI, p_svs, pv, p_instantiationType);
124:
125: if (pvc != null)
126: p_res.add(pvc);
127: }
128:
129: private PVCandidate isValidInstantiation(
130: SVInstantiations p_currentSVI, SVTypeInfos p_currentSVTI,
131: ListOfSchemaVariable p_svs, IProgramVariable p_pv,
132: int p_instantiationType) {
133:
134: if (!StaticCheckerSVI.isValidType(getOriginalFormula(),
135: p_currentSVI, p_svs, p_pv, getServices()))
136: return null;
137:
138: final SVInstantiations svi = StaticCheckerSVI.addInstantiation(
139: p_currentSVI, p_svs, p_pv, p_instantiationType);
140:
141: if (svi == null)
142: return null;
143:
144: final IteratorOfSchemaVariable it = p_svs.iterator();
145: SVTypeInfos svti = p_currentSVTI;
146: while (it.hasNext())
147: svti = svti.addInfo(new SVTypeInfo(it.next(), p_pv
148: .getKeYJavaType()));
149:
150: return new PVCandidate(p_pv, svi, svti);
151: }
152:
153: /**
154: * Remove from the given set of skolem sets those which are
155: * subsumed by others, return the remaining ones
156: */
157: private IteratorOfSkolemSet handleSubsumption(
158: IteratorOfSkolemSet p_it) {
159: ListOfSkolemSet res = SLListOfSkolemSet.EMPTY_LIST;
160: IteratorOfSkolemSet compareIt;
161: SkolemSet ss;
162: SkolemSet compareSS;
163:
164: mainloop: while (p_it.hasNext()) {
165: ss = p_it.next();
166: compareIt = res.iterator();
167: res = SLListOfSkolemSet.EMPTY_LIST;
168:
169: while (compareIt.hasNext()) {
170: compareSS = compareIt.next();
171:
172: switch (compare(ss, compareSS)) {
173: case -1:
174: // ss may be removed
175: res = res.prepend(compareSS);
176: while (compareIt.hasNext())
177: res = res.prepend(compareIt.next());
178: continue mainloop;
179:
180: case 0:
181: res = res.prepend(compareSS);
182: break;
183:
184: case 1:
185: // compareSS may be removed
186: break;
187: }
188: }
189:
190: res = res.prepend(ss);
191: }
192:
193: return res.iterator();
194: }
195:
196: /**
197: * @return <code>0</code> if <code>p_a</code> and <code>p_b</code>
198: * are not in relation, <code>-1</code> if <code>p_a</code> is
199: * subsumed by <code>p_b</code>, <code>1</code> if
200: * <code>p_a</code> subsumes <code>p_b</code>
201: */
202: private int compare(SkolemSet p_a, SkolemSet p_b) {
203: int res = 0;
204:
205: int i = getSVPartitioning().size();
206: final KeYJavaType object = getObjectKeYJavaType();
207:
208: while (i-- != 0) {
209: KeYJavaType akjt = getSVPartitioning().getType(i,
210: p_a.getSVTypeInfos());
211: KeYJavaType bkjt = getSVPartitioning().getType(i,
212: p_b.getSVTypeInfos());
213:
214: if (getSVPartitioning().isNative(i)) {
215: // for native partitions, only instantiation with the
216: // same type is allowed for subsumption
217: if (akjt == bkjt)
218: continue;
219: return 0;
220: }
221:
222: switch (res) {
223: case -1:
224: if (bkjt == object || akjt == bkjt)
225: break;
226: return 0;
227:
228: case 0:
229: if (akjt == object) {
230: if (bkjt != object)
231: res = 1;
232: } else {
233: if (bkjt == object)
234: res = -1;
235: else if (akjt != bkjt)
236: return 0;
237: }
238: break;
239:
240: case 1:
241: if (akjt == object || akjt == bkjt)
242: break;
243: return 0;
244: }
245: }
246:
247: return res;
248: }
249:
250: private static class PVCandidate {
251: public final IProgramVariable pv;
252: public final SVInstantiations svi;
253: public final SVTypeInfos svti;
254:
255: public PVCandidate(IProgramVariable p_pv,
256: SVInstantiations p_svi, SVTypeInfos p_svti) {
257: pv = p_pv;
258: svi = p_svi;
259: svti = p_svti;
260: }
261: }
262:
263: }
|