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.JPFException;
023: import gov.nasa.jpf.util.HashData;
024:
025: /**
026: * the class that encapsulates not only the current execution state of the VM
027: * (the KernelState), but also the part of it's history that is required
028: * by JVM to backtrack, plus some potential annotations that can be used to
029: * control the search (i.e. forward/backtrack calls)
030: */
031: public class SystemState implements Storable, State {
032:
033: /**
034: * instances of this class are used to store the SystemState parts which are
035: * subject to backtracking/state resetting. At some point, we might have
036: * stripped SystemState down enough to just store the SystemState itself
037: * (so far, we don't change it's identity, there is only one)
038: * the KernelState is still stored separately (which seems to be another
039: * anachronism)
040: *
041: * <2do> - should be probably a inner class object - given that we have only
042: * one SystemState instance (but bears the potential of memory leaks then)
043: */
044: static class Memento {
045: ChoiceGenerator gen; // <2do> this is going to replace 'sch'
046: Scheduler sch; // a clone of the Scheduler (mostly to store/restore)
047: // the scheduling enumeration state
048: // <2do> Scheduler should have it's own Memento
049:
050: int id; // the state id
051:
052: Memento(SystemState ss) {
053: gen = ss.gen;
054: sch = (Scheduler) ss.sch.clone();
055: id = ss.id;
056: }
057:
058: void restore(SystemState ss) {
059: ss.gen = gen;
060: //ss.sch = sch;
061: ss.sch = (Scheduler) sch.clone();
062: ss.id = id;
063: }
064: }
065:
066: int id;
067: /** the state id */
068:
069: ChoiceGenerator gen; // <2do> this is going to replace the Scheduler 'sch'
070: public Scheduler sch;
071: /** our scheduling sequence enumerator */
072:
073: /** current execution state of the VM (stored separately by VM) */
074: public KernelState ks;
075:
076: public TrailInfo ti;
077: /** trace information */
078:
079: /** True if an assertion has been violated in current transition */
080: public boolean violatedAssertion;
081:
082: /** True if a Verify.ignoreIf() has been satisfied in current transition */
083: public boolean ignored;
084:
085: /** True if a Verify.interesting() has been satisfied in current transition */
086: public boolean interesting;
087:
088: /** True if a Verify.boring() has been satisfied */
089: public boolean boring;
090:
091: /** Signals when a wait introduces a deadlock */
092: public boolean waitDeadlockDetected = false;
093:
094: /** uncaught exception in current transition */
095: public UncaughtException uncaughtException;
096:
097: /** set to true if garbage collection is necessary */
098: boolean GCNeeded = false;
099:
100: /**
101: * Creates a new system state.
102: */
103: public SystemState(Config config, Scheduler scheduler) {
104: ks = new KernelState(config, this );
105: sch = scheduler;
106: id = StateSet.UNKNOWN_ID;
107:
108: // so that we have something we can store the path into
109: ti = new TrailInfo(sch.getThread(), sch.getRandom());
110: }
111:
112: public int getId() {
113: return id;
114: }
115:
116: void setId(int newId) {
117: id = newId;
118: }
119:
120: public ChoiceGenerator getChoiceGenerator() {
121: return gen;
122: }
123:
124: public void setChoiceGenerator(ChoiceGenerator cg) {
125: gen = cg;
126: }
127:
128: public Object getBacktrackData() {
129: return new Memento(this );
130: }
131:
132: public void backtrackTo(ArrayOffset storing, Object backtrack) {
133: ((Memento) backtrack).restore(this );
134: }
135:
136: public boolean getBoring() {
137: return boring;
138: }
139:
140: public Reference getClass(String name) {
141: if (ks.sa.containsClass(name)) {
142: return ks.sa.get(name);
143: }
144:
145: return null;
146: }
147:
148: public boolean isIgnored() {
149: return ignored;
150: }
151:
152: public boolean getInteresting() {
153: return interesting;
154: }
155:
156: public int getNonDaemonThreadCount() {
157: return ks.tl.getNonDaemonThreadCount();
158: }
159:
160: public Reference getObject(int reference) {
161: return ks.da.get(reference);
162: }
163:
164: public ThreadInfo getRunningThread() {
165: // if (sch == null) return null;
166: if (sch.getThread() >= ks.tl.length()) {
167: return null;
168: }
169:
170: return ks.tl.get(sch.getThread());
171: }
172:
173: public Scheduler getScheduler() {
174: return sch;
175: }
176:
177: public int[] getStoringData() {
178: return ks.getStoringData();
179: }
180:
181: public ThreadInfo getThread(int index) {
182: return ks.tl.get(index);
183: }
184:
185: public ThreadInfo getThread(Reference reference) {
186: return getThread(((ElementInfo) reference).getIndex());
187: }
188:
189: public int getThreadCount() {
190: return ks.tl.length();
191: }
192:
193: public int getRunnableThreadCount() {
194: return ks.tl.getRunnableThreadCount();
195: }
196:
197: public ThreadInfo getThreadInfo(int idx) {
198: return ks.tl.get(idx);
199: }
200:
201: public TrailInfo getTrailInfo() {
202: return ti;
203: }
204:
205: public UncaughtException getUncaughtException() {
206: return uncaughtException;
207: }
208:
209: public void activateGC() {
210: GCNeeded = true;
211: }
212:
213: public void gcIfNeeded() {
214: if (GCNeeded) {
215: ks.gc();
216: GCNeeded = false;
217: }
218: }
219:
220: public void hash(HashData hd) {
221: ks.hash(hd);
222: }
223:
224: public int hashCode() {
225: HashData hd = new HashData();
226:
227: hash(hd);
228:
229: return hd.getValue();
230: }
231:
232: /**
233: * Compute next state.
234: * return 'true' if we actually executed instructions, 'false' if this
235: * state was already completely processed
236: */
237: public boolean nextSuccessor(JVM vm) throws JPFException {
238: ThreadInfo th; // Thread that is going to be executed
239:
240: violatedAssertion = false;
241: ignored = false;
242: interesting = false;
243: boring = false;
244: th = (ThreadInfo) sch.locateThread(this );
245:
246: if (gen != null) {
247: gen.advance(vm); // <2do> will replace the scheduler
248: }
249:
250: if (ks.isIntermediate()) {
251: int intermediateThread = ks.getIntermediateThread();
252:
253: if (th != null) {
254: while ((th != null) && (th.index != intermediateThread)) {
255: sch.next();
256: th = (ThreadInfo) sch.locateThread(this );
257: }
258: }
259: }
260:
261: // there are no executable threads (this is the exit point for exhausted
262: // scheduling or nondeterminism successor choices)
263: if (th == null) {
264: return false;
265: }
266:
267: // this is the beginning of a new transition
268: ti = new TrailInfo(sch.getThread(), sch.getRandom());
269:
270: if (th.executeStep()) { // might set an uncaught exception
271: ks.clearIntermediate();
272: } else {
273: // make sure we don't treat this as a already visited state
274: // <?> pcm - that's what 'intermediate' means?
275: ks.setIntermediate();
276: }
277:
278: return true;
279: }
280:
281: public boolean isEndState() {
282: return ks.isTerminated();
283: }
284:
285: public int random(int max) {
286: int random = sch.random(max);
287:
288: TrailInfo ti = trail();
289: ti.setRandom(random);
290:
291: return random;
292: }
293:
294: public TrailInfo trail() {
295: return ti;
296: }
297:
298: // the three primitive ops used from within JVM.forward()
299:
300: // <2do> - not sure if this cannot be dumped
301: void checkNext(JVM jvm) {
302: sch.checkNext(this );
303: }
304:
305: void prepareNext(JVM jvm) {
306: gen = null;
307: sch.initialize();
308: }
309:
310: void scheduleNext(JVM jvm) {
311: // <2do> this is a hack for now to avoid having to change "nextSuccessor"
312: // but it should go away as soon as the Scheduler becomes a Choice Generator too
313: if ((gen != null) && (gen.hasMoreChoices(jvm)))
314: return;
315:
316: sch.next();
317: }
318: }
|