---

Reflection.java

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

import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.util.*;
import gov.nasa.arc.ase.jpf.jvm.*;
import gov.nasa.arc.ase.jpf.jvm.bytecode.ATHROW;
import gov.nasa.arc.ase.util.Debug;
import de.fub.bytecode.Constants;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;

public class Reflection implements Cloneable, Constants {
  /**
   * Packages where to look for reflection classes.
   */
  private static String[] reflectionPath = {
    "gov.nasa.arc.ase.jpf.jvm.reflection", ""
  };

  /**
   * Class the reflection refers to.
   */
  protected ClassInfo ci;

  /**
   * Object the reflection refers to.
   */
  protected int objref;

  /**
   * The system state.
   */
  protected SystemState ss;

  /**
   * The kernel state.
   */
  protected KernelState ks;

  /**
   * The Thread Info of the running thread.
   */
  protected ThreadInfo th;

  /**
   * The Dynamic Area.
   */ 
  protected DynamicArea da;

  /**
   * The Static Area.
   */
  protected StaticArea sa;

  /**
   * Creates a new default reflection object.
   */
  public Reflection() {
    ci = null;
    objref = -1;
    ss = null;
    ks = null;
    th = null;
    da = null;
    sa = null;
  }  
  /**
   * Returns an array of booleans.
   */
  protected boolean[] asBooleanArray() {
    return da.get(objref).asBooleanArray();
  }  
  /**
   * Returns an array of bytes.
   */
  protected byte[] asByteArray() {
    return da.get(objref).asByteArray();
  }  
  /**
   * Returns an array of chars.
   */
  protected char[] asCharArray() {
    return da.get(objref).asCharArray();
  }  
  /**
   * Returns an array of doubles.
   */
  protected double[] asDoubleArray() {
    return da.get(objref).asDoubleArray();
  }  
  /**
   * Returns an array of floats.
   */
  protected float[] asFloatArray() {
    return da.get(objref).asFloatArray();
  }  
  /**
   * Returns an array of integers.
   */
  protected int[] asIntArray() {
    return da.get(objref).asIntArray();
  }  
  /**
   * Returns an array of longs.
   */
  protected long[] asLongArray() {
    return da.get(objref).asLongArray();
  }  
  /**
   * Returns an array of objects.
   */
  protected Reflection[] asObjectArray() {
    return da.get(objref).asObjectArray();
  }  
  /**
   * Returns an array of shorts.
   */
  protected short[] asShortArray() {
    return da.get(objref).asShortArray();
  }  
  /**
   * Returns the string representation of a string object.
   */
  protected String asString() {
    return da.get(objref).asString();
  }  
  /**
   * Real code that executes the method. Override this method to change
   * the behavior of the method.
   */
  protected Instruction executeMethod(MethodInfo mi) {
    if(mi.isNative()) {
      throw new NativeMethodException(mi.getFullName());
    }

    mi.enter(th);

    return start();
  }  
  /**
   * Executes a method call.
   */
  public final Instruction executeMethod(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    Instruction i = executeMethod(mi);
    setThreadInfo(null);

    return i;
  }  
  /**
   * Real code that executes the static method. Override this method to change
   * the behavior of the method.
   */
  protected Instruction executeStaticMethod(MethodInfo mi) {
    if(mi.isNative()) {
      throw new NativeMethodException(mi.getFullName());
    }

    mi.enter(th);

    return start();
  }  
  /**
   * Executes a static method call.
   */
  public final Instruction executeStaticMethod(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    Instruction i = executeStaticMethod(mi);
    setThreadInfo(null);

    return i;
  }  
  /**
   * Exits from a void method.
   */
  protected final Instruction exit() {
    MethodInfo mi = th.getMethod();
    th.popFrame();
    th.removeArguments(mi);

    if(th.getPC() == null) return null;

    return th.getPC().getNext();
  }  
  /**
   * Exits from a method with a byte return value.
   */
  protected Instruction exit(byte retval) {
    return exit((int)retval);
  }  
  /**
   * Exits from a method with a char return value.
   */
  protected Instruction exit(char retval) {
    return exit((int)retval);
  }  
  /**
   * Exits from a method with a double return value.
   */
  protected Instruction exit(double retval) {
    return exit(Types.doubleToLong(retval));
  }  
  /**
   * Exits from a method with a float return value.
   */
  protected Instruction exit(float retval) {
    return exit(Types.floatToInt(retval));
  }  
  /**
   * Exits from a method with an integer return value.
   */
  protected Instruction exit(int retval) {
    MethodInfo mi = th.getMethod();
    th.popFrame();
    th.removeArguments(mi);
    th.push(retval, false);

    return th.getPC().getNext();
  }  
  /**
   * Exits from a method with a long return value.
   */
  protected Instruction exit(long retval) {
    MethodInfo mi = th.getMethod();
    th.popFrame();
    th.removeArguments(mi);
    th.longPush(retval);

    return th.getPC().getNext();
  }  
  /**
   * Exits from a method with an object return value.
   */
  protected Instruction exit(Reflection retval) {
    return exitReference(retval.objref);
  }  
  /**
   * Exits from a method with a short return value.
   */
  protected Instruction exit(short retval) {
    return exit((int)retval);
  }  
  /**
   * Exits from a method with a boolean return value.
   */
  protected Instruction exit(boolean retval) {
    return exit(Types.booleanToInt(retval));
  }  
  /**
   * Exits from a method with an object return value using a reference.
   */
  protected Instruction exitReference(int retval) {
    MethodInfo mi = th.getMethod();
    th.popFrame();
    th.removeArguments(mi);
    th.push(retval, true);

    return th.getPC().getNext();
  }  
  public String getArrayType() {
    return da.get(objref).getArrayType();
  }  
  public int getArrayTypeSize() {
    return Types.getTypeSize(getArrayType());
  }  
  /**
   * Gets a boolean argument.
   */
  protected boolean getBooleanArgument(int index) {
    return Types.intToBoolean(getIntArgument(index));
  }  
  /**
   * Returns a boolean value.
   */
  public boolean getBooleanArrayElement(int index) {
    return Types.intToBoolean(getIntArrayElement(index * getArrayTypeSize()));
  }  
  /**
   * Returns a boolean value.
   */
  public boolean getBooleanField(String fname) {
    return Types.intToBoolean(getIntField(fname));
  }  
  /**
   * Returns a boolean value.
   */
  public boolean getBooleanStaticField(String fname) {
    return Types.intToBoolean(getIntStaticField(fname));
  }  
  /**
   * Gets a byte argument.
   */
  protected byte getByteArgument(int index) {
    return (byte)getIntArgument(index);
  }  
  /**
   * Returns the value of a byte array element.
   */
  public byte getByteArrayElement(int index) {
    return (byte)getIntArrayElement(index * getArrayTypeSize());
  }  
  /**
   * Returns the value of a byte field.
   */
  public byte getByteField(String fname) {
    return (byte)getIntField(fname);
  }  
  /**
   * Returns the value of a byte static field.
   */
  public byte getByteStaticField(String fname) {
    return (byte)getIntStaticField(fname);
  }  
  /**
   * Gets a char argument.
   */
  protected char getCharArgument(int index) {
    return (char)getIntArgument(index);
  }  
  /**
   * Returns the value of a character array element.
   */
  public char getCharArrayElement(int index) {
    return (char)getIntArrayElement(index * getArrayTypeSize());
  }  
  /**
   * Returns the value of a character field.
   */
  public char getCharField(String fname) {
    return (char)getIntField(fname);
  }  
  /**
   * Returns the value of a character static field.
   */
  public char getCharStaticField(String fname) {
    return (char)getIntStaticField(fname);
  }  
  /**
   * Gets a double argument.
   */
  protected double getDoubleArgument(int index) {
    return Types.longToDouble(getLongArgument(index));
  }  
  /**
   * Returns the value of a double array element.
   */
  public double getDoubleArrayElement(int index) {
    return Types.longToDouble(getLongArrayElement(index * getArrayTypeSize()));
  }  
  /**
   * Returns the value of a double field.
   */
  public double getDoubleField(String fname) {
    return Types.longToDouble(getLongField(fname));
  }  
  /**
   * Returns the value of a double static field.
   */
  public double getDoubleStaticField(String fname) {
    return Types.longToDouble(getLongStaticField(fname));
  }  
  /**
   * Gets a float argument.
   */
  protected float getFloatArgument(int index) {
    return Types.intToFloat(getIntArgument(index));
  }  
  /**
   * Returns the value of a float array element.
   */
  public float getFloatArrayElement(int index) {
    return Types.intToFloat(getIntArrayElement(index * getArrayTypeSize()));
  }  
  /**
   * Returns the value of a float field.
   */
  public float getFloatField(String fname) {
    return Types.intToFloat(getIntField(fname));
  }  
  /**
   * Returns the value of a float static field.
   */
  public float getFloatStaticField(String fname) {
    return Types.intToFloat(getIntStaticField(fname));
  }  
  /**
   * Gets an integer argument.
   */
  protected int getIntArgument(int idx) {
    return th.getLocalVariable(idx);
  }  
  /**
   * Returns the value of an integer array element.
   */
  public int getIntArrayElement(int index) {
    return da.get(objref).getField(index);
  }  
  /**
   * Returns the value of an integer field.
   */
  public int getIntField(String fname) {
    return da.get(objref).getField(fname);
  }  
  /**
   * Returns the value of an integer static field.
   */
  public int getIntStaticField(String fname) {
    return sa.get(ci.getName()).getField(fname);
  }  
  /**
   * Gets a long argument.
   */
  protected long getLongArgument(int idx) {
    return th.getLongLocalVariable(idx);
  }  
  /**
   * Returns the value of a long array element.
   */
  public long getLongArrayElement(int index) {
    return da.get(objref).getLongField(index);
  }  
  /**
   * Returns the value of a long field.
   */
  public long getLongField(String fname) {
    return da.get(objref).getLongField(fname);
  }  
  /**
   * Returns the value of a long static field.
   */
  public long getLongStaticField(String fname) {
    return sa.get(ci.getName()).getLongField(fname);
  }  
  /**
   * Gets an object argument.
   */
  protected Reflection getObjectArgument(int idx) {
    Reflection r = da.get(getIntArgument(idx)).getReflection();
    r.setThreadInfo(th);

    return r;
  }  
  /**
   * Returns the value of an object array element.
   */
  public Reflection getObjectArrayElement(int index) {
    Reflection r = da.get(getIntArrayElement(index * getArrayTypeSize())).getReflection();
    r.setThreadInfo(th);

    return r;
  }  
  /**
   * Returns the value of an object field.
   */
  public Reflection getObjectField(String fname) {
    Reflection r = da.get(getIntField(fname)).getReflection();
    r.setThreadInfo(th);

    return r;
  }  
  /**
   * Returns the value of an object static field.
   */
  public Reflection getObjectStaticField(String fname) {
    Reflection r = da.get(getIntStaticField(fname)).getReflection();
    r.setThreadInfo(th);

    return r;
  }  
  /**
   * Returns the reflection for a class.
   */
  protected static Reflection getReflection(String classname) {
    return ClassInfo.getClassInfo(classname).getReflection();
  }  
  /**
   * Gets a short argument.
   */
  protected short getShortArgument(int index) {
    return (short)getIntArgument(index);
  }  
  /**
   * Returns a short value.
   */
  public short getShortArrayElement(int index) {
    return (short)getIntArrayElement(index * getArrayTypeSize());
  }  
  /**
   * Returns a short value.
   */
  public short getShortField(String fname) {
    return (short)getIntField(fname);
  }  
  /**
   * Returns a short value.
   */
  public short getShortStaticField(String fname) {
    return (short)getIntStaticField(fname);
  }  
  /**
   * As a special case, returns the string representation of an argument.
   */
  protected String getStringArgument(int index) {
    return da.get(getIntArgument(index)).asString();
  }  
  public Reflection instantiate() {
    try {
      Reflection r = (Reflection)clone();
      r.objref = -1;

      return r;
    } catch(CloneNotSupportedException e) {
      return null;
    }
  }  
  /**
   * Creates an instance of the reflection class for an object.
   */
  public Reflection instantiate(int objref) {
    try {
      Reflection r = (Reflection)clone();
      r.objref = objref;

      return r;
    } catch(CloneNotSupportedException e) {
      return null;
    }
  }  
  /**
   * Really cheks for determinism.
   */
  protected boolean isMethodDeterministic(MethodInfo mi) {
    return true;
  }  
  /**
   * Checks to see if a method is deterministic.
   */
  public final boolean isMethodDeterministic(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    boolean result = isMethodDeterministic(mi);
    setThreadInfo(null);

    return result;
  }  
  /**
   * Really checks for executability.
   */
  protected boolean isMethodExecutable(MethodInfo mi) {
    return mi.canEnter(th);
  }  
  /**
   * Checks is a method is executable.
   */ 
  public final boolean isMethodExecutable(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    boolean result = isMethodExecutable(mi);
    setThreadInfo(null);

    return result;
  }  
  /**
   * Really checks for static method determinism.
   */
  protected boolean isStaticMethodDeterministic(MethodInfo mi) {
    return true;
  }  
  /**
   * Checks to see if a static method is deterministic.
   */
  public final boolean isStaticMethodDeterministic(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    boolean result = isStaticMethodDeterministic(mi);
    setThreadInfo(null);

    return result;
  }  
  /**
   * Really checks for static method executability.
   */
  protected boolean isStaticMethodExecutable(MethodInfo mi) {
    return mi.canEnter(th);
  }  
  /**
   * Checks to see if a static method is executable.
   */
  public final boolean isStaticMethodExecutable(ThreadInfo th, MethodInfo mi) {
    setThreadInfo(th);
    boolean result = isStaticMethodExecutable(mi);
    setThreadInfo(null);

    return result;
  }  
  /**
   * Loads the reflection for a given class.
   */
  public static Reflection load(String name) {
    Reflection r = null;
    int l = reflectionPath.length;

    for(int i = 0; i < l && r == null; i++) {
      String cn;

      if(reflectionPath[i].equals(""))
    cn = name + "Reflection";
      else
    cn = reflectionPath[i] + "." + name + "Reflection";

      try {
    Class clazz = Class.forName(cn);
    r = (Reflection)clazz.newInstance();
    Debug.println(Debug.MESSAGE, "Loading class " + cn);
      } catch(InstantiationException e) {
    throw new InternalErrorException("Can't instantiate " + cn);
      } catch(IllegalAccessException e) {
    throw new InternalErrorException("Can't instantiate " + cn);
      } catch(ClassNotFoundException e) {
      }
    }

    for(int i = 0; i < l && r == null; i++) {
      String cn;

      if(reflectionPath[i].equals(""))
    cn = reflectionClassName(name) + "Reflection";
      else
    cn = reflectionPath[i] + "." + reflectionClassName(name) + "Reflection";

      try {
    Class clazz = Class.forName(cn);
    r = (Reflection)clazz.newInstance();
    Debug.println(Debug.WARNING, "Loading class " + cn);
      } catch(InstantiationException e) {
    throw new InternalErrorException("Can't instantiate " + cn);
      } catch(IllegalAccessException e) {
    throw new InternalErrorException("Can't instantiate " + cn);
      } catch(ClassNotFoundException e) {
      }
    }

    if(r == null) r = new Reflection();

    return r;
  }  
  /**
   * Translates a class name with package into the possible name
   * for a reflection class.
   */
  private static String reflectionClassName(String name) {
    int index = 0;
    int last = 0;
    StringBuffer sb = new StringBuffer();

    while((index = name.indexOf(".", last)) != -1) {
      sb.append(Character.toUpperCase(name.charAt(last)));
      sb.append(name.substring(last + 1, index));
      last = index + 1;
    }

    sb.append(name.substring(last));

    return sb.toString();
  }  
  /**
   * Repeats this method again.
   */
  protected Instruction repeat() {
    th.popFrame();

    return th.getPC();
  }  
  /**
   * Sets the value of a boolean static field.
   */
  public void setBooleanStaticField(String fname, boolean value) {
    setIntStaticField(fname, Types.booleanToInt(value));
  }  
  /**
   * Sets the value of a boolean array element.
   */
  public void setBooleanValue(int index, boolean value) {
    setIntArrayElement(index * getArrayTypeSize(), Types.booleanToInt(value));
  }  
  /**
   * Sets the value of a boolean field.
   */
  public void setBooleanValue(String fname, boolean value) {
    setIntField(fname, Types.booleanToInt(value));
  }  
  /**
   * Sets the value of a byte array element.
   */
  public void setByteArrayElement(int index, byte value) {
    setIntArrayElement(index * getArrayTypeSize(), (int)value);
  }  
  /**
   * Sets the value of a byte field.
   */
  public void setByteField(String fname, byte value) {
    setIntField(fname, (int)value);
  }  
  /**
   * Sets the value of a byte static field.
   */
  public void setByteStaticField(String fname, byte value) {
    setIntStaticField(fname, (int)value);
  }  
  /**
   * Sets the value of a char array element.
   */
  public void setCharArrayElement(int index, char value) {
    setIntArrayElement(index * getArrayTypeSize(), (int)value);
  }  
  /**
   * Sets the value of a char field.
   */
  public void setCharField(String fname, char value) {
    setIntField(fname, (int)value);
  }  
  /**
   * Sets the value of a char static field.
   */
  public void setCharStaticField(String fname, char value) {
    setIntStaticField(fname, (int)value);
  }  
  /**
   * Sets the class info.
   */
  public void setClassInfo(ClassInfo c) {
    ci = c;
  }  
  /**
   * Sets the value of a double array element.
   */
  public void setDoubleArrayElement(int index, double value) {
    setLongArrayElement(index * getArrayTypeSize(), Types.doubleToLong(value));
  }  
  /**
   * Sets the value of a double field.
   */
  public void setDoubleField(String fname, double value) {
    setLongField(fname, Types.doubleToLong(value));
  }  
  /**
   * Sets the value of a double static field.
   */
  public void setDoubleStaticField(String fname, double value) {
    setLongStaticField(fname, Types.doubleToLong(value));
  }  
  /**
   * Sets the value of a float array element.
   */
  public void setFloatArrayElement(int index, float value) {
    setIntArrayElement(index * getArrayTypeSize(), Types.floatToInt(value));
  }  
  /**
   * Sets the value of a float field.
   */
  public void setFloatField(String fname, float value) {
    setIntField(fname, Types.floatToInt(value));
  }  
  /**
   * Sets the value of a float static field.
   */
  public void setFloatStaticField(String fname, float value) {
    setIntStaticField(fname, Types.floatToInt(value));
  }  
  /**
   * Sets the value of an integer array element.
   */
  public void setIntArrayElement(int index, int value) {
    da.get(objref).setField(index, value);
  }  
  /**
   * Sets the value of an integer field.
   */
  public void setIntField(String fname, int value) {
    da.get(objref).setField(fname, value);
  }  
  /**
   * Sets the value of an integer static field.
   */
  public void setIntStaticField(String fname, int value) {
    sa.get(ci.getName()).setField(fname, value);
  }  
  /**
   * Sets the value of an integer array element.
   */
  public void setLongArrayElement(int index, long value) {
    da.get(objref).setLongField(index, value);
  }  
  /**
   * Sets the value of an integer field.
   */
  public void setLongField(String fname, long value) {
    da.get(objref).setLongField(fname, value);
  }  
  /**
   * Sets the value of an integer static field.
   */
  public void setLongStaticField(String fname, long value) {
    sa.get(ci.getName()).setLongField(fname, value);
  }  
  /**
   * Sets the value of an object array element.
   */
  public void setObjectArrayElement(int index, Reflection value) {
    if(value == null)
      setIntArrayElement(index * getArrayTypeSize(), -1);
    else
      setIntArrayElement(index * getArrayTypeSize(), value.objref);
  }  
  /**
   * Sets the value of an object field.
   */
  public void setObjectField(String fname, Reflection value) {
    if(value == null)
      setIntField(fname, -1);
    else
      setIntField(fname, value.objref);
  }  
  /**
   * Sets the value of an object static field.
   */
  public void setObjectStaticField(String fname, Reflection value) {
    if(value == null)
      setIntStaticField(fname, -1);
    else
      setIntStaticField(fname, value.objref);
  }  
  /**
   * Sets the value of a reference field.
   */
  public void setReferenceField(String fname, int value) {
    setIntField(fname, value);
  }  
  /**
   * Sets the value of a reference field.
   */
  public void setReferenceStaticField(String fname, int value) {
    setIntStaticField(fname, value);
  }  
  /**
   * Sets the value of a short array element.
   */
  public void setShortArrayElement(int index, short value) {
    setIntArrayElement(index * getArrayTypeSize(), (int)value);
  }  
  /**
   * Sets the value of a short field.
   */
  public void setShortField(String fname, short value) {
    setIntField(fname, (int)value);
  }  
  /**
   * Sets the value of a short static field.
   */
  public void setShortStaticField(String fname, short value) {
    setIntStaticField(fname, (int)value);
  }  
  /**
   * Sets the thread info and all the related info.
   */
  private void setThreadInfo(ThreadInfo th) {
    if(th == null) {
      this.th = null;
      ss = null;
      ks = null;
      da = null;
      sa = null;
    } else {
      this.th = th;
      ks = th.list.ks;
      ss = ks.ss;
      da = ks.da;
      sa = ks.sa;
    }
  }  
  /**
   * Returns the start of the method.
   */
  protected final Instruction start() {
    return th.getPC();
  }  
  /**
   * Throws a new exception of the given class.
   */
  protected Instruction throwException(String classname) {
    ClassInfo ci = ClassInfo.getClassInfo(classname);

    MethodInfo mi = th.getMethod();
    th.popFrame();
    th.removeArguments(mi);

    return th.createAndThrowException(ci);
  }  
}

---