---

ThreadInfo.java

package gov.nasa.arc.ase.jpf.jvm;

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.jpf.jvm.bytecode.ReturnInstruction;
import gov.nasa.arc.ase.jpf.jvm.bytecode.InvokeInstruction;
import gov.nasa.arc.ase.jpf.jvm.bytecode.INVOKESTATIC;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import gov.nasa.arc.ase.util.HashPool;
import gov.nasa.arc.ase.util.Right;
import java.util.BitSet;
import java.util.Set;
import java.util.HashSet;
//#ifdef JDK11

//#else JDK11
import java.util.LinkedList;
//#endif JDK11
//#ifdef REACHABILITY


//#endif REACHABILITY
//#ifdef RACE


//#endif RACE
//#ifdef LOCK_ORDER




//#endif LOCK_ORDER
//#ifdef COVERAGE

//#endif COVERAGE

/**
 * Represents a thread. It contains the state of the thread, static
 * information about the thread, and the stack frames.
 * Race detection and lock order also store some information
 * in this data structure.
 */
public class ThreadInfo implements iThreadInfo, Storable, Thread {
  /**
   * Pool used to store the thread data.
   */
  private static HashPool threadDataPool = new HashPool();

  /**
   * Pool used to store the stack frames.
   */
  private static HashPool stackFramePool = new HashPool();

  /**
   * Information about the thread.
   */
  private ThreadData threadData;

  /**
   * Some information about the thread that are used to handle
   * atomicity.
   */
  private AtomicData atomicData;

  /**
   * The stack frames of the JVM. 
   */
  private StackFrame[] stack;

  /**
   * Reference of the thread list it is in.
   */
  public ThreadList list;

  /**
   * Position in the thread list.
   */
  public int index;

  /**
   * Contains the index of the thread data last used.
   */
  public int tdIndex = -1;

  /**
   * Identifies which thread has changed.
   */
  public BitSet hasChanged;

  /**
   * Set if any stack frame changed.
   */
  public boolean anyChanged;

  /**
   * Keeps the information from the last storing.
   */
  private int[] data;

  /**
   * Remembers which is the lowest changed stack frame.
   */
  private int lowestChanged;
  
  /**
   * Creates a new empty thread info. Used to backtrack.
   */
  ThreadInfo() {
    stack = new StackFrame[0];
    tdIndex = -1;
    data = new int[0];
    hasChanged = new BitSet();
  }  
  /**
   * Creates a new thread info. It is associated with the object
   * passed and sets the target object as well.
   */
  public ThreadInfo(int o) {
    threadData = new ThreadData();
    threadData.status = NEW;
    if(o != -1)
      threadData.ci = VirtualMachine.getSS().ks.da.get(o).getClassInfo();
    threadData.objref = o;
    threadData.target = -1;
    threadData.lockCount = 0;
//#ifdef RACE




//#endif RACE
//#ifdef LOCK_ORDER







//#endif LOCK_ORDER

    atomicData = new AtomicData();
    atomicData.currentMethod = null;
    atomicData.line = -1;
    atomicData.inSameMethod = false;
    atomicData.softAtomicLevel = 0;

    stack = new StackFrame[0];

    hasChanged = new BitSet();
    anyChanged = false;
    data = new int[0];
    lowestChanged = -1;
  }  
  public ThreadInfo(ThreadInfo ti) {
    if(ti.tdIndex == -1)
      threadData = (ThreadData)ti.threadData.clone();
    else
      threadData = ti.threadData;

    atomicData = (AtomicData)ti.atomicData.clone();

    if(ti.stack != null) {
      int l = ti.stack.length;
      stack = new StackFrame[l];
      if(ti.anyChanged)
    for(int i = 0; i < l; i++)
      if(ti.hasChanged.get(i))
        stack[i] = (StackFrame)ti.stack[i].clone();
      else
        stack[i] = ti.stack[i];
      else
    System.arraycopy(ti.stack, 0, stack, 0, l);
    } else
      stack = null;

    list = null;

    index = -1;

    tdIndex = ti.tdIndex;

    hasChanged = (BitSet)ti.hasChanged.clone();

    anyChanged = ti.anyChanged;

    data = ti.data;

    lowestChanged = ti.lowestChanged;
  }  
  public boolean atInvoke(String mname) {
    if(stack.length == 0) return false;

    Instruction pc = getPC();

    if(!(pc instanceof InvokeInstruction)) return false;
    
    InvokeInstruction i = (InvokeInstruction)pc;
    
    return mname.equals(i.cname + "." + i.mname);
  }  
  public boolean atLabel(String label) {
//#ifdef BUCHI
    return Labels.isAt(label, this);
//#else BUCHI

//#endif BUCHI
  }  
  public boolean atMethod(String mname) {
    if(stack.length == 0) return false;

    return getMethod().getCompleteName().equals(mname);
  }  
  public boolean atPosition(int position) {
    if(stack.length == 0) return false;

    Instruction pc = getPC();

    if(pc == null) return false;

    return pc.getPosition() == position;
  }  
  public boolean atReturn() {
    if(stack.length == 0) return false;

    Instruction pc = getPC();

    if(pc == null) return false;

    return pc instanceof ReturnInstruction;
  }  
  /**
   * Restores the state of the system.
   */
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    setThreadDataIndex(storing.get());
    
    int length = storing.get();
    int l = stack.length;

    int[] data = new int[length+2];
    data[0] = tdIndex;
    data[1] = length;
    System.arraycopy(storing.data, storing.offset, data, 2, length);

    if(length != l) {
      if(l > length) l = length;
      StackFrame[] n = new StackFrame[length];
      if(l > 0)
    System.arraycopy(stack, 0, n, 0, l);
      stack = n;
    }
    
    for(int i = 0; i < length; i++)
      setStackFrameIndex(i, storing.get());

    atomicData = (AtomicData)backtrack;

    anyChanged = false;
    hasChanged = new BitSet();
    lowestChanged = -1;

    this.data = data;
  }  
  /**
   * Pops a set of values from the caller stack frame.
   */
  public void callerPop(int n) {
    frameClone(-1).pop(n);
  }  
  /**
   * Clears the operand stack of all value.
   */
  public void clearOperandStack() {
    topClone().clearOperandStack();
  }  
//#ifdef DISTRIBUTED || PARALLEL








//#endif DISTRIBUTED || PARALLEL

  public Object clone() {
    return new ThreadInfo(this);
  }  
  /**
   * Returns the number of stack frames.
   */
  public int countStackFrames() {
    return stack.length;
  }  
  /**
   * Creates an exception and throws it.
   */
  public Instruction createAndThrowException(ClassInfo ci) {
    int objref = list.ks.da.newObject(ci, this);

    return throwException(objref);
  }  
  /**
   * Creates an exception and throws it.
   */
  public Instruction createAndThrowException(String cname) {
    return createAndThrowException(ClassInfo.getClassInfo(cname));
  }  
  /**
   * Creates a stack frame for a newly called method.
   */
  public void createMethodStackFrame(MethodInfo mi) {
    int nargs = mi.getArgumentsSize();
    int[] args = new int[nargs];
    boolean[] refs = new boolean[nargs];
    if(nargs > 0) {
      StackFrame sf = top();

      for(int i = 0, cnt = nargs-1; i < nargs; i++, cnt--) {
    args[cnt] = sf.peek(i);
    refs[cnt] = sf.isOperandRef(i);
      }
    }

    newFrame(mi);

    if(nargs > 0) {
      StackFrame sf = top();

      for(int i = 0; i < nargs; i++)
    setLocalVariable(i, args[i], refs[i]);
    }
  }  
  /**
   * Duplicates a value on the top stack frame.
   */
  public void dup() {
    topClone().dup();
  }  
  /**
   * Duplicates a value on the top stack frame.
   */
  public void dup_x1() {
    topClone().dup_x1();
  }  
  /**
   * Duplicates a value on the top stack frame.
   */
  public void dup_x2() {
    topClone().dup_x2();
  }  
  /**
   * Duplicates a long value on the top stack frame.
   */
  public void dup2() {
    topClone().dup2();
  }  
  /**
   * Duplicates a long value on the top stack frame.
   */
  public void dup2_x1() {
    topClone().dup2_x1();
  }  
  /**
   * Duplicates a long value on the top stack frame.
   */
  public void dup2_x2() {
    topClone().dup2_x2();
  }  
  /**
   * Starts a soft atomic block.
   */
  public void enterSoftAtomic() {
    atomicData.softAtomicLevel++;
  }  
  /**
   * Executes a step where lines are atomic.
   * @return false if intermediate step (due to Nondeterminism or Buchi observable)
   */
  private boolean executeAtomicLinesStep() {
    atomicData.line = getLine();
    atomicData.currentMethod = getMethod();
    atomicData.inSameMethod = true;

    int[] lines = atomicData.currentMethod.getLineNumbers();

    if(list.ks.ss.ti == null)
      list.ks.ss.ti = new TrailInfo(index, list.ks.ss.sch.getRandom());

//#ifdef LIVELOCK_IN_ATOMIC


//#endif LIVELOCK_IN_ATOMIC

    while(true) {
      Instruction pc = executeInstruction();
    
      if(list.ks.ss.violatedAssertion) break;
    
//#ifdef LIVELOCK_IN_ATOMIC









//#endif LIVELOCK_IN_ATOMIC

      Engine.getJPF().status.instructions++;

      if(pc == null) break;

//#ifdef BUCHI
      if(pc.isObservable()) {
    list.ks.ss.ti.addComment("observable instruction");
    return false;
      }
//#endif BUCHI

      if(pc.examine(list.ks.ss, list.ks, this)) {
    return false;
      }

      if(list.ks.atomicLevel != 0) {
    if(!isRunnable()) {
      printStackTrace();
      throw new JPFErrorException("Non-executable statement in atomic block");
    }
    continue;
      }

      if(!isRunnable()) break;

      if(atomicData.softAtomicLevel != 0) {
    continue;
      }

      if(!atomicData.inSameMethod || (
        atomicData.line != lines[pc.getOffset()] && 
        !(pc instanceof ReturnInstruction))) {
    atomicData.currentMethod = null;
    atomicData.line = -1;
    break;
      }
    }

//#ifdef REACHABILITY










//#endif REACHABILITY

    return true;
  }  
  /**
   * Execute next instruction.
   */
  public Instruction executeInstruction() {
    Instruction pc = getPC();
//#ifdef COVERAGE
//#ifdef HEURISTIC


//#endif HEURISTIC
//#endif COVERAGE
//#ifdef DEBUG

//#endif DEBUG

    list.ks.ss.ti.addStep(getMethod().getClassInfo().getName(), getLine());
    list.ks.ss.ti.addBytecode(pc);

    // execute the next bytecode
    pc = pc.execute(list.ks.ss, list.ks, this);

    // we did not return from the last frame stack
    if(stack.length != 0) setPC(pc);

    return pc;
  }  
  /**
   * Executes a method call. It executes the whole method as one * atomic step and returns when the call is over. It also allows
   * for methods to be reflected. The arguments to the method
   * must already be onto the stack.
   */
  public void executeMethod(MethodInfo mi) {
    int depth = countStackFrames();

    // first sets the trail information so that we can reconstruct the trail
    if(list.ks.ss.ti == null)
      list.ks.ss.ti = new TrailInfo(index, list.ks.ss.sch.getRandom());

//#ifdef LIVELOCK_IN_ATOMIC


//#endif LIVELOCK_IN_ATOMIC

    mi.getClassInfo().executeMethod(this, mi.getFullName());
    while(depth < countStackFrames()) {
      Instruction pc = executeInstruction();
    
      if(list.ks.ss.violatedAssertion) break;
    
//#ifdef LIVELOCK_IN_ATOMIC









//#endif LIVELOCK_IN_ATOMIC

      Engine.getJPF().status.instructions++;

      if(pc == null)
    throw new InternalErrorException("pc == null in executeMethod");

      if(!isRunnable())
    throw new InternalErrorException("blocked in executeMethod");
    }
  }  
  /**
   * execute a step without considering lines to be atomic.
   */
  private boolean executeNoAtomicLinesStep() {
    // first sets the trail information so that we can reconstruct the trail
    if(list.ks.ss.ti == null)
      list.ks.ss.ti = new TrailInfo(index, list.ks.ss.sch.getRandom());

//#ifdef LIVELOCK_IN_ATOMIC


//#endif LIVELOCK_IN_ATOMIC

    while(true) {
      Instruction pc = executeInstruction();

      if(list.ks.ss.violatedAssertion) break;
    
//#ifdef LIVELOCK_IN_ATOMIC








//#endif LIVELOCK_IN_ATOMIC

      Engine.getJPF().status.instructions++;

      if(pc == null) break;
      
//#ifdef BUCHI
      if(pc.isObservable()) {
    list.ks.ss.ti.addComment("observable instruction");
    return false;
      }
//#endif BUCHI

      if(pc.examine(list.ks.ss, list.ks, this))
    return false;

      if(list.ks.atomicLevel != 0) {
    if(!isRunnable()) {
      printStackTrace();
      throw new JPFErrorException("Non-executable statement in atomic block");
    }
    continue;
      }
      if(!isRunnable()) break;
      if(atomicData.softAtomicLevel != 0) {
    continue;
      }

      break;
    }

//#ifdef REACHABILITY










//#endif REACHABILITY

    return true;
  }  
  /**
   * Executes a static method call. It executes the whole method as one
   * atomic step and returns when the call is over. It also allows
   * for methods to be reflected. The arguments to the method
   * must already be onto the stack.
   */
  public void executeStaticMethod(MethodInfo mi) {
    int depth = countStackFrames();

    // first sets the trail information so that we can reconstruct the trail
    if(list.ks.ss.ti == null)
      list.ks.ss.ti = new TrailInfo(index, list.ks.ss.sch.getRandom());

//#ifdef LIVELOCK_IN_ATOMIC


//#endif LIVELOCK_IN_ATOMIC

    mi.getClassInfo().executeStaticMethod(this, mi.getFullName());
    while(depth < countStackFrames()) {
      Instruction pc = executeInstruction();

      if(list.ks.ss.violatedAssertion) break;
    
//#ifdef LIVELOCK_IN_ATOMIC









//#endif LIVELOCK_IN_ATOMIC

      Engine.getJPF().status.instructions++;

      if(pc == null)
    break;

      if(!pc.isExecutable(list.ks.ss, list.ks, this)) {
    list.ks.jvmError(new InternalErrorException("blocked in executeStaticMethod"), this);
      }
    }
  }  
  /**
   * Executes next step.
   * @return false if intermediate step (due to Nondeterminism or Buchi observable)
   */
  public boolean executeStep() {
//#ifdef DEBUG

//#endif DEBUG
    if(VirtualMachine.options.atomic_lines)
      return executeAtomicLinesStep();
    else
      return executeNoAtomicLinesStep();
  }  
  /**
   * Returns a specific stack frame.
   */
  private StackFrame frame(int idx) {
    if(idx < 0) idx += stack.length - 1;

    return stack[idx];
  }  
  /**
   * Returns a clone of a specific stack frame.
   */
  private StackFrame frameClone(int i) {
    if(i < 0) i += stack.length - 1;

    if(hasChanged.get(i)) return stack[i];

    hasChanged.set(i);
    anyChanged = true;
    list.ks.data = null;
    if(lowestChanged == -1 || lowestChanged > i)
      lowestChanged = i;

    return stack[i] = (StackFrame)stack[i].clone();
  }  
  /**
   * Returns the information necessary to backtrack.
   */
  public Object getBacktrackData() {
    return atomicData.clone();
  }  
  public boolean getBooleanLocal(int lindex) { return Types.intToBoolean(getLocalVariable(lindex)); }  
  public boolean getBooleanLocal(String lname) { return Types.intToBoolean(getLocalVariable(lname)); }  
  public boolean getBooleanReturnValue() { return Types.intToBoolean(peek()); }  
  public byte getByteLocal(int lindex) { return (byte)getLocalVariable(lindex); }  
  public byte getByteLocal(String lname) { return (byte)getLocalVariable(lname); }  
  public byte getByteReturnValue() { return (byte)peek(); }  
  /**
   * Returns the this pointer of the callee from the stack.
   */
  public int getCalleeThis(int size) {
    return top().getCalleeThis(size);
  }  
  /**
   * Returns the this pointer of the callee from the stack.
   */
  public int getCalleeThis(MethodInfo mi) {
    return top().getCalleeThis(mi);
  }  
  public String[] getCallStack() {
    int size = stack.length;
    String[] callStack = new String[size];

    for(int i = 0; i < size; i++) {
      StackFrame sf = frame(i);
      
      callStack[i] = sf.getClassInfo().getName() + "." +
    sf.getMethodInfo().getName() + " line " +
    sf.getLine();
    }

    return callStack;
  }  
  public char getCharLocal(int lindex) { return (char)getLocalVariable(lindex); }  
  public char getCharLocal(String lname) { return (char)getLocalVariable(lname); }  
  public char getCharReturnValue() { return (char)peek(); }  
  /**
   * Returns the class information.
   */
  public ClassInfo getClassInfo() {
    return threadData.ci;
  }  
  public double getDoubleLocal(int lindex) { return Types.longToDouble(getLongLocalVariable(lindex)); }  
  public double getDoubleLocal(String lname) { return Types.longToDouble(getLongLocalVariable(lname)); }  
  public double getDoubleReturnValue() { return Types.longToDouble(longPeek()); }  
  public float getFloatLocal(int lindex) { return Types.intToFloat(getLocalVariable(lindex)); }  
  public float getFloatLocal(String lname) { return Types.intToFloat(getLocalVariable(lname)); }  
  public float getFloatReturnValue() { return Types.intToFloat(peek()); }  
  public int getIntLocal(int lindex) { return getLocalVariable(lindex); }  
  public int getIntLocal(String lname) { return getLocalVariable(lname); }  
  public int getIntReturnValue() { return peek(); }  
  /**
   * Returns the line number of the program counter of the top stack frame.
   */
  public int getLine() {
    return top().getLine();
  }  
  /**
   * Returns the line the thread is at.
   */
  public int getLine(int idx) {
    return frame(idx).getLine();
  }  
  /**
   * Returns the value of a local variable.
   */
  public int getLocalVariable(int idx) {
    return top().getLocalVariable(idx);
  }  
  /**
   * Gets the value of a local variable from its name.
   */
  public int getLocalVariable(String name) {
    return top().getLocalVariable(name);
  }  
  /**
   * Gets the type associated with a local variable.
   */
  public String getLocalVariableType(String name) {
    return top().getLocalVariableType(name);
  }  
  /**
   * Returns the number of locks in the last wait.
   */
  public int getLockCount(){
    return threadData.lockCount;
  }  
  public long getLongLocal(int lindex) { return getLongLocalVariable(lindex); }  
  public long getLongLocal(String lname) { return getLongLocalVariable(lname); }  
  /**
   * Returns the value of a long local variable.
   */
  public long getLongLocalVariable(int idx) {
    return top().getLongLocalVariable(idx);
  }  
  /**
   * Gets the value of a long local variable from its name.
   */
  public long getLongLocalVariable(String name) {
    return top().getLongLocalVariable(name);
  }  
  public long getLongReturnValue() { return longPeek(); }  
  /**
   * Returns the current method in the top stack frame.
   */
  public MethodInfo getMethod() {
    return top().getMethodInfo();
  }  
  /**
   * Returns the method info of a specific stack frame.
   */
  public MethodInfo getMethod(int idx) {
    return frame(idx).getMethodInfo();
  }  
  public Reference getObjectLocal(int lindex) { return list.ks.da.get(getLocalVariable(lindex)); }  
  public Reference getObjectLocal(String lname) { return list.ks.da.get(getLocalVariable(lname)); }  
//#ifdef LOCK_ORDER







//#endif LOCK_ORDER

//#ifdef RACE || LOCK_ORDER





//#ifdef LOCK_ORDER












//#endif LOCK_ORDER
//#ifdef RACE


//#endif RACE







//#ifdef LOCK_ORDER

//#endif LOCK_ORDER
//#ifdef RACE


//#endif RACE

//#endif RACE || LOCK_ORDER

  /**
   * Returns the object reference.
   */
  public int getObjectReference() {
    return threadData.objref;
  }  
  public Reference getObjectReturnValue() { return list.ks.da.get(peek()); }  
  /**
   * Returns the program counter of the top stack frame.
   */
  public Instruction getPC() {
    if(stack.length == 0) return null;

    return top().getPC();
  }  
  /**
   * Returns the program counter of a stack frame.
   */
  public Instruction getPC(int i) {
    return frame(i).getPC();
  }  
  public short getShortLocal(int lindex) { return (short)getLocalVariable(lindex); }  
  public short getShortLocal(String lname) { return (short)getLocalVariable(lname); }  
  public short getShortReturnValue() { return (short)peek(); }  
  private int getStackFrameIndex(int i) {
    if(hasChanged.get(i)) {
      HashPool.PoolEntry e = stackFramePool.getEntry(stack[i]);

      stack[i] = (StackFrame)e.getObject();

      return e.getIndex();
    } else
      return data[i+2];
  }  
  /**
   * Returns the current status of the thread.
   */
  public int getStatus() {
    return threadData.status;
  }  
  /**
   * Returns the information necessary to store.
   */
  public int[] getStoringData() {
    int length = stack.length;

    int[] data = new int[length+2];
    data[0] = getThreadDataIndex();
    data[1] = length;

    if(anyChanged) {
      if(lowestChanged > 0)
    System.arraycopy(this.data, 2, data, 2, lowestChanged);

      for(int i = lowestChanged, j = i+2; i < length; i++, j++)
    data[j] = getStackFrameIndex(i);
    } else
      if(length > 0)
    System.arraycopy(this.data, 2, data, 2, length);

    anyChanged = false;
    hasChanged = new BitSet();
    lowestChanged = -1;

    this.data = data;

    return data;
  }  
  public String getStringLocal(int lindex) { return list.ks.da.get(getLocalVariable(lindex)).asString(); }  
  public String getStringLocal(String lname) { return list.ks.da.get(getLocalVariable(lname)).asString(); }  
  public String getStringReturnValue() { return list.ks.da.get(peek()).asString(); }  
  /**
   * Returns the object reference of the target.
   */
  public int getTarget() {
    return threadData.target;
  }  
  /**
   * Returns the pointer to the object reference.
   */
  public int getThis() {
    return top().getThis();
  }  
//#ifdef DISTRIBUTED









//#endif DISTRIBUTED

  private int getThreadDataIndex() {
    if(tdIndex != -1) return tdIndex;

    HashPool.PoolEntry e = threadDataPool.getEntry(threadData);
    threadData = (ThreadData)e.getObject();
    
    return tdIndex = e.getIndex();
  }  
  public void hash(HashData hd) {
    threadData.hash(hd);
    atomicData.hash(hd);

    for(int i = 0, l = stack.length; i < l; i++)
      frame(i).hash(hd);
  }  
  public int hashCode() {
    HashData hd = new HashData();

    hash(hd);

    return hd.getValue();
  }  
  public void interrupt() {
    if(getStatus() != WAITING) return;

    setStatus(INTERRUPTED);
  }  
  /**
   * An alive thread is either running, waiting, notified, or interrupted.
   */
  public boolean isAlive(){
    return threadData.status == RUNNING || 
      threadData.status == WAITING || 
      threadData.status == INTERRUPTED || 
      threadData.status == NOTIFIED;
  }  
  public boolean isCalleeThis(Reference r) {
    if(stack.length == 0) return false;

    Instruction pc = getPC();

    if(pc == null) return false;

    if(!(pc instanceof InvokeInstruction)) return false;
    if(pc instanceof INVOKESTATIC) return false;
    
    InvokeInstruction i = (InvokeInstruction)pc;
    
    return getCalleeThis(Types.getArgumentsSize(i.signature)) ==
      ((ElementInfo)r).index;
  }  
  /**
   * An enabled thread is either running, notified, or interrupted.
   * It also checks if it belongs to the race window.
   */
  public boolean isEnabled() {
//#ifdef RACE




//#endif RACE
      return threadData.status == RUNNING || 
    threadData.status == INTERRUPTED || 
    threadData.status == NOTIFIED;
  }  
  /**
   * Checks if a local variable is a reference.
   */
  public boolean isLocalVariableRef(int idx) {
    return top().isLocalVariableRef(idx);
  }  
  /**
   * Checks if the top operand is a reference.
   */
  public boolean isOperandRef() {
    return top().isOperandRef();
  }  
  /**
   * Checks if an operand is a reference.
   */
  public boolean isOperandRef(int idx) {
    return top().isOperandRef(idx);
  }  
  /**
   * Returns true if it is possible to execute the next instruction
   * of this thread. This function is used by the scheduler to determine
   * which threads can be executed.
   */
  public boolean isRunnable() {
    if(!isEnabled())
      return false;

    Instruction i = getPC();

    if(i == null) return false;

//#ifdef CORINA









//#endif CORINA

//#ifdef COVERAGE




//#endif COVERAGE

    // the instruction needs to be executable as well
    return i.isExecutable(list.ks.ss, list.ks, this);
  }  
  /**
   * Checks if the thread is safe. A thread is safe if its next
   * instruction is safe.
   */
  public boolean isSafe() {
    if(!isEnabled())
      return false;

    return top().isSafe();
  }  
  public boolean isThis(Reference r) {
    if(stack.length == 0) return false;

    return getMethod().isStatic() ?
      false :
      ((ElementInfo)r).index == getLocalVariable(0);
  }  
  /**
   * Leaves a soft atomic block.
   */
  public void leaveSoftAtomic() {
    atomicData.softAtomicLevel--;
  }  
  public void log() {
    Debug.println(Debug.MESSAGE, "TH#" + index + " #" + threadData.target + " #" + threadData.objref + " " + threadData.status);
    for(int i = 0; i < stack.length; i++)
      frame(i).log(i);
  }  
  /**
   * Peeks the top long value from the top stack frame.
   */
  public long longPeek() {
    return top().longPeek();
  }  
  /**
   * Peeks a long value from the top stack frame.
   */
  public long longPeek(int n) {
    return top().longPeek(n);
  }  
  /**
   * Pops the top long value from the top stack frame.
   */
  public long longPop() {
    return topClone().longPop();
  }  
  /**
   * Pushes a long value of the top stack frame.
   */
  public void longPush(long v) {
    topClone().longPush(v);
  }  
//#ifdef MARK_N_SWEEP
  /**
   * Marks the objects referenced by the stack frames.
   */
  public void mark() {
    list.ks.da.mark(threadData.objref);
    if(threadData.target != -1) list.ks.da.mark(threadData.target);

    for(int i = 0, l = stack.length; i < l; i++)
      frame(i).mark(list.ks.da);
  }  
  /**
   * Adds a new stack frame for a new called method.
   */
  public void newFrame(MethodInfo mi) {
    StackFrame sf = new StackFrame(mi);
    if(sf.isSystemMethod())
      enterSoftAtomic();

    atomicData.inSameMethod = false;

    int depth = stack.length;
    StackFrame[] n = new StackFrame[depth + 1];
    System.arraycopy(stack, 0, n, 0, depth);
    stack = n;

    stack[depth] = sf;

    hasChanged.set(depth);
    anyChanged = true;
    list.ks.data = null;
    if(lowestChanged == -1 || lowestChanged > depth)
      lowestChanged = depth;
  }  
//#endif MARK_N_SWEEP

  /**
   * Peeks the top value from the top stack frame.
   */
  public int peek() {
    return top().peek();
  }  
  /**
   * Peeks a value from the top stack frame.
   */
  public int peek(int n) {
    return top().peek(n);
  }  
  /**
   * Pops the top value from the top stack frame.
   */
  public int pop() {
    return topClone().pop();
  }  
  /**
   * Pops a set of values from the top stack frame.
   */
  public void pop(int n) {
    topClone().pop(n);
  }  
  /**
   * Removes a stack frame.
   */
  public void popFrame() {
    int last = stack.length - 1;
    StackFrame sf = stack[last];
//#ifdef MARK_N_SWEEP
    if(sf.hasAnyRef())
      VirtualMachine.getSS().activateGC();
//#endif MARK_N_SWEEP

//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

    if(sf.isSystemMethod())
      leaveSoftAtomic();

    StackFrame[] n = new StackFrame[last];
    System.arraycopy(stack, 0, n, 0, last);
    stack = n;

    if(last == 0) {
      atomicData.inSameMethod = false;
      setStatus(STOPPED);
      list.ks.da.get(threadData.objref).notifies();
    } else
      atomicData.inSameMethod = getMethod() == atomicData.currentMethod;

    hasChanged.set(last);
    anyChanged = true;
    list.ks.data = null;
    if(lowestChanged == -1 || lowestChanged > last)
      lowestChanged = last;
  }  
  public void printInternalErrorTrace(Throwable e) {
    String msg = e.getMessage();
    if(msg != null)
      Debug.println(Debug.ERROR, "exception " + e.getClass().getName() + ": " + msg);
    else
      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
    printStackTrace();
    if(msg != null)
      Debug.println(Debug.ERROR, "exception " + e.getClass().getName() + ": " + msg);
    else
      Debug.println(Debug.ERROR, "exception " + e.getClass().getName());
    printStackContent();
  }  
  /**
   * Prints the content of the stack.
   */
  public void printStackContent() {
    for(int i = stack.length - 1; i >= 0; i--)
      frame(i).printStackContent();
  }  
  /**
   * Prints the trace of the stack.
   */
  public void printStackTrace() {
    for(int i = stack.length-1; i >= 0; i--)
      frame(i).printStackTrace();
  }  
  /**
   * Pushes a value on the top stack frame.
   */
  public void push(int v, boolean ref) {
    topClone().push(v, ref);
  }  
  /**
   * Removes the arguments of a method call.
   */
  public void removeArguments(MethodInfo mi) {
    int i = mi.getArgumentsSize();

    if(i != 0) pop(i);
  }  
  /**
   * Sets the value of a local variable.
   */
  public void setLocalVariable(int idx, int v, boolean ref) {
    topClone().setLocalVariable(idx, v, ref);
  }  
  /**
   * Sets the number of locks held at the time of a wait.
   */
  public void setLockCount(int l){
    if(threadData.lockCount != l)
      threadDataClone().lockCount = l;
  }  
  /**
   * Sets the value of a long local variable.
   */
  public void setLongLocalVariable(int idx, long v) {
    topClone().setLongLocalVariable(idx, v);
  }  
  /**
   * Sets the program counter of the top stack frame.
   */
  public void setPC(Instruction pc) {
    topClone().setPC(pc);
  }  
  private void setStackFrameIndex(int i, int idx) {
    if(hasChanged.get(i) || i+2 >= data.length || data[i+2] != idx)
      stack[i] = (StackFrame)stackFramePool.getObject(idx);
  }  
  /**
   * Updates the status of the thread.
   */
  public void setStatus(int s) {
    if(threadData.status != s)
      threadDataClone().status = s;
  }  
//#ifdef RACE






//#endif RACE

  /**
   * Sets the target of the thread.
   */
  public void setTarget(int t) {
    threadDataClone().target = t;
  }  
  private void setThreadDataIndex(int idx) {
    if(tdIndex == idx) return;

    tdIndex = idx;
    threadData = (ThreadData)threadDataPool.getObject(idx);
  }  
  /**
   * Swaps two entry on the stack.
   */
  public void swap() {
    topClone().swap();
  }  
  /**
   * Returns a clone of the thread data.
   */
  private ThreadData threadDataClone() {
    if(tdIndex == -1) return threadData;

    tdIndex = -1;
    list.ks.data = null;
    return threadData = (ThreadData)threadData.clone();
  }  
  /**
   * Throws an exception throught the stack frames.
   */
  public Instruction throwException(int objref) {
    ClassInfo ci = list.ks.da.get(objref).getClassInfo();

    while (countStackFrames() != 0) {
      MethodInfo mi = getMethod();
      ExceptionHandler[] exceptions = mi.getExceptions();

      if(exceptions != null) {
    int p = getPC().getPosition();

    // checks the exception catched in order
    for(int i = 0, s = exceptions.length; i < s; i++) {
      ExceptionHandler eh = exceptions[i];

      // if it falls in the right range
      if (p >= eh.getBegin() && p <= eh.getEnd()) {
        String en = eh.getName();

        // checks if this type of exception is caught here
        if(en == null || ci.instanceOf(en)) {
          // clears all the operand stack
          clearOperandStack();

          // pushes the exception on the stack instead
          push(objref, true);

          // jumps to the exception handler
          return mi.getInstructionAt(eh.getHandler());
        }
      }
    }
      }

      mi.leave(this);

      // remove a frame
      popFrame();
    }

    // no handler found
    setStatus(STOPPED);
    list.ks.da.get(threadData.objref).notifies();
    throw new UncaughtException(ci.getName());
  }  
  /**
   * Returns the top stack frame.
   */
  private StackFrame top() {
    return stack[stack.length-1];
  }  
  /**
   * Returns a clone of the top stack frame.
   */
  private StackFrame topClone() {
    int i = stack.length - 1;
    
    if(hasChanged.get(i)) return stack[i];

    hasChanged.set(i);
    anyChanged = true;
    list.ks.data = null;
    if(lowestChanged == -1 || lowestChanged > i)
      lowestChanged = i;

    return stack[i] = (StackFrame)stack[i].clone();
  }  
}

---