---

ElementInfo.java

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

import java.util.List;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashPool;
import gov.nasa.arc.ase.util.HashData;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.jpf.InternalErrorException;
//#ifdef RACE


//#endif RACE

/**
 * Describes an element. An element can be an object or a class.
 */
public class ElementInfo implements Storable, Reference {
  private static HashPool fieldsPool = new HashPool();
  private static HashPool monitorPool = new HashPool();
//#ifdef RACE

//#endif RACE

  public Fields fields;
  public Monitor monitor;
//#ifdef RACE

//#endif RACE
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

  public Area area;
  public int index;

  /*
   * The following information is used to cache the value of the indexes so that
   * an explicit indexing is not necessary at each storing.
   */
  private int fIndex = -1;
  private int mIndex = -1;

  public ElementInfo() {
  }  
  public ElementInfo(ElementInfo ei) {
    if(ei.fIndex == -1)
      fields = (Fields)ei.fields.clone();
    else
      fields = ei.fields;

    if(ei.mIndex == -1)
      monitor = (Monitor)ei.monitor.clone();
    else
      monitor = ei.monitor;

//#ifdef RACE

//#endif RACE

//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

    area = null;

    index = -1;

    fIndex = ei.fIndex;

    mIndex = ei.mIndex;
  }  
//#ifdef RACE





//#else RACE
  public ElementInfo(Fields f, Monitor m) {
    fields = f;
    monitor = m;
  }  
  public int arrayLength() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");

    return fields.countFields();
  }  
  public boolean[] asBooleanArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    boolean[] result = new boolean[length];

    for(int i = 0; i < length; i++)
      result[i] = Types.intToBoolean(getField(i));

    return result;
  }  
  public byte[] asByteArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    byte[] result = new byte[length];

    for(int i = 0; i < length; i++)
      result[i] = (byte)getField(i);

    return result;
  }  
  public char[] asCharArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    char[] result = new char[length];

    for(int i = 0; i < length; i++)
      result[i] = (char)getField(i);

    return result;
  }  
  public double[] asDoubleArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    double[] result = new double[length];

    for(int i = 0; i < length; i++)
      result[i] = Types.longToDouble(getLongField(i));

    return result;
  }  
  public float[] asFloatArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    float[] result = new float[length];

    for(int i = 0; i < length; i++)
      result[i] = Types.intToFloat(getField(i));

    return result;
  }  
  public int[] asIntArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    int[] result = new int[length];

    for(int i = 0; i < length; i++)
      result[i] = getField(i);

    return result;
  }  
  public long[] asLongArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");

    int length = fields.countFields();
    long[] result = new long[length];

    for(int i = 0; i < length; i += 2)
      result[i] = getLongField(i);

    return result;
  }  
  public Reflection[] asObjectArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    Reflection[] result = new Reflection[length];

    for(int i = 0; i < length; i++)
      result[i] = area.get(getField(i)).getReflection();

    return result;
  }  
  public short[] asShortArray() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");
    
    int length = fields.countFields();
    short[] result = new short[length];

    for(int i = 0; i < length; i++)
      result[i] = (short)getField(i);

    return result;
  }  
  public String asString() {
    if(!fields.getClassInfo().instanceOf("java.lang.String"))
      throw new InternalErrorException("object is not of type java.lang.String");

    int value = getField("value");
    int length = getField("count");

    ElementInfo e = area.get(value);

    StringBuffer sb = new StringBuffer();
    for(int i = 0; i < length; i++)
      sb.append((char)e.getField(i));

    return sb.toString();
  }  
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    setFieldsIndex(storing.get());
    setMonitorIndex(storing.get());
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

//#ifdef RACE


//#endif RACE
  }  
//#endif MARK_N_SWEEP

  public boolean canLock(ThreadInfo th) {
    return monitor.canLock(th);
  }  
  public Object clone() {
    return new ElementInfo(this);
  }  
  private Fields cloneFields() {
    if(fIndex == -1) return fields;

    fIndex = -1;
    area.ks.data = null;
    area.hasChanged.set(index);
    area.anyChanged = true;
    return fields = (Fields)fields.clone();
  }  
  private Monitor cloneMonitor() {
    if(mIndex == -1) return monitor;

    mIndex = -1;
    area.ks.data = null;
    area.hasChanged.set(index);
    area.anyChanged = true;
    return monitor = (Monitor)monitor.clone();
  }  
//#endif MARK_N_SWEEP || REFERENCE_COUNT

  public String getArrayType() {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");

    return Types.getArrayElementType(fields.getType());
  }  
  public Object getBacktrackData() {
//#ifdef RACE


//#endif RACE

    return null;
  }  
  public boolean getBooleanArrayElement(int findex) { return Types.intToBoolean(getField(findex)); }  
  public boolean getBooleanField(String fname) { return Types.intToBoolean(getField(fname)); }  
  public byte getByteArrayElement(int findex) { return (byte)getField(findex); }  
  public byte getByteField(String fname) { return (byte)getField(fname); }  
  public char getCharArrayElement(int findex) { return (char)getField(findex); }  
  public char getCharField(String fname) { return (char)getField(fname); }  
  public ClassInfo getClassInfo() {
    return fields.getClassInfo();
  }  
  public double getDoubleArrayElement(int findex) { return Types.longToDouble(getLongField(findex)); }  
  public double getDoubleField(String fname) { return Types.longToDouble(getLongField(fname)); }  
  public int getField(int findex) {
    return fields.getField(findex);
  }  
  public int getField(String fname) {
    return fields.getField(fname);
  }  
//#endif RACE

  private int getFieldsIndex() {
    if(fIndex != -1) return fIndex;

    HashPool.PoolEntry e = fieldsPool.getEntry(fields);
    fields = (Fields)e.getObject();

    return fIndex = e.getIndex();
  }  
  public String getFieldType(int findex) {
    return fields.getFieldType(findex);
  }  
  public String getFieldType(String fname) {
    return fields.getFieldType(fname);
  }  
  public float getFloatArrayElement(int findex) { return Types.intToFloat(getField(findex)); }  
  public float getFloatField(String fname) { return Types.intToFloat(getField(fname)); }  
  public int getIntArrayElement(int findex) { return getField(findex); }  
  public int getIntField(String fname) { return getField(fname); }  
  public int getLockCount() {
    return monitor.getLockCount();
  }  
  public int getLockingThread() {
    return monitor.getLockingThread();
  }  
  public long getLongArrayElement(int findex) { return getLongField(findex); }  
  public long getLongField(int findex) {
    return fields.getLongField(findex);
  }  
  public long getLongField(String fname) {
    return fields.getLongField(fname);
  }  
  private int getMonitorIndex() {
    if(mIndex != -1) return mIndex;

    HashPool.PoolEntry e = monitorPool.getEntry(monitor);
    monitor = (Monitor)e.getObject();

    return mIndex = e.getIndex();
  }  
  public Reference getObjectArrayElement(int findex) { return area.ks.da.get(getField(findex)); }  
  public Reference getObjectField(String fname) { return area.ks.da.get(getField(fname)); }  
  public Reflection getReflection() {
    return fields.getClassInfo().getReflection().instantiate(index);
  }  
  public short getShortArrayElement(int findex) { return (short)getField(findex); }  
  // public long getLongField(String fname) { return getLongField(fname); }
  public short getShortField(String fname) { return (short)getField(fname); }  
  public int[] getStoringData() {
//#ifdef REFERENCE_COUNT

//#else REFERENCE_COUNT
    int[] data = new int[2];
//#endif REFERENCE_COUNT

    data[0] = getFieldsIndex();
    data[1] = getMonitorIndex();
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT

    return data;
  }  
  public String getStringArrayElement(int findex) { return area.ks.da.get(getField(findex)).asString(); }  
  public String getStringField(String fname) { return area.ks.da.get(getField(fname)).asString(); }  
  public String getType() {
    return fields.getType();
  }  
  public int[] getWaitingThreads() {
    return monitor.getWaitingThreads();
  }  
  public void hash(HashData hd) {
    fields.hash(hd);
    monitor.hash(hd);
//#ifdef RACE


//#endif RACE
//#ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT
  }  
//#ifdef REFERENCE_COUNT


















//#endif REFERENCE_COUNT

  public int hashCode() {
    HashData hd = new HashData();

    hash(hd);

    return hd.getValue();
  }  
  public boolean instanceOf(String type) {
    return Types.instanceOf(fields.getType(), type);
  }  
  public void interrupt() {
    area.ks.tl.locate(index).interrupt();
  }  
  public boolean isFieldRef(int findex) {
    return fields.isRef(findex);
  }  
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT
  public boolean isFieldRef(String fname) {
    return fields.isRef(fname);
  }  
  public void lock(ThreadInfo th) {
    cloneMonitor().lock(th, area.isStatic ? (Ref)new ClassRef(index) : (Ref)new ObjRef(index));
  }  
  public void lockNotified(ThreadInfo th) {
    cloneMonitor().lockNotified(th, area.isStatic ? (Ref)new ClassRef(index) : (Ref)new ObjRef(index));
  }  
//#ifdef RACE



//#endif RACE

  public void log() {
    if(fIndex == -1) Debug.println(Debug.MESSAGE, "(fields have changed)");
    fields.log(index);
    if(mIndex == -1) Debug.println(Debug.MESSAGE, "(monitor has changed)");
    monitor.log();
  }  
//#ifdef MARK_N_SWEEP
  public void mark() {
    fields.mark(area.ks.da);
  }  
  public void notifies() {
    cloneMonitor().notify(area.ks.ss);
  }  
  public void notifiesAll() {
    cloneMonitor().notifyAll(area.ks.ss);
  }  
//#ifdef RACE







//#endif RACE

  public boolean outOfBounds(int index) {
    if(!fields.isArray())
      throw new InternalErrorException("object is not an array");

    return (index < 0 || index >= fields.size());
  }  
  public void setField(int findex, int value) {
    cloneFields().setField(findex, value);
  }  
  public void setField(String fname, int value) {
    cloneFields().setField(fname, value);
  }  
  private void setFieldsIndex(int index) {
    if(fIndex == index) return;

    fIndex = index;
    fields = (Fields)fieldsPool.getObject(index);
  }  
  public void setLongField(int findex, long value) {
    cloneFields().setLongField(findex, value);
  }  
  public void setLongField(String fname, long value) {
    cloneFields().setLongField(fname, value);
  }  
  private void setMonitorIndex(int index) {
    if(mIndex == index) return;

    mIndex = index;
    monitor = (Monitor)monitorPool.getObject(index);
  }  
  public void unlock(ThreadInfo th) {
    cloneMonitor().unlock(th, area.isStatic ? (Ref)new ClassRef(index) : (Ref)new ObjRef(index));
  }  
  public void wait(ThreadInfo th) {
    cloneMonitor().wait(th, area.isStatic ? (Ref)new ClassRef(index) : (Ref)new ObjRef(index));
  }  
}

---