---

StaticArea.java

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

import de.fub.bytecode.*;
import de.fub.bytecode.classfile.*;
import de.fub.bytecode.generic.*;
import gov.nasa.arc.ase.jpf.*;
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 StaticArea {
  Vector classes;           // value of static variables
  Vector objinfo;           // monitor associated with the class

// ifdef NO_COMPRESSION
  // These variables are used to speed up recomputation
  // of the storing data keeping track of what is changed.
  BitSet classChanged;
  BitSet objinfoChanged;
  boolean anyClassChanged;
  boolean anyObjectInfoChanged;

  // These variables contain the indexes used by the storing
  // information in a sort of cache.
  int[] classData;
  int[] objinfoData;
//#endif NO_COMPRESSION

  private static final int EXTRA_GROW_SIZE  = 10;

  // Creates a new (empty) static area.
  public StaticArea() {
    classes = new Vector();     // no classes loaded
    objinfo = new Vector();

// ifdef NO_COMPRESSION
    // nothing has been changed yet
    classChanged = new BitSet();
    objinfoChanged = new BitSet();
    anyClassChanged = false;
    anyObjectInfoChanged = false;

    // Initially there are no classes and so the data is an empty array
    classData = new int[0];
    objinfoData = new int[0];
//#endif NO_COMPRESSION
  }  
  // loads a new class
  //** warning: using heap symmetry classes don't have a new_id **//
  public int addClass(ClassInfo ci) {
    int index = indexFor(ci.getClassName());

// ifdef DEBUG


//#endif DEBUG

    if (index >= classes.size()) {
      classes.setSize(index + EXTRA_GROW_SIZE);
      objinfo.setSize(index + EXTRA_GROW_SIZE);
    }

    Fields fs = ci.createStaticFields();
    classes.setElementAt(fs, index);

    ci.reflection.setClassRef(index);

    objinfo.setElementAt(new ObjectInfo(), index);

// ifdef NO_COMPRESSION
    // sets the flags so that the new class will be detected
    classChanged.set(index);
    objinfoChanged.set(index);
    anyClassChanged = true;
    anyObjectInfoChanged = true;
//#endif NO_COMPRESSION

    return index;
  }  
// ifdef NO_COMPRESSION
  // creates a clone of the class entry so that changes affect the current
  // state but not the pools. The entry will be indexed again later.
  private void cloneClass(int index) {
    // if it has been changed already it's already a clone!
    if(!classChanged.get(index)) {
      Object o = ((Fields)classes.get(index)).clone();
      classes.setElementAt(o, index);
      // we can't compute a new index now because more then one change at the
      // same time may happen so we just invalidate that index
      classChanged.set(index);
      anyClassChanged = true;
    }
  }  
  // creates a clone of the object info so that changes affect the current
  // state but not the pools. The entry will be indexed again later.
  private void cloneObjectInfo(int index) {
    // if it has been changed already it's already a clone!
    if(!objinfoChanged.get(index)) {
      Object o = ((ObjectInfo)objinfo.get(index)).clone();
      objinfo.setElementAt(o, index);
      // we can't compute new index now because more then one change at the
      // same time may happen so we just invalidate that index
      objinfoChanged.set(index);
      anyObjectInfoChanged = true;
    }
  }  
  // checks if a class has already been loaded
  public boolean containsClass(String classname) {
    return hasClass(classname);
  }  
  // returns the class information for a specific class
  public ClassInfo getClass(int classref) {
    return ((Fields)classes.get(classref)).getClassInfo();
  }  
  // these functions are used to hide the objinfo internal structure
  // and to make the pool system work. Every call to methods is filtered
  // thought these methods that can duplicate the object info if it
  // is going to be altered.

// ifdef RACE
  // get the status of the lock for a class
  public LockStatus getLockStatus(String classname,String fieldname) {
    int index = indexOf(classname);
    return ((Fields)classes.get(index)).getLockStatus(fieldname);
  }  
// ifdef NO_FASTBACKTRACK




// ifdef NO_COMPRESSION
















//#endif NO_COMPRESSION

//#endif NO_FASTBACKTRACK

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

    // Mainly we need to create one big array from the two we have
    int cl = classData.length;      // how many classes
    int il = objinfoData.length;    // these numbers should be the same
// ifdef DEBUG

//#endif DEBUG

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

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

    return data;
  }  
//#endif MARK_N_SWEEP

  // ------------------------------------------
  //   access to the underlying fields object
  // ------------------------------------------

  public long getValue(int classref, String fieldname) {
    return ((Fields)classes.get(classref)).getValue(fieldname);
  }  
  public long getValue(String classname, String fieldname) {
    return ((Fields)classes.get(indexOf(classname))).getValue(fieldname);
  }  
  public int getVariableType(int classref, int index) {
    return ((Fields)classes.get(classref)).getClassInfo().getStaticFieldType(index);
  }  
  public int getVariableType(int classref, String fname) {
    return ((Fields)classes.get(classref)).getClassInfo().getStaticFieldType(fname);
  }  
//#endif NO_COMPRESSION

  public int getVariableType(String classname, int index) {
    int classref = indexOf(classname);
    return ((Fields)classes.get(classref)).getClassInfo().getStaticFieldType(index);
  }  
  public int getVariableType(String classname, String fname) {
    int classref = indexOf(classname);
    return ((Fields)classes.get(classref)).getClassInfo().getStaticFieldType(fname);
  }  
  // checks if a class is present in the static area
  public boolean hasClass(String classname) {
// ifdef NO_STATIC_SYMMETRY
    if(!StaticMap.hasEntry(classname)) return false;
//#endif NO_STATIC_SYMMETRY
    int index = indexOf(classname);
    return (index >= 0 && index < classes.size() && classes.get(index) != null);
  }  
  public void hash(HashData hd) {
    for(int i = 0, l = classes.size(); i < l; i++) {
      Object o = classes.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 = classes.size(); i < l; i++) {
      Object o = classes.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();
  }  
  private int indexFor(String classname) {
// ifdef NO_STATIC_SYMMETRY
    return StaticMap.addEntry(classname);
//#else NO_STATIC_SYMMETRY








//#endif NO_STATIC_SYMMETRY
  }  
// ifdef DEBUG











//#endif DEBUG

// ifdef DEBUG











//#endif DEBUG
//#endif NO_COMPRESSION

  // these functions are use to access the information stored in the classes
  // vector without having direct access so that if something is going to be
  // changed a copy is created first. This is necessary to make the pool system
  // work properly.

  // returns the identifier of a class given the name
  public int indexOf(String classname) {
// ifdef NO_STATIC_SYMMETRY
    return StaticMap.getEntry(classname);
//#else NO_STATIC_SYMMETRY










//#endif NO_STATIC_SYMMETRY
  }  
// ifdef NO_COMPRESSION



















































































//#endif NO_COMPRESSION

// ifdef NO_FASTBACKTRACK
























//#endif NO_FASTBACKTRACK
  public boolean isLoaded(String classname) {
    return StaticMap.hasEntry(classname);
  }  
  public void log() {
    Debug.println(Debug.MESSAGE, "SA");
    for(int i = 0; i < classes.size(); i++) {
      Fields f = (Fields)classes.get(i);
      if(f != null) {
    Debug.println(Debug.MESSAGE, "  @" + i + " " + f.getClassInfo().getClassName());
    f.log(i, false);
      }
    }
  }  
// ifdef MARK_N_SWEEP
  public void mark(DynamicArea da) {
    int length = classes.size();
    for(int index = 0; index < length; index++) {
      Fields f = (Fields)classes.get(index);
      if(f != null) f.mark(da);
    }
  }  
//#endif RACE

  // checks if a lock is possible
  public boolean monitorCheckLock(int classref, ThreadInfo th) {
    return ((ObjectInfo)objinfo.get(classref)).getMonitor().checkLock(th);
  }  
  // The followings functions are used only to access the previous one
  // using a class name instead of an index.

  public boolean monitorCheckLock(String className, ThreadInfo th) {
    return monitorCheckLock(indexOf(className), th);
  }  
  // checks if it can acquire the lock
  public boolean monitorCheckLockAfterNotified(int classref, ThreadInfo th) {
    return ((ObjectInfo)objinfo.get(classref)).getMonitor().checkLockAfterNotified(th);
  }  
  public boolean monitorCheckLockAfterNotified(String className, ThreadInfo th) {
    return monitorCheckLockAfterNotified(indexOf(className), th);
  }  
  // tries to acquire the lock on the monitor of the class
  public boolean monitorLock(int classref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    return ((ObjectInfo)objinfo.get(classref)).getMonitor().lock(th, new ClassRef(classref));
  }  
  public boolean monitorLock(String className, ThreadInfo th) {
    return monitorLock(indexOf(className), th);
  }  
  // tries to acquire the lock
  public boolean monitorLockAfterNotified(int classref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    return ((ObjectInfo)objinfo.get(classref)).getMonitor().lockAfterNotified(th, new ClassRef(classref));
  }  
  public boolean monitorLockAfterNotified(String className, ThreadInfo th) {
    return monitorLockAfterNotified(indexOf(className), th);
  }  
  // notifies the processes waiting
  public void monitorNotify(int classref, KernelState ks, Scheduler sch) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    ((ObjectInfo)objinfo.get(classref)).getMonitor().notify(ks, sch);
  }  
  public void monitorNotify(String className, KernelState ks, Scheduler sch) {
    monitorNotify(indexOf(className), ks, sch);
  }  
  // notifies all the threads waiting
  public void monitorNotifyAll(int classref, KernelState ks) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    ((ObjectInfo)objinfo.get(classref)).getMonitor().notifyAll(ks);
  }  
  public void monitorNotifyAll(String className, KernelState ks) {
    monitorNotifyAll(indexOf(className), ks);
  }  
  // releases the monitor
  public void monitorUnlock(int classref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    ((ObjectInfo)objinfo.get(classref)).getMonitor().unlock(th, new ClassRef(classref));
  }  
  public void monitorUnlock(String className, ThreadInfo th) {
    monitorUnlock(indexOf(className), th);
  }  
  // waits on the class monitor
  public void monitorWait(int classref, ThreadInfo th) {
// ifdef NO_COMPRESSION
    // needs to clone the object info because it is going to change
    cloneObjectInfo(classref);
//#endif NO_COMPRESSION
    ((ObjectInfo)objinfo.get(classref)).getMonitor().wait(th, new ClassRef(classref));
  }  
  public void monitorWait(String className, ThreadInfo th) {
    monitorWait(indexOf(className), th);
  }  
//#endif NO_COMPRESSION

// ifdef NO_COMPRESSION
  // this function recreated a static area from the storing data
  // tries to reuse as much as possible using the indexes we already have
  public void revertTo(int[] data) {
    // extracts the new class and object info data
    int len = data.length / 2;

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

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

    int s = classData.length;

    if (s >= len) {
      // if there are less classes now then before
      // we just update the one in common
      for (int idx = 0; idx < len; idx++) {
    if(nClassData[idx] != classData[idx])
      classes.setElementAt(
          VirtualMachine.fieldsPool.getObject(nClassData[idx]),
          idx);
    if(nObjinfoData[idx] != objinfoData[idx])
      objinfo.setElementAt(
          VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
          idx);
      }
      // then throw away the rest
      classes.setSize(len);
      objinfo.setSize(len);
    } else {
      // otherwise we update the one in common
      for (int idx = 0; idx < s; idx++) {
    if(nClassData[idx] != classData[idx])
      classes.setElementAt(
          VirtualMachine.fieldsPool.getObject(nClassData[idx]),
          idx);
    if(nObjinfoData[idx] != objinfoData[idx])
      objinfo.setElementAt(
          VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
          idx);
      }
      classes.setSize(len);
      objinfo.setSize(len);
      // and we add the next ones (if any)
      for (int idx = s; idx < len; idx++) {
    classes.setElementAt(
        VirtualMachine.fieldsPool.getObject(nClassData[idx]),
        idx);
    objinfo.setElementAt(
        VirtualMachine.objectInfoPool.getObject(nObjinfoData[idx]),
        idx);
      }
    }
    classData = nClassData;
    objinfoData = nObjinfoData;
  }  
  public void setValue(int classref, String fieldname, long value) {
// ifdef NO_COMPRESSION
    cloneClass(classref);
//#endif NO_COMPRESSION
    ((Fields)classes.get(classref)).setValue(fieldname, value);
  }  
  public void setValue(String classname, String fieldname, long value) {
// ifdef NO_COMPRESSION
    cloneClass(indexOf(classname));
//#endif NO_COMPRESSION
    ((Fields)classes.get(indexOf(classname))).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 (anyClassChanged) {
      // Updates classData
      updateClasses();

      // Clears all the flags because no updates are necessary anymore
      classChanged = new BitSet();
      anyClassChanged = false;
    }

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

      // Clears all the flags because no updates are necessary anymore
      objinfoChanged = new BitSet();
      anyObjectInfoChanged = false;
    }
  }  
  // updates the classes
  private void updateClasses() {
    // we have to keep in mind that there could be empty spaces
    // due to unloaded classes or classes loaded in a different
    // order and to when classes are added or removed
    int size = classes.size();
    int old_size = classData.length;
    int actual_size = -1;   // there could be empty slots at the end!

// ifdef DEBUG


//#endif DEBUG

    // first we create an array as long as the classes 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)classes.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 (classChanged.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
      classes.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 class data
// ifdef DEBUG

//#endif DEBUG
      data[i] = classData[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 class data avoid to
    // store all the zeros at the end (that are unuseful).
    classData = new int[++actual_size];
    System.arraycopy(data, 0, classData, 0, actual_size);
  }  
  // updates the object infos
  private void updateObjectInfos() {
    // we have to keep in mind that there could be empty spaces
    // due to unloaded classes or classes loaded in a different
    // order and to when classes are added or removed
    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 create 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);
  }  
}

---