001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import gov.nasa.jpf.JPFException;
022: import gov.nasa.jpf.util.HashData;
023:
024: import java.util.BitSet;
025: import java.util.NoSuchElementException;
026:
027: /**
028: * Area defines a memory class. An area can be used for objects
029: * in the DynamicArea (heap) or classes in the StaticArea (classinfo with
030: * static fields).
031: */
032: public abstract class Area implements Storable {
033: /**
034: * The number of entries per element. Has to be set by our concrete subclasses!
035: */
036: private final int delta;
037:
038: /**
039: * Contains the information for each element.
040: */
041: protected ElementInfo[] elements;
042:
043: /**
044: * The number of elements. It can differ from the
045: * size of the elements array.
046: */
047: private int nElements;
048:
049: /**
050: * Last used element.
051: */
052: private int lastElement;
053:
054: /**
055: * Reference of the kernel state this dynamic area is in.
056: */
057: public KernelState ks;
058:
059: /**
060: * Set of bits used to see which elements has changed.
061: */
062: public BitSet hasChanged;
063:
064: /**
065: * Set if any element is changed (includes has been added or removed)
066: */
067: public boolean anyChanged;
068:
069: /**
070: * Contains the data from the last call to get storing data.
071: */
072: public int[] data;
073:
074: /**
075: * very simplistic iterator so that clients can abstract away from
076: * our internal heap representation during Object enumeration
077: */
078: public class Iterator implements java.util.Iterator {
079: int i, visited;
080:
081: public void remove() {
082: throw new UnsupportedOperationException(
083: "illegal operation, only GC can remove objects");
084: }
085:
086: public boolean hasNext() {
087: return (i < elements.length) && (visited < nElements);
088: }
089:
090: public Object next() {
091: for (; i < elements.length; i++) {
092: ElementInfo ei = elements[i];
093: if (ei != null) {
094: i++;
095: visited++;
096: return ei;
097: }
098: }
099:
100: throw new NoSuchElementException();
101: }
102: }
103:
104: public Area(KernelState ks, int elementLength) {
105: this .ks = ks;
106: elements = new ElementInfo[0];
107: nElements = 0;
108: lastElement = -1;
109: hasChanged = new BitSet();
110: anyChanged = false;
111: data = new int[0];
112:
113: delta = elementLength;
114: }
115:
116: protected Area(Area a) {
117: int l = a.elements.length;
118: elements = new ElementInfo[l];
119:
120: for (int i = 0; i < l; i++) {
121: if (a.elements[i] != null) {
122: elements[i] = (ElementInfo) a.elements[i].clone();
123: elements[i].setArea(this );
124: elements[i].setIndex(i);
125: } else {
126: elements[i] = null;
127: }
128: }
129:
130: delta = a.delta;
131:
132: nElements = a.nElements;
133: lastElement = a.lastElement;
134: ks = null;
135: hasChanged = (BitSet) a.hasChanged.clone();
136: anyChanged = a.anyChanged;
137: l = a.data.length;
138: data = new int[l];
139: System.arraycopy(a.data, 0, data, 0, l);
140: }
141:
142: /**
143: * Is this the static area?
144: * <2do> pcm - there's something called 'method overriding', which is supposed
145: * to be used to overcome type flags..
146: */
147: public abstract boolean isStatic();
148:
149: public Iterator iterator() {
150: return new Iterator();
151: }
152:
153: public Object getBacktrackData() {
154: // <2do> - check if this obsolete now that race analysis is done externally
155: int length = elements.length;
156: Object[] data = new Object[length];
157:
158: return data;
159: }
160:
161: public int[] getStoringData() {
162: if (!anyChanged) {
163: return data;
164: }
165:
166: int length = lastElement + 1;
167: int size = length * delta;
168: int s = data.length - 1;
169:
170: if (s != size) {
171: if (s > size) {
172: s = size;
173: }
174:
175: int[] n = new int[size + 1];
176:
177: if (s > 0) {
178: System.arraycopy(data, 1, n, 1, s);
179: }
180:
181: data = n;
182: }
183:
184: data[0] = length;
185:
186: for (int i = 0, j = 1; i < length; i++, j += delta) {
187: if (elements[i] == null) {
188: int l = j;
189: int l1 = j + delta;
190:
191: for (; l < l1; l++) {
192: data[l] = 0;
193: }
194: } else if (hasChanged.get(i)) {
195: elements[i].storeDataTo(data, j);
196: }
197: }
198:
199: anyChanged = false;
200: hasChanged = new BitSet();
201:
202: return data;
203: }
204:
205: /**
206: * reset any information that has to be re-computed in a backtrack
207: * (i.e. hasn't been stored explicitly)
208: */
209: void resetVolatiles() {
210: // nothing yet
211: }
212:
213: public void backtrackTo(ArrayOffset storing, Object backtrack) {
214: Object[] b = (Object[]) backtrack;
215: int length = storing.get();
216: int l = elements.length;
217: int s = length * delta;
218:
219: resetVolatiles();
220:
221: if (data.length != (s + 1)) {
222: data = new int[s + 1];
223: }
224:
225: if (s > 0) {
226: System.arraycopy(storing.data, storing.offset, data, 1, s);
227: }
228:
229: anyChanged = false;
230: hasChanged = new BitSet();
231: data[0] = length;
232:
233: lastElement = length - 1;
234:
235: if (length != l) {
236: if (l > length) {
237: l = length;
238: }
239:
240: ElementInfo[] n = new ElementInfo[length];
241: System.arraycopy(elements, 0, n, 0, l);
242:
243: elements = n;
244: }
245:
246: for (int i = 0; i < length; i++) {
247: ElementInfo e = elements[i];
248:
249: if (storing.peek() != 0) {
250: if (e == null) {
251: e = elements[i] = createElementInfo();
252: e.setArea(this );
253: e.setIndex(i);
254: }
255:
256: e.backtrackTo(storing, b[i]);
257: } else {
258: elements[i] = null;
259:
260: for (int j = 0; j < delta; j++) {
261: storing.get();
262: }
263: }
264: }
265: }
266:
267: public int count() {
268: return nElements;
269: }
270:
271: public ElementInfo get(int index) {
272: if ((index < 0) || (elements.length <= index)) {
273: return null;
274: }
275:
276: return elements[index];
277: }
278:
279: public void hash(HashData hd) {
280: int length = elements.length;
281:
282: for (int i = 0; i < length; i++) {
283: if (elements[i] != null) {
284: elements[i].hash(hd);
285: }
286: }
287: }
288:
289: public int hashCode() {
290: HashData hd = new HashData();
291:
292: hash(hd);
293:
294: return hd.getValue();
295: }
296:
297: public void removeAll() {
298: int l = elements.length;
299:
300: for (int i = 0; i < l; i++) {
301: if (elements[i] != null) {
302: remove(i);
303: }
304: }
305: }
306:
307: // BUG! nElements is not consistent with the elements array length
308: // somtimes it seems to be bigger: also not conistent with lastElement
309: protected void add(int index, ElementInfo e) {
310: e.setArea(this );
311: e.setIndex(index);
312:
313: if (index >= elements.length) {
314: ElementInfo[] n = new ElementInfo[index + 10];
315: System.arraycopy(elements, 0, n, 0, elements.length);
316: elements = n;
317: }
318:
319: if (index > lastElement) {
320: lastElement = index;
321: }
322:
323: // We'll increment the count only if we're not overwriting an old element
324: // <?> pcm - why do we ever overwrite a non-null entry ?
325: if (elements[index] == null) {
326: nElements++;
327: } else {
328: // <?> pcm - this sounds too suspicious for me, cry fool here
329: // ..right so. Turned out that was the "silent fix" for recursive
330: // inits leading to multiple static inits of the same class
331: throw new JPFException(
332: "overwriting non-null object reference: " + index);
333: }
334:
335: elements[index] = e;
336: hasChanged.set(index);
337: anyChanged = true;
338: ks.data = null;
339: }
340:
341: protected void remove(int index) {
342: elements[index].setArea(null);
343: elements[index].setIndex(-1);
344: elements[index] = null;
345: nElements--;
346: hasChanged.set(index);
347: anyChanged = true;
348:
349: if (lastElement == index) {
350: while ((lastElement >= 0)
351: && (elements[lastElement] == null)) {
352: lastElement--;
353: }
354: }
355:
356: ks.data = null;
357: }
358:
359: abstract ElementInfo createElementInfo();
360: }
|