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.visualdebugger.statevisualisation;
009:
010: import java.util.HashSet;
011: import java.util.Iterator;
012: import java.util.LinkedList;
013:
014: import de.uka.ilkd.key.gui.KeYMediator;
015: import de.uka.ilkd.key.java.JavaInfo;
016: import de.uka.ilkd.key.java.Services;
017: import de.uka.ilkd.key.java.abstraction.ClassType;
018: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
019: import de.uka.ilkd.key.logic.*;
020: import de.uka.ilkd.key.logic.op.*;
021: import de.uka.ilkd.key.logic.sort.ListOfSort;
022: import de.uka.ilkd.key.logic.sort.SLListOfSort;
023: import de.uka.ilkd.key.logic.sort.Sort;
024: import de.uka.ilkd.key.proof.*;
025: import de.uka.ilkd.key.proof.init.InitConfig;
026: import de.uka.ilkd.key.proof.init.ProofOblInput;
027: import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
028: import de.uka.ilkd.key.rule.NoPosTacletApp;
029: import de.uka.ilkd.key.rule.TacletApp;
030: import de.uka.ilkd.key.rule.updatesimplifier.*;
031: import de.uka.ilkd.key.strategy.DebuggerStrategy;
032: import de.uka.ilkd.key.strategy.StrategyFactory;
033: import de.uka.ilkd.key.strategy.StrategyProperties;
034: import de.uka.ilkd.key.visualdebugger.DebuggerEvent;
035: import de.uka.ilkd.key.visualdebugger.DebuggerPO;
036: import de.uka.ilkd.key.visualdebugger.ProofStarter;
037: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
038: import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
039:
040: public class StateVisualization {
041:
042: private SetOfTerm arrayIndexTerms;
043:
044: private final SetOfTerm arrayLocations;
045:
046: private SetOfTerm[][] indexConfigurations;
047:
048: private SetOfTerm[] instanceConfigurations;
049:
050: private final ITNode itNode;
051:
052: private final ListOfTerm locations;
053:
054: private final KeYMediator mediator;
055:
056: // ListOfTerm terms = SLListOfTerm.EMPTY_LIST;
057:
058: private DebuggerPO po = new DebuggerPO("DebuggerPo");
059:
060: private Term[] postAttributes;
061:
062: private ListOfTerm[][] postValues;
063:
064: private PosInOccurrence programPio;
065:
066: private ProofStarter ps;
067:
068: private SetOfTerm refInPC = SetAsListOfTerm.EMPTY_SET;
069:
070: private final Services serv;
071:
072: private RigidFunction stateOp;
073:
074: private Term statePred;
075:
076: private TermBuilder TB = TermBuilder.DF;
077:
078: private VisualDebugger vd;
079:
080: private int maxProofSteps;
081:
082: private boolean useDecisionProcedures;
083:
084: public StateVisualization(ITNode itn, KeYMediator mediator,
085: int maxProofSteps, boolean useDecisionProcedures) {
086:
087: this .itNode = itn;
088: this .vd = VisualDebugger.getVisualDebugger();
089: this .mediator = mediator;
090:
091: this .serv = mediator.getServices();
092:
093: this .maxProofSteps = maxProofSteps;
094: this .useDecisionProcedures = useDecisionProcedures;
095:
096: refInPC = getReferences(itNode.getPc());
097:
098: this .programPio = vd.getProgramPIO(itNode.getNode().sequent());
099: if (programPio == null) {
100: programPio = vd.getExecutionTerminatedNormal(itNode
101: .getNode());
102: }
103: if (programPio == null)
104: throw new RuntimeException(
105: "Program Pio not found in Sequent "
106: + itNode.getNode().sequent());
107:
108: simplifyUpdate();
109:
110: setUpProof(null, null);
111:
112: locations = vd.getLocations(programPio);
113: arrayIndexTerms = vd.getArrayIndex(programPio);
114:
115: // getRefsInPreState(locations);
116: arrayLocations = vd.getArrayLocations(programPio);
117: final Term programPio2 = addRememberPrestateUpdates(programPio
118: .constrainedFormula().formula());
119: // statePred = this.createPredicate(locations);
120:
121: applyCuts(refInPC);
122:
123: computeInstanceConfigurations();
124: this .indexConfigurations = new SetOfTerm[this .instanceConfigurations.length][];
125: for (int i = 0; i < instanceConfigurations.length; i++) {
126: setUpProof(instanceConfigurations[i], null);
127: applyCuts(arrayIndexTerms);
128: computeArrayConfigurations(i);
129: }
130:
131: postValues = new ListOfTerm[instanceConfigurations.length][];
132: for (int i = 0; i < instanceConfigurations.length; i++) {
133: postValues[i] = new ListOfTerm[indexConfigurations[i].length];
134: for (int j = 0; j < indexConfigurations[i].length; j++) {
135: setUpProof(instanceConfigurations[i]
136: .union(indexConfigurations[i][j]), programPio2);
137:
138: ps.run(mediator.getProof().env());
139:
140: postValues[i][j] = getPostState(ps.getProof()
141: .openGoals().head().node().sequent());
142: }
143: }
144:
145: vd.fireDebuggerEvent(new DebuggerEvent(DebuggerEvent.VIS_STATE,
146: this ));
147: }
148:
149: private Term addRememberPrestateUpdates(Term target) {
150: Term locs[] = locations.toArray();
151: postAttributes = new Term[locs.length];
152:
153: Update up = Update.createUpdate(target);
154:
155: LinkedList newAP = new LinkedList();
156: // for(IteratorOfTerm it= this.refsInPreState.iterator();it.hasNext();){
157: for (int i = 0; i < locs.length; i++) {
158: if (locs[i].op() instanceof AttributeOp) {
159: final LocationVariable pv = new LocationVariable(
160: new ProgramElementName("pre" + i), locs[i].sub(
161: 0).sort());
162:
163: final Term t = TB.var(pv);
164:
165: postAttributes[i] = TB.dot(t,
166: (ProgramVariable) (((AttributeOp) locs[i].op())
167: .attribute()));
168:
169: newAP.add(new AssignmentPairImpl(pv, new Term[0],
170: locs[i].sub(0)));
171: } else if (locs[i].op() instanceof ProgramVariable) {
172: postAttributes[i] = locs[i];
173:
174: } else if (locs[i].op() instanceof ArrayOp) {
175: final LocationVariable pv_array_ref = new LocationVariable(
176: new ProgramElementName("pre_array_" + i),
177: locs[i].sub(0).sort());
178: final Term t = TB.var(pv_array_ref);
179:
180: newAP.add(new AssignmentPairImpl(pv_array_ref,
181: new Term[0], locs[i].sub(0)));
182:
183: final LocationVariable pv_index = new LocationVariable(
184: new ProgramElementName("pre_array_index_" + i),
185: locs[i].sub(1).sort());
186:
187: final Term indexT = TB.var(pv_index);
188: newAP.add(new AssignmentPairImpl(pv_index, new Term[0],
189: locs[i].sub(1)));
190:
191: postAttributes[i] = TB.array(t, indexT);
192: }
193:
194: }
195:
196: ArrayOfAssignmentPair apOld = up.getAllAssignmentPairs();
197: AssignmentPair[] aps = new AssignmentPair[newAP.size()
198: + apOld.size()];
199:
200: for (int i = newAP.size(); i < apOld.size() + newAP.size(); i++) {
201: aps[i] = apOld.getAssignmentPair(i - newAP.size());
202: }
203:
204: for (int i = 0; i < newAP.size(); i++) {
205: aps[i] = (AssignmentPair) newAP.get(i); // TODO
206:
207: }
208:
209: statePred = createPredicate(SLListOfTerm.EMPTY_LIST
210: .append(postAttributes));
211:
212: return UpdateSimplifierTermFactory.DEFAULT.createUpdateTerm(
213: aps, this .statePred);
214:
215: }
216:
217: private synchronized void applyCutAndRun(ListOfGoal goals, Term inst) {
218: for (IteratorOfGoal it = goals.iterator(); it.hasNext();) {
219: final Goal g = it.next();
220: final NoPosTacletApp c = g.indexOfTaclets().lookup("cut");
221: assert c != null;
222: // c.
223: SetOfSchemaVariable set2 = c.neededUninstantiatedVars();
224: SchemaVariable cutF = set2.iterator().next();
225:
226: TacletApp t2 = c.addInstantiation(cutF, inst, false);
227:
228: g.apply(t2);
229:
230: ps.run(mediator.getProof().env());
231: }
232:
233: }
234:
235: private void applyCuts(SetOfTerm terms) {
236: Term[] t1 = terms.toArray();
237: Term[] t2 = terms.toArray();
238:
239: for (int i1 = 0; i1 < t1.length; i1++) {
240: for (int i2 = i1; i2 < t2.length; i2++) {
241: if (!t1[i1].equals(t2[i2])) {
242: if (t1[i1].sort().extendsTrans(t2[i2].sort())
243: || t2[i2].sort()
244: .extendsTrans(t1[i1].sort())) {
245: applyCutAndRun(ps.getProof().openGoals(), TB
246: .equals(t1[i1], t2[i2]));
247: }
248: }
249: }
250: }
251: }
252:
253: private void computeArrayConfigurations(int instanceConf) {
254: final HashSet indexConf = new HashSet();
255:
256: final Proof proof = ps.getProof();
257: final Node root = proof.root();
258: for (IteratorOfGoal it = proof.openGoals().iterator(); it
259: .hasNext();) {
260: indexConf.add(getAppliedCutsSet(it.next().node(), root));
261: }
262: this .indexConfigurations[instanceConf] = new SetOfTerm[indexConf
263: .size()];
264: int i = 0;
265: for (Iterator it = indexConf.iterator(); it.hasNext(); i++) {
266: indexConfigurations[instanceConf][i] = (SetOfTerm) it
267: .next();
268: }
269:
270: }
271:
272: private void computeInstanceConfigurations() {
273: HashSet indexConf = new HashSet();
274:
275: final Proof proof = ps.getProof();
276: final Node root = proof.root();
277: for (IteratorOfGoal it = proof.openGoals().iterator(); it
278: .hasNext();) {
279: indexConf.add(getAppliedCutsSet(it.next().node(), root));
280: }
281: this .instanceConfigurations = new SetOfTerm[indexConf.size()];
282: int i = 0;
283: for (Iterator it = indexConf.iterator(); it.hasNext(); i++) {
284: instanceConfigurations[i] = (SetOfTerm) it.next();
285: }
286:
287: }
288:
289: private Term createPredicate(ListOfTerm locs) {
290: Term result = null;
291: ListOfSort s = SLListOfSort.EMPTY_LIST;
292:
293: for (IteratorOfTerm it = locs.iterator(); it.hasNext();) {
294: s = s.append(it.next().sort());
295: }
296:
297: stateOp = new RigidFunction(new Name("STATE"), Sort.FORMULA, s
298: .toArray());
299:
300: result = TermFactory.DEFAULT.createFunctionTerm(stateOp, locs
301: .toArray());
302:
303: return result;
304: }
305:
306: private SetOfTerm getAppliedCutsSet(Node n, Node root) {
307: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
308: if (!root.find(n)) {
309: throw new RuntimeException(
310: "node n ist not a childs of node root");
311: }
312:
313: while (!(n.serialNr() == root.serialNr())) {
314: final Node oldN = n;
315: n = n.parent();
316: if (n.getAppliedRuleApp() instanceof NoPosTacletApp) {
317: NoPosTacletApp npta = (NoPosTacletApp) n
318: .getAppliedRuleApp();
319: if (npta.taclet().name().toString().toUpperCase()
320: .equals("CUT")) {
321: Term inst = (Term) npta.instantiations()
322: .lookupEntryForSV(new Name("cutFormula"))
323: .value().getInstantiation();
324: if (n.child(1) == oldN)// TODO or 0
325: inst = TB.not(inst);
326: result = result.add(inst);
327:
328: }
329: }
330: }
331:
332: return result;
333:
334: }
335:
336: public SetOfTerm[] getPossibleIndexTermsForPcState(int i) {
337: return indexConfigurations[i];
338:
339: }
340:
341: private ListOfTerm getPostState(Sequent s) {
342: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
343: for (final IteratorOfConstrainedFormula it = s.succedent()
344: .iterator(); it.hasNext();) {
345: final Term formula = it.next().formula();
346: if (formula.op() == stateOp) {
347: for (int i = 0, ar = formula.arity(); i < ar; i++) {
348: result = result.append(formula.sub(i));
349: }
350: }
351: }
352: return result;
353: }
354:
355: private SetOfTerm getReferences(ListOfTerm terms) {
356: // ListOfTerm pc = itNode.getPc();
357: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
358: for (IteratorOfTerm it = terms.iterator(); it.hasNext();) {
359: result = result.union(getReferences(it.next()));
360: }
361: return result;
362: }
363:
364: private SetOfTerm getReferences(Term t) {
365: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
366: if (referenceSort(t.sort()) && t.freeVars().size() == 0)
367: result = result.add(t);
368: for (int i = 0; i < t.arity(); i++) {
369: result = result.union(getReferences(t.sub(i)));
370: }
371: return result;
372: }
373:
374: public SymbolicObjectDiagram getSymbolicState(int i,
375: SetOfTerm indexTerms, boolean pre) {
376: for (int j = 0; j < indexConfigurations[i].length; j++) {
377: if (indexTerms.subset(indexConfigurations[i][j])) {
378: final ListOfTerm pt = postValues[i][j];
379: final SymbolicObjectDiagram s = new SymbolicObjectDiagram(
380: itNode, mediator.getServices(), itNode.getPc(),
381: refInPC, locations, pt, pre,
382: this .arrayLocations, indexConfigurations[i],
383: indexConfigurations[i][j],
384: instanceConfigurations[i]);
385: return s;
386: }
387: }
388:
389: return null;
390: }
391:
392: public int numberOfPCStates() {
393: return this .instanceConfigurations.length;
394: }
395:
396: private boolean referenceSort(Sort s) {
397: final JavaInfo info = serv.getJavaInfo();
398: final KeYJavaType kjt = info.getKeYJavaType(s);
399: if (kjt == null)
400: return false;
401: // a ClassType represents classes, interfaces, arrays and null
402: return kjt.getJavaType() instanceof ClassType;
403: }
404:
405: private void initProofStarter(ProofOblInput po) {
406: ps = new ProofStarter();
407: ps.init(po);
408: ps.setMaxSteps(maxProofSteps);
409: ps.setUseDecisionProcedure(useDecisionProcedures);
410: vd.setProofStrategy(ps.getProof(), true, false);
411: }
412:
413: private void setUpProof(SetOfTerm indexConf, Term forPostValues) {
414: po = new DebuggerPO("DebuggerPo");
415: if (forPostValues != null) {
416: po.setUp(vd.getPrecondition(), itNode, indexConf,
417: forPostValues);
418: } else {
419: if (indexConf == null) {
420: po.setUp(vd.getPrecondition(), itNode);
421: } else {
422: po.setUp(vd.getPrecondition(), itNode, indexConf);
423: }
424: }
425: final Proof proof = mediator.getProof();
426: final InitConfig initConfig = proof.env().getInitConfig();
427: po.setIndices(initConfig.createTacletIndex(), initConfig
428: .createBuiltInRuleIndex());
429: po.setProofSettings(proof.getSettings());
430: po.setConfig(initConfig);
431:
432: initProofStarter(po);
433: }
434:
435: private void simplifyUpdate() {
436: this .setUpProof(SetAsListOfTerm.EMPTY_SET.add(TB.not(programPio
437: .constrainedFormula().formula())), null);
438:
439: vd.setInitPhase(true);
440: vd.getBpManager().setNoEx(true);
441:
442: final ProofEnvironment env = mediator.getProof().env();
443:
444: final Proof simplificationProof = ps.getProof();
445:
446: StrategyProperties strategyProperties = DebuggerStrategy
447: .getDebuggerStrategyProperties(true, true, vd
448: .isInitPhase());
449:
450: StrategyFactory factory = new DebuggerStrategy.Factory();
451:
452: mediator.getProof()
453: .setActiveStrategy(
454: factory.create(mediator.getProof(),
455: strategyProperties));
456:
457: ps.run(env);
458:
459: vd.setInitPhase(false);
460: vd.getBpManager().setNoEx(false);
461:
462: strategyProperties = DebuggerStrategy
463: .getDebuggerStrategyProperties(true, false, vd
464: .isInitPhase());
465:
466: mediator.getProof()
467: .setActiveStrategy(
468: factory.create(mediator.getProof(),
469: strategyProperties));
470:
471: assert simplificationProof.openGoals().size() == 1;
472:
473: final Goal openGoal = simplificationProof.openGoals().head();
474: this.programPio = vd.getProgramPIO(openGoal.sequent());
475: if (programPio == null) {
476: programPio = vd.getExecutionTerminatedNormal(openGoal
477: .node());
478: }
479: }
480:
481: }
|