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.Collection;
011: import java.util.HashMap;
012: import java.util.Iterator;
013: import java.util.Set;
014:
015: import de.uka.ilkd.key.java.Services;
016: import de.uka.ilkd.key.java.abstraction.ClassType;
017: import de.uka.ilkd.key.java.abstraction.NullType;
018: import de.uka.ilkd.key.logic.*;
019: import de.uka.ilkd.key.logic.op.*;
020: import de.uka.ilkd.key.visualdebugger.VisualDebugger;
021:
022: public class SymbolicObject {
023:
024: private final HashMap associations = new HashMap();
025:
026: private final HashMap attr2Constraint = new HashMap();
027:
028: private HashMap attr2ValueTerm = new HashMap();
029:
030: private int id;
031:
032: private String instanceName;
033:
034: private boolean isStatic = false;
035:
036: private ProgramMethod method = null;
037:
038: private HashMap par2constraint = new HashMap();
039:
040: private HashMap par2value = new HashMap();
041:
042: private ListOfProgramVariable parameter;
043:
044: private final SetOfTerm terms;
045:
046: private final ClassType type;
047:
048: private boolean unknownObject = false;
049:
050: VisualDebugger vd = VisualDebugger.getVisualDebugger();
051:
052: public SymbolicObject(ClassType t, Services s) {
053: this .type = t;
054: this .terms = SetAsListOfTerm.EMPTY_SET;
055: this .isStatic = true;
056: this .computeInstanceName();
057: }
058:
059: public SymbolicObject(SetOfTerm cl, ClassType t, Services s) {
060: this .terms = cl;
061: assert cl != null && t != null && s != null;
062: type = t;
063: computeInstanceName();
064: }
065:
066: public SymbolicObject(Term cl, ClassType t, Services s) {
067: this (SetAsListOfTerm.EMPTY_SET.add(cl), t, s);
068: }
069:
070: public SymbolicObject(Term cl, ClassType t, Services s,
071: boolean unKnown) {
072: this (SetAsListOfTerm.EMPTY_SET.add(cl), t, s);
073: this .unknownObject = unKnown;
074: }
075:
076: public void addAssociation(IProgramVariable f, SymbolicObject o) {
077: associations.put(f, o);
078:
079: }
080:
081: public void addAttributeConstraint(ProgramVariable f, Term o) {
082: if (attr2Constraint.containsKey(f)) {
083: ListOfTerm t = (ListOfTerm) attr2Constraint.get(f);
084: t = t.append(o);
085: attr2Constraint.remove(f);
086: attr2Constraint.put(f, t);
087:
088: } else {
089: ListOfTerm t = SLListOfTerm.EMPTY_LIST.append(o);
090: attr2Constraint.put(f, t);
091: }
092:
093: }
094:
095: /**
096: *
097: * @param par
098: * parameter pv
099: * @param value
100: * instanceof SymbolicObject or Term
101: */
102: public void addPara2Value(ProgramVariable par, Object value) {
103: this .par2value.put(par, value);
104: }
105:
106: public void addParameterConstraint(ProgramVariable f, ListOfTerm o) {
107: if (this .par2constraint.containsKey(f)) {
108: ListOfTerm t = (ListOfTerm) par2constraint.get(f);
109: t = t.append(o);
110: par2constraint.remove(f);
111: par2constraint.put(f, t);
112: } else {
113: ListOfTerm t = SLListOfTerm.EMPTY_LIST.append(o);
114: par2constraint.put(f, t);
115: }
116: }
117:
118: public void addParameterConstraint(ProgramVariable f, Term o) {
119: if (this .par2constraint.containsKey(f)) {
120: ListOfTerm t = (ListOfTerm) par2constraint.get(f);
121: t = t.append(o);
122: par2constraint.remove(f);
123: par2constraint.put(f, t);
124: } else {
125: ListOfTerm t = SLListOfTerm.EMPTY_LIST.append(o);
126: par2constraint.put(f, t);
127: }
128: }
129:
130: public void addValueTerm(ProgramVariable pv, Term val) {
131: attr2ValueTerm.put(pv, val);
132: }
133:
134: private void computeInstanceName() {
135: if (isStatic()) {
136: this .instanceName = "<Class>";
137:
138: } else if (!vd.isStaticMethod()
139: && terms.contains((Term) VisualDebugger
140: .getVisualDebugger().getInputPV2term().get(
141: vd.getSelfTerm()))) {
142: this .instanceName = "self";
143:
144: } else if (id == -1) {
145:
146: }
147:
148: else {
149: final String className = getType().getName().toString();
150: final String b = className.substring(0, 1).toLowerCase();
151: instanceName = b
152: + className.substring(1, className.length());
153: instanceName += "_" + id;
154: }
155: }
156:
157: public Collection getAllAssociationEnds() {
158: return this .associations.values();
159:
160: }
161:
162: public SetOfProgramVariable getAllModifiedPrimitiveAttributes() {
163: SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
164: Set s = attr2ValueTerm.keySet();
165: for (Iterator it = s.iterator(); it.hasNext();) {
166: result = result.add((ProgramVariable) it.next());
167: }
168: return result;
169: }
170:
171: public SymbolicObject getAssociationEnd(ProgramVariable f) {
172: return (SymbolicObject) associations.get(f);
173: }
174:
175: public ListOfTerm getAttrConstraints(ProgramVariable f) {
176: return (ListOfTerm) attr2Constraint.get(f);
177: }
178:
179: public SetOfProgramVariable getAttributes() {
180: SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
181: Set s = attr2Constraint.keySet();
182: for (Iterator it = s.iterator(); it.hasNext();) {
183: result = result.add((ProgramVariable) it.next());
184: }
185: return result;
186: }
187:
188: public int getId() {
189: return id;
190: }
191:
192: public String getInstanceName() {
193: return this .instanceName;
194: }
195:
196: public ProgramMethod getMethod() {
197: return method;
198: }
199:
200: public SetOfProgramVariable getNonPrimAttributes() {
201: SetOfProgramVariable result = SetAsListOfProgramVariable.EMPTY_SET;
202: Set s = associations.keySet();
203: for (Iterator it = s.iterator(); it.hasNext();) {
204: result = result.add((ProgramVariable) it.next());
205: }
206: return result;
207: }
208:
209: public ListOfTerm getParaConstraints(ProgramVariable f) {
210: return (ListOfTerm) this .par2constraint.get(f);
211: }
212:
213: public ListOfProgramVariable getParameter() {
214: return parameter;
215: }
216:
217: // ------------------------------------------------------------------
218: // Methods for post state
219:
220: public SetOfTerm getTerms() {
221: return terms;
222: }
223:
224: public ClassType getType() {
225: return type;
226: }
227:
228: /**
229: *
230: * @param para
231: * @return instanceof SymbolicObject or Term
232: */
233: public Term getValueOfParameter(ProgramVariable para) {
234: return (Term) par2value.get(para);
235:
236: }
237:
238: public Term getValueTerm(ProgramVariable pv) {
239: return (Term) this .attr2ValueTerm.get(pv);
240: }
241:
242: public boolean isNull() {
243: return (type instanceof NullType);
244: }
245:
246: public boolean isStatic() {
247: return isStatic;
248: }
249:
250: public boolean isUnknownObject() {
251: return unknownObject;
252: }
253:
254: // public void setName(String name) {
255: // this.name = name;
256: // }
257: //
258: public void setId(int id) {
259: this .id = id;
260: this .computeInstanceName();
261: }
262:
263: public void setMethod(ProgramMethod method) {
264: this .method = method;
265: }
266:
267: public void setParameter(ListOfProgramVariable parameter) {
268: this .parameter = parameter;
269: }
270:
271: public String toString() {
272: String result = "Symbolic Object " + this .instanceName + " ";
273: result += "Members " + terms;
274:
275: return result;
276:
277: }
278:
279: }
|