0001: // This file is part of KeY - Integrated Deductive Software Design
0002: // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
0003: // Universitaet Koblenz-Landau, Germany
0004: // Chalmers University of Technology, Sweden
0005: //
0006: // The KeY system is protected by the GNU General Public License.
0007: // See LICENSE.TXT for details.
0008: package de.uka.ilkd.key.visualdebugger.statevisualisation;
0009:
0010: import java.util.*;
0011:
0012: import de.uka.ilkd.key.java.JavaInfo;
0013: import de.uka.ilkd.key.java.Services;
0014: import de.uka.ilkd.key.java.abstraction.ClassType;
0015: import de.uka.ilkd.key.java.abstraction.KeYJavaType;
0016: import de.uka.ilkd.key.java.declaration.ArrayOfParameterDeclaration;
0017: import de.uka.ilkd.key.java.reference.ReferencePrefix;
0018: import de.uka.ilkd.key.java.reference.TypeRef;
0019: import de.uka.ilkd.key.java.statement.MethodBodyStatement;
0020: import de.uka.ilkd.key.logic.*;
0021: import de.uka.ilkd.key.logic.ldt.BooleanLDT;
0022: import de.uka.ilkd.key.logic.ldt.IntegerLDT;
0023: import de.uka.ilkd.key.logic.op.*;
0024: import de.uka.ilkd.key.logic.sort.ArraySort;
0025: import de.uka.ilkd.key.logic.sort.Sort;
0026: import de.uka.ilkd.key.proof.Node;
0027: import de.uka.ilkd.key.proof.ProgVarReplacer;
0028: import de.uka.ilkd.key.unittest.ModelGenerator;
0029: import de.uka.ilkd.key.visualdebugger.HashMapFromPosInOccurrenceToLabel;
0030: import de.uka.ilkd.key.visualdebugger.IteratorOfPosInOccurrence;
0031: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
0032: import de.uka.ilkd.key.visualdebugger.executiontree.ITNode;
0033:
0034: public class SymbolicObjectDiagram {
0035: private static Term nullTerm = TermFactory.DEFAULT
0036: .createFunctionTerm(Op.NULL);
0037:
0038: public static boolean checkIndices(Term t, Services serv) {
0039: if (t.op() instanceof AttributeOp) {
0040: return checkIndices(t.sub(0), serv);
0041: }
0042: if (t.op() instanceof ArrayOp) {
0043: if (serv.getTypeConverter().getIntegerLDT()
0044: .getNumberSymbol() == t.sub(1).op()) {
0045: if (AbstractMetaOperator.convertToDecimalString(
0046: t.sub(1), serv).startsWith("-")) {
0047: return false;
0048: }
0049: }
0050: return checkIndices(t.sub(0), serv);
0051: }
0052: return true;
0053: }
0054:
0055: public static boolean isLocation(Term t, Services serv) {
0056: OpCollector oc = new OpCollector();
0057: t.execPostOrder(oc);
0058: if (oc.contains(Op.NULL)) {
0059: return false;
0060: }
0061:
0062: final IntegerLDT iLDT = serv.getTypeConverter().getIntegerLDT();
0063: final BooleanLDT bLDT = serv.getTypeConverter().getBooleanLDT();
0064:
0065: final Function numberTerminator = iLDT.getNumberTerminator();
0066: final Function boolTRUE = bLDT.getTrueConst();
0067: final Function boolFALSE = bLDT.getFalseConst();
0068:
0069: final Operator op = t.op();
0070: return op instanceof AttributeOp
0071: && checkIndices(t, serv)
0072: && !((ProgramVariable) ((AttributeOp) op).attribute())
0073: .isImplicit()
0074: || op instanceof ProgramVariable
0075: && !((ProgramVariable) op).isImplicit()
0076: || op instanceof ArrayOp
0077: && checkIndices(t, serv)
0078: // TODO Why is a RigidFunction a location?
0079: // Was a ProgramConstant intended? if so replace the rest
0080: // by instanceof ProgramConstant
0081: || op instanceof RigidFunction && t.arity() == 0
0082: && numberTerminator != op && boolTRUE != op
0083: && boolFALSE != op
0084: // TODO remove string comparison in next line
0085: && op.name().toString().indexOf("undef(") == -1;
0086: }
0087:
0088: private ListOfTerm ante = SLListOfTerm.EMPTY_LIST,
0089: succ = SLListOfTerm.EMPTY_LIST;
0090:
0091: private SetOfTerm arrayLocations;
0092:
0093: private SetOfTerm indexTerms;
0094:
0095: private SetOfTerm instanceConfiguration;
0096:
0097: private ITNode itNode;
0098:
0099: private SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
0100:
0101: private Term methodReferences[];
0102:
0103: private Node node;
0104:
0105: ListOfTerm pc = SLListOfTerm.EMPTY_LIST;
0106:
0107: private SetOfTerm[] possibleIndexTerms;
0108:
0109: private ListOfTerm postTerms;
0110:
0111: private HashMap ref2ser;
0112:
0113: private SetOfTerm refInPC = SetAsListOfTerm.EMPTY_SET;
0114:
0115: private Services serv;
0116:
0117: private LinkedList symbolicObjects;
0118:
0119: private HashMap term2class;
0120:
0121: LinkedList terms = new LinkedList();
0122:
0123: private VisualDebugger vd;
0124:
0125: public SymbolicObjectDiagram(ITNode itNode, Services serv,
0126: ListOfTerm pc, SetOfTerm refInPC, ListOfTerm preTerms,
0127: ListOfTerm postTerms, boolean pre,
0128: SetOfTerm arrayLocations, SetOfTerm[] possibleIndexTerms,
0129: SetOfTerm indexTerms, SetOfTerm instanceConfiguration) {
0130: this .instanceConfiguration = instanceConfiguration;
0131: prepare(itNode, serv, pc, refInPC);
0132: this .postTerms = postTerms;
0133:
0134: this .arrayLocations = arrayLocations;
0135:
0136: this .possibleIndexTerms = possibleIndexTerms;
0137:
0138: this .indexTerms = indexTerms;
0139:
0140: createSymbolicObjects();
0141: if (!pre) {
0142: createSymbolicObjectsForNewInstances(preTerms);
0143: createPostState(preTerms, postTerms);
0144: setMethodStack(pre);
0145: }
0146:
0147: setInstanceNames(symbolicObjects);
0148: }
0149:
0150: private void addArrayEntry(LinkedList objects, Term ref,
0151: Term index, Term con) {
0152: final Iterator it = objects.iterator();
0153: while (it.hasNext()) {
0154: SymbolicObject so = (SymbolicObject) it.next();
0155: if (so.getTerms().contains(ref)) {
0156: ((SymbolicArrayObject) so).addIndexConstraint(index,
0157: con);
0158: }
0159: }
0160:
0161: }
0162:
0163: private void addAttribute(LinkedList objects, AttributeOp op,
0164: Term sub, Term cTerm) {
0165: Iterator it = objects.iterator();
0166: while (it.hasNext()) {
0167: SymbolicObject so = (SymbolicObject) it.next();
0168: if (so.getTerms().contains(sub)) {
0169: if (!((ProgramVariable) op.attribute()).isImplicit()
0170: || VisualDebugger.showImpliciteAttr)
0171: so.addAttributeConstraint((ProgramVariable) op
0172: .attribute(), cTerm);
0173: }
0174: }
0175:
0176: }
0177:
0178: private void addIndexReference(Term sub, Term index,
0179: SymbolicObject soReferenced, LinkedList objects) {
0180: Iterator it = objects.iterator();
0181: while (it.hasNext()) {
0182: SymbolicObject so = (SymbolicObject) it.next();
0183: if (so.getTerms().contains(sub)) {
0184: ((SymbolicArrayObject) so).addAssociationFromIndex(
0185: index, soReferenced);
0186: }
0187: }
0188: }
0189:
0190: private void addReference(AttributeOp op, Term sub,
0191: SymbolicObject soReferenced, LinkedList objects) {
0192: Iterator it = objects.iterator();
0193: while (it.hasNext()) {
0194: SymbolicObject so = (SymbolicObject) it.next();
0195: if (so.getTerms().contains(sub)) {
0196: if (op.attribute() instanceof ProgramVariable)
0197: so.addAssociation(op.attribute(), soReferenced);
0198: else
0199: System.err
0200: .println("op.attribute not instance of ProgramVariable");
0201: }
0202: }
0203: }
0204:
0205: private void addStaticAttribute(LinkedList objects,
0206: ProgramVariable pv, ClassType ct, Term cTerm) {
0207: Iterator it = objects.iterator();
0208: while (it.hasNext()) {
0209: SymbolicObject so = (SymbolicObject) it.next();
0210: if (so.isStatic() && so.getType().equals(ct)) {
0211: if (!pv.isImplicit()
0212: || VisualDebugger.showImpliciteAttr)
0213: so.addAttributeConstraint(pv, cTerm);
0214: }
0215: }
0216:
0217: }
0218:
0219: private void addStaticReference(ProgramVariable op,
0220: SymbolicObject soReferenced, LinkedList objects) {
0221: Iterator it = objects.iterator();
0222: while (it.hasNext()) {
0223: SymbolicObject so = (SymbolicObject) it.next();
0224: if (so.isStatic()
0225: && so.getType().equals(
0226: op.getContainerType().getJavaType()))
0227: so.addAssociation(op, soReferenced);
0228:
0229: }
0230:
0231: }
0232:
0233: private void collectLocations(Term t) {
0234: if (isLocation(t, serv)) {
0235: getEqvClass(t);
0236: locations = locations.add(t);
0237: }
0238: if (!(t.op() instanceof Modality
0239: || t.op() instanceof IUpdateOperator || t.op() instanceof Quantifier)) {
0240: for (int i = 0; i < t.arity(); i++) {
0241: collectLocations(t.sub(i));
0242: }
0243: }
0244: }
0245:
0246: private SetOfTerm collectLocations2(Term t) {
0247: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0248: if (isLocation(t, serv)) {
0249: result = result.add(t);
0250:
0251: }
0252: if (!(t.op() instanceof Modality
0253: || t.op() instanceof IUpdateOperator || t.op() instanceof Quantifier)) {
0254: for (int i = 0; i < t.arity(); i++) {
0255: result = result.union(collectLocations2(t.sub(i)));
0256: }
0257: }
0258: return result;
0259: }
0260:
0261: private boolean containsJavaBlock(Term t) {
0262: if (t.op() == vd.getPostPredicate()) {
0263: return true; // TODO
0264: }
0265: if (t.javaBlock() != JavaBlock.EMPTY_JAVABLOCK) {
0266: return true;
0267: }
0268: for (int i = 0; i < t.arity(); i++) {
0269: if (containsJavaBlock(t.sub(i))) {
0270: return true;
0271: }
0272: }
0273: return false;
0274: }
0275:
0276: private void createEquivalenceClassesAndConstraints() {
0277: term2class = new HashMap();
0278: IteratorOfTerm it = ante.iterator();
0279: while (it.hasNext()) {
0280: EquClass ec = null;
0281: Term t = it.next();
0282: collectLocations(t);
0283: if (t.op() instanceof Equality /* && !containsImplicitAttr(t) */) {
0284: if (term2class.containsKey(t.sub(0))) {
0285: ec = (EquClass) term2class.get(t.sub(0));
0286: if (term2class.containsKey(t.sub(1))) {
0287: ec.add((EquClass) term2class.get(t.sub(1)));
0288: } else {
0289: ec.add(t.sub(1));
0290: }
0291: } else if (term2class.containsKey(t.sub(1))) {
0292: ec = (EquClass) term2class.get(t.sub(1));
0293: ec.add(t.sub(0));
0294: } else {
0295: ec = new EquClass(t.sub(0), t.sub(1));
0296: }
0297: IteratorOfTerm ecIt = ec.getMembers().iterator();
0298: while (ecIt.hasNext()) {
0299: term2class.put(ecIt.next(), ec);
0300: }
0301: }
0302:
0303: }
0304: it = succ.iterator();
0305: while (it.hasNext()) {
0306: Term t = it.next();
0307: collectLocations(t);
0308: }
0309: }
0310:
0311: private void createPostState(ListOfTerm pre, ListOfTerm post) {
0312: VisualDebugger.print("createPostState -----");
0313: IteratorOfTerm pIt = post.iterator();
0314: for (IteratorOfTerm it = pre.iterator(); it.hasNext();) {
0315: Term preTerm = it.next();
0316: Term postTerm = pIt.next();
0317: // System.out.println(preTerm+":="+postTerm);
0318: if (preTerm.op() instanceof AttributeOp) {
0319: final Term sub = preTerm.sub(0);
0320: final SymbolicObject so = getObject(sub,
0321: symbolicObjects);
0322: if (referenceSort(preTerm.sort()))
0323: so.addAssociation(((AttributeOp) preTerm.op())
0324: .attribute(), getObject(postTerm,
0325: symbolicObjects));
0326: else if (!((ProgramVariable) ((AttributeOp) preTerm
0327: .op()).attribute()).isImplicit()
0328: || VisualDebugger.showImpliciteAttr)
0329: so.addValueTerm(
0330: (ProgramVariable) ((AttributeOp) preTerm
0331: .op()).attribute(), postTerm);
0332: } else if (preTerm.op() instanceof ArrayOp) {
0333: final Term sub = preTerm.sub(0);
0334: final SymbolicArrayObject sao = (SymbolicArrayObject) getObject(
0335: sub, symbolicObjects);
0336: if (referenceSort(preTerm.sort()))
0337: sao.addAssociationFromIndex(preTerm.sub(1),
0338: getObject(postTerm, symbolicObjects));
0339: else
0340: sao.setValueTermForIndex(preTerm.sub(1), postTerm);
0341: } else if (preTerm.op() instanceof ProgramVariable) {
0342: final ProgramVariable pv = (ProgramVariable) preTerm
0343: .op();
0344: SymbolicObject staticO = getStaticObject((ClassType) pv
0345: .getContainerType().getJavaType(),
0346: symbolicObjects);
0347: if (staticO == null) {
0348: if (!pv.isImplicit()
0349: || VisualDebugger.showImpliciteAttr) {
0350: staticO = new SymbolicObject((ClassType) pv
0351: .getContainerType().getJavaType(), serv);
0352: symbolicObjects.add(staticO);
0353: }
0354: }
0355:
0356: if (referenceSort(preTerm.sort()))
0357: staticO.addAssociation(pv, getObject(postTerm,
0358: symbolicObjects));
0359: else if (!pv.isImplicit()
0360: || VisualDebugger.showImpliciteAttr)
0361: staticO.addValueTerm(pv, postTerm);
0362: }
0363:
0364: }
0365:
0366: }
0367:
0368: private void createSymbolicObjects() {
0369: LinkedList result = new LinkedList();
0370: EquClass[] npClasses = getNonPrimitiveLocationEqvClasses();
0371: for (int i = 0; i < npClasses.length; i++) {
0372: KeYJavaType t = npClasses[i].getKeYJavaType();
0373: if (!disjunct(npClasses[i].getMembers(), refInPC)) {
0374: if (npClasses[i].isArray()) {
0375: SymbolicArrayObject sao = new SymbolicArrayObject(
0376: npClasses[i].getMembers(), (ClassType) t
0377: .getJavaType(), serv);
0378: sao
0379: .setPossibleIndexTermConfigurations(getPossibleIndexTerms(npClasses[i]
0380: .getMembers()));
0381: sao
0382: .setIndexConfiguration(getPossibleIndexTermsForArray(
0383: sao.getTerms(), indexTerms));
0384: result.add(sao);
0385: } else
0386: result.add(new SymbolicObject(npClasses[i]
0387: .getMembers(), (ClassType) t.getJavaType(),
0388: serv));
0389:
0390: }
0391: }
0392:
0393: // create static objects
0394: // System.out.println("Static Type "+);
0395: for (Iterator it = this .getStaticClasses().iterator(); it
0396: .hasNext();) {
0397: result
0398: .add(new SymbolicObject((ClassType) (it.next()),
0399: serv));
0400: }
0401:
0402: // create self object/ self static class, if not happened
0403: if (vd.isStaticMethod()) {
0404: final ClassType ct = vd.getType();
0405: if (this .getStaticObject(ct, result) == null)
0406: result.add(new SymbolicObject(ct, serv));
0407: } else {
0408: final Term self = (Term) vd.getInputPV2term().get(
0409: (vd.getSelfTerm()));
0410: if (this .getObject(self, result) == null)
0411: result.add(new SymbolicObject(self, (ClassType) serv
0412: .getJavaInfo().getKeYJavaType(self.sort())
0413: .getJavaType(), serv));
0414: }
0415:
0416: // create unknown objects
0417: for (IteratorOfTerm it = postTerms.iterator(); it.hasNext();) {
0418: Term next = it.next();
0419: if (this .referenceSort(next.sort())
0420: && !VisualDebugger.containsImplicitAttr(next)) {
0421: if (getObject(next, result) == null) {
0422: result.add(new SymbolicObject(next,
0423: (ClassType) serv.getJavaInfo()
0424: .getKeYJavaType(next.sort())
0425: .getJavaType(), serv, true));
0426: }
0427:
0428: }
0429:
0430: }
0431:
0432: // Compute Associations...
0433: Iterator it = result.iterator();
0434: while (it.hasNext()) {
0435: SymbolicObject so = (SymbolicObject) it.next();
0436: IteratorOfTerm it2 = so.getTerms().iterator();
0437: // SetOfTerm result;
0438: // System.out.println("adding assos");
0439: while (it2.hasNext()) {
0440:
0441: Term t = it2.next();
0442: // System.out.println("ref" +t);
0443:
0444: if (t.op() instanceof AttributeOp) {
0445: Term sub = t.sub(0);
0446: AttributeOp op = (AttributeOp) t.op();
0447: if (refInPC.contains(t) || postTerms.contains(t)) // TODO
0448: // ???//only
0449: // assoc
0450: // that
0451: // are
0452: // in
0453: // the
0454: // pc
0455: addReference(op, sub, so, result);
0456: } else if (t.op() instanceof ArrayOp) {
0457: if (refInPC.contains(t) || postTerms.contains(t)) // TODO??
0458: addIndexReference(t.sub(0), t.sub(1), so,
0459: result);
0460:
0461: } else if (t.op() instanceof ProgramVariable) {
0462: if (refInPC.contains(t) || postTerms.contains(t)) // TODO
0463: // ???//only
0464: // assoc
0465: // that
0466: // are
0467: // in
0468: // the
0469: // pc
0470: addStaticReference((ProgramVariable) t.op(),
0471: so, result);
0472:
0473: }
0474:
0475: }
0476: }
0477:
0478: for (IteratorOfTerm it2 = pc.iterator(); it2.hasNext();) {
0479: Term currentTerm = it2.next();
0480: SetOfTerm locs = collectLocations2(currentTerm);
0481:
0482: for (IteratorOfTerm it3 = locs.iterator(); it3.hasNext();) {
0483:
0484: Term t2 = it3.next();
0485: if (!referenceSort(t2.sort())) {
0486: if (t2.op() instanceof AttributeOp) {
0487: addAttribute(result, (AttributeOp) t2.op(), t2
0488: .sub(0), currentTerm);
0489: } else if (t2.op() instanceof ArrayOp) {
0490: this .addArrayEntry(result, t2.sub(0),
0491: t2.sub(1), currentTerm);
0492: } else if (t2.op() instanceof ProgramVariable) {
0493: ProgramVariable pv = (ProgramVariable) t2.op();
0494: KeYJavaType kjt = pv.getContainerType();
0495: if (kjt != null) {
0496: ClassType ct = (ClassType) kjt
0497: .getJavaType();
0498: this .addStaticAttribute(result, pv, ct,
0499: currentTerm);
0500:
0501: }
0502:
0503: }
0504:
0505: }
0506:
0507: }
0508: }
0509: setInstanceNames(result);
0510: symbolicObjects = result;
0511: }
0512:
0513: private void createSymbolicObjectsForNewInstances(ListOfTerm pre) {
0514: for (IteratorOfTerm it = pre.iterator(); it.hasNext();) {
0515: Term next = it.next();
0516:
0517: if (next.op() instanceof AttributeOp) {
0518: Term sub = next.sub(0);
0519:
0520: if (getObject(sub, this .symbolicObjects) == null) {
0521: symbolicObjects.add(new SymbolicObject(sub,
0522: (ClassType) serv.getJavaInfo()
0523: .getKeYJavaType(sub.sort())
0524: .getJavaType(), this .serv));
0525: }
0526:
0527: }
0528: }
0529:
0530: }
0531:
0532: private boolean disjunct(SetOfTerm s1, SetOfTerm s2) {
0533: for (IteratorOfTerm it = s1.iterator(); it.hasNext();) {
0534: if (s2.contains(it.next()))
0535: return false;
0536: }
0537: return true;
0538: }
0539:
0540: private LinkedList filterStaticObjects(LinkedList objects) {
0541: LinkedList result = new LinkedList();
0542: Iterator it = objects.iterator();
0543: while (it.hasNext()) {
0544: final SymbolicObject so = (SymbolicObject) it.next();
0545: if (!so.isStatic())
0546: result.add(so);
0547: }
0548: return result;
0549: }
0550:
0551: private void findDisjointClasses() {
0552: IteratorOfTerm it = succ.iterator();
0553: while (it.hasNext()) {
0554: Term t = it.next();
0555: EquClass e0, e1;
0556: if (t.op() instanceof Equality /* &&!containsImplicitAttr(t) */) {
0557: e0 = getEqvClass(t.sub(0));
0558: e1 = getEqvClass(t.sub(1));
0559: e0.addDisjoint(t.sub(1));
0560: e1.addDisjoint(t.sub(0));
0561: }
0562: }
0563: }
0564:
0565: public ListOfTerm getConstraints(Term toFind) {
0566: // Term pvTerm = TermFactory.DEFAULT.createVariableTerm(pv);
0567: ListOfTerm result = SLListOfTerm.EMPTY_LIST;
0568: for (IteratorOfTerm it = pc.iterator(); it.hasNext();) {
0569: final Term t = it.next();
0570: OpCollector vis = new OpCollector();
0571: t.execPostOrder(vis);
0572:
0573: if (vis.contains(toFind.op()))
0574: result = result.append(t);
0575:
0576: // System.out.println(vis.);
0577:
0578: }
0579:
0580: return result;
0581:
0582: }
0583:
0584: private EquClass getEqvClass(Term t) {
0585: if (!term2class.containsKey(t)) {
0586: term2class.put(t, new EquClass(t));
0587: }
0588: return (EquClass) term2class.get(t);
0589: }
0590:
0591: public SetOfTerm getIndexTerms() {
0592: return indexTerms;
0593: }
0594:
0595: public EquClass[] getNonPrimitiveLocationEqvClasses() {
0596: Object[] oa = (new HashSet(term2class.values())).toArray();
0597: EquClass[] temp = new EquClass[oa.length];
0598: int l = 0;
0599: for (int i = 0; i < oa.length; i++) {
0600: if (((EquClass) oa[i]).getLocations().size() > 0
0601: && (!((EquClass) oa[i]).isInt() && !((EquClass) oa[i])
0602: .isBoolean())) {
0603: temp[l++] = (EquClass) oa[i];
0604: }
0605: }
0606: EquClass[] result = new EquClass[l];
0607: for (int i = 0; i < l; i++) {
0608: result[i] = temp[i];
0609: }
0610: return result;
0611: }
0612:
0613: private SymbolicObject getObject(Term sub, LinkedList objects) {
0614: Iterator it = objects.iterator();
0615: while (it.hasNext()) {
0616: final SymbolicObject so = (SymbolicObject) it.next();
0617: if (so.getTerms().contains(sub)) {
0618: return so;
0619: }
0620: }
0621: return null;
0622: }
0623:
0624: private ListOfTerm getPc(HashMapFromPosInOccurrenceToLabel labels) {
0625: IteratorOfPosInOccurrence pioIt = labels.keyIterator();
0626: ListOfTerm pc2 = SLListOfTerm.EMPTY_LIST;
0627:
0628: while (pioIt.hasNext()) {
0629: PosInOccurrence pio = pioIt.next();
0630: // PCLabel pcLabel = ((PCLabel)labels.get(pio));
0631: if (!containsJavaBlock(pio.constrainedFormula().formula())) {
0632: Term t = pio.constrainedFormula().formula();
0633: if (pio.isInAntec())
0634: pc2 = pc2.append(t);
0635: else {
0636: if (t.op() == Op.NOT) {
0637: pc2 = pc2.append(t.sub(0));
0638: } else
0639: pc2 = pc2
0640: .append(TermFactory.DEFAULT
0641: .createJunctorTermAndSimplify(
0642: Op.NOT, t));
0643: }
0644:
0645: // pc = pc.append(pio.constrainedFormula().formula());
0646: }
0647:
0648: }
0649: return pc2;
0650: }
0651:
0652: private LinkedList getPossibleIndexTerms(SetOfTerm members) {
0653: LinkedList result = new LinkedList();
0654: if (possibleIndexTerms != null)
0655: for (int i = 0; i < possibleIndexTerms.length; i++) {
0656: SetOfTerm currentIndexTerms = possibleIndexTerms[i];
0657: SetOfTerm locInd = SetAsListOfTerm.EMPTY_SET;
0658: SetOfTerm res = SetAsListOfTerm.EMPTY_SET;
0659:
0660: for (IteratorOfTerm locIt = this .arrayLocations
0661: .iterator(); locIt.hasNext();) {
0662: Term t = locIt.next();
0663: if (members.contains(t.sub(0))) {
0664: locInd = locInd.add(t.sub(1));
0665: }
0666: }
0667:
0668: for (IteratorOfTerm posIndexTermsIt = currentIndexTerms
0669: .iterator(); posIndexTermsIt.hasNext();) {
0670: final Term t = posIndexTermsIt.next();
0671: final Term t2;
0672: if (t.op() == Op.NOT)
0673: t2 = t.sub(0);
0674: else
0675: t2 = t;
0676: if (locInd.contains(t2.sub(0))
0677: && locInd.contains(t2.sub(1)))
0678: res = res.add(t);
0679: }
0680: result.add(res);
0681: }
0682: // VisualDebugger.print("POS INDEX TERMS "+result);
0683: return result;
0684:
0685: }
0686:
0687: private SetOfTerm getPossibleIndexTermsForArray(SetOfTerm members,
0688: SetOfTerm ic) {
0689: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0690:
0691: SetOfTerm currentIndexTerms = ic;
0692: SetOfTerm locInd = SetAsListOfTerm.EMPTY_SET;
0693: for (IteratorOfTerm locIt = this .arrayLocations.iterator(); locIt
0694: .hasNext();) {
0695: Term t = locIt.next();
0696: if (members.contains(t.sub(0))) {
0697: locInd = locInd.add(t.sub(1));
0698: }
0699: }
0700:
0701: for (IteratorOfTerm posIndexTermsIt = currentIndexTerms
0702: .iterator(); posIndexTermsIt.hasNext();) {
0703: final Term t = posIndexTermsIt.next();
0704: final Term t2;
0705: if (t.op() == Op.NOT)
0706: t2 = t.sub(0);
0707: else
0708: t2 = t;
0709: if (locInd.contains(t2.sub(0))
0710: && locInd.contains(t2.sub(1)))
0711: result = result.add(t);
0712: }
0713: // result=(res);
0714:
0715: // VisualDebugger.print("Index terms for member"+ members+" :"+result);
0716: return result;
0717:
0718: }
0719:
0720: // TODO duplicate in statevisualization
0721: private SetOfTerm getReferences(ListOfTerm terms) {
0722: // ListOfTerm pc = itNode.getPc();
0723: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0724: for (IteratorOfTerm it = terms.iterator(); it.hasNext();) {
0725: result = result.union(getReferences2(it.next()));
0726: }
0727: return result;
0728: }
0729:
0730: private SetOfTerm getReferences2(Term t) {
0731: // System.out.println(t);
0732: // if (t.sort()!= Sort.FORMULA && !this.isBool(t)&&!this.isInt(t))
0733:
0734: SetOfTerm result = SetAsListOfTerm.EMPTY_SET;
0735: if (referenceSort(t.sort()))
0736: result = result.add(t);
0737: for (int i = 0; i < t.arity(); i++) {
0738: result = result.union(getReferences2(t.sub(i)));
0739: }
0740: return result;
0741: }
0742:
0743: private int getSerialNumber(SetOfTerm refs) {
0744: int current = -1;
0745:
0746: for (IteratorOfTerm it = refs.iterator(); it.hasNext();) {
0747: final Term t = it.next();
0748: if (ref2ser.containsKey(t)
0749: && ((current == -1) || ((Integer) ref2ser.get(t))
0750: .intValue() < current)) {
0751: current = ((Integer) ref2ser.get(t)).intValue();
0752: }
0753: }
0754:
0755: return current;
0756: }
0757:
0758: private Set getStaticClasses() {
0759: HashSet res = new HashSet();
0760: for (IteratorOfTerm it = this .pc.iterator(); it.hasNext();) {
0761: Term t = it.next();
0762: res.addAll(this .getStaticClasses(t));
0763:
0764: }
0765:
0766: return res;
0767: }
0768:
0769: private Set getStaticClasses(Term t) {
0770: Set result = new HashSet();
0771: if (t.op() instanceof ProgramVariable) {
0772: if (((ProgramVariable) t.op()).getContainerType() != null)
0773: if (!((ProgramVariable) t.op()).isImplicit()
0774: || VisualDebugger.showImpliciteAttr)
0775: result.add(((ProgramVariable) t.op())
0776: .getContainerType().getJavaType());
0777:
0778: }
0779:
0780: for (int i = 0; i < t.arity(); i++) {
0781: result.addAll(getStaticClasses(t.sub(i)));
0782: }
0783: return result;
0784:
0785: }
0786:
0787: private SymbolicObject getStaticObject(ClassType ct,
0788: LinkedList objects) {
0789: final Iterator it = objects.iterator();
0790: while (it.hasNext()) {
0791: final SymbolicObject so = (SymbolicObject) it.next();
0792: if (so.isStatic() && so.getType().equals(ct))
0793: return so;
0794: }
0795: return null;
0796: }
0797:
0798: public LinkedList getSymbolicObjects() {
0799: return symbolicObjects;
0800: }
0801:
0802: // TODO duplicate in prooflistener
0803:
0804: private void prepare(ITNode itNode, Services serv, ListOfTerm pc,
0805: SetOfTerm refInPc) {
0806:
0807: this .vd = VisualDebugger.getVisualDebugger();
0808: this .pc = pc;
0809: // this.node = n;
0810: this .node = itNode.getNode();
0811: this .itNode = itNode;
0812: // this.mediator=mediator;
0813: // mediator = Main.getInstance().mediator();
0814: this .serv = serv;
0815: // goals = mediator.getProof().getSubtreeGoals(node);
0816:
0817: VisualDebugger.print("--------------------------");
0818: VisualDebugger.print("Calculating Equ classes for "
0819: + node.serialNr());
0820:
0821: IteratorOfConstrainedFormula itc = node.sequent().antecedent()
0822: .iterator();
0823: while (itc.hasNext()) {
0824: ante = ante.append(itc.next().formula());
0825: }
0826: itc = node.sequent().succedent().iterator();
0827: succ = SLListOfTerm.EMPTY_LIST;
0828: while (itc.hasNext()) {
0829: succ = succ.append(itc.next().formula());
0830: }
0831:
0832: for (IteratorOfTerm it = this .instanceConfiguration.iterator(); it
0833: .hasNext();) {
0834: final Term t = it.next();
0835: if (t.op() == Op.NOT)
0836: succ = succ.append(t.sub(0));
0837: else
0838: ante = ante.append(t);
0839: }
0840:
0841: this .refInPC = refInPc;
0842:
0843: createEquivalenceClassesAndConstraints();
0844: getEqvClass(nullTerm);
0845: findDisjointClasses();
0846:
0847: Collection cl = term2class.values();
0848: HashSet s = new HashSet(cl);
0849: Iterator it5 = s.iterator();
0850: VisualDebugger.print("All Equi Classses: ");
0851: while (it5.hasNext())
0852: VisualDebugger.print(it5.next());
0853: }
0854:
0855: private boolean referenceSort(Sort s) {
0856: JavaInfo info = serv.getJavaInfo();
0857: KeYJavaType kjt = info.getKeYJavaType(s);
0858: // System.out.println("KJT "+kjt);
0859: if (kjt == null)
0860: return false;
0861: if (kjt.getJavaType() instanceof ClassType)
0862: return true;
0863:
0864: return false;
0865: }
0866:
0867: private void setInstanceNames(LinkedList objects) {
0868: objects = filterStaticObjects(objects);
0869: ref2ser = new HashMap();
0870: ITNode n = this .itNode;
0871: while (n.getParent() != null) {
0872: HashMapFromPosInOccurrenceToLabel labels = n.getNode()
0873: .getNodeInfo().getVisualDebuggerState().getLabels();
0874: ListOfTerm pc2 = getPc(labels);
0875: SetOfTerm refs = getReferences(pc2);
0876: for (IteratorOfTerm it = refs.iterator(); it.hasNext();) {
0877: Term t = it.next();
0878: ref2ser.put(t, new Integer(n.getId()));
0879:
0880: }
0881: n = n.getParent();
0882: }
0883:
0884: // references in post term
0885: int j = 0;
0886: if (postTerms != null)
0887: for (IteratorOfTerm it = postTerms.iterator(); it.hasNext();) {
0888:
0889: Term t = it.next();
0890: // System.out.println("pt "+t);
0891: if (referenceSort(t.sort())) {
0892: if (!ref2ser.containsKey(t)) {
0893: j++;
0894: ref2ser.put(t, new Integer(itNode.getId() + j));
0895:
0896: }
0897: }
0898:
0899: }
0900:
0901: VisualDebugger.print("HashMap for Instance Names");
0902:
0903: if (!vd.isStaticMethod())
0904: ref2ser.put(vd.getInputPV2term().get(
0905: TermFactory.DEFAULT.createVariableTerm(vd
0906: .getSelfPV())), new Integer(1));
0907:
0908: VisualDebugger.print(ref2ser);
0909:
0910: // System.out.println("INPUT VALUES"+inputVal);
0911:
0912: Iterator it2 = objects.iterator();
0913: while (it2.hasNext()) {
0914: SymbolicObject so = (SymbolicObject) it2.next();
0915: so.setId(getSerialNumber(so.getTerms()));
0916: }
0917:
0918: SymbolicObject[] sos = (SymbolicObject[]) objects
0919: .toArray(new SymbolicObject[objects.size()]);
0920:
0921: // sort symbolic objects according to their ids
0922: sort(sos);
0923:
0924: HashMap counters = new HashMap();
0925:
0926: for (int i = 0; i < sos.length; i++) {
0927: SymbolicObject so = sos[i];
0928:
0929: if (so.getId() == -1)
0930: continue;
0931:
0932: Integer newValue;
0933: if (counters.containsKey(so.getType())) {
0934: Integer value = (Integer) counters.get(so.getType());
0935: newValue = new Integer(value.intValue() + 1);
0936: counters.remove(so.getType());
0937: counters.put(so.getType(), newValue);
0938: } else {
0939: newValue = new Integer(0);
0940: counters.put(so.getType(), newValue);
0941:
0942: }
0943:
0944: // instanceName+=newValue.intValue();
0945:
0946: // so.setName(instanceName);
0947:
0948: so.setId(newValue.intValue());
0949:
0950: }
0951:
0952: }
0953:
0954: private void setMethodStack(boolean pre) {
0955: try {
0956: ITNode it = itNode.getMethodNode();
0957: if (it == null) {
0958: return;
0959: }
0960:
0961: MethodBodyStatement mbs = // vd.getLastMethodBodyStatement(itNode.getNode());
0962: (MethodBodyStatement) it.getActStatement();
0963: // MethodBodyStatement mbs =
0964: // vd.getLastMethodBodyStatement(itNode.getNode());
0965: if (mbs == null)
0966: return;
0967: ReferencePrefix refPre = mbs.getMethodReference()
0968: .getReferencePrefix();
0969: SymbolicObject so;
0970:
0971: if (refPre instanceof TypeRef) {
0972: final KeYJavaType kjt = ((TypeRef) refPre)
0973: .getKeYJavaType();
0974: final ClassType type = (ClassType) kjt.getJavaType();
0975: so = getStaticObject(type, symbolicObjects);
0976: if (so == null) {
0977: so = new SymbolicObject(type, serv);
0978: symbolicObjects.add(so);
0979: }
0980:
0981: so.setMethod(mbs.getProgramMethod(serv));
0982:
0983: } else {
0984:
0985: final Term t = serv.getTypeConverter()
0986: .convertToLogicElement(refPre);
0987: methodReferences = new Term[1];
0988: methodReferences[0] = t;
0989: // System.out.println("AAAAAAAAAAAAAAAAAAAAAA "+t);
0990: HashMap map = new HashMap();
0991: Term self = vd.getSelfTerm();
0992: // vd.getSelfTerm() //TODO
0993: // ProgramVariable val =
0994: // (ProgramVariable)((Term)vd.getInputPV2term().get(self)).op();
0995: Term val = ((Term) vd.getInputPV2term().get(self));
0996: map.put(self.op(), val);
0997: ProgVarReplacer pvr = new ProgVarReplacer(map);
0998: Term res = pvr.replace(t);
0999:
1000: so = getObject(res, symbolicObjects);
1001: so.setMethod(mbs.getProgramMethod(serv));
1002:
1003: }
1004:
1005: // ArrayOfExpression aof = mbs.getArguments();;
1006: HashSet set = vd.getParam(mbs);
1007: ListOfProgramVariable inputPara = vd
1008: .arrayOfExpression2ListOfProgVar(
1009: mbs.getArguments(), 0);
1010: ProgramVariable[] inputParaArray = inputPara.toArray();
1011:
1012: ArrayOfParameterDeclaration paraDecl = mbs
1013: .getProgramMethod(serv).getParameters();
1014:
1015: final HashMap values = vd.getValuesForLocation(set, vd
1016: .getProgramPIO(itNode.getNode().sequent()));
1017:
1018: ListOfProgramVariable paramDeclAsPVList = SLListOfProgramVariable.EMPTY_LIST;
1019:
1020: for (int i = 0; i < paraDecl.size(); i++) {
1021: ProgramVariable next = (ProgramVariable) paraDecl
1022: .getParameterDeclaration(i)
1023: .getVariableSpecification()
1024: .getProgramVariable();
1025: Term val = (Term) values.get(TermFactory.DEFAULT
1026: .createVariableTerm(inputParaArray[i]));// TODO
1027: so.addPara2Value(next, val);
1028: paramDeclAsPVList = paramDeclAsPVList.append(next);
1029: }
1030: so.setParameter(paramDeclAsPVList);
1031:
1032: } catch (Exception e) {
1033: return;
1034:
1035: }
1036:
1037: }
1038:
1039: private void sort(SymbolicObject a[]) {
1040:
1041: int n = a.length;
1042: SymbolicObject temp;
1043:
1044: for (int i = 0; i < n - 1; i = i + 1)
1045: for (int j = n - 1; j > i; j = j - 1)
1046: if (a[j - 1].getId() > a[j].getId()) {
1047: temp = a[j - 1];
1048: a[j - 1] = a[j];
1049: a[j] = temp;
1050: }
1051: }
1052:
1053: private class EquClass {
1054: private SetOfTerm disjointRep = SetAsListOfTerm.EMPTY_SET;
1055:
1056: private SetOfTerm members;
1057:
1058: public EquClass(SetOfTerm members) {
1059: this .members = members;
1060: }
1061:
1062: public EquClass(Term t) {
1063: this (SetAsListOfTerm.EMPTY_SET.add(t));
1064: }
1065:
1066: public EquClass(Term t1, Term t2) {
1067: this (SetAsListOfTerm.EMPTY_SET.add(t1).add(t2));
1068: }
1069:
1070: public void add(EquClass ec) {
1071: members = members.union(ec.getMembers());
1072: }
1073:
1074: public void add(Term t) {
1075: members = members.add(t);
1076: }
1077:
1078: public void addDisjoint(Term t) {
1079: disjointRep = disjointRep.add(t);
1080: }
1081:
1082: public boolean equals(Object o) {
1083: if (!(o instanceof EquClass)) {
1084: return false;
1085: }
1086: EquClass eqc = (EquClass) o;
1087: if (eqc.members.size() != members.size()) {
1088: return false;
1089: }
1090: IteratorOfTerm it = members.iterator();
1091: l: while (it.hasNext()) {
1092: IteratorOfTerm it2 = eqc.members.iterator();
1093: Term t = it.next();
1094: while (it2.hasNext()) {
1095: if (t.toString().equals(it2.next().toString())) {
1096: continue l;
1097: }
1098: }
1099: return false;
1100: }
1101: return true;
1102: }
1103:
1104: public SetOfTerm getDisjoints() {
1105: return disjointRep;
1106: }
1107:
1108: public KeYJavaType getKeYJavaType() {
1109: IteratorOfTerm it = members.iterator();
1110: Sort s = it.next().sort();
1111: while (it.hasNext()) {
1112: Sort s1 = it.next().sort();
1113: if (s1.extendsTrans(s)) {
1114: s = s1;
1115: }
1116: }
1117: KeYJavaType result = serv.getJavaInfo().getKeYJavaType(s);
1118: if (result == null && isInt(s)) {
1119: result = serv.getJavaInfo().getKeYJavaType(
1120: serv.getTypeConverter().getIntLDT()
1121: .targetSort());
1122: }
1123: return result;
1124: }
1125:
1126: /**
1127: * Returns the locations that are members of this equivalence class.
1128: */
1129: public SetOfTerm getLocations() {
1130: SetOfTerm locations = SetAsListOfTerm.EMPTY_SET;
1131: IteratorOfTerm it = members.iterator();
1132: while (it.hasNext()) {
1133: Term t = it.next();
1134: if (ModelGenerator.isLocation(t, serv)) {
1135: locations = locations.add(t);
1136: }
1137: }
1138: return locations;
1139: }
1140:
1141: public SetOfTerm getMembers() {
1142: return members;
1143: }
1144:
1145: public boolean isArray() {
1146: for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1147: Term t = it.next();
1148: return isArraySort(t.sort());
1149: }
1150: return false;
1151: }
1152:
1153: private boolean isArraySort(Sort s) {
1154:
1155: return (s instanceof ArraySort);
1156: }
1157:
1158: public boolean isBoolean() {
1159: for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1160: if (serv.getTypeConverter().getBooleanLDT()
1161: .targetSort() == it.next().sort()) {
1162: return true;
1163: }
1164: }
1165: return false;
1166: }
1167:
1168: public boolean isInt() {
1169: for (IteratorOfTerm it = members.iterator(); it.hasNext();) {
1170: Term t = it.next();
1171: return isInt(t.sort());
1172: }
1173: return false;
1174: }
1175:
1176: private boolean isInt(Sort s) {
1177: return s.extendsTrans(serv.getTypeConverter()
1178: .getIntegerLDT().targetSort());
1179: }
1180:
1181: public String toString() {
1182: return "EquClass: (" + members + ") Disjoint + "
1183: + this .disjointRep + " /";
1184: }
1185:
1186: }
1187: }
|