---

JavaLangThreadReflection.java

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

import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.*;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
//#ifdef RACE

//#endif RACE

public class JavaLangThreadReflection extends Reflection {
  public Instruction executeMethod(MethodInfo mi) {
    String name = mi.getFullName();

    // this is not native but we overload it
    if(name.equals("<init>()V")) {
      ks.tl.locate(objref).setTarget(-1);

      return exit();
    }

    // this is not native but we overload it
    if(name.equals("<init>(Ljava/lang/Runnable;)V")) {
      int target = getIntArgument(1);

      ks.tl.locate(objref).setTarget(target);
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

      return exit();
    }

    // this is not native but we overload it
    if(name.equals("stop()V")) {
      //** warning: should maybe check if the thread can be stopped **//
      ks.tl.locate(objref).setStatus(ThreadInfo.STOPPED);

      return exit();
    }

    if(name.equals("countStackFrames()I")) {
      return exit(ks.tl.locate(objref).countStackFrames());
    }

    if(name.equals("interrupt0()V")) {
      da.get(objref).interrupt();

      return exit();
    }

    if(name.equals("isAlive()Z")) {
      return exit(ks.tl.locate(objref).isAlive());
    }

    if(name.equals("isInterrupted(Z)Z")) {
      // throws a runtime exception for now
      throw new NativeMethodException("isInterrupted(Z)Z");
    }

    if(name.equals("resume0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("resume0()V");
    }

    if(name.equals("setPriority0(I)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("setPriority0(I)V");
    }

    if(name.equals("start()V")) {
      ThreadInfo newThread = ks.tl.locate(objref);
      int target = newThread.getTarget();

      if (target == -1) target = objref;

      da.get(target).lock(newThread);

      ClassInfo ci = da.get(target).getClassInfo();

      MethodInfo run = ci.getDynamicMethod("run()V");

      newThread.setStatus(iThreadInfo.RUNNING);
      newThread.newFrame(run);
      newThread.setLocalVariable(0, target, true);

//#ifdef RACE


//#endif RACE

      return exit();
    }

    if(name.equals("stop0(Ljava/lang/Object;)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("stop0(Ljava/lang/Object;)V");
    }

    if(name.equals("suspend0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("suspend0()V");
    }

    return super.executeMethod(mi);
  }  
  public Instruction executeStaticMethod(MethodInfo mi) {
    String name = mi.getFullName();

    if(name.equals("currentThread()Ljava/lang/Thread;")) {
      return exitReference(th.getObjectReference());
    }

    if(name.equals("registerNatives()V")) {
      return exit();
    }

    if(name.equals("sleep(J)V")) {
      return exit();
    }

    if(name.equals("yield()V")) {
      return exit();
    }

    return super.executeStaticMethod(mi);
  }  
  public boolean isMethodDeterministic(MethodInfo mi) {
    String name = mi.getFullName();

    //if(name.equals("isAlive()Z")) {
      // throws a runtime exception for now
    // throw new NativeMethodException("isAlive()Z");
    //}

    if(name.equals("isInterrupted(Z)Z")) {
      // throws a runtime exception for now
      throw new NativeMethodException("isInterrupted(Z)Z");
    }

    if(name.equals("resume0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("resume0()V");
    }

    if(name.equals("setPriority0(I)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("setPriority0(I)V");
    }

    if(name.equals("stop0(Ljava/lang/Object;)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("stop0(Ljava/lang/Object;)V");
    }

    if(name.equals("suspend0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("suspend0()V");
    }

    return super.isMethodDeterministic(mi);
  }  
  public boolean isMethodExecutable(MethodInfo mi) {
    String name = mi.getFullName();

    // this is not native but we overload it
    if(name.equals("<init>"))
      return true;

    //    if(name.equals("isAlive()Z")) {
    // throws a runtime exception for now
    // throw new NativeMethodException("isAlive()Z");
    //}

    if(name.equals("isInterrupted(Z)Z")) {
      // throws a runtime exception for now
      throw new NativeMethodException("isInterrupted(Z)Z");
    }

    if(name.equals("resume0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("resume0()V");
    }

    if(name.equals("setPriority0(I)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("setPriority0(I)V");
    }

    if(name.equals("start()V")) {
      ThreadInfo newThread = ks.tl.locate(objref);
      int target = newThread.getTarget();

      if (target == -1) target = objref;

      return da.get(target).canLock(newThread);
    }

    if(name.equals("stop0(Ljava/lang/Object;)V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("stop0(Ljava/lang/Object;)V");
    }

    if(name.equals("suspend0()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("suspend0()V");
    }

    return super.isMethodExecutable(mi);
  }  
  public boolean isStaticMethodDeterministic(MethodInfo mi) {
    String name = mi.getFullName();

    return super.isStaticMethodDeterministic(mi);
  }  
  public boolean isStaticMethodExecutable(MethodInfo mi) {
    String name = mi.getFullName();

    return super.isStaticMethodExecutable(mi);
  }  
}

---