KickJava   Java API By Example, From Geeks To Geeks.

Java > Open Source Codes > gov > nasa > jpf > jvm > SystemState


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.JPFException;
23 import gov.nasa.jpf.util.HashData;
24
25
26 /**
27  * the class that encapsulates not only the current execution state of the VM
28  * (the KernelState), but also the part of it's history that is required
29  * by JVM to backtrack, plus some potential annotations that can be used to
30  * control the search (i.e. forward/backtrack calls)
31  */
32 public class SystemState implements Storable, State {
33   
34   /**
35    * instances of this class are used to store the SystemState parts which are
36    * subject to backtracking/state resetting. At some point, we might have
37    * stripped SystemState down enough to just store the SystemState itself
38    * (so far, we don't change it's identity, there is only one)
39    * the KernelState is still stored separately (which seems to be another
40    * anachronism)
41    *
42    * <2do> - should be probably a inner class object - given that we have only
43    * one SystemState instance (but bears the potential of memory leaks then)
44    */
45   static class Memento {
46     ChoiceGenerator gen; // <2do> this is going to replace 'sch'
47 Scheduler sch; // a clone of the Scheduler (mostly to store/restore)
48 // the scheduling enumeration state
49 // <2do> Scheduler should have it's own Memento
50
51     int id; // the state id
52
53     Memento (SystemState ss) {
54       gen = ss.gen;
55       sch = (Scheduler)ss.sch.clone();
56       id = ss.id;
57     }
58     
59     void restore (SystemState ss) {
60       ss.gen = gen;
61       //ss.sch = sch;
62 ss.sch = (Scheduler)sch.clone();
63       ss.id = id;
64     }
65   }
66   
67   int id; /** the state id */
68   
69   ChoiceGenerator gen; // <2do> this is going to replace the Scheduler 'sch'
70 public Scheduler sch; /** our scheduling sequence enumerator */
71
72   /** current execution state of the VM (stored separately by VM) */
73   public KernelState ks;
74
75   public TrailInfo ti; /** trace information */
76
77   /** True if an assertion has been violated in current transition */
78   public boolean violatedAssertion;
79
80   /** True if a Verify.ignoreIf() has been satisfied in current transition */
81   public boolean ignored;
82
83   /** True if a Verify.interesting() has been satisfied in current transition */
84   public boolean interesting;
85
86   /** True if a Verify.boring() has been satisfied */
87   public boolean boring;
88
89   /** Signals when a wait introduces a deadlock */
90   public boolean waitDeadlockDetected = false;
91
92   /** uncaught exception in current transition */
93   public UncaughtException uncaughtException;
94
95   /** set to true if garbage collection is necessary */
96   boolean GCNeeded = false;
97
98   /**
99    * Creates a new system state.
100    */
101   public SystemState (Config config, Scheduler scheduler) {
102     ks = new KernelState(config, this);
103     sch = scheduler;
104     id = StateSet.UNKNOWN_ID;
105     
106     // so that we have something we can store the path into
107 ti = new TrailInfo(sch.getThread(), sch.getRandom());
108   }
109
110   public int getId () {
111     return id;
112   }
113   
114   void setId (int newId) {
115     id = newId;
116   }
117   
118   public ChoiceGenerator getChoiceGenerator () {
119     return gen;
120   }
121   
122   public void setChoiceGenerator (ChoiceGenerator cg) {
123     gen = cg;
124   }
125   
126   public Object JavaDoc getBacktrackData () {
127     return new Memento(this);
128   }
129
130   public void backtrackTo (ArrayOffset storing, Object JavaDoc backtrack) {
131     ((Memento) backtrack).restore( this);
132   }
133
134   public boolean getBoring () {
135     return boring;
136   }
137
138   public Reference getClass (String JavaDoc name) {
139     if (ks.sa.containsClass(name)) {
140       return ks.sa.get(name);
141     }
142
143     return null;
144   }
145
146   public boolean isIgnored () {
147     return ignored;
148   }
149
150   public boolean getInteresting () {
151     return interesting;
152   }
153
154   public int getNonDaemonThreadCount () {
155     return ks.tl.getNonDaemonThreadCount();
156   }
157
158   public Reference getObject (int reference) {
159     return ks.da.get(reference);
160   }
161
162   public ThreadInfo getRunningThread () {
163     // if (sch == null) return null;
164 if (sch.getThread() >= ks.tl.length()) {
165       return null;
166     }
167
168     return ks.tl.get(sch.getThread());
169   }
170
171   public Scheduler getScheduler () {
172     return sch;
173   }
174
175   public int[] getStoringData () {
176     return ks.getStoringData();
177   }
178
179   public ThreadInfo getThread (int index) {
180     return ks.tl.get(index);
181   }
182
183   public ThreadInfo getThread (Reference reference) {
184     return getThread(((ElementInfo) reference).getIndex());
185   }
186
187   public int getThreadCount () {
188     return ks.tl.length();
189   }
190
191   public int getRunnableThreadCount () {
192     return ks.tl.getRunnableThreadCount();
193   }
194   
195   public ThreadInfo getThreadInfo (int idx) {
196     return ks.tl.get(idx);
197   }
198
199   public TrailInfo getTrailInfo () {
200     return ti;
201   }
202
203   public UncaughtException getUncaughtException () {
204     return uncaughtException;
205   }
206
207   public void activateGC () {
208     GCNeeded = true;
209   }
210
211   public void gcIfNeeded () {
212     if (GCNeeded) {
213       ks.gc();
214       GCNeeded = false;
215     }
216   }
217
218   public void hash (HashData hd) {
219     ks.hash(hd);
220   }
221
222   public int hashCode () {
223     HashData hd = new HashData();
224
225     hash(hd);
226
227     return hd.getValue();
228   }
229
230   /**
231    * Compute next state.
232    * return 'true' if we actually executed instructions, 'false' if this
233    * state was already completely processed
234    */
235   public boolean nextSuccessor (JVM vm) throws JPFException {
236     ThreadInfo th; // Thread that is going to be executed
237
238     violatedAssertion = false;
239     ignored = false;
240     interesting = false;
241     boring = false;
242     th = (ThreadInfo) sch.locateThread(this);
243
244     if (gen != null) {
245       gen.advance(vm); // <2do> will replace the scheduler
246 }
247     
248     if (ks.isIntermediate()) {
249       int intermediateThread = ks.getIntermediateThread();
250
251       if (th != null) {
252         while ((th != null) && (th.index != intermediateThread)) {
253           sch.next();
254           th = (ThreadInfo) sch.locateThread(this);
255         }
256       }
257     }
258
259     // there are no executable threads (this is the exit point for exhausted
260 // scheduling or nondeterminism successor choices)
261 if (th == null) {
262       return false;
263     }
264
265     // this is the beginning of a new transition
266 ti = new TrailInfo(sch.getThread(), sch.getRandom());
267     
268     if (th.executeStep()) { // might set an uncaught exception
269 ks.clearIntermediate();
270     } else {
271       // make sure we don't treat this as a already visited state
272 // <?> pcm - that's what 'intermediate' means?
273 ks.setIntermediate();
274     }
275        
276     return true;
277   }
278
279   public boolean isEndState () {
280     return ks.isTerminated();
281   }
282   
283   public int random (int max) {
284     int random = sch.random(max);
285
286     TrailInfo ti = trail();
287     ti.setRandom(random);
288
289     return random;
290   }
291
292   public TrailInfo trail () {
293     return ti;
294   }
295   
296   // the three primitive ops used from within JVM.forward()
297
298   // <2do> - not sure if this cannot be dumped
299 void checkNext (JVM jvm) {
300     sch.checkNext(this);
301   }
302
303   void prepareNext (JVM jvm) {
304     gen = null;
305     sch.initialize();
306   }
307
308   void scheduleNext (JVM jvm) {
309     // <2do> this is a hack for now to avoid having to change "nextSuccessor"
310 // but it should go away as soon as the Scheduler becomes a Choice Generator too
311 if ((gen != null) && (gen.hasMoreChoices(jvm))) return;
312
313     sch.next();
314   }
315 }
316
Popular Tags