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.Config;
022: import gov.nasa.jpf.util.CoverageManager;
023: import gov.nasa.jpf.util.Debug;
024: import gov.nasa.jpf.util.HashData;
025:
026: /**
027: * This class represents the stack of the JVM.
028: */
029: public class KernelState implements Storable {
030: /**
031: * The area containing the classes.
032: */
033: public StaticArea sa;
034:
035: /**
036: * The area containing the objects.
037: */
038: public DynamicArea da;
039:
040: /**
041: * The list of the threads.
042: */
043: public ThreadList tl;
044:
045: /**
046: * Link to the system state.
047: */
048: public SystemState ss;
049:
050: /**
051: * Number of nested atomic blocks.
052: */
053: public int atomicLevel;
054:
055: /**
056: * True if the last was an intermediate step (non-deterministic)
057: * <?> pcm - does that mean we don't store any data for this state, e.g.
058: * to make sure we don't treat it as visited?
059: */
060: private boolean intermediateStep;
061:
062: /**
063: * Thread that made stopped at an intermediate step.
064: */
065: private int intermediateThread;
066:
067: /**
068: * The data returned by last get data.
069: */
070: public int[] data;
071:
072: /**
073: * Creates a new kernel state object.
074: */
075: public KernelState(Config config, SystemState system_state) {
076: sa = new StaticArea(config, this );
077: da = new DynamicArea(config, this );
078: tl = new ThreadList(config, this );
079:
080: ss = system_state;
081: atomicLevel = 0;
082: intermediateStep = false;
083: intermediateThread = -1;
084: data = null;
085: }
086:
087: public void setAtomic() {
088: atomicLevel++;
089: }
090:
091: public Object getBacktrackData() {
092: Object[] data = new Object[6];
093:
094: data[0] = sa.getBacktrackData();
095: data[1] = da.getBacktrackData();
096: data[2] = tl.getBacktrackData();
097: data[3] = new Integer(atomicLevel);
098: data[4] = new Boolean(intermediateStep);
099: data[5] = new Integer(intermediateThread);
100:
101: return data;
102: }
103:
104: public void setIntermediate() {
105: intermediateStep = true;
106: intermediateThread = ss.getScheduler().getThread();
107: }
108:
109: public boolean isIntermediate() {
110: return intermediateStep;
111: }
112:
113: public int getIntermediateThread() {
114: return intermediateThread;
115: }
116:
117: public int[] getStoringData() {
118: if (data != null) {
119: return data;
120: }
121:
122: int[] tlData = tl.getStoringData();
123: int[] saData = sa.getStoringData();
124: int[] daData = da.getStoringData();
125:
126: int sal = saData.length;
127: int dal = daData.length;
128: int tll = tlData.length;
129:
130: data = new int[sal + dal + tll];
131:
132: System.arraycopy(tlData, 0, data, 0, tll);
133: System.arraycopy(saData, 0, data, tll, sal);
134: System.arraycopy(daData, 0, data, tll + sal, dal);
135:
136: return data;
137: }
138:
139: /**
140: * The program is terminated if there are no alive threads.
141: */
142: public boolean isTerminated() {
143: return !tl.anyAliveThread();
144: }
145:
146: public int getThreadCount() {
147: return tl.length();
148: }
149:
150: public ThreadInfo getThreadInfo(int index) {
151: return tl.get(index);
152: }
153:
154: public void backtrackTo(ArrayOffset storing, Object backtrack) {
155:
156: // we need to restore the Thread list first, since objects (ElementInfos)
157: // might refer to it (e.g. when re-computing volatiles)
158: tl.backtrackTo(storing, ((Object[]) backtrack)[2]);
159:
160: sa.backtrackTo(storing, ((Object[]) backtrack)[0]);
161: da.backtrackTo(storing, ((Object[]) backtrack)[1]);
162:
163: atomicLevel = ((Integer) ((Object[]) backtrack)[3]).intValue();
164: intermediateStep = ((Boolean) ((Object[]) backtrack)[4])
165: .booleanValue();
166: intermediateThread = ((Integer) ((Object[]) backtrack)[5])
167: .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: }
|