KernelState


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.Config;
22  import gov.nasa.jpf.util.CoverageManager;
23  import gov.nasa.jpf.util.Debug;
24  import gov.nasa.jpf.util.HashData;
25  
26  
27  /**
28   * This class represents the stack of the JVM.
29   */
30  public class KernelState implements Storable {
31    /**
32     * The area containing the classes.
33     */
34    public StaticArea sa;
35  
36    /**
37     * The area containing the objects.
38     */
39    public DynamicArea da;
40  
41    /**
42     * The list of the threads.
43     */
44    public ThreadList tl;
45  
46    /**
47     * Link to the system state.
48     */
49    public SystemState ss;
50  
51    /**
52     * Number of nested atomic blocks.
53     */
54    public int atomicLevel;
55  
56    /**
57     * True if the last was an intermediate step (non-deterministic)
58     * <?> pcm - does that mean we don't store any data for this state, e.g.
59     *     to make sure we don't treat it as visited?
60     */
61    private boolean intermediateStep;
62  
63    /**
64     * Thread that made stopped at an intermediate step.
65     */
66    private int intermediateThread;
67  
68    /**
69     * The data returned by last get data.
70     */
71    public int[] data;
72    
73    /**
74     * Creates a new kernel state object.
75     */
76    public KernelState (Config config, SystemState system_state) {
77      sa = new StaticArea(config,this);
78      da = new DynamicArea(config,this);
79      tl = new ThreadList(config,this);
80      
81      ss = system_state;
82      atomicLevel = 0;
83      intermediateStep = false;
84      intermediateThread = -1;
85      data = null;
86    }
87  
88    public void setAtomic () {
89      atomicLevel++;
90    }
91  
92    public Object   getBacktrackData () {
93      Object  [] data = new Object  [6];
94  
95      data[0] = sa.getBacktrackData();
96      data[1] = da.getBacktrackData();
97      data[2] = tl.getBacktrackData();
98      data[3] = new Integer  (atomicLevel);
99      data[4] = new Boolean  (intermediateStep);
100     data[5] = new Integer  (intermediateThread);
101     
102     return data;
103   }
104 
105   public void setIntermediate () {
106     intermediateStep = true;
107     intermediateThread = ss.getScheduler().getThread();
108   }
109 
110   public boolean isIntermediate () {
111     return intermediateStep;
112   }
113 
114   public int getIntermediateThread () {
115     return intermediateThread;
116   }
117 
118   public int[] getStoringData () {
119     if (data != null) {
120       return data;
121     }
122 
123     int[] tlData = tl.getStoringData();
124     int[] saData = sa.getStoringData();
125     int[] daData = da.getStoringData();
126 
127     int   sal = saData.length;
128     int   dal = daData.length;
129     int   tll = tlData.length;
130 
131     data = new int[sal + dal + tll];
132 
133     System.arraycopy(tlData, 0, data, 0, tll);
134     System.arraycopy(saData, 0, data, tll, sal);
135     System.arraycopy(daData, 0, data, tll+sal, dal);
136 
137     return data;
138   }
139 
140   /**
141    * The program is terminated if there are no alive threads.
142    */
143   public boolean isTerminated () {
144     return !tl.anyAliveThread();
145   }
146 
147   public int getThreadCount () {
148     return tl.length();
149   }
150 
151   public ThreadInfo getThreadInfo (int index) {
152     return tl.get(index);
153   }
154 
155   
156   public void backtrackTo (ArrayOffset storing, Object   backtrack) {
157     
158     // we need to restore the Thread list first, since objects (ElementInfos)
159     // might refer to it (e.g. when re-computing volatiles)
160     tl.backtrackTo(storing, ((Object  []) backtrack)[2]);
161 
162     sa.backtrackTo(storing, ((Object  []) backtrack)[0]);
163     da.backtrackTo(storing, ((Object  []) backtrack)[1]);
164     
165     atomicLevel = ((Integer  ) ((Object  []) backtrack)[3]).intValue();
166     intermediateStep = ((Boolean  ) ((Object  []) backtrack)[4]).booleanValue();
167     intermediateThread = ((Integer  ) ((Object  []) backtrack)[5]).intValue();
168     data = storing.data;
169   }
170 
171   public void clearAtomic () {
172     atomicLevel--;
173   }
174 
175   public void clearIntermediate () {
176     intermediateStep = false;
177     intermediateThread = -1;
178   }
179 
180   public void gc () {
181     da.gc();
182   }
183 
184   public void hash (HashData hd) {
185     da.hash(hd);
186     sa.hash(hd);
187 
188     for (int i = 0, l = tl.length(); i < l; i++) {
189       tl.get(i).hash(hd);
190     }
191   }
192 
193   public ThreadList getThreadList () {
194     return tl;
195   }
196   
197   public int hashCode () {
198     HashData hd = new HashData();
199 
200     hash(hd);
201 
202     return hd.getValue();
203   }
204 
205   public void log () {
206     da.log();
207     sa.log();
208 
209     for (int i = 0; i < tl.length(); i++) {
210       tl.get(i).log();
211     }
212 
213     Debug.println(Debug.MESSAGE);
214   }
215   
216   void addThread (ThreadInfo ti) {
217     tl.add(tl.length(), ti);
218     CoverageManager.addThread(ti.index);    
219   }
220 }
221
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags