KickJava   Java API By Example, From Geeks To Geeks.

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


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.jvm.bytecode.INVOKESTATIC;
24 import gov.nasa.jpf.jvm.bytecode.Instruction;
25 import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
26 import gov.nasa.jpf.jvm.bytecode.MONITORENTER;
27 import gov.nasa.jpf.jvm.bytecode.ReturnInstruction;
28 import gov.nasa.jpf.util.CoverageManager;
29 import gov.nasa.jpf.util.Debug;
30 import gov.nasa.jpf.util.HashData;
31 import gov.nasa.jpf.util.HashPool;
32
33 import java.io.PrintWriter JavaDoc;
34
35 import java.util.BitSet JavaDoc;
36 import java.util.Iterator JavaDoc;
37 import java.util.LinkedList JavaDoc;
38
39
40 /**
41  * Represents a thread. It contains the state of the thread, static
42  * information about the thread, and the stack frames.
43  * Race detection and lock order also store some information
44  * in this data structure.
45  */

46 public class ThreadInfo implements Storable {
47   
48   /** <2do> - just a bloody guess, we need to change the livelock detection */
49   static final int LIVELOCK_STEPS = 5000;
50   
51   static final int NEW = 0;
52   static final int RUNNING = 1;
53   
54   // thread is running, but has to acquire target/this lock on first op
55
// (first insn in a synchronized run method)
56
public static final int SYNC_RUNNING = 2;
57   public static final int WAITING = 3;
58   public static final int NOTIFIED = 4;
59   public static final int STOPPED = 5;
60   public static final int INTERRUPTED = 6;
61   public static final int TERMINATED = 7;
62   
63   /**Pool used to store the thread data.*/
64   protected static HashPool threadDataPool = new HashPool();
65   
66   /** Pool used to store the stack frames.*/
67   protected static HashPool stackFramePool = new HashPool();
68   
69   static ThreadInfo current;
70   
71   /** do we want a forced reschedule */
72   boolean yield;
73   
74   protected ExceptionInfo pendingException;
75   
76   /** backtrack-relevant Information about the thread */
77   protected ThreadData threadData;
78   
79   /**
80    * Some information about the thread that are used to handle
81    * atomicity.
82    */

83   protected AtomicData atomicData;
84   
85   /**
86    * The stack frames of the JVM.
87    * <2do> pcm - right now this gets re-allocated on every push/pop,
88    * turn it into a real stack at some point
89    */

90   protected StackFrame[] stack;
91   
92   /**
93    * Reference of the thread list it is in.
94    */

95   public ThreadList list;
96   
97   /**
98    * Position in the thread list.
99    */

100   public int index;
101   
102   /**
103    * Contains the index of the thread data last used.
104    */

105   public int tdIndex = -1;
106   
107   /**
108    * Identifies which thread has changed.
109    */

110   public BitSet JavaDoc hasChanged;
111   
112   /**
113    * Set if any stack frame changed.
114    */

115   public boolean anyChanged;
116   
117   /**
118    * Keeps the information from the last storing.
119    */

120   protected int[] data;
121   
122   /**
123    * Remembers which is the lowest changed stack frame.
124    */

125   protected int lowestChanged;
126   
127   /**
128    * cache for last return value (useful for direct calls that don't change the stack)
129    */

130   long returnValue;
131   
132   /**
133    * not so nice we cross-couple the NativePeers with ThreadInfo,
134    * but to carry on with the JNI analogy, a MJIEnv is clearly
135    * owned by a thread (even though we don't have much ThreadInfo
136    * state dependency in here (yet), hence the simplistic init)
137    */

138   MJIEnv env;
139   
140   /**
141    * the VM we are running on. Bad backlink, but then again, we can't really
142    * test a ThreadInfo outside a VM context anyways.
143    * <2do> If we keep 'list' as a field, 'vm' might be moved over there
144    * (all threads in the list share the same VM)
145    */

146   JVM vm;
147   
148   /**
149    * list of lock objects currently held by this thread.
150    * unfortunately, we cannot organize this as a stack, since it might get
151    * restored (from the heap) in random order
152    */

153   LinkedList JavaDoc lockedObjects = new LinkedList JavaDoc();
154   
155   
156   // the following parameters are configurable. Would be nice if we could keep
157
// them on a per-instance basis, but there are a few locations
158
// (e.g. ThreadList) where we loose the init context, and it's questionable
159
// if we want to change this at runtime, or POR might make sense on a per-thread
160
// basis
161

162   /** do we halt on each throw, i.e. don't look for an exception handler?
163    * Useful to find empty handler blocks, or misusd exceptions
164    */

165   static boolean haltOnThrow;
166   
167   /** is on-the-fly partial order in effect? */
168   static boolean porInEffect;
169   
170   /** do we treat access of fields referring to objects that are reachable
171    * from different threads as boundary steps (i.e. starting a new Transition)?
172    */

173   static boolean porFieldBoundaries;
174   
175   /** detect field synchronization (find locks which are used to synchronize
176    * field access - if we have viable candidates, and we find the locks taken,
177    * we don't treat access of the corresponding field as a boundary step
178    */

179   static boolean porSyncDetection;
180     
181   static boolean init (Config config) {
182     threadDataPool = new HashPool();
183     stackFramePool = new HashPool();
184     current = null;
185     
186     haltOnThrow = config.getBoolean("vm.halt_on_throw");
187     porInEffect = config.getBoolean("vm.por");
188     porFieldBoundaries = config.getBoolean("vm.por.field_boundaries");
189     porSyncDetection = config.getBoolean("vm.por.sync_detection");
190     
191     return true;
192   }
193   
194   /**
195    * Creates a new thread info. It is associated with the object
196    * passed and sets the target object as well.
197    */

198   public ThreadInfo (JVM vm, int o) {
199     DynamicArea da = vm.getDynamicArea();
200     ElementInfo ei = da.get(o);
201     
202     this.vm = vm;
203     
204     threadData = new ThreadData();
205     threadData.status = NEW;
206     
207     if (o != -1) {
208       threadData.ci = ei.getClassInfo();
209     }
210     
211     threadData.objref = o;
212     threadData.target = -1;
213     threadData.lockCount = 0;
214     
215     // this is nasty - 'priority', 'name', 'target' and 'group' are not taken
216
// from the object, but set within the java.lang.Thread ctors
217

218     atomicData = new AtomicData();
219     atomicData.currentMethod = null;
220     atomicData.line = -1;
221     atomicData.inSameMethod = false;
222     
223     stack = new StackFrame[0];
224     
225     hasChanged = new BitSet JavaDoc();
226     anyChanged = false;
227     data = new int[0];
228     lowestChanged = -1;
229     
230     env = new MJIEnv(this);
231   }
232   
233   public ThreadInfo (ThreadInfo ti) {
234     if (ti.tdIndex == -1) {
235       threadData = (ThreadData) ti.threadData.clone();
236     } else {
237       threadData = ti.threadData;
238     }
239     
240     atomicData = (AtomicData) ti.atomicData.clone();
241     
242     if (ti.stack != null) {
243       int l = ti.stack.length;
244       stack = new StackFrame[l];
245       
246       if (ti.anyChanged) {
247         for (int i = 0; i < l; i++) {
248           if (ti.hasChanged.get(i)) {
249             stack[i] = (StackFrame) ti.stack[i].clone();
250           } else {
251             stack[i] = ti.stack[i];
252           }
253         }
254       } else {
255         System.arraycopy(ti.stack, 0, stack, 0, l);
256       }
257     } else {
258       stack = null;
259     }
260     
261     vm = ti.vm;
262     list = null;
263     index = -1;
264     tdIndex = ti.tdIndex;
265     hasChanged = (BitSet JavaDoc) ti.hasChanged.clone();
266     anyChanged = ti.anyChanged;
267     data = ti.data;
268     lowestChanged = ti.lowestChanged;
269     
270     env = new MJIEnv(this);
271   }
272   
273   /**
274    * Creates a new empty thread info. Used to backtrack.
275    */

276   ThreadInfo (ThreadList l, int i) {
277     list = l;
278     index = i;
279     
280     stack = new StackFrame[0];
281     tdIndex = -1;
282     data = new int[0];
283     hasChanged = new BitSet JavaDoc();
284     
285     vm = JVM.getVM(); // <2do> cut this
286

287     env = new MJIEnv(this);
288     
289     // <2do> what about the other fields?
290
}
291   
292   public static ThreadInfo getCurrent() {
293     return current;
294   }
295
296   public boolean holdsLock (ElementInfo ei) {
297     return lockedObjects.contains(ei);
298   }
299     
300   public JVM getVM () {
301     return vm;
302   }
303   
304   
305   public void setReturnValue (long ret) {
306     returnValue = ret;
307   }
308   /**
309    * the return value from the last StackFrame (that had a return)
310    * Note: it's the callers responsibility to know about type and validity
311    * (the method might have no / int / long return value)
312    */

313   public long getReturnValue () {
314     return returnValue;
315   }
316   
317   public boolean usePor () {
318     return porInEffect;
319   }
320   
321   public boolean usePorFieldBoundaries () {
322     return porFieldBoundaries;
323   }
324   
325   public boolean usePorSyncDetection () {
326     return porSyncDetection;
327   }
328   
329   /**
330    * Checks if the thread is waiting to execute a nondeterministic choice
331    * due to an abstraction, i.e. due to a Bandera.choose() call
332    */

333   public boolean isAbstractionNonDeterministic () {
334     if (getPC() == null) {
335       return false;
336     }
337     
338     return getPC().examineAbstraction(list.ks.ss, list.ks, this);
339   }
340   
341   /**
342    * An alive thread is either running, waiting, notified, or interrupted.
343    */

344   public boolean isAlive () {
345     return (threadData.status != TERMINATED);
346     /*
347      boolean alive = (threadData.status == RUNNING) ||
348      (threadData.status == SYNC_RUNNING) ||
349      (threadData.status == WAITING) ||
350      (threadData.status == INTERRUPTED) ||
351      (threadData.status == NOTIFIED);
352      
353      return alive;
354      */

355   }
356   
357   /**
358    * Returns the information necessary to backtrack.
359    */

360   public Object JavaDoc getBacktrackData () {
361     return atomicData.clone();
362   }
363   
364   public boolean getBooleanLocal (String JavaDoc lname) {
365     return Types.intToBoolean(getLocalVariable(lname));
366   }
367   
368   public boolean getBooleanLocal (int lindex) {
369     return Types.intToBoolean(getLocalVariable(lindex));
370   }
371   
372   public boolean getBooleanLocal (int fr, String JavaDoc lname) {
373     return Types.intToBoolean(getLocalVariable(fr, lname));
374   }
375   
376   public boolean getBooleanLocal (int fr, int lindex) {
377     return Types.intToBoolean(getLocalVariable(fr, lindex));
378   }
379   
380   public boolean getBooleanReturnValue () {
381     return Types.intToBoolean(peek());
382   }
383   
384   public byte getByteLocal (String JavaDoc lname) {
385     return (byte) getLocalVariable(lname);
386   }
387   
388   public byte getByteLocal (int lindex) {
389     return (byte) getLocalVariable(lindex);
390   }
391   
392   public byte getByteLocal (int fr, String JavaDoc lname) {
393     return (byte) getLocalVariable(fr, lname);
394   }
395   
396   public byte getByteLocal (int fr, int lindex) {
397     return (byte) getLocalVariable(fr, lindex);
398   }
399   
400   public byte getByteReturnValue () {
401     return (byte) peek();
402   }
403   
404   public String JavaDoc[] getCallStack () {
405     int size = stack.length;
406     String JavaDoc[] callStack = new String JavaDoc[size];
407     
408     for (int i = 0; i < size; i++) {
409       callStack[i] = frame(i).getStackTrace();
410     }
411     
412     return callStack;
413   }
414   
415   public String JavaDoc getCallStackClass (int i) {
416     if (i < stack.length) {
417       StackFrame fr = frame(i);
418       
419       return fr.getClassInfo().getName();
420     }
421     
422     return null;
423   }
424   
425   public String JavaDoc getCallStackFile (int i) {
426     if (i < stack.length) {
427       StackFrame fr = frame(i);
428       
429       return fr.getClassInfo().getSourceFileName();
430     }
431     
432     return null;
433   }
434   
435   public int getCallStackLine (int i) {
436     if (i < stack.length) {
437       StackFrame fr = frame(i);
438       
439       return fr.getLine();
440     }
441     
442     return 0;
443   }
444   
445   public String JavaDoc getCallStackMethod (int i) {
446     if (i < stack.length) {
447       StackFrame fr = frame(i);
448       
449       return fr.getMethodInfo().getName();
450     }
451     
452     return null;
453   }
454   
455   /**
456    * Returns the this pointer of the callee from the stack.
457    */

458   public int getCalleeThis (MethodInfo mi) {
459     return top().getCalleeThis(mi);
460   }
461   
462   /**
463    * Returns the this pointer of the callee from the stack.
464    */

465   public int getCalleeThis (int size) {
466     return top().getCalleeThis(size);
467   }
468   
469   public boolean isCalleeThis (Reference r) {
470     if ((stack.length == 0) || (r == null)) {
471       return false;
472     }
473     
474     Instruction pc = getPC();
475     
476     if (pc == null) {
477       return false;
478     }
479     
480     if (!(pc instanceof InvokeInstruction)) {
481       return false;
482     }
483     
484     if (pc instanceof INVOKESTATIC) {
485       return false;
486     }
487     
488     InvokeInstruction i = (InvokeInstruction) pc;
489     
490     return getCalleeThis(Types.getArgumentsSize(i.signature) + 1) == ((ElementInfo) r).getIndex();
491   }
492   
493   public char getCharLocal (String JavaDoc lname) {
494     return (char) getLocalVariable(lname);
495   }
496   
497   public char getCharLocal (int lindex) {
498     return (char) getLocalVariable(lindex);
499   }
500   
501   public char getCharLocal (int fr, String JavaDoc lname) {
502     return (char) getLocalVariable(fr, lname);
503   }
504   
505   public char getCharLocal (int fr, int lindex) {
506     return (char) getLocalVariable(fr, lindex);
507   }
508   
509   public char getCharReturnValue () {
510     return (char) peek();
511   }
512   
513   /**
514    * Returns the class information.
515    */

516   public ClassInfo getClassInfo () {
517     return threadData.ci;
518   }
519   
520   public double getDoubleLocal (String JavaDoc lname) {
521     return Types.longToDouble(getLongLocalVariable(lname));
522   }
523   
524   public double getDoubleLocal (int lindex) {
525     return Types.longToDouble(getLongLocalVariable(lindex));
526   }
527   
528   public double getDoubleLocal (int fr, String JavaDoc lname) {
529     return Types.longToDouble(getLongLocalVariable(fr, lname));
530   }
531   
532   public double getDoubleLocal (int fr, int lindex) {
533     return Types.longToDouble(getLongLocalVariable(fr, lindex));
534   }
535   
536   public double getDoubleReturnValue () {
537     return Types.longToDouble(longPeek());
538   }
539   
540   /**
541    * An enabled thread is either running, notified, or interrupted.
542    */

543   public boolean isEnabled () {
544     boolean isEnabled = (threadData.status == RUNNING) ||
545                         (threadData.status == SYNC_RUNNING) ||
546                         (threadData.status == INTERRUPTED) ||
547                         (threadData.status == NOTIFIED);
548     return isEnabled;
549   }
550   
551   public float getFloatLocal (String JavaDoc lname) {
552     return Types.intToFloat(getLocalVariable(lname));
553   }
554   
555   public float getFloatLocal (int lindex) {
556     return Types.intToFloat(getLocalVariable(lindex));
557   }
558   
559   public float getFloatLocal (int fr, String JavaDoc lname) {
560     return Types.intToFloat(getLocalVariable(fr, lname));
561   }
562   
563   public float getFloatLocal (int fr, int lindex) {
564     return Types.intToFloat(getLocalVariable(fr, lindex));
565   }
566   
567   public float getFloatReturnValue () {
568     return Types.intToFloat(peek());
569   }
570   
571   public int getIntLocal (String JavaDoc lname) {
572     return getLocalVariable(lname);
573   }
574   
575   public int getIntLocal (int lindex) {
576     return getLocalVariable(lindex);
577   }
578   
579   public int getIntLocal (int fr, String JavaDoc lname) {
580     return getLocalVariable(fr, lname);
581   }
582   
583   public int getIntLocal (int fr, int lindex) {
584     return getLocalVariable(fr, lindex);
585   }
586   
587   public int getIntReturnValue () {
588     return peek();
589   }
590   
591   public boolean isInterrupted (boolean resetStatus) {
592     boolean ret = (getStatus() == INTERRUPTED);
593     
594     if (resetStatus) {
595       // <2do> pcm is that true? check the specs
596
setStatus(RUNNING);
597     }
598     
599     return ret;
600   }
601   
602   /**
603    * return our internal thread number (order of creation)
604    */

605   public int getIndex () {
606     return index;
607   }
608   
609   /**
610    * Returns the line number of the program counter of the top stack frame.
611    */

612   public int getLine () {
613     if (stack.length == 0) return -1;
614     
615     return top().getLine();
616   }
617   
618   /**
619    * Returns the line the thread is at.
620    */

621   public int getLine (int idx) {
622     return frame(idx).getLine();
623   }
624   
625   public String JavaDoc[] getLocalNames () {
626     return top().getLocalVariableNames();
627   }
628   
629   public String JavaDoc[] getLocalNames (int fr) {
630     return frame(fr).getLocalVariableNames();
631   }
632   
633   /**
634    * Sets the value of a local variable.
635    */

636   public void setLocalVariable (int idx, int v, boolean ref) {
637     topClone().setLocalVariable(idx, v, ref);
638   }
639   
640   /**
641    * Returns the value of a local variable in a particular frame.
642    */

643   public int getLocalVariable (int fr, int idx) {
644     return frame(fr).getLocalVariable(idx);
645   }
646   
647   /**
648    * Returns the value of a local variable.
649    */

650   public int getLocalVariable (int idx) {
651     return top().getLocalVariable(idx);
652   }
653   
654   /**
655    * Gets the value of a local variable from its name and frame.
656    */

657   public int getLocalVariable (int fr, String JavaDoc name) {
658     return frame(fr).getLocalVariable(name);
659   }
660   
661   /**
662    * Gets the value of a local variable from its name.
663    */

664   public int getLocalVariable (String JavaDoc name) {
665     return top().getLocalVariable(name);
666   }
667   
668   /**
669    * Checks if a local variable is a reference.
670    */

671   public boolean isLocalVariableRef (int idx) {
672     return top().isLocalVariableRef(idx);
673   }
674   
675   /**
676    * Gets the type associated with a local variable.
677    */

678   public String JavaDoc getLocalVariableType (int fr, String JavaDoc name) {
679     return frame(fr).getLocalVariableType(name);
680   }
681   
682   /**
683    * Gets the type associated with a local variable.
684    */

685   public String JavaDoc getLocalVariableType (String JavaDoc name) {
686     return top().getLocalVariableType(name);
687   }
688   
689   /**
690    * Sets the number of locks held at the time of a wait.
691    */

692   public void setLockCount (int l) {
693     if (threadData.lockCount != l) {
694       threadDataClone().lockCount = l;
695     }
696   }
697   
698   /**
699    * Returns the number of locks in the last wait.
700    */

701   public int getLockCount () {
702     return threadData.lockCount;
703   }
704     
705   public LinkedList JavaDoc getLockedObjects () {
706     return lockedObjects;
707   }
708   
709   public int[] getLockedObjectReferences () {
710     int[] a = new int[lockedObjects.size()];
711     int i=0;
712     for (Iterator JavaDoc it=lockedObjects.iterator(); it.hasNext();) {
713       a[i++] = ((ElementInfo)it.next()).getIndex();
714     }
715     
716     return a;
717   }
718   
719   public long getLongLocal (String JavaDoc lname) {
720     return getLongLocalVariable(lname);
721   }
722   
723   public long getLongLocal (int lindex) {
724     return getLongLocalVariable(lindex);
725   }
726   
727   public long getLongLocal (int fr, String JavaDoc lname) {
728     return getLongLocalVariable(fr, lname);
729   }
730   
731   public long getLongLocal (int fr, int lindex) {
732     return getLongLocalVariable(fr, lindex);
733   }
734   
735   /**
736    * Sets the value of a long local variable.
737    */

738   public void setLongLocalVariable (int idx, long v) {
739     topClone().setLongLocalVariable(idx, v);
740   }
741   
742   /**
743    * Returns the value of a long local variable.
744    */

745   public long getLongLocalVariable (int fr, int idx) {
746     return frame(fr).getLongLocalVariable(idx);
747   }
748   
749   /**
750    * Returns the value of a long local variable.
751    */

752   public long getLongLocalVariable (int idx) {
753     return top().getLongLocalVariable(idx);
754   }
755   
756   /**
757    * Gets the value of a long local variable from its name.
758    */

759   public long getLongLocalVariable (int fr, String JavaDoc name) {
760     return frame(fr).getLongLocalVariable(name);
761   }
762   
763   /**
764    * Gets the value of a long local variable from its name.
765    */

766   public long getLongLocalVariable (String JavaDoc name) {
767     return top().getLongLocalVariable(name);
768   }
769   
770   public long getLongReturnValue () {
771     return longPeek();
772   }
773   
774   /**
775    * Returns the current method in the top stack frame.
776    */

777   public MethodInfo getMethod () {
778     if (stack.length > 0) {
779       return top().getMethodInfo();
780     } else {
781       return null;
782     }
783   }
784   
785   public boolean isInCtor () {
786     // <2do> - hmm, if we don't do this the whole stack, we miss factored
787
// init funcs
788
MethodInfo mi = getMethod();
789     return mi.isCtor();
790   }
791   
792   /**
793    * Returns the method info of a specific stack frame.
794    */

795   public MethodInfo getMethod (int idx) {
796     if (stack.length > 0) {
797       return frame(idx).getMethodInfo();
798     } else {
799       return null;
800     }
801   }
802   
803   public String JavaDoc getName () {
804     return threadData.name;
805   }
806   
807   /**
808    * Checks if the thread is waiting to execute a nondeterministic choice,
809    * due to the use of Verify.random... calls.
810    *
811    * <?> pcm - this is not called anywhere, but is part of the 'iThreadInfo'
812    * interface. We clean this up when we remove the interface
813    */

814   public boolean isNonDeterministic () {
815     if (getPC() == null) {
816       return false;
817     }
818     
819     return !getPC().isDeterministic(list.ks.ss, list.ks, this);
820   }
821   
822   public Reference getObjectLocal (String JavaDoc lname) {
823     return list.ks.da.get(getLocalVariable(lname));
824   }
825   
826   public Reference getObjectLocal (int lindex) {
827     return list.ks.da.get(getLocalVariable(lindex));
828   }
829   
830   public Reference getObjectLocal (int fr, String JavaDoc lname) {
831     return list.ks.da.get(getLocalVariable(fr, lname));
832   }
833   
834   public Reference getObjectLocal (int fr, int lindex) {
835     return list.ks.da.get(getLocalVariable(fr, lindex));
836   }
837   
838   /**
839    * Returns the object reference.
840    */

841   public int getObjectReference () {
842     return threadData.objref;
843   }
844   
845   public Reference getObjectReturnValue () {
846     return list.ks.da.get(peek());
847   }
848   
849   public Object JavaDoc getOperandAttr () {
850     return top().getOperandAttr();
851   }
852   
853   public Object JavaDoc getOperandAttr (int opStackOffset) {
854     return top().getOperandAttr(opStackOffset);
855   }
856   
857   public void setOperandAttr (Object JavaDoc attr) {
858     top().setOperandAttr(attr);
859   }
860   
861   /**
862    * Checks if the top operand is a reference.
863    */

864   public boolean isOperandRef () {
865     return top().isOperandRef();
866   }
867   
868   /**
869    * Checks if an operand is a reference.
870    */

871   public boolean isOperandRef (int idx) {
872     return top().isOperandRef(idx);
873   }
874   
875   /**
876    * Sets the program counter of the top stack frame.
877    */

878   public void setPC (Instruction pc) {
879     topClone().setPC(pc);
880   }
881   
882   /**
883    * Returns the program counter of a stack frame.
884    */

885   public Instruction getPC (int i) {
886     return frame(i).getPC();
887   }
888   
889   /**
890    * Returns the program counter of the top stack frame.
891    */

892   public Instruction getPC () {
893     if (stack.length == 0) {
894       return null;
895     }
896     
897     return top().getPC();
898   }
899   
900   public ExceptionInfo getPendingException () {
901     return pendingException;
902   }
903   
904   /**
905    * Returns true if it is possible to execute the next instruction
906    * of this thread. This function is used by the scheduler to determine
907    * which threads can be executed.
908    *
909    * <?> pcm - watch out, it's not just used from Scheduler, but also from
910    * within ThreadInfo itself
911    */

912   public boolean isRunnable () {
913     if (!isEnabled()) {
914       // this filters out waits
915
return false;
916     }
917     
918     // this is for newly created threads with synchronized run() methods
919
if (threadData.status == SYNC_RUNNING) {
920       int sync = (threadData.target != -1)
921         ? threadData.target : threadData.objref;
922       ElementInfo ei = list.ks.da.get(sync);
923       
924       if ((ei != null) && !ei.canLock(this)) {
925         return false;
926       }
927     }
928     
929     Instruction pc = getPC();
930     
931     if (pc == null) {
932       return false;
933     }
934     
935     // the instruction needs to be executable as well
936
// pcm - for now, this is about insns which might require a lock in order to be
937
// executable (invokeX,monitorEnter)
938
return pc.isExecutable(list.ks.ss, list.ks, this);
939   }
940   
941   public short getShortLocal (String JavaDoc lname) {
942     return (short) getLocalVariable(lname);
943   }
944   
945   public short getShortLocal (int lindex) {
946     return (short) getLocalVariable(lindex);
947   }
948   
949   public short getShortLocal (int fr, String JavaDoc lname) {
950     return (short) getLocalVariable(fr, lname);
951   }
952   
953   public short getShortLocal (int fr, int lindex) {
954     return (short) getLocalVariable(fr, lindex);
955   }
956   
957   public short getShortReturnValue () {
958     return (short) peek();
959   }
960   
961   /**
962    * get the current stack trace of this thread
963    * this is called during creation of a Throwable, hence we should skip
964    * all throwable ctors in here
965    * <2do> this is only a partial solution,since we don't catch exceptions
966    * in Throwable ctors yet
967    */

968   public String JavaDoc getStackTrace () {
969     StringBuffer JavaDoc sb = new StringBuffer JavaDoc(256);
970
971     for (int i = stack.length - 1; i >= 0; i--) {
972       StackFrame sf = frame(i);
973       MethodInfo mi = sf.getMethodInfo();
974       
975       if (mi.isCtor()){
976         ClassInfo ci = mi.getClassInfo();
977         if (ci.instanceOf("java.lang.Throwable")) {
978           continue;
979         }
980       }
981
982       sb.append(frame(i).getStackTrace());
983       sb.append("\n");
984     }
985     
986     return sb.toString();
987   }
988   
989   /**
990    * Updates the status of the thread.
991    */

992   public void setStatus (int s) {
993     if (threadData.status != s) {
994       
995       if ((s == RUNNING) || (s == SYNC_RUNNING)) {
996         JVM.getVM().notifyThreadStarted(this);
997       } else if (s == TERMINATED) {
998         JVM.getVM().notifyThreadTerminated(this);
999       }
1000      
1001      threadDataClone().status = s;
1002    }
1003  }
1004  
1005  /**
1006   * Returns the current status of the thread.
1007   */

1008  public int getStatus () {
1009    return threadData.status;
1010  }
1011  
1012  /**
1013   * Returns the information necessary to store.
1014   *
1015   * <2do> pcm - not clear to me how lower stack frames can contribute to
1016   * a different threadinfo state hash - only the current one can be changed
1017   * by the executing method
1018   */

1019  public int[] getStoringData () {
1020    int length = stack.length;
1021    
1022    int[] data = new int[length + 2];
1023    data[0] = getThreadDataIndex();
1024    data[1] = length;
1025    
1026    if (anyChanged) {
1027      if (lowestChanged > 0) {
1028        System.arraycopy(this.data, 2, data, 2, lowestChanged);
1029      }
1030      
1031      for (int i = lowestChanged, j = i + 2; i < length; i++, j++) {
1032        data[j] = getStackFrameIndex(i);
1033      }
1034    } else if (length > 0) {
1035      System.arraycopy(this.data, 2, data, 2, length);
1036    }
1037    
1038    anyChanged = false;
1039    hasChanged = new BitSet JavaDoc();
1040    lowestChanged = -1;
1041    
1042    this.data = data;
1043    
1044    return data;
1045  }
1046  
1047  public String JavaDoc getStringLocal (String JavaDoc lname) {
1048    return list.ks.da.get(getLocalVariable(lname)).asString();
1049  }
1050  
1051  public String JavaDoc getStringLocal (int lindex) {
1052    return list.ks.da.get(getLocalVariable(lindex)).asString();
1053  }
1054  
1055  public String JavaDoc getStringLocal (int fr, String JavaDoc lname) {
1056    return list.ks.da.get(getLocalVariable(fr, lname)).asString();
1057  }
1058  
1059  public String JavaDoc getStringLocal (int fr, int lindex) {
1060    return list.ks.da.get(getLocalVariable(fr, lindex)).asString();
1061  }
1062  
1063  public String JavaDoc getStringReturnValue () {
1064    return list.ks.da.get(peek()).asString();
1065  }
1066  
1067  /**
1068   * Sets the target of the thread.
1069   */

1070  public void setTarget (int t) {
1071    if (threadData.target != t) {
1072      threadDataClone().target = t;
1073    }
1074  }
1075  
1076  /**
1077   * Returns the object reference of the target.
1078   */

1079  public int getTarget () {
1080    return threadData.target;
1081  }
1082  
1083  /**
1084   * Returns the pointer to the object reference of the executing method
1085   */

1086  public int getThis () {
1087    return top().getThis();
1088  }
1089  
1090  public boolean isThis (Reference r) {
1091    if (r == null) {
1092      return false;
1093    }
1094    
1095    if (stack.length == 0) {
1096      return false;
1097    }
1098    
1099    return getMethod().isStatic()
1100      ? false : ((ElementInfo) r).getIndex() == getLocalVariable(0);
1101  }
1102  
1103  public boolean atInvoke (String JavaDoc mname) {
1104    if (stack.length == 0) {
1105      return false;
1106    }
1107    
1108    Instruction pc = getPC();
1109    
1110    if (!(pc instanceof InvokeInstruction)) {
1111      return false;
1112    }
1113    
1114    InvokeInstruction i = (InvokeInstruction) pc;
1115    
1116    return mname.equals(i.cname + "." + i.mname);
1117  }
1118  
1119  public boolean atLabel (String JavaDoc label) {
1120    return Labels.isAt(label, this);
1121  }
1122  
1123  public boolean atMethod (String JavaDoc mname) {
1124    if (stack.length == 0) {
1125      return false;
1126    }
1127    
1128    return getMethod().getCompleteName().equals(mname);
1129  }
1130  
1131  public boolean atPosition (int position) {
1132    if (stack.length == 0) {
1133      return false;
1134    }
1135    
1136    Instruction pc = getPC();
1137    
1138    if (pc == null) {
1139      return false;
1140    }
1141    
1142    return pc.getPosition() == position;
1143  }
1144  
1145  public boolean atReturn () {
1146    if (stack.length == 0) {
1147      return false;
1148    }
1149    
1150    Instruction pc = getPC();
1151    
1152    if (pc == null) {
1153      return false;
1154    }
1155    
1156    return pc instanceof ReturnInstruction;
1157  }
1158  
1159  
1160  /**
1161   * reset any information that has to be re-computed in a backtrack
1162   * (i.e. hasn't been stored explicitly)
1163   */

1164  void resetVolatiles () {
1165    // resetting lock sets goes here
1166
lockedObjects = new LinkedList JavaDoc();
1167  }
1168  
1169  void addLockedObject (ElementInfo ei) {
1170    lockedObjects.add(ei);
1171  }
1172  
1173  void removeLockedObject (ElementInfo ei) {
1174    lockedObjects.remove(ei);
1175  }
1176  
1177  /**
1178   * Restores the state of the system.
1179   */

1180  public void backtrackTo (ArrayOffset storing, Object JavaDoc backtrack) {
1181    
1182    resetVolatiles();
1183    
1184    setThreadDataIndex(storing.get());
1185    
1186    int length = storing.get();
1187    int l = stack.length;
1188    
1189    int[] data = new int[length + 2];
1190    data[0] = tdIndex;
1191    data[1] = length;
1192    System.arraycopy(storing.data, storing.offset, data, 2, length);
1193    
1194    if (length != l) {
1195      if (l > length) {
1196        l = length;
1197      }
1198      
1199      StackFrame[] n = new StackFrame[length];
1200      
1201      if (l > 0) {
1202        System.arraycopy(stack, 0, n, 0, l);
1203      }
1204      
1205      stack = n;
1206    }
1207    
1208    for (int i = 0; i < length; i++) {
1209      setStackFrameIndex(i, storing.get());
1210    }
1211    
1212    atomicData = (AtomicData) backtrack;
1213    
1214    anyChanged = false;
1215    hasChanged = new BitSet JavaDoc();
1216    lowestChanged = -1;
1217    
1218    this.data = data;
1219  }
1220  
1221  /**
1222   * Pops a set of values from the caller stack frame.
1223   */

1224  public void callerPop (int n) {
1225    frameClone(-1).pop(n);
1226  }
1227  
1228  /**
1229   * Clears the operand stack of all value.
1230   */

1231  public void clearOperandStack () {
1232    topClone().clearOperandStack();
1233  }
1234  
1235  public Object JavaDoc clone () {
1236    return new ThreadInfo(this);
1237  }
1238  
1239  public StackFrame[] cloneStack() {
1240    StackFrame[] sf = null;
1241    
1242    // add a StackFrame if the current method is native
1243
// (we only use this in debuging and exception handling so far)
1244

1245    // are we executing in a native method? If yes, it's not on the stack
1246
// and we have to add it on the fly (assuming this is called rather
1247
// infrequently as part of exception handling). Otherwise we really should
1248
// add a StackFrame for every native call
1249
MethodInfo nativeMth = env.getMethodInfo();
1250    if (nativeMth != null){
1251      sf = new StackFrame[stack.length +1];
1252      System.arraycopy(stack, 0, sf, 0, stack.length);
1253      sf[stack.length] = new StackFrame(nativeMth, false, null);
1254      // <2do> we probably should fill in the params/locals here
1255
} else {
1256      sf = (StackFrame[]) stack.clone();
1257    }
1258    
1259    return sf;
1260  }
1261  
1262  /**
1263   * Returns the number of stack frames.
1264   */

1265  public int countStackFrames () {
1266    return stack.length;
1267  }
1268  
1269  int createStackTraceElement ( String JavaDoc clsName, String JavaDoc mthName, String JavaDoc fileName, int line) {
1270    DynamicArea da = DynamicArea.getHeap();
1271    
1272    ClassInfo ci = ClassInfo.getClassInfo("java.lang.StackTraceElement");
1273    int sRef = da.newObject(ci, this);
1274    
1275    ElementInfo sei = da.get(sRef);
1276    sei.setReferenceField("clsName", da.newString(clsName, this));
1277    sei.setReferenceField("mthName", da.newString(mthName, this));
1278    sei.setReferenceField("fileName", da.newString(fileName, this));
1279    sei.setIntField("line", line);
1280    
1281    return sRef;
1282  }
1283  
1284  public int getStackTrace (int objref) {
1285    DynamicArea da = DynamicArea.getHeap();
1286    int stackDepth = countStackFrames();
1287    int i, j=0;
1288    int aRef;
1289    ElementInfo aei;
1290    
1291    // are we executing in a native method? If yes, it's not on the stack
1292
MethodInfo nativeMth = env.getMethodInfo();
1293    if (nativeMth != null){
1294      aRef = da.newArray("Ljava/lang/StackTraceElement", stackDepth+1, this);
1295      aei = da.get(aRef);
1296      
1297      aei.setElement( j++,
1298          createStackTraceElement( nativeMth.getClassInfo().getName(),
1299                                    nativeMth.getName(),
1300                                    nativeMth.getClassInfo().getSourceFileName(), -1));
1301    } else {
1302      aRef = da.newArray("Ljava/lang/StackTraceElement", stackDepth, this);
1303      aei = da.get(aRef);
1304    }
1305    
1306    for (i = stackDepth - 1; i >= 0; i--, j++) {
1307      aei.setElement( j,
1308          createStackTraceElement( getCallStackClass(i), getCallStackMethod(i),
1309                         getCallStackFile(i), getCallStackLine(i)));
1310     }
1311
1312    return aRef;
1313  }
1314  
1315  void print (PrintWriter JavaDoc pw, String JavaDoc s) {
1316    if (pw != null){
1317      pw.print(s);
1318    } else {
1319      vm.print(s);
1320    }
1321  }
1322    
1323  public void printStackTrace (int objRef) {
1324    printStackTrace(null, objRef);
1325  }
1326  
1327  public void printPendingExceptionOn (PrintWriter JavaDoc pw) {
1328    if (pendingException != null) {
1329      printStackTrace( pw, pendingException.getExceptionReference());
1330    }
1331  }
1332  
1333  public void printStackTrace (PrintWriter JavaDoc pw, int objRef) {
1334    // 'env' usage is not ideal, since we don't know from what context we are called, and
1335
// hence the MJIEnv calling context might not be set (no Method or ClassInfo)
1336
// on the other hand, we don't want to re-implement all the MJIEnv accessor methods
1337
print(pw, env.getClassInfo(objRef).getName());
1338    
1339    int msgRef = env.getReferenceField(objRef,"detailMessage");
1340    if (msgRef != MJIEnv.NULL) {
1341      print(pw, ": ");
1342      print(pw, env.getStringObject(msgRef));
1343    }
1344    print(pw, "\n");
1345    
1346    int aRef = env.getReferenceField(objRef, "stackTrace"); // StackTrace[]
1347
if (aRef != MJIEnv.NULL) {
1348      int len = env.getArrayLength(aRef);
1349      for (int i=0; i<len; i++) {
1350        int sRef = env.getReferenceArrayElement(aRef, i);
1351        String JavaDoc clsName = env.getStringObject(env.getReferenceField(sRef, "clsName"));
1352        String JavaDoc mthName = env.getStringObject(env.getReferenceField(sRef, "mthName"));
1353        String JavaDoc fileName = env.getStringObject(env.getReferenceField(sRef, "fileName"));
1354        int line = env.getIntField(sRef, "line");
1355        
1356        print(pw, "\tat ");
1357        print(pw, clsName);
1358        print(pw, ".");
1359        print(pw, mthName);
1360        print(pw, "(");
1361        print(pw, fileName);
1362        print(pw, ":");
1363        
1364        if (line < 0){
1365          print(pw, "native");
1366        } else {
1367          print(pw, Integer.toString(line));
1368        }
1369        
1370        print(pw, ")");
1371        print(pw, "\n");
1372      }
1373    }
1374  }
1375  
1376  // <2do> - not yet functional, fix free calls!!
1377
void callThrowableCtor (ClassInfo ci, int objRef, int msgRef) {
1378    MethodInfo mi = ci.getMethod("<init>(Ljava/lang/String;)", true);
1379    if (mi != null) {
1380      push(objRef, true);
1381      push(msgRef, true);
1382      executeMethod(mi);
1383    }
1384  }
1385  
1386  /**
1387   * Creates an exception and throws it.
1388   */

1389  public Instruction createAndThrowException (ClassInfo ci, String JavaDoc details) {
1390    DynamicArea da = DynamicArea.getHeap();
1391    int objref = da.newObject(ci, this);
1392    int msgref = -1;
1393        
1394    ElementInfo ei = da.get(objref);
1395    
1396    // <2do> pcm - this is not correct! We have to call a propper ctor
1397
// for the Throwable (for now, we just explicitly set the details)
1398
if (details != null) {
1399      msgref = da.newString(details, this);
1400      ei.setReferenceField("detailMessage", "java.lang.Throwable", msgref);
1401    }
1402    
1403    return throwException(objref);
1404  }
1405    
1406  /**
1407   * Creates an exception and throws it.
1408   */

1409  public Instruction createAndThrowException (String JavaDoc cname) {
1410    return createAndThrowException(ClassInfo.getClassInfo(cname), null);
1411  }
1412  
1413  public Instruction createAndThrowException (String JavaDoc cname, String JavaDoc details) {
1414    return createAndThrowException(ClassInfo.getClassInfo(cname), details);
1415  }
1416    
1417  /**
1418   * Duplicates a value on the top stack frame.
1419   */

1420  public void dup () {
1421    topClone().dup();
1422  }
1423  
1424  /**
1425   * Duplicates a long value on the top stack frame.
1426   */

1427  public void dup2 () {
1428    topClone().dup2();
1429  }
1430  
1431  /**
1432   * Duplicates a long value on the top stack frame.
1433   */

1434  public void dup2_x1 () {
1435    topClone().dup2_x1();
1436  }
1437  
1438  /**
1439   * Duplicates a long value on the top stack frame.
1440   */

1441  public void dup2_x2 () {
1442    topClone().dup2_x2();
1443  }
1444  
1445  /**
1446   * Duplicates a value on the top stack frame.
1447   */

1448  public void dup_x1 () {
1449    topClone().dup_x1();
1450  }
1451  
1452  /**
1453   * Duplicates a value on the top stack frame.
1454   */

1455  public void dup_x2 () {
1456    topClone().dup_x2();
1457  }
1458  
1459  /**
1460   * Execute next instruction.
1461   */

1462  public Instruction executeInstruction () {
1463    // this is for threads with synchronized run() methods
1464
// (where we have to grab the lock as soon as we start to execute, no
1465
// matter what the insn is)
1466
if (threadData.status == SYNC_RUNNING) {
1467      int sync = (threadData.target != -1)
1468        ? threadData.target : threadData.objref;
1469      ElementInfo ei = list.ks.da.get(sync);
1470      // gets unlocked when we return from run();
1471
ei.lock(this);
1472      setStatus(RUNNING);
1473    }
1474    
1475    Instruction pc = getPC();
1476    
1477    CoverageManager.incInstruction(pc, index); // <2do> should be a listener!
1478

1479    TrailInfo trail = list.ks.ss.trail();
1480    Step step = new Step(getMethod().getClassInfo().getSourceFileName(),
1481                         getLine(), pc);
1482    trail.addStep(step);
1483    
1484    if (pc.isFirstInstruction() && getMethod().isAtomic()) {
1485      list.ks.setAtomic();
1486    }
1487    
1488//System.out.println("@ " + pc.getMethod().getCompleteName() + " " + pc.getPosition() + " : " + pc);
1489
// execute the next bytecode
1490
Instruction nextPc = pc.execute(list.ks.ss, list.ks, this);
1491    
1492    // we did not return from the last frame stack
1493
if (stack.length != 0) {
1494      setPC(nextPc);
1495    }
1496    
1497    // here we have our bytecode exec observation point
1498
// (note we have to do this after we have set the pc, since a listener
1499
// might come back to do checks like isRunnable)
1500
vm.notifyInstructionExecuted(this, pc, nextPc);
1501    
1502    return nextPc;
1503  }
1504  
1505  
1506  /**
1507   * Executes a method call. It executes the whole method as one atomic step and
1508   * returns when the call is over Arguments have to be already on the stack
1509   *
1510   * This is our entry point for calling methods without corresponding
1511   * INVOKE insns (e.g. <clinit>(), finalize() or method executions from native code
1512   */

1513  public void executeMethod (MethodInfo mi) {
1514    int depth = countStackFrames();
1515 
1516    mi.execute(this, true);
1517 
1518    KernelState ks = list.ks;
1519    SystemState ss = ks.ss;
1520    
1521    while (depth < countStackFrames()) {
1522      Instruction pc = executeInstruction();
1523      
1524      if (ss.violatedAssertion) {
1525        break;
1526      }
1527            
1528      if (pc == null) { // might be a thread in static init
1529
break;
1530      }
1531
1532      if (!pc.isExecutable(ss, ks, this)) {
1533        throw new BlockedAtomicException();
1534      }
1535    }
1536  }
1537    
1538  /**
1539   * Executes next step.
1540   * @return false if intermediate step (due to Nondeterminism or Buchi observable)
1541   */

1542  public boolean executeStep () throws JPFException {
1543    current = this;
1544    
1545    if (porInEffect) {
1546      return executePorStep();
1547    } else {
1548      return executeAtomicLinesStep();
1549    }
1550  }
1551  
1552  // we just got our last stack frame popped, so it's time to close down
1553
public void finish () {
1554    setStatus(TERMINATED);
1555    
1556    // need to own the lock before we can notify
1557
int objref = getObjectReference();
1558    ElementInfo ei = list.ks.da.get(objref);
1559    
1560    ei.lock(this);
1561    ei.notifiesAll();
1562    ei.unlock(this);
1563    
1564    // stack is gone, so reachability might change
1565
list.ks.ss.activateGC();
1566    
1567    //list.remove(index);
1568
}
1569  
1570  public void hash (HashData hd) {
1571    threadData.hash(hd);
1572    atomicData.hash(hd);
1573    
1574    for (int i = 0, l = stack.length; i < l; i++) {
1575      frame(i).hash(hd);
1576    }
1577  }
1578  
1579  public int hashCode () {
1580    HashData hd = new HashData();
1581    
1582    hash(hd);
1583    
1584    return hd.getValue();
1585  }
1586  
1587  public void interrupt () {
1588    if (getStatus() != WAITING) {
1589      return;
1590    }
1591    
1592    setStatus(INTERRUPTED);
1593  }
1594  
1595  /**
1596   * Called when a lock is acquired. Updates the information
1597   * related to the locks.
1598   */

1599  public void lock (Ref ref) {
1600  }
1601  
1602  public void log () {
1603    Debug.println(Debug.MESSAGE,
1604                  "TH#" + index + " #" + threadData.target + " #" +
1605                    threadData.objref + " " + threadData.status);
1606    
1607    for (int i = 0; i < stack.length; i++) {
1608      frame(i).log(i);
1609    }
1610  }
1611  
1612  /**
1613   * Peeks the top long value from the top stack frame.
1614   */

1615  public long longPeek () {
1616    return top().longPeek();
1617  }
1618  
1619  /**
1620   * Peeks a long value from the top stack frame.
1621   */

1622  public long longPeek (int n) {
1623    return top().longPeek(n);
1624  }
1625  
1626  /**
1627   * Pops the top long value from the top stack frame.
1628   */

1629  public long longPop () {
1630    return topClone().longPop();
1631  }
1632  
1633  /**
1634   * Pushes a long value of the top stack frame.
1635   */

1636  public void longPush (long v) {
1637    topClone().longPush(v);
1638  }
1639  
1640  
1641  /**
1642   * mark all objects during gc phase1 which are reachable from this threads
1643   * root set (Thread object, Runnable, stack)
1644   * @aspects: gc
1645   */

1646  void markRoots () {
1647    DynamicArea heap = DynamicArea.getHeap();
1648    
1649    // 1. mark the Thread object itself
1650
heap.markThreadRoot(threadData.objref, index);
1651    
1652    // 2. and its runnable
1653
if (threadData.target != -1) {
1654      heap.markThreadRoot(threadData.target,index);
1655    }
1656    
1657    // 3. now all references on the stack
1658
for (int i = 0, l = stack.length; i < l; i++) {
1659      frame(i).markThreadRoots(index);
1660    }
1661  }
1662    
1663  /**
1664   * Adds a new stack frame for a new called method.
1665   *
1666   * <2do> - turn this into a real stack - don't reallocate
1667   */

1668  public void pushFrame (StackFrame frame) {
1669    atomicData.inSameMethod = false;
1670    
1671    int depth = stack.length;
1672    StackFrame[] n = new StackFrame[depth + 1];
1673    System.arraycopy(stack, 0, n, 0, depth);
1674    stack = n;
1675    
1676    stack[depth] = frame;
1677    
1678    hasChanged.set(depth);
1679    anyChanged = true;
1680    list.ks.data = null;
1681    
1682    if ((lowestChanged == -1) || (lowestChanged > depth)) {
1683      lowestChanged = depth;
1684    }
1685  }
1686  
1687  public ElementInfo objectAtBlockedSynchronized () {
1688    if (stack.length == 0) {
1689      return null;
1690    }
1691    
1692    Instruction pc = getPC();
1693    
1694    if (pc == null) {
1695      return null;
1696    }
1697    
1698    if (pc instanceof InvokeInstruction) {
1699      if (!getMethod().canEnter(this)) {
1700        return getMethod().getBlockedObject(this, true);
1701      }
1702    }
1703    
1704    if (pc instanceof MONITORENTER) {
1705      if (!pc.isExecutable(list.ks.ss, list.ks, this)) {
1706        return list.ks.da.get(peek());
1707      }
1708    }
1709    
1710    return null;
1711  }
1712  
1713  /**
1714   * Peeks the top value from the top stack frame.
1715   */

1716  public int peek () {
1717    if (stack.length > 0) {
1718      return top().peek();
1719    } else {
1720      // <?> not really sure what to do here, but if the stack is gone, so is the thread
1721
return -1;
1722    }
1723  }
1724  
1725  /**
1726   * Peeks a int value from the top stack frame.
1727   */

1728  public int peek (int n) {
1729    if (stack.length > 0) {
1730      return top().peek(n);
1731    } else {
1732      // <?> see peek()
1733
return -1;
1734    }
1735  }
1736  
1737  /**
1738   * Pops the top value from the top stack frame.
1739   */

1740  public int pop () {
1741    if (stack.length > 0) {
1742      return topClone().pop();
1743    } else {
1744      // <?> see peek()
1745
return -1;
1746    }
1747  }
1748  
1749  /**
1750   * Pops a set of values from the top stack frame.
1751   */

1752  public void pop (int n) {
1753    if (stack.length > 0) {
1754      topClone().pop(n);
1755    }
1756  }
1757  
1758  /**
1759   * Removes a stack frame.
1760   */

1761  public boolean popFrame () {
1762    int last = stack.length - 1;
1763    StackFrame sf = stack[last];
1764    
1765    if (getMethod().isAtomic()) {
1766      list.ks.clearAtomic();
1767    }
1768    
1769    if (sf.hasAnyRef()) {
1770      ((SystemState) JVM.getVM().getSystemState()).activateGC();
1771    }
1772    
1773    StackFrame[] n = new StackFrame[last];
1774    System.arraycopy(stack, 0, n, 0, last);
1775    stack = n;
1776    
1777    if (last == 0) {
1778      atomicData.inSameMethod = false;
1779      finish();
1780    } else {
1781      atomicData.inSameMethod = (getMethod() == atomicData.currentMethod);
1782    }
1783    
1784    hasChanged.set(last);
1785    anyChanged = true;
1786    list.ks.data = null;
1787    
1788    if ((lowestChanged == -1) || (lowestChanged > last)) {
1789      lowestChanged = last;
1790    }
1791    
1792    return (last > 0);
1793  }
1794  
1795  public void printInternalErrorTrace (Throwable JavaDoc e) {
1796    String JavaDoc msg = e.getMessage();
1797    
1798    if (msg != null) {
1799      Debug.println(Debug.ERROR,
1800                    "exception " + e.getClass().getName() + ": " + msg);
1801    } else {
1802      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
1803    }
1804    
1805    printStackTrace();
1806    
1807    if (msg != null) {
1808      Debug.println(Debug.ERROR,
1809                    "exception " + e.getClass().getName() + ": " + msg);
1810    } else {
1811      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
1812    }
1813    
1814    printStackContent();
1815  }
1816  
1817  /**
1818   * Prints the content of the stack.
1819   */

1820  public void printStackContent () {
1821    for (int i = stack.length - 1; i >= 0; i--) {
1822      frame(i).printStackContent();
1823    }
1824  }
1825  
1826  /**
1827   * Prints the trace of the stack.
1828   */

1829  public void printStackTrace () {
1830    for (int i = stack.length - 1; i >= 0; i--) {
1831      frame(i).printStackTrace();
1832    }
1833  }
1834  
1835  /**
1836   * Pushes a value on the top stack frame.
1837   */

1838  public void push (int v, boolean ref) {
1839    if (stack.length > 0) { // otherwise we don't have anything to push onto
1840
topClone().push(v, ref);
1841    }
1842  }
1843  
1844  /**
1845   * Removes the arguments of a method call.
1846   */

1847  public void removeArguments (MethodInfo mi) {
1848    int i = mi.getArgumentsSize();
1849    
1850    if (i != 0) {
1851      pop(i);
1852    }
1853  }
1854  
1855  /**
1856   * Swaps two entry on the stack.
1857   */

1858  public void swap () {
1859    topClone().swap();
1860  }
1861  
1862  /**
1863   * Throws an exception throught the stack frames.
1864   */

1865  public Instruction throwException (int objref) {
1866    DynamicArea da = DynamicArea.getHeap();
1867    ElementInfo ei = da.get(objref);
1868    ClassInfo ci = ei.getClassInfo();
1869    MethodInfo mi;
1870    Instruction insn;
1871    int nFrames = countStackFrames();
1872    int i, j;
1873
1874//System.out.println("## ---- got: " + ci.getName());
1875

1876    // we need to store the stack trace in the exception object before
1877
// we start to unwind the stack looking for a handler. Unfortunately,
1878
// the stack dump is accessible for the application, so we have to
1879
// create it in JPF object land
1880
int stRef = getStackTrace(objref);
1881    ei.setReferenceField("stackTrace", "java.lang.Throwable", stRef);
1882    
1883    // but we still keep this in JPF itself too, so that it's more accessible
1884
// for post-mortem 'debugging', and preserves as much JPF execution
1885
// state as possible (e.g. prevents subsequent GC)
1886
pendingException = new ExceptionInfo(this, ei);
1887    
1888    vm.notifyExceptionThrown(this, ei);
1889    
1890    if (!haltOnThrow) {
1891      for (j=0; j<nFrames; j++) {
1892        mi = getMethod();
1893        insn = getPC();
1894        
1895        ExceptionHandler[] exceptions = mi.getExceptions();
1896//System.out.println("## unwinding to: " + mi.getClassInfo().getName() + "." + mi.getUniqueName());
1897
// this is the point where we can check for
1898
// "articifial" stack frames. There is no corresponding
1899
// INVOKE instruction in the frame underneath
1900
if ( (j==0) || (insn instanceof InvokeInstruction)) {
1901          int p = insn.getPosition();
1902                    
1903          if (exceptions != null) {
1904            // checks the exception catched in order
1905
for (i = 0; i < exceptions.length; i++) {
1906              ExceptionHandler eh = exceptions[i];
1907              
1908              // if it falls in the right range
1909
if ((p >= eh.getBegin()) && (p <= eh.getEnd())) {
1910                String JavaDoc en = eh.getName();
1911//System.out.println("## checking: " + ci.getName() + " handler: " + en + " depth: " + stack.length);
1912

1913                // checks if this type of exception is caught here
1914
if ((en == null) || ci.instanceOf(en)) {
1915//System.out.println("## handle");
1916
// clears all the operand stack
1917
clearOperandStack();
1918                  
1919                  // pushes the exception on the stack instead
1920
push(objref, true);
1921                  
1922                  // jumps to the exception handler
1923
Instruction startOfHandlerBlock = mi.getInstructionAt(eh.getHandler());
1924                  setPC(startOfHandlerBlock); // set! we might be in a isDeterministic / isRunnable
1925

1926                  pendingException = null; // handled, no need to keep it
1927

1928                  return startOfHandlerBlock;
1929                }
1930              }
1931            }
1932          }
1933          
1934          if ("<clinit>".equals(mi.getName())) {
1935//System.out.println("## bail");
1936
// we are done here, nobody can handle this - <clinits> don't nest, there is no calling
1937
// context but we should maybe wrap it up into an ExceptionInInitializerError (even though
1938
// that makes it harder to read, and the indirection is not buying us anything)
1939
break;
1940          }
1941          
1942        } else { // ! (insn instanceof InvokeInstruction)
1943
}
1944        
1945        mi.leave(this);
1946        
1947        // remove a frame
1948
popFrame();
1949      }
1950      
1951      // we keep the thread alive to ease post mortem debugging
1952
// <2do> really just required if we check for uncaught exceptions,
1953
// but we always do
1954
//finish(); // toast this thread
1955
}
1956
1957//System.out.println("## unhandled!");
1958

1959    // Ok, I finally made my peace wuth UncaughtException - we can be called from various places,
1960
// including the VM (<clinit>, finalizer) and we can't rely on that all these locations check
1961
// for pc == null. Even if they would, at this point there is nothing to do anymore, get to the
1962
// NoUncaughtProperty reporting as quickly as possible, since chances are we would be even
1963
// obfuscating the problem
1964
NoUncaughtExceptionsProperty.setExceptionInfo(pendingException);
1965    throw new UncaughtException(this, objref);
1966  }
1967  
1968  /**
1969   * Called when a lock is released. Updates the information
1970   * related to the locks.
1971   */

1972  public void unlock (Ref ref) {
1973  }
1974  
1975  protected void setStackFrameIndex (int i, int idx) {
1976    if (hasChanged.get(i) || ((i + 2) >= data.length) ||
1977          (data[i + 2] != idx)) {
1978      stack[i] = (StackFrame) stackFramePool.getObject(idx);
1979    }
1980  }
1981  
1982  protected int getStackFrameIndex (int i) {
1983    if (hasChanged.get(i)) {
1984      HashPool.PoolEntry e = stackFramePool.getEntry(stack[i]);
1985      
1986      stack[i] = (StackFrame) e.getObject();
1987      
1988      return e.getIndex();
1989    } else {
1990      return data[i + 2];
1991    }
1992  }
1993  
1994  protected void setThreadDataIndex (int idx) {
1995    if (tdIndex == idx) {
1996      return;
1997    }
1998    
1999    tdIndex = idx;
2000    threadData = (ThreadData) threadDataPool.getObject(idx);
2001  }
2002  
2003  protected int getThreadDataIndex () {
2004    if (tdIndex != -1) {
2005      return tdIndex;
2006    }
2007    
2008    HashPool.PoolEntry e = threadDataPool.getEntry(threadData);
2009    threadData = (ThreadData) e.getObject();
2010    
2011    return tdIndex = e.getIndex();
2012  }
2013    
2014  /**
2015   * Executes a step where lines are atomic.
2016   * @return false if intermediate step (due to Nondeterminism or Buchi observable)
2017   */

2018  protected boolean executeAtomicLinesStep () throws JPFException {
2019    atomicData.line = getLine();
2020    atomicData.currentMethod = getMethod();
2021    atomicData.inSameMethod = true;
2022    
2023    int[] lines = atomicData.currentMethod.getLineNumbers();
2024    
2025    while (true) {
2026      Instruction pc = executeInstruction();
2027      
2028      if (list.ks.ss.violatedAssertion) {
2029        break;
2030      }
2031            
2032      if (pc == null) {
2033        break;
2034      }
2035      
2036      if (pc.isObservable()) {
2037        list.ks.ss.trail().setAnnotation("observable instruction");
2038        return false;
2039      }
2040      
2041      if (list.ks.ss.isIgnored()) {
2042        throw new IgnoreIfException();
2043      }
2044      
2045      if (!pc.isDeterministic(list.ks.ss, list.ks, this)) {
2046        return false;
2047      }
2048      
2049      if (list.ks.atomicLevel > 0) {
2050        if (!isRunnable()) {
2051          throw new BlockedAtomicException();
2052        }
2053        
2054        continue; // we are still atomic, loop
2055
}
2056      
2057      if (!isRunnable()) {
2058        break;
2059      }
2060      
2061      // <?> pcm - how do we treat methods without line number tables?
2062
// Apparently, AspectJ does this, and I would assume the same for many
2063
// bytecode (re)writers
2064
if (!atomicData.inSameMethod || (lines == null) ||
2065            (atomicData.line != lines[pc.getOffset()] &&
2066               !(pc instanceof ReturnInstruction))) {
2067        atomicData.currentMethod = null;
2068        atomicData.line = -1;
2069        
2070        break;
2071      }
2072    }
2073    
2074    return true;
2075  }
2076    
2077  /**
2078   * execute a step using on-the-fly partial order reduction
2079   */

2080  protected boolean executePorStep () throws JPFException {
2081        
2082    while (true) {
2083      Instruction pc = executeInstruction();
2084            
2085      if (list.ks.ss.violatedAssertion) {
2086        break;
2087      }
2088            
2089      if (pc == null) {
2090        break;
2091      }
2092      
2093      if (pc.isObservable()) {
2094        list.ks.ss.trail().setAnnotation("observable instruction");
2095        return false;
2096      }
2097      
2098      if (list.ks.ss.isIgnored()) {
2099        throw new IgnoreIfException();
2100      }
2101      
2102      if (!pc.isDeterministic(list.ks.ss, list.ks, this)) {
2103        return false;
2104      }
2105      
2106      if (list.ks.atomicLevel > 0) {
2107        // <2do> this is dangerous with Object.wait(J) from an atomic
2108
// section in a lib method (like Thread.join()) !
2109
if (!isRunnable()) {
2110          throw new BlockedAtomicException();
2111        }
2112        continue; // we are still atomic, loop
2113
}
2114
2115      // this will catch MONITOR_ENTER/EXIT, wait, sync run, if they can't exec
2116
if (!isRunnable()) {
2117        return true;
2118      }
2119      
2120      // this will filter out all insns which might alter the state differently
2121
// depending on the scheduling sequence
2122
// Thread.start : always
2123
// sync invoke, MonitorEnter/Exit : other runnable threads
2124
// field / array access : other runnable threads & multi-thread reachable
2125
// runnable wait/notify ??
2126
if ( yield || pc.isSchedulingRelevant(list.ks.ss, list.ks, this)) {
2127        yield = false;
2128        break;
2129      }
2130    }
2131    
2132    return true;
2133  }
2134  
2135  /**
2136   * request a reschedule no matter what the next insn is
2137   * (can be used by listeners who directly modify thread states)
2138   */

2139  public void yield () {
2140    yield = true;
2141  }
2142  
2143  public boolean hasOtherRunnables () {
2144    return list.hasOtherRunnablesThan(index);
2145  }
2146  
2147  /**
2148   * Returns a specific stack frame.
2149   */

2150  protected StackFrame frame (int idx) {
2151    if (idx < 0) {
2152      idx += (stack.length - 1);
2153    }
2154    
2155    return stack[idx];
2156  }
2157  
2158  /**
2159   * Returns a clone of a specific stack frame.
2160   */

2161  protected StackFrame frameClone (int i) {
2162    if (i < 0) {
2163      i += (stack.length - 1);
2164    }
2165    
2166    if (hasChanged.get(i)) {
2167      return stack[i];
2168    }
2169    
2170    hasChanged.set(i);
2171    anyChanged = true;
2172    list.ks.data = null;
2173    
2174    if ((lowestChanged == -1) || (lowestChanged > i)) {
2175      lowestChanged = i;
2176    }
2177    
2178    return stack[i] = (StackFrame) stack[i].clone();
2179  }
2180  
2181  /**
2182   * Returns a clone of the thread data.
2183   */

2184  protected ThreadData threadDataClone () {
2185    if (tdIndex == -1) {
2186      return threadData;
2187    }
2188    
2189    tdIndex = -1;
2190    list.ks.data = null;
2191    
2192    return threadData = (ThreadData) threadData.clone();
2193  }
2194  
2195  /**
2196   * Returns the top stack frame.
2197   */

2198  public StackFrame top () {
2199    if (stack.length > 0) {
2200      return stack[stack.length - 1];
2201    } else {
2202      return null;
2203    }
2204  }
2205  
2206  /**
2207   * Returns a clone of the top stack frame.
2208   */

2209  protected StackFrame topClone () {
2210    int i = stack.length - 1;
2211    
2212    if (hasChanged.get(i)) {
2213      return stack[i];
2214    }
2215    
2216    hasChanged.set(i);
2217    anyChanged = true;
2218    list.ks.data = null;
2219    
2220    if ((lowestChanged == -1) || (lowestChanged > i)) {
2221      lowestChanged = i;
2222    }
2223    
2224    return stack[i] = (StackFrame) stack[i].clone();
2225  }
2226  
2227  void setDaemon (boolean isDaemon) {
2228    threadDataClone().isDaemon = isDaemon;
2229  }
2230  
2231  boolean isDaemon () {
2232    return threadData.isDaemon;
2233  }
2234  
2235  MJIEnv getMJIEnv () {
2236    return env;
2237  }
2238  
2239  void setName (String JavaDoc newName) {
2240    threadDataClone().name = newName;
2241    
2242    // see 'setPriority()', only that it's more serious here, because the
2243
// java.lang.Thread name is stored as a char[]
2244
}
2245  
2246  void setPriority (int newPrio) {
2247    if (threadData.priority != newPrio) {
2248      threadDataClone().priority = newPrio;
2249      
2250      // note that we don't update the java.lang.Thread object, but
2251
// use our threadData value (which works because the object
2252
// values are just used directly from the Thread ctors (from where we pull
2253
// it out in our ThreadInfo ctor), and henceforth only via our intercepted
2254
// native getters
2255
}
2256  }
2257  
2258  int getPriority () {
2259    return threadData.priority;
2260  }
2261  
2262  /**
2263   * this is the method that factorizes common Thread object initialization
2264   * (get's called by all ctors).
2265   * BEWARE - it's hidden magic (undocumented), and should be replaced by our
2266   * own Thread impl at some point
2267   */

2268  void init (int rGroup, int rRunnable, int rName, long stackSize,
2269             boolean setPriority) {
2270    DynamicArea da = JVM.getVM().getDynamicArea();
2271    ElementInfo ei = da.get(rName);
2272    
2273    ThreadData td = threadDataClone();
2274    threadData.name = ei.asString();
2275    threadData.target = rRunnable;
2276    
2277    // stackSize and setPriority are only used by native subsystems
2278
}
2279  
2280  /**
2281   * did we call the current method directly, i.e. no via a INVOKE bytecode insn?
2282   */

2283  public boolean wasDirectCall () {
2284    return top().isDirectCall();
2285  }
2286}
2287
2288
2289
2290
2291
2292
2293
2294
2295
2296
2297
2298
Popular Tags