---

JavaLangObjectReflection.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.reflection.*;
import de.fub.bytecode.generic.InstructionHandle;

public class JavaLangObjectReflection extends Reflection {
  public InstructionHandle executeMethod(MethodInfo mi, boolean atomic) {
    String name = mi.getFullName();

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

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

    if(name.equals("java.lang.Object.hashCode()I")) {
      // throws a runtime exception for now
      throw new NativeMethodException("java.lang.Object.hashCode()I");
    }

    if(name.equals("java.lang.Object.notify()V")) {
      da.monitorNotify(objref, ks, ss.getScheduler());
      return exit();
    }

    if(name.equals("java.lang.Object.notifyAll()V")) {
      da.monitorNotifyAll(objref, ks);
      return exit();
    }

    if(name.equals("java.lang.Object.wait(J)V")) {
      long length = th.getLongLocalVariable(1);
      boolean timeout = false;

      if(length != 0) timeout = (ss.getScheduler().getCurrentRandom() == 0);

      if(timeout)
    return exit();
      else {
    if (th.getStatus() == STATUS.RUNNING) {
      da.monitorWait(objref, th);
      return repeat();
    } else if(th.getStatus() == STATUS.NOTIFIED) {
      if (da.monitorLockAfterNotified(objref, th))
        return exit();
      else
        return repeat();
    } else
      throw new InternalErrorException("invalid thread state");
      }
    }

    if(name.equals("java.lang.Object.wait()V")) {
      if (th.getStatus() == STATUS.RUNNING) {
    da.monitorWait(objref, th);

    return repeat();
      } else if(th.getStatus() == STATUS.NOTIFIED) {
    if (da.monitorLockAfterNotified(objref, th)) {
      return exit();
    } else
      return repeat();
      } else
    throw new InternalErrorException("invalid thread state");
    }

    return super.executeMethod(mi, atomic);
  }  
  public InstructionHandle executeStaticMethod(MethodInfo mi, boolean atomic) {
    String name = mi.getFullName();

    if(name.equals("java.lang.Object.<clinit>()V")) {
      return repeat();
    }
    
    if(name.equals("java.lang.Object.registerNatives()V")) {
      // throws a runtime exception for now
      throw new NativeMethodException("java.lang.Object.registerNatives()V");
    }

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

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

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

    if(name.equals("java.lang.Object.hashCode()I")) {
      // throws a runtime exception for now
      throw new NativeMethodException("java.lang.Object.hashCode()I");
    }

    if(name.equals("java.lang.Object.wait(J)V")) {
      long length = th.peek2();

      return length == 0;
    }

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

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

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

    if(name.equals("java.lang.Object.hashCode()I")) {
      // throws a runtime exception for now
      throw new NativeMethodException("java.lang.Object.hashCode()I");
    }

    if(name.equals("java.lang.Object.wait(J)V")) {
      long length = th.peek2();
      boolean timeout = false;

      if(length != 0) timeout = (ss.getScheduler().getCurrentRandom() == 0);

      if(timeout)
    return true;
      else if (th.getStatus() == STATUS.RUNNING)
    return true;
      else if(th.getStatus() == STATUS.NOTIFIED)
    return da.monitorCheckLockAfterNotified(objref, th);
      else
    throw new InternalErrorException("invalid thread state");
    }

    if(name.equals("java.lang.Object.wait()V")) {
      if (th.getStatus() == STATUS.RUNNING)
    return true;
      else if(th.getStatus() == STATUS.NOTIFIED)
    return da.monitorCheckLockAfterNotified(objref, th);
      else
    return false;
    }

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

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

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

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

    return super.isStaticMethodExecutable(mi);
  }  
}

---