---

JavaLangObjectReflection.java

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

import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.jvm.*;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;

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

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

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

    if(name.equals("hashCode()I")) {
      return exit(objref ^ 0xABCD);
    }

    if(name.equals("notify()V")) {
      da.get(objref).notifies();

      return exit();
    }

    if(name.equals("notifyAll()V")) {
      da.get(objref).notifiesAll();

      return exit();
    }

    if(name.equals("wait(J)V")) {
      long length = getLongArgument(0);
      boolean timeout = false;

      if(length != 0)
    timeout = ss.random(2) == 0;

      if(timeout)
    return exit();
      else {
    if (th.getStatus() == iThreadInfo.RUNNING) {
      da.get(objref).wait(th);
      return repeat();
    } else if(th.getStatus() == iThreadInfo.NOTIFIED) {
      da.get(objref).lockNotified(th);

      return exit();
    } else if(th.getStatus() == iThreadInfo.INTERRUPTED) {
      da.get(objref).lockNotified(th);

      return throwException("java.lang.InterruptedException");
    } else
      throw new InternalErrorException("invalid thread state");
      }
    }

    if(name.equals("wait()V")) {
      if (th.getStatus() == iThreadInfo.RUNNING) {
    da.get(objref).wait(th);

    return repeat();
      } else if(th.getStatus() == iThreadInfo.NOTIFIED) {
    da.get(objref).lockNotified(th);

    return exit();
      } else if(th.getStatus() == iThreadInfo.INTERRUPTED) {
    da.get(objref).lockNotified(th);

    return throwException("java.lang.InterruptedException");
      } else
    throw new InternalErrorException("invalid thread state");
    }

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

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

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

    if(name.equals("notify()V")) {
      return false;
    }

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

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

    if(name.equals("wait(J)V")) {
      long length = getLongArgument(0);

      return length == 0;
    }

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

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

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

    if(name.equals("wait(J)V")) {
      long length = getLongArgument(0);
      boolean timeout = false;

      if(length != 0)
    timeout = ss.random(2) == 0;

      if(timeout)
    return true;
      else if (th.getStatus() == iThreadInfo.RUNNING)
    return true;
      else if(th.getStatus() == iThreadInfo.NOTIFIED)
    return da.get(objref).canLock(th);
      else if(th.getStatus() == iThreadInfo.INTERRUPTED)
    return da.get(objref).canLock(th);
      else
    throw new InternalErrorException("invalid thread state");
    }

    if(name.equals("wait()V")) {
      if (th.getStatus() == iThreadInfo.RUNNING)
    return true;
      else if(th.getStatus() == iThreadInfo.NOTIFIED)
    return da.get(objref).canLock(th);
      else if(th.getStatus() == iThreadInfo.INTERRUPTED)
    return da.get(objref).canLock(th);
      else
    return false;
    }

    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);
  }  
}

---