Area


1   //
2   // Copyright (C) 2005 United States Government as represented by the
3   // Administrator of the National Aeronautics and Space Administration
4   // (NASA).  All Rights Reserved.
5   // 
6   // This software is distributed under the NASA Open Source Agreement
7   // (NOSA), version 1.3.  The NOSA has been approved by the Open Source
8   // Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
9   // directory tree for the complete NOSA document.
10  // 
11  // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12  // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13  // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14  // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15  // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16  // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17  // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18  //
19  package gov.nasa.jpf.jvm;
20  
21  import gov.nasa.jpf.JPFException;
22  import gov.nasa.jpf.util.HashData;
23  
24  import java.util.BitSet  ;
25  import java.util.NoSuchElementException  ;
26  
27  /**
28   * Area defines a memory class. An area can be used for objects
29   * in the DynamicArea (heap) or classes in the StaticArea (classinfo with
30   * static fields).
31   */
32  public abstract class Area implements Storable {
33    /**
34     * The number of entries per element. Has to be set by our concrete subclasses!
35     */
36    private final int delta;
37  
38    /**
39     * Contains the information for each element.
40     */
41    protected ElementInfo[] elements;
42  
43    /**
44     * The number of elements. It can differ from the
45     * size of the elements array.
46     */
47    private int nElements;
48  
49    /**
50     * Last used element.
51     */
52    private int lastElement;
53  
54    /**
55     * Reference of the kernel state this dynamic area is in.
56     */
57    public KernelState ks;
58  
59    /**
60     * Set of bits used to see which elements has changed.
61     */
62    public BitSet   hasChanged;
63  
64    /**
65     * Set if any element is changed (includes has been added or removed)
66     */
67    public boolean anyChanged;
68  
69    /**
70     * Contains the data from the last call to get storing data.
71     */
72    public int[] data;
73  
74    /**
75     * very simplistic iterator so that clients can abstract away from
76     * our internal heap representation during Object enumeration
77     */
78    public class Iterator implements java.util.Iterator   {
79      int i, visited;
80      
81      public void remove() {
82        throw new UnsupportedOperationException   ("illegal operation, only GC can remove objects");
83      }
84      
85      public boolean hasNext() {
86        return (i < elements.length) && (visited < nElements);
87      }
88      
89      public Object   next() {
90        for (; i<elements.length; i++) {
91          ElementInfo ei = elements[i];
92          if (ei != null) {
93            i++; visited++;
94            return ei;
95          }
96        }
97        
98        throw new NoSuchElementException  ();
99      }
100   }
101   
102   public Area (KernelState ks, int elementLength) {
103     this.ks = ks;
104     elements = new ElementInfo[0];
105     nElements = 0;
106     lastElement = -1;
107     hasChanged = new BitSet  ();
108     anyChanged = false;
109     data = new int[0];
110 
111     delta = elementLength;
112   }
113 
114   protected Area (Area a) {
115     int l = a.elements.length;
116     elements = new ElementInfo[l];
117 
118     for (int i = 0; i < l; i++) {
119       if (a.elements[i] != null) {
120         elements[i] = (ElementInfo) a.elements[i].clone();
121         elements[i].setArea(this);
122         elements[i].setIndex(i);
123       } else {
124         elements[i] = null;
125       }
126     }
127 
128     delta = a.delta;
129 
130     nElements = a.nElements;
131     lastElement = a.lastElement;
132     ks = null;
133     hasChanged = (BitSet  ) a.hasChanged.clone();
134     anyChanged = a.anyChanged;
135     l = a.data.length;
136     data = new int[l];
137     System.arraycopy(a.data, 0, data, 0, l);
138   }
139 
140   /**
141    * Is this the static area?
142    * <2do> pcm - there's something called 'method overriding', which is supposed
143    * to be used to overcome type flags..
144    */
145   public abstract boolean isStatic ();
146 
147   public Iterator iterator() {
148     return new Iterator();
149   }
150   
151   public Object   getBacktrackData () {
152     // <2do> - check if this obsolete now that race analysis is done externally 
153     int      length = elements.length;
154     Object  [] data = new Object  [length];
155 
156     return data;
157   }
158 
159   public int[] getStoringData () {
160     if (!anyChanged) {
161       return data;
162     }
163 
164     int length = lastElement + 1;
165     int size = length * delta;
166     int s = data.length - 1;
167 
168     if (s != size) {
169       if (s > size) {
170         s = size;
171       }
172 
173       int[] n = new int[size + 1];
174 
175       if (s > 0) {
176         System.arraycopy(data, 1, n, 1, s);
177       }
178 
179       data = n;
180     }
181 
182     data[0] = length;
183 
184     for (int i = 0, j = 1; i < length; i++, j += delta) {
185       if (elements[i] == null) {
186         int l = j;
187         int l1 = j + delta;
188 
189         for (; l < l1; l++) {
190           data[l] = 0;
191         }
192       } else if (hasChanged.get(i)) {
193         elements[i].storeDataTo(data, j);
194       }
195     }
196 
197     anyChanged = false;
198     hasChanged = new BitSet  ();
199 
200     return data;
201   }
202 
203   /**
204    * reset any information that has to be re-computed in a backtrack
205    * (i.e. hasn't been stored explicitly)
206    */
207   void resetVolatiles () {
208     // nothing yet
209   }
210   
211   public void backtrackTo (ArrayOffset storing, Object   backtrack) {
212     Object  [] b = (Object  []) backtrack;
213     int      length = storing.get();
214     int      l = elements.length;
215     int      s = length * delta;
216 
217     resetVolatiles();
218     
219     if (data.length != (s + 1)) {
220       data = new int[s + 1];
221     }
222 
223     if (s > 0) {
224       System.arraycopy(storing.data, storing.offset, data, 1, s);
225     }
226 
227     anyChanged = false;
228     hasChanged = new BitSet  ();
229     data[0] = length;
230 
231     lastElement = length - 1;
232 
233     if (length != l) {
234       if (l > length) {
235         l = length;
236       }
237 
238       ElementInfo[] n = new ElementInfo[length];
239       System.arraycopy(elements, 0, n, 0, l);
240 
241       elements = n;
242     }
243 
244     for (int i = 0; i < length; i++) {
245       ElementInfo e = elements[i];
246 
247       if (storing.peek() != 0) {
248         if (e == null) {
249           e = elements[i] = createElementInfo();
250           e.setArea(this);
251           e.setIndex(i);
252         }
253 
254         e.backtrackTo(storing, b[i]);
255       } else {
256         elements[i] = null;
257 
258         for (int j = 0; j < delta; j++) {
259           storing.get();
260         }
261       }
262     }
263   }
264 
265   public int count () {
266     return nElements;
267   }
268 
269   public ElementInfo get (int index) {
270     if ((index < 0) || (elements.length <= index)) {
271       return null;
272     }
273 
274     return elements[index];
275   }
276 
277   public void hash (HashData hd) {
278     int length = elements.length;
279 
280     for (int i = 0; i < length; i++) {
281       if (elements[i] != null) {
282         elements[i].hash(hd);
283       }
284     }
285   }
286 
287   public int hashCode () {
288     HashData hd = new HashData();
289 
290     hash(hd);
291 
292     return hd.getValue();
293   }
294 
295   public void removeAll () {
296     int l = elements.length;
297 
298     for (int i = 0; i < l; i++) {
299       if (elements[i] != null) {
300         remove(i);
301       }
302     }
303   }
304 
305   // BUG! nElements is not consistent with the elements array length
306   // somtimes it seems to be bigger: also not conistent with lastElement
307   protected void add (int index, ElementInfo e) {
308     e.setArea(this);
309     e.setIndex(index);
310 
311     if (index >= elements.length) {
312       ElementInfo[] n = new ElementInfo[index + 10];
313       System.arraycopy(elements, 0, n, 0, elements.length);
314       elements = n;
315     }
316 
317     if (index > lastElement) {
318       lastElement = index;
319     }
320 
321     // We'll increment the count only if we're not overwriting an old element
322     // <?> pcm - why do we ever overwrite a non-null entry ?
323     if (elements[index] == null) {
324       nElements++;
325     } else {
326       // <?> pcm - this sounds too suspicious for me, cry fool here
327       // ..right so. Turned out that was the "silent fix" for recursive
328       // inits leading to multiple static inits of the same class
329       throw new JPFException("overwriting non-null object reference: " + index);
330     }
331 
332     elements[index] = e;
333     hasChanged.set(index);
334     anyChanged = true;
335     ks.data = null;
336   }
337 
338   protected void remove (int index) {
339     elements[index].setArea(null);
340     elements[index].setIndex(-1);
341     elements[index] = null;
342     nElements--;
343     hasChanged.set(index);
344     anyChanged = true;
345 
346     if (lastElement == index) {
347       while ((lastElement >= 0) && (elements[lastElement] == null)) {
348         lastElement--;
349       }
350     }
351 
352     ks.data = null;
353   }
354 
355   abstract ElementInfo createElementInfo ();
356 }
357
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags