---

DynamicArea.java

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

import de.fub.bytecode.*;
import de.fub.bytecode.classfile.*;
import gov.nasa.arc.ase.util.PoolObject;
import de.fub.bytecode.generic.*;
import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import gov.nasa.arc.ase.util.HashPool;
import java.io.*;
import java.util.*;
// ifdef RACE
import gov.nasa.arc.ase.jpf.jvm.runtime.*;
//#endif RACE

public class DynamicArea {
  static BitSet ZERO = new BitSet();
  Vector objects;           // value of the object variables
  Vector objinfo;           // monitor associated with the object

// ifdef NO_COMPRESSION
  // These variables are used to speed up recomputation
  // of the storing data keeping track of what is changed
  BitSet objectChanged;
  BitSet objinfoChanged;
  private boolean anyObjectChanged;
  private boolean anyObjectInfoChanged;
  
  // These variables contain the indexes used by the storing
  // information in a sort of cache.
  int[] objectData;
  int[] objinfoData;
//#endif RACE

  // this is the main entry for the garbage collection
  // when garbage collection is switched on this function
  // is called to free unused objects.
  // the current implementation is a mark and sweep algorithm.
// ifdef MARK_N_SWEEP
  public BitSet isUsed = null;

//#endif NO_COMPRESSION

  // Creates a new (empty) dynamic area
  public DynamicArea() {
    objects = new Vector();     // no object created yet
    objinfo = new Vector();

// ifdef NO_COMPRESSION
    // nothing has been changed yet
    objectChanged = new BitSet();
    objinfoChanged = new BitSet();
    anyObjectChanged = false;
    anyObjectInfoChanged = false;
//#endif NO_COMPRESSION

// ifdef NO_COMPRESSION
    // Initially there are no objects and so the data is an empty array
    objectData = new int[0];
    objinfoData = new int[0];
//#endif NO_COMPRESSION
  }  
  //** warning: this is not necesserely the length of an array **//
  // returns the length of an array (or the number of field of an object)
  public int arraylength(int objref) {
    return ((Fields)objects.get(objref)).getVariables().length;
  }  
//#endif MARK_N_SWEEP

// ifdef NO_COMPRESSION
  // this function creates a copy of an object entry in case it needs to
  // be modified
  private void cloneObject(int index) {
    // if it has already been cloned we don't need to do it again
    if(!objectChanged.get(index)) {
      Object o = ((Fields)objects.get(index)).clone();
      objects.setElementAt(o, index);

      // we just invalidate the entry because the same fields can be changed
      // more then once in a single step
      objectChanged.set(index);
      anyObjectChanged = true;
    }
  }  
  // creates a copy of the object info entry
  private void cloneObjectInfo(int index) {
    // if it has already been cloned there's no need to clone it again
    if(!objinfoChanged.get(index)) {
      Object o = ((ObjectInfo)objinfo.get(index)).clone();
      objinfo.setElementAt(o, index);

      // invalidate the current entry so that the index will be recalculated
      objinfoChanged.set(index);
      anyObjectInfoChanged = true;
    }
  }  
  // converts an array object into an array of integers
  public long[] convert2Array(int objref) {
    //** warning: does not check if this is really an array
    int length = arraylength(objref);       // length of the array

// ifdef DEBUG

//#endif DEBUG

    // creates an array and fills it with data
    long[] result = new long[length];
    for(int i = 0; i < length; i++) {
      result[i] = getValue(objref, i);
// ifdef DEBUG

//#endif DEBUG
    }

    // returns the array (for a normal class would be the list of field values
    return result;
  }  
  // even if the object is a string, it is not stored in the system as a string
  // like for the other primitive types. it is necessary so to have a function
  // to convert between the two
  public String convert2String(int objref) {
    // object reference of the array containing the characters
    int value = (int)getValue(objref, "value");
  
    // number of characters in the string
    int length = (int)getValue(objref, "count");

// ifdef DEBUG

//#endif DEBUG

    // get a new empty string and then adds one character at the time
    StringBuffer sb = new StringBuffer();

    for(int i = 0; i < length; i++)
      sb.append((char)getValue(value, i));

// ifdef DEBUG

//#endif DEBUG

    // returns the string object corresponding to the one we internally have
    // this makes possible for function that know about the internal
    // rapresentation of strings to work, but gives us a way to use normal
    // string functions on string objects.
    return sb.toString();
  }  
  public void gc(KernelState ks) {
    List o = objects;

    int length = o.size() - 1;
    while(length > 0 && o.get(length) == null)
      length--;
    length++;

    isUsed = new BitSet(length);

    List threads = ks.threads;
    int nthreads = threads.size();

// ifdef DEBUG

//#endif DEBUG
    for(int i = 0; i < nthreads; i++) {
      ThreadInfo th = (ThreadInfo)threads.get(i);
      th.mark(this);
    }
    ks.static_area.mark(this);
// ifdef DEBUG


//#endif DEBUG

    int count = 0;

    for(int i = 0; i < length; i++)
      if(!isUsed.get(i)) {
    if(objects.get(i) != null) {
      count++;
// ifdef DEBUG

//#endif DEBUG

      objects.setElementAt(null, i);
      objinfo.setElementAt(null, i);
      anyObjectChanged = true;
      anyObjectInfoChanged = true;
      objectChanged.set(i);
      objinfoChanged.set(i);
    }
// ifdef DEBUG


//#endif DEBUG
      }
// ifdef DEBUG





//#endif DEBUG

    Runner.GCs += count;

    isUsed = null;
  }  
  // get the class information for an object
  public ClassInfo getClass(int objref) {
    return ((Fields)objects.get(objref)).getClassInfo();
  }  
  public LockStatus getLockStatus(int objref) {
    return ((Fields)objects.get(objref)).getLockStatus();  
  }  
// ifdef RACE
  // the following functions are used to access the fields information
  public LockStatus getLockStatus(int objref, String fieldname) {
    return ((Fields)objects.get(objref)).getLockStatus(fieldname);
  }  
//#endif NO_COMPRESSION

  public Reflection getReflection(int objref) {
    Reflection r = (Reflection)getClass(objref).reflection.clone();
    r.setObjectReference(objref);

    return r;
  }  
// ifdef NO_FASTBACKTRACK




// ifdef NO_COMPRESSION
















//#endif NO_COMPRESSION

//#endif NO_FASTBACKTRACK

// ifdef NO_COMPRESSION
  // Gets the storing information from the dynamic area
  public int[] getStoringData() {
    // First we need to update the information in case there had been
    // any change
    update();

    // Mainly we need to get one big array from the two we have
    int ol = objectData.length;     // how many objects
    int il = objinfoData.length;    // these numbers should be the same
// ifdef DEBUG

//#endif DEBUG

    // allocate enough space for both structures
    int[] data = new int[ol + il];

    // copy the information in the new array
    System.arraycopy(objectData, 0, data, 0, ol);
    System.arraycopy(objinfoData, 0, data, ol, il);

    return data;
  }  
  public long getValue(int objref, int index) {
    return ((Fields)objects.get(objref)).getValue(index);
  }  
  // ------------------------------------------
  //   access to the underlying fields object
  // ------------------------------------------

  public long getValue(int objref, String fieldname) {
    return ((Fields)objects.get(objref)).getValue(fieldname);
  }  
// ifdef INITIALIZE










//#endif INITIALIZE

  public int getVariableType(int objref, int index) {
    return ((Fields)objects.get(objref)).getClassInfo().getFieldType(index);
  }  
  public int getVariableType(int objref, String fname) {
    return ((Fields)objects.get(objref)).getClassInfo().getFieldType(fname);
  }  
  public void hash(HashData hd) {
    for(int i = 0, l = objects.size(); i < l; i++) {
      Object o = objects.get(i);
      if(o != null) hd.add(o.hashCode());
    }

    for(int i = 0, l = objinfo.size(); i < l; i++) {
      Object o = objinfo.get(i);
      if(o != null) hd.add(o.hashCode());
    }
  }  
  public int hashCode() {
    HashData hd = new HashData();

    for(int i = 0, l = objects.size(); i < l; i++) {
      Object o = objects.get(i);
      if(o != null) hd.add(o.hashCode());
    }

    for(int i = 0, l = objinfo.size(); i < l; i++) {
      Object o = objinfo.get(i);
      if(o != null) hd.add(o.hashCode());
    }

    return hd.getValue();
  }  
// ifdef NO_COMPRESSION



















































































//#endif NO_COMPRESSION

// ifdef NO_FASTBACKTRACK
























//#endif NO_FASTBACKTRACK

  private int indexFor(ThreadInfo th) {
// ifdef NO_DYNAMIC_SYMMETRY






//#else NO_DYNAMIC_SYMMETRY
    DynamicMapIndex i = new DynamicMapIndex(th.getPC(),
// ifdef THREAD_SYMMETRY

//#endif THREAD_SYMMETRY
    0);

    if(!DynamicMap.hasEntry(i)) return DynamicMap.addEntry(i);

    int index = DynamicMap.getEntry(i);

    if(index < objects.size())
      while(objects.get(index) != null) {
    i.next();

    if(!DynamicMap.hasEntry(i)) return DynamicMap.addEntry(i);
    index = DynamicMap.getEntry(i);
    if(index >= objects.size()) return index;
      }

    return index;
//#endif NO_DYNAMIC_SYMMETRY
  }  
  // checks if an object is an instance of the given class (directly or indirectly)
  public boolean instanceOfClass(int objref, String classname) {
    Fields f = (Fields)objects.get(objref);
    if(f == null) return false;

    // gets the class information for that object
    ClassInfo ci =  f.getClassInfo();
    // can't have a null classinfo reference
    if (ci == null) {
      Debug.println(Debug.ERROR, "ci field for object " + objref + " is null");
      System.exit(0);
    }
    
    // now we go up until we get to the top of the hierarchy
    while (ci != null)
      // check if this is the class we are looking for
      if (ci.getClassName().equals(classname)) 
    return true;
      else
    // goes up one level
    ci = ci.getSuperClassInfo();

    // at this point we know it's not an instance of that class
    return false;
  }  
// ifdef REFERENCE_COUNT













































































//#endif REFERENCE_COUNT

// ifdef MARK_N_SWEEP
  public boolean isFieldRef(int objref, String fieldname) {
    return ((Fields)objects.get(objref)).isRef(fieldname);
  }  
//#endif MARK_N_SWEEP

  public void log() {
    Debug.println(Debug.MESSAGE, "DA");
    for(int i = 0; i < objects.size(); i++) {
      Fields f = (Fields)objects.get(i);
      if(f != null) {
// ifdef REFERENCE_COUNT

//#else REFERENCE_COUNT
    Debug.println(Debug.MESSAGE, "  #" + i);
//#endif REFERENCE_COUNT
    f.log(i, true);
      }
    }
  }  
  public void mark(int objref) {
// ifdef DEBUG

//#endif DEBUG
    if(objref == -1) return;

    if(isUsed.get(objref)) return;
    isUsed.set(objref);
    
    ((Fields)objects.get(objref)).mark(this);
  }  
//#endif NO_COMPRESSION

  // the following functions are used to access the monitor information
  public boolean monitorCheckLock(int objref, ThreadInfo th) {
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().checkLock(th);
  }  
  public boolean monitorCheckLockAfterNotified(int objref, ThreadInfo th) {
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().checkLockAfterNotified(th);
  }  
  public boolean monitorLock(int objref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().lock(th, new ObjRef(objref));
  }  
  public boolean monitorLockAfterNotified(int objref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().lockAfterNotified(th, new ObjRef(objref));
  }  
  public int monitorLockCount(int objref) {
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().getLockCount();
  }  
  public int monitorLockingThread(int objref) {
    return ((ObjectInfo)objinfo.get(objref)).getMonitor().getLockingThread();
  }  
  public void monitorNotify(int objref, KernelState ks, Scheduler sch) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    ((ObjectInfo)objinfo.get(objref)).getMonitor().notify(ks, sch);
  }  
  public void monitorNotifyAll(int objref, KernelState ks) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    ((ObjectInfo)objinfo.get(objref)).getMonitor().notifyAll(ks);
  }  
  public void monitorUnlock(int objref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    ((ObjectInfo)objinfo.get(objref)).getMonitor().unlock(th, new ObjRef(objref));
  }  
  public void monitorWait(int objref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // the object info needs to be cloned
    cloneObjectInfo(objref);
//#endif NO_COMPRESSION
    // needs to get the object info again because clone object info changed it
    ((ObjectInfo)objinfo.get(objref)).getMonitor().wait(th, new ObjRef(objref));
  }  
  public List monitorWaitingThreads(int objref) {
    return (List)((ArrayList)((ObjectInfo)objinfo.get(objref)).getMonitor().getWaitingThreads()).clone();
  }  
  // Creates a new array object of the given type.
  //** optimization: ci is actually never used here... **//
  public int newArrayObject(String type, int size, ThreadInfo th) {
    Fields fields = new Fields(null, size); // the fields of the object
    ObjectInfo oi;          // The object info of the new object

    // we need to get the new object info
    oi = new ObjectInfo();
// ifdef INITIALIZE

//#endif INITIALIZE

    // compute the position for the new object
    int index = indexFor(th);

    // once we got the index we should check a couple of things
    // first if there is not enough space then we should make room for it
    if (index >= objects.size()) {
      objects.setSize(index+10); 
      objinfo.setSize(index+10); 
    }

    // at this point we insert the fields we created for that object
    // and a new object info in the dynamic area
    objects.setElementAt(fields, index);
    objinfo.setElementAt(oi, index);

// ifdef NO_COMPRESSION
    // states that we changed something
    objectChanged.set(index);
    objinfoChanged.set(index);
    anyObjectChanged= true;
    anyObjectInfoChanged = true;
//#endif NO_COMPRESSION

    // now we should get the elements of the array
    for(int i = 0; i < size; i++) {
      fields.setValue(i, Types.newValue(type));
// ifdef MARK_N_SWEEP
      if(Types.isReference(type))
    fields.setValueRef(i);
//#endif MARK_N_SWEEP
    }

    // this is the object reference for the newly created object
    return index;
  }  
  // another "special" object is the class object. Here's how we get one
  //** optimization: jpfvm could be a static class or merged with virtual machine **//
  public int newClassObject(String str, ThreadInfo th) {
    JPFVM jpfvm = JPFVM.getJPFVM();

    // loads and links the java.lang.Class class
    ClassInfo ci = jpfvm.getClass("java.lang.Class");

    // creates an object and it will fill the fields by hand
    int objref   = newObject(ci, th);

    //** missing: the object should be initialized but implemetation is incomplete **//
    
    // returns the object reference
    return objref;
  }  
// ifdef DEBUG











//#endif DEBUG

// ifdef DEBUG











//#endif DEBUG
//#endif NO_COMPRESSION

  // creates a new object of the given class
  // every instruction that creates a new object is assigned a distinct id
  // used by the heap symmetry
  public int newObject(ClassInfo ci, ThreadInfo th) {
// ifdef DEBUG

//#endif DEBUG

    // gets the non static fields. these will have to be stored in the
    // dynamic area.
    Fields fs = ci.createFields();
    ObjectInfo oi;          // The object info of the new object

    // we need to get the new object info
    oi = new ObjectInfo();

    // We need to decide now which entry in the dynamic area to use
    int index = indexFor(th);

    // once we got the index we should check a couple of things
    // first if there is not enough space then we should make room for it
    if (index >= objects.size()) {
      objects.setSize(index+10); 
      objinfo.setSize(index+10); 
    }

    // at this point we insert the fields we created for that object
    // and a new object info in the dynamic area
    objects.setElementAt(fs, index);
    objinfo.setElementAt(oi, index);

// ifdef NO_COMPRESSION
    // states that we changed something
    objectChanged.set(index);
    objinfoChanged.set(index);
    anyObjectChanged= true;
    anyObjectInfoChanged = true;
//#endif NO_COMPRESSION

// ifdef DEBUG

//#endif DEBUG
    //
    // returns the object reference of the newly created object
    return index;
  }  
  // creates a new string object
  // strings are handled separately due to their special nature
  // in the java virtual machine
  //** optimization: jpfvm could be a static class or merged with virtual machine **//
  public int newStringObject(String str, ThreadInfo th) {
    JPFVM jpfvm = JPFVM.getJPFVM();

    // gets the class information (and link the class if it was not done before)
    ClassInfo ci = jpfvm.getClass("java.lang.String");

    // creates the new object for the string
    int objref = newObject(ci, th);

    // creates a new array for storing the characters
    int value = newArrayObject("C", str.length(), th);

    // now fills the various fields
    setValue(objref, "value", value);
    for(int i = 0, s = str.length(); i < s; i++)
      setValue(value, i, str.charAt(i));
    setValue(objref, "offset", 0);
    setValue(objref, "count", str.length());

    // returns the object reference
    return objref;
  }  
// ifdef NO_COMPRESSION
  public void revertTo(int[] data) {
    int len = data.length / 2;

    int[] nObjectData = new int[len];
    int[] nObjinfoData = new int[len];

    System.arraycopy(data, 0, nObjectData, 0, len);
    System.arraycopy(data, len, nObjinfoData, 0, len);

    int s = objectData.length;

    if (s >= len) {
      for (int idx = 0; idx < len; idx++) {
    if(nObjectData[idx] != objectData[idx])
      objects.setElementAt(
          VirtualMachine.fieldsPool.getObject(nObjectData[idx]),
          idx);
    if(nObjinfoData[idx] != objinfoData[idx])
      objinfo.setElementAt(
          VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
          idx);
      }
      objects.setSize(len);
      objinfo.setSize(len);
    } else {
      for (int idx = 0; idx < s; idx++) {
    if(nObjectData[idx] != objectData[idx])
      objects.setElementAt(
          VirtualMachine.fieldsPool.getObject(nObjectData[idx]),
          idx);
    if(nObjinfoData[idx] != objinfoData[idx])
      objinfo.setElementAt(
          VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
          idx);
      }
      objects.setSize(len);
      objinfo.setSize(len);
      for (int idx = s; idx < len; idx++) {
    objects.setElementAt(
        VirtualMachine.fieldsPool.getObject(nObjectData[idx]),
        idx);
    objinfo.setElementAt(
        VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
        idx);
      }
    }
    objectData = nObjectData;
    objinfoData = nObjinfoData;
  }  
  public void setValue(int objref, int index, long value) {
// ifdef NO_COMPRESSION
    cloneObject(objref);
//#endif NO_COMPRESSION
    ((Fields)objects.get(objref)).setValue(index, value);
  }  
  public void setValue(int objref, String fieldname, long value) {
// ifdef NO_COMPRESSION
    cloneObject(objref);
//#endif NO_COMPRESSION
    ((Fields)objects.get(objref)).setValue(fieldname, value);
  }  
  // The following group of functions are used when something is changed
  // all the data structure must be updated but we can do it in a smart
  // way and avoid updating what's not changed.
  private void update() {
    if (anyObjectChanged) {
      // Updates objectData
      updateObjects();

      // Clears all the flags because no updates are necessary anymore
      objectChanged.and(ZERO);
      anyObjectChanged = false;
    }

    if (anyObjectInfoChanged) {
      // Updates objinfoData
      updateObjectInfos();

      // Clears all the flags because no updates are necessary anymore
      objinfoChanged.and(ZERO);
      anyObjectInfoChanged = false;
    }
  }  
  // updates the object infos
  private void updateObjectInfos() {
    // we have to keep in mind that there could be empty spaces
    // due to object created and destroyed.
    int size = objinfo.size();
    int old_size = objinfoData.length;
    int actual_size = -1;   // there could be empty slots at the end!

// ifdef DEBUG


//#endif DEBUG

    // first we get an array as long as the object info vector
    int[] data = new int[size];
    for(int i = 0; i < size; i++) {
      // for each entry we have to test a couple of conditions
      ObjectInfo o = (ObjectInfo)objinfo.get(i);
      if(o != null) {
    // if the entry at index i it's not null then
    // the actual size it's at least i.
    actual_size = i;

    if (objinfoChanged.get(i)) {
      // if it's changed then we have to check the pool
      HashPool.PoolEntry e = VirtualMachine.objectInfoPool.getEntry(o);
      // set the reference so that we keep just one copy if it was in the
      // pool already
      objinfo.setElementAt(e.getObject(), i);
      // set the correct index we got from the pool
      data[i] = e.getIndex();
    } else {
      // if it's not changed it means it was already there
      // so we get the old value from the old object info data
// ifdef DEBUG

//#endif DEBUG
      data[i] = objinfoData[i];
    }
      } else {
    // if the entry is null it will be a 0 in the data
    data[i] = 0;
      }
    }

    // now we have to put the information in the object info data avoid to
    // store all the zeros at the end (that are unuseful).
    objinfoData = new int[++actual_size];
    System.arraycopy(data, 0, objinfoData, 0, actual_size);
  }  
  // updates the objects
  private void updateObjects() {
    // we have to keep in mind that there could be empty spaces
    // due to object created and destroyed
    int size = objects.size();
    int old_size = objectData.length;
    int actual_size = -1;   // there could be empty slots at the end!

// ifdef DEBUG


//#endif DEBUG

    // first we get an array as long as the object vector
    int[] data = new int[size];
    for(int i = 0; i < size; i++) {
      // for each entry we have to test a couple of conditions
      Fields o = (Fields)objects.get(i);
      if(o != null) {
    // if the entry at index i it's not null then
    // the actual size it's at least i.
    actual_size = i;

    if (objectChanged.get(i)) {
      // if it's changed then we have to check the pool
      HashPool.PoolEntry e = VirtualMachine.fieldsPool.getEntry(o);
      // set the reference so that we keep just one copy if it was in the
      // pool already
      objects.setElementAt(e.getObject(), i);
      // set the correct index we got from the pool
      data[i] = e.getIndex();
    } else {
      // if it's not changed it means it was already there
      // so we get the old value from the old object data
// ifdef DEBUG

//#endif DEBUG
      data[i] = objectData[i];
    }
      } else {
    // if the entry is null it will be a 0 in the data
    data[i] = 0;
      }
    }

    // now we have to put the information in the object data avoid to
    // store all the zeros at the end (that are unuseful).
    objectData = new int[++actual_size];
    System.arraycopy(data, 0, objectData, 0, actual_size);
  }  
}

---