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: package de.uka.ilkd.key.unittest;
009:
010: import de.uka.ilkd.key.logic.*;
011: import de.uka.ilkd.key.logic.op.*;
012: import de.uka.ilkd.key.java.*;
013: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
014: import de.uka.ilkd.key.proof.*;
015: import de.uka.ilkd.key.proof.decproc.*;
016: import de.uka.ilkd.key.unittest.simplify.*;
017: import de.uka.ilkd.key.unittest.cogent.*;
018: import java.util.*;
019:
020: public class ModelGenerator {
021:
022: //debug info
023: public static int cached = 0;
024:
025: public static final int COGENT = 0;
026: public static final int SIMPLIFY = 1;
027: public static int decProdForTestGen = COGENT;
028:
029: private ListOfTerm ante, succ;
030: private HashMap term2class;
031: // Maps a location to the set of formulas it occurs in.
032: private HashMap eqvC2constr;
033: private Services serv;
034: private SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
035: private SetOfProgramVariable pvs = SetAsListOfProgramVariable.EMPTY_SET;
036: private Node node;
037: private Constraint userConstraint;
038: private String executionTrace;
039:
040: private Node originalNode;
041:
042: public ModelGenerator(Services serv, Constraint userConstraint,
043: Node node, String executionTrace, Node originalNode) {
044: IteratorOfConstrainedFormula itc = node.sequent().antecedent()
045: .iterator();
046: ante = SLListOfTerm.EMPTY_LIST;
047: while (itc.hasNext()) {
048: ante = ante.append(itc.next().formula());
049: }
050: itc = node.sequent().succedent().iterator();
051: succ = SLListOfTerm.EMPTY_LIST;
052: while (itc.hasNext()) {
053: succ = succ.append(itc.next().formula());
054: }
055: this .node = node;
056: this .originalNode = originalNode;
057: this .userConstraint = userConstraint;
058: this .serv = serv;
059: this .executionTrace = executionTrace;
060: eqvC2constr = new HashMap();
061: createEquivalenceClassesAndConstraints();
062: findBounds();
063: findDisjointClasses();
064: collectProgramVariables();
065: }
066:
067: public static boolean isLocation(Term t, Services serv) {
068: OpCollector oc = new OpCollector();
069: t.execPostOrder(oc);
070: if (oc.contains(Op.NULL)) {
071: return false;
072: }
073: return t.op() instanceof AttributeOp
074: && checkIndices(t, serv)
075: && !((ProgramVariable) ((AttributeOp) t.op())
076: .attribute()).isImplicit()
077: || t.op() instanceof ProgramVariable
078: && !((ProgramVariable) t.op()).isImplicit()
079: || t.op() instanceof ArrayOp && checkIndices(t, serv)
080: || t.op() instanceof RigidFunction && t.arity() == 0
081: && !"#".equals(t.op().name().toString())
082: && !"TRUE".equals(t.op().name().toString())
083: && !"FALSE".equals(t.op().name().toString())
084: && t.op().name().toString().indexOf("undef(") == -1;
085: }
086:
087: /**
088: * Returns the associated ExecutionTrace as a String.
089: */
090: public String getExecutionTrace() {
091: return executionTrace;
092: }
093:
094: /**
095: * Returns true iff no negative array indices are contained in t.
096: */
097: public static boolean checkIndices(Term t, Services serv) {
098: if (t.op() instanceof AttributeOp) {
099: return checkIndices(t.sub(0), serv);
100: }
101: if (t.op() instanceof ArrayOp) {
102: if (t.sub(1).op().name().toString().equals("Z")) {
103: if (AbstractMetaOperator.convertToDecimalString(
104: t.sub(1), serv).startsWith("-")) {
105: return false;
106: }
107: }
108: return checkIndices(t.sub(0), serv);
109: }
110: return true;
111: }
112:
113: /** Ensures the existence of an EquivalenceClass for each location and
114: * logic variable found
115: * in <code>t</code> and updates the mapping from this class to the
116: * formulas it occurs in.
117: */
118: private void collectLocations(Term t) {
119: if (isLocation(t, serv)) {
120: getEqvClass(t);
121: locations = locations.add(t);
122: SetOfTerm constr = (SetOfTerm) eqvC2constr.get(t);
123: if (constr == null) {
124: constr = SetAsListOfTerm.EMPTY_SET;
125: }
126: eqvC2constr.put(t, constr.add(t));
127: }
128: if (!(t.op() instanceof Modality
129: || t.op() instanceof IUpdateOperator || t.op() instanceof Quantifier)) {
130: /* if(t.op() instanceof IUpdateOperator){
131: IUpdateOperator uop = (IUpdateOperator) t.op();
132: for(int i = 0; i<uop.locationCount(); i++){
133: collectLocations(uop.value(t, i));
134: }
135: }*/
136: for (int i = 0; i < t.arity(); i++) {
137: collectLocations(t.sub(i));
138: }
139: }
140: }
141:
142: public static boolean containsImplicitAttr(Term t) {
143: if (t.op() instanceof AttributeOp
144: && ((ProgramVariable) ((AttributeOp) t.op())
145: .attribute()).isImplicit()
146: || t.op() instanceof ProgramVariable
147: && ((ProgramVariable) t.op()).isImplicit()) {
148: return true;
149: }
150: for (int i = 0; i < t.arity(); i++) {
151: if (containsImplicitAttr(t.sub(i))) {
152: return true;
153: }
154: }
155: return false;
156: }
157:
158: /**
159: * Returns the set of locations occuring in node.
160: */
161: public SetOfTerm getLocations() {
162: return locations;
163: }
164:
165: /**
166: * Collects the program variables occuring in node.
167: */
168: public void collectProgramVariables() {
169: IteratorOfTerm it = locations.iterator();
170: while (it.hasNext()) {
171: Term t = it.next();
172: if ((t.op() instanceof ProgramVariable)
173: && !((ProgramVariable) t.op()).isStatic()) {
174: pvs = pvs.add((ProgramVariable) t.op());
175: } else if (t.op() instanceof RigidFunction) {
176: KeYJavaType kjt;
177: if (t.sort().toString().startsWith("jint")
178: || t.sort().toString().startsWith("jshort")
179: || t.sort().toString().startsWith("jbyte")
180: || t.sort().toString().startsWith("jlong")
181: || t.sort().toString().startsWith("jchar")) {
182: kjt = serv.getJavaInfo().getKeYJavaType(
183: t.sort().toString().substring(1));
184: } else {
185: kjt = serv.getJavaInfo().getKeYJavaType(
186: t.sort().toString());
187: }
188: assert kjt != null;
189: pvs = pvs
190: .add(new LocationVariable(
191: new ProgramElementName(t.op().name()
192: .toString()), kjt));
193: }
194: }
195: }
196:
197: public SetOfProgramVariable getProgramVariables() {
198: return pvs;
199: }
200:
201: public HashMap getTerm2Class() {
202: return term2class;
203: }
204:
205: private SetOfTerm getConstraintsForEqvClass(EquivalenceClass ec) {
206: IteratorOfTerm it = ec.getMembers().iterator();
207: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
208: while (it.hasNext()) {
209: SetOfTerm constr = (SetOfTerm) eqvC2constr.get(it.next());
210: if (constr != null) {
211: result = result.union(constr);
212: }
213: }
214: return result;
215: }
216:
217: /**
218: * Creates equivalence classes based on the equality formulas (l=r)
219: * contained in <code>formulas</code>.
220: */
221: private void createEquivalenceClassesAndConstraints() {
222: term2class = new HashMap();
223: IteratorOfTerm it = ante.iterator();
224: while (it.hasNext()) {
225: EquivalenceClass ec = null;
226: Term t = it.next();
227: collectLocations(t);
228: if (t.op() instanceof Equality && !containsImplicitAttr(t)) {
229: if (term2class.containsKey(t.sub(0))) {
230: ec = (EquivalenceClass) term2class.get(t.sub(0));
231: if (term2class.containsKey(t.sub(1))) {
232: ec.add((EquivalenceClass) term2class.get(t
233: .sub(1)));
234: } else {
235: ec.add(t.sub(1));
236: }
237: } else if (term2class.containsKey(t.sub(1))) {
238: ec = (EquivalenceClass) term2class.get(t.sub(1));
239: ec.add(t.sub(0));
240: } else {
241: ec = new EquivalenceClass(t.sub(0), t.sub(1), serv);
242: }
243: IteratorOfTerm ecIt = ec.getMembers().iterator();
244: while (ecIt.hasNext()) {
245: term2class.put(ecIt.next(), ec);
246: }
247: }
248: }
249: it = succ.iterator();
250: while (it.hasNext()) {
251: Term t = it.next();
252: collectLocations(t);
253: }
254: }
255:
256: /**
257: * Obsolete!
258: * Used when it is tried to generate a model without the help of a decision
259: * procedure.
260: */
261: private void findBounds() {
262: IteratorOfTerm it = ante.iterator();
263: while (it.hasNext()) {
264: Term t = it.next();
265: EquivalenceClass e0, e1;
266: if ("lt".equals(t.op().name().toString())) {
267: e0 = getEqvClass(t.sub(0));
268: e1 = getEqvClass(t.sub(1));
269: e0.addUpperBound(e1, true);
270: e1.addLowerBound(e0, true);
271: }
272: }
273: it = succ.iterator();
274: while (it.hasNext()) {
275: Term t = it.next();
276: EquivalenceClass e0, e1;
277: if ("lt".equals(t.op().name().toString())) {
278: e0 = getEqvClass(t.sub(0));
279: e1 = getEqvClass(t.sub(1));
280: if (e1.addUpperBound(e0, false)) {
281: term2class.put(t.sub(0), e1);
282: term2class.put(t.sub(1), e1);
283: } else if (e0.addLowerBound(e1, false)) {
284: term2class.put(t.sub(0), e0);
285: term2class.put(t.sub(1), e0);
286: }
287: }
288: }
289: }
290:
291: private void findDisjointClasses() {
292: IteratorOfTerm it = succ.iterator();
293: while (it.hasNext()) {
294: Term t = it.next();
295: EquivalenceClass e0, e1;
296: if (t.op() instanceof Equality && !containsImplicitAttr(t)) {
297: e0 = getEqvClass(t.sub(0));
298: e1 = getEqvClass(t.sub(1));
299: e0.addDisjoint(t.sub(1));
300: e1.addDisjoint(t.sub(0));
301: }
302: }
303: }
304:
305: /**
306: * Resets the concrete values of all EquivalenceClasses.
307: */
308: private void resetAllClasses(LinkedList classes) {
309: for (int i = 0; i < classes.size(); i++) {
310: ((EquivalenceClass) classes.get(i)).resetValue();
311: }
312: }
313:
314: /**
315: * Obsolete. Checks whether the current partial model is consistent.
316: */
317: private boolean consistencyCheck() {
318: Iterator it = term2class.values().iterator();
319: while (it.hasNext()) {
320: EquivalenceClass ec = (EquivalenceClass) it.next();
321: if (ec.isBoolean() && !ec.consistencyCheck(term2class)) {
322: return false;
323: }
324: }
325: return true;
326: }
327:
328: /**
329: * Trys to create a model and returns the equivalence classes contained in
330: * the partial model.
331: */
332: public Model[] createModels() {
333: DecProdModelGenerator dmg;
334: Set intModelSet = new HashSet();
335: LinkedList classes = new LinkedList(term2class.values());
336: for (int i = classes.size() - 1; i >= 0; i--) {
337: if (//!((EquivalenceClass) classes.get(i)).isInt() &&
338: !((EquivalenceClass) classes.get(i)).isBoolean()
339: || ((EquivalenceClass) classes.get(i))
340: .getLocations().size() == 0) {
341: classes.remove(i);
342: }
343: }
344: if (decProdForTestGen == COGENT) {
345: dmg = new CogentModelGenerator(new CogentTranslation(node
346: .sequent()), serv, term2class, locations);
347: intModelSet = dmg.createModels();
348: }
349: if (decProdForTestGen == SIMPLIFY /*|| intModelSet.isEmpty()*/) {
350: dmg = new SimplifyModelGenerator(
351: new DecisionProcedureSimplify(
352: node,
353: userConstraint,
354: new JavaDecisionProcedureTranslationFactory(),
355: serv), serv, term2class, locations);
356: intModelSet = dmg.createModels();
357: }
358: Set modelSet = new HashSet();
359: Iterator it = intModelSet.iterator();
360: while (it.hasNext()) {
361: modelSet
362: .addAll(createModelHelp((Model) it.next(), classes));
363: }
364: Model[] models = new Model[modelSet.size()];
365: it = modelSet.iterator();
366: int k = 0;
367: while (it.hasNext()) {
368: models[k++] = (Model) it.next();
369: }
370: // try to merge some models
371: int merged = 0;
372: Model[] result = new Model[models.length - merged];
373: for (int i = 0; i < result.length; i++) {
374: result[i] = models[i];
375: }
376: return result;
377: }
378:
379: /**
380: * Computes values for EquivalenceClasses of type boolean and adds these
381: * assignments to the partial model <code>model</code>.
382: */
383: private Set createModelHelp(Model model, LinkedList classes) {
384: HashSet models = new HashSet();
385: if (!consistencyCheck()) {
386: return models;
387: }
388: classes = (LinkedList) classes.clone();
389: Model m;
390: for (int i = classes.size() - 1; i >= 0; i--) {
391: if (((EquivalenceClass) classes.get(i))
392: .hasConcreteValue(term2class)
393: && ((EquivalenceClass) classes.get(i))
394: .getLocations().size() > 0) {
395: model.setValue((EquivalenceClass) classes.remove(i));
396: }
397: }
398: if (classes.isEmpty()) {
399: //model creation successful
400: models.add(model);
401: return models;
402: }
403: EquivalenceClass ec;
404: for (int i = 0; i < classes.size(); i++) {
405: ec = (EquivalenceClass) classes.get(i);
406: if (ec.getLocations().size() == 0)
407: continue;
408: if (ec.isBoolean()) {
409: ec.setBoolean(true);
410: m = model.copy();
411: m.setValue(ec, true);
412: models.addAll(createModelHelp(m, classes));
413: resetAllClasses(classes);
414: ec.setBoolean(false);
415: m = model.copy();
416: m.setValue(ec, false);
417: models.addAll(createModelHelp(m, classes));
418: resetAllClasses(classes);
419: }/*else if(ec.isInt()){
420: int bound = ec.getMaximalConcreteLowerBound(term2class);
421: ec.setInteger(bound);
422: m = model.copy();
423: m.setValue(ec, bound);
424: models.addAll(createModelHelp(m, classes));
425: resetAllClasses(classes);
426: bound = ec.getMinimalConcreteUpperBound(term2class);
427: // if(bound != Integer.MAX_VALUE){
428: ec.setInteger(bound);
429: m = model.copy();
430: m.setValue(ec, bound);
431: models.addAll(createModelHelp(m, classes));
432: resetAllClasses(classes);
433: // }
434: }*/
435: }
436: return models;
437: }
438:
439: /**
440: * Returns the EquivalenceClasses that contain locations of type int or
441: * boolean
442: */
443: public EquivalenceClass[] getPrimitiveLocationEqvClasses() {
444: Object[] oa = (new HashSet(term2class.values())).toArray();
445: EquivalenceClass[] temp = new EquivalenceClass[oa.length];
446: int l = 0;
447: for (int i = 0; i < oa.length; i++) {
448: if (((EquivalenceClass) oa[i]).getLocations().size() > 0
449: && (((EquivalenceClass) oa[i]).isInt() || ((EquivalenceClass) oa[i])
450: .isBoolean())) {
451: temp[l++] = (EquivalenceClass) oa[i];
452: }
453: }
454: EquivalenceClass[] result = new EquivalenceClass[l];
455: for (int i = 0; i < l; i++) {
456: result[i] = temp[i];
457: }
458: return result;
459: }
460:
461: /**
462: * Returns the EquivalenceClasses that contain locations of nonprimitive
463: * types.
464: */
465: public EquivalenceClass[] getNonPrimitiveLocationEqvClasses() {
466: Object[] oa = (new HashSet(term2class.values())).toArray();
467: EquivalenceClass[] temp = new EquivalenceClass[oa.length];
468: int l = 0;
469: for (int i = 0; i < oa.length; i++) {
470: if (((EquivalenceClass) oa[i]).getLocations().size() > 0
471: && (!((EquivalenceClass) oa[i]).isInt() && !((EquivalenceClass) oa[i])
472: .isBoolean())) {
473: temp[l++] = (EquivalenceClass) oa[i];
474: }
475: }
476: EquivalenceClass[] result = new EquivalenceClass[l];
477: for (int i = 0; i < l; i++) {
478: result[i] = temp[i];
479: }
480: return result;
481: }
482:
483: /**
484: * Returns the equivalence class of term t. If it doesn't exist yet a new
485: * one is created.
486: */
487: private EquivalenceClass getEqvClass(Term t) {
488: if (!term2class.containsKey(t)) {
489: term2class.put(t, new EquivalenceClass(t, serv));
490: }
491: return (EquivalenceClass) term2class.get(t);
492: }
493:
494: public Node getNode() {
495: return node;
496: }
497:
498: public Node getOriginalNode() {
499: return originalNode;
500: }
501:
502: }
|