---

JavaLangSystemReflection.java

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

import gov.nasa.arc.ase.jpf.jvm.ClassInfo;
import gov.nasa.arc.ase.jpf.jvm.ThreadInfo;
import gov.nasa.arc.ase.jpf.jvm.MethodInfo;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
//#ifdef JDK11


//#else JDK11
import java.util.List;
import java.util.Iterator;
//#endif JDK11

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

    if(name.equals("<clinit>()V")) {
      // this is the class initialization code for the System class
      // it should create the in, out, and err stream.
      int objref = ks.da.newObject(
        ClassInfo.getClassInfo("java.io.PrintStream"), 
        th);
      setReferenceStaticField("out", objref);
      setReferenceStaticField("err", objref);

      return exit();
    }

    if(name.equals("arraycopy(Ljava/lang/Object;ILjava/lang/Object;II)V")) {
      Reflection src = getObjectArgument(0);
      int src_position = getIntArgument(1);
      Reflection dst = getObjectArgument(2);
      int dst_position = getIntArgument(3);
      int length = getIntArgument(4);

      if(src.getArrayTypeSize() == 1)
    for(int i = 0; i < length; i++)
      dst.setIntArrayElement(dst_position++,
          src.getIntArrayElement(src_position++));
      else
    for(int i = 0; i < length; i++)
      dst.setLongArrayElement(dst_position++,
          src.getLongArrayElement(src_position++));

      return exit();
    }

    if(name.equals("exit(I)V")) {
      int length = ks.tl.length();

      for(int i = 0; i < length; i++) {
    ThreadInfo ti = ks.tl.get(i);

    while(th.countStackFrames() != 0)
      ti.popFrame();
      }
    }

    if(name.equals("currentTimeMillis()J")) {
      return exit(0L);
    }

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

    if(name.equals("identityHashCode(Ljava/lang/Object;)I")) {
      int objref = th.getLocalVariable(0);
      return exit(objref ^ 0xABCD);
    }

    if(name.equals("initProperties(Ljava/util/Properties;)Ljava/util/Properties;")) {
      // throws a runtime exception for now
      throw new NativeMethodException("initProperties(Ljava/util/Properties;)Ljava/util/Properties;");
    }

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

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

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

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

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

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

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

    if(name.equals("initProperties(Ljava/util/Properties;)Ljava/util/Properties;")) {
      // throws a runtime exception for now
      throw new NativeMethodException("initProperties(Ljava/util/Properties;)Ljava/util/Properties;");
    }

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

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

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

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

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

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

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

    if(name.equals("initProperties(Ljava/util/Properties;)Ljava/util/Properties;")) {
      // throws a runtime exception for now
      throw new NativeMethodException("initProperties(Ljava/util/Properties;)Ljava/util/Properties;");
    }

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

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

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

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

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

    return super.isStaticMethodExecutable(mi);
  }  
}

---