---

KernelState.java

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

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 KernelState implements iKernelState {
  public StaticArea  static_area;   // information about the loaded classes
  public DynamicArea dynamic_area;  // information about the created objects
  public List        threads;       // list of the threads

// ifdef NO_COMPRESSION
  private int[] data;
// ifdef NO_COMPRESSION














//#endif NO_COMPRESSION

// ifdef NO_COMPRESSION








//#endif NO_COMPRESSION
//#endif NO_COMPRESSION

  public KernelState() {
    static_area = new StaticArea();
    dynamic_area = new DynamicArea();
    threads = new ArrayList();
  }  
  // Looks for the thread info corresponding to the given object reference
  public iThreadInfo findThread(Ref ref) {
    // This is a very cheap implementation
    // just iterates the threads and checks their object reference
    //** Space for optimizations here too **//
    for(Iterator it = threads.iterator(); it.hasNext(); ) {
      ThreadInfo ti = (ThreadInfo)it.next(); 
      if (ti.getReference().equals(ref)) {
// ifdef DEBUG

//#endif DEBUG
    return ti;
      }
    }

    return null;
  }  
// ifdef MARK_N_SWEEP
  public void gc() {
    Runner.GCRuns++;
    dynamic_area.gc(this);
  }  
// ifdef NO_FASTBACKTRACK





//#endif NO_FASTBACKTRACK

// ifdef NO_COMPRESSION
// ifdef NO_FASTBACKTRACK
  public int[] getBacktrackData() {
    // gets the information from the static area
    int[] sa = static_area.getStoringData();
    int sal = sa.length;

    // gets the information from the dynamic area
    int[] da = dynamic_area.getStoringData();
    int dal = da.length;

    // gets the information from the list of threads

    // okay here is a little more complicated
    // the class List doesn't have any method called
    // getStoringData, but each of the objects in it
    // do, because we put ThreadInfo objects

    // for each of the threads in the list we collect the information
    int tl = threads.size();
    int[][] ts = new int[tl][];
    int len = 0; // this will contain the total length

    for(int idx = 0; idx < tl; idx++) {
      ts[idx] = ((ThreadInfo)threads.get(idx)).getStoringData();
      // there is an extra value for the size of each thread info
      len += ts[idx].length + 1;
    }

    // the total size includes static area size, static area, dynamic area
    // size, dynamic area, number of threads and the information about each
    // thread (with already include the size of them).
    int size = 1 + sal + 1 + dal + 1 + len;

    // allocate an array big enough to fit all the information
    data = new int[size];

    data[0] = sal;              // static area size
    System.arraycopy(sa, 0, data, 1, sal);  // static area
    data[1 + sal] = dal;            // dynamic area size
    System.arraycopy(da, 0, data, 1 + sal + 1, dal);
    // dynamic area
    data[1 + sal + 1 + dal] = tl;       // number of threads
    for(int idx = 0, pos = 1 + sal + 1 + dal + 1; idx < tl; idx++) {
      int tsl = ts[idx].length;
      data[pos++] = tsl;            // length of the thread info
      System.arraycopy(ts[idx], 0, data, pos, tsl);
      // thread info
      // skips the positions used by the thread information
      pos += tsl;
    }

    return data;
  }  
//#endif RACE

  public DynamicArea getDynamicArea() {
    return dynamic_area;
  }  
  public StaticArea getStaticArea() {
    return static_area;
  }  
//#else NO_FASTBACKTRACK




















































//#endif NO_FASTBACKTRACK
//#endif NO_COMPRESSION

// ifdef NO_COMPRESSION
  // returns a compact rapresentation of the state
  public Object getStoringData() {
// ifdef NO_FASTBACKTRACK

//#endif NO_FASTBACKTRACK
    // computes and hash value for the data
    int hash_value = hash_data(data);

    ////#ifdef HASHCOMPACT
    if (VirtualMachine.options.hashcompact) {
      int[] hash_compact_value = new int[1];
      hash_compact_value[0] = hash_reverse_data(data);
      return new ArrayWrapper(hash_compact_value, hash_value);
    } else
    ////#endif HASHCOMPACT
      return new ArrayWrapper(data, hash_value);
  }  
//#endif NO_COMPRESSION

  public int getThreadCount() {
    return threads.size();
  }  
  // Returns the information about a particular thread
  public iThreadInfo getThreadInfo(int thread) {
    if (thread < 0 || thread >= threads.size()) {
// ifdef DEBUG

//#endif DEBUG
      return null;
    }

    return (iThreadInfo)threads.get(thread);
  }  
// ifdef RACE
  public LockTree getThreadLockTree(int idx) {
    return ((ThreadInfo)threads.get(idx)).getLockTree();
  }  
  // these are two polinomial hash functions
  private int hash_data(int[] data) {
    HashData hd = new HashData();

    for (int i = 0, l = data.length; i < l; i++)
      hd.add(data[i]);

    return hd.getValue();
  }  
  // this one looks like the first one but processes
  // the data backward giving a pretty statistically
  // indipendent value
  private int hash_reverse_data(int[] data) {
    HashData hd = new HashData();

    for (int i = data.length-1; i >= 0; i--)
      hd.add(data[i]);

    return hd.getValue();
  }  
  public int hashCode() {
    HashData hd = new HashData();

    dynamic_area.hash(hd);
    static_area.hash(hd);

    for(int i = 0, l = threads.size(); i < l; i++)
      ((ThreadInfo)threads.get(i)).hash(hd);

    return hd.getValue();
  }  
  // Checks if there are no alive threads
  //** This could be optimized (timewise) having a local table **//
  public boolean isTerminated() {
    for(Iterator it = threads.iterator(); it.hasNext(); )
      if (((ThreadInfo)it.next()).isAlive()) return false;
    return true;
  }  
//#endif MARK_N_SWEEP

// ifdef REFERENCE_COUNT







//#endif REFERENCE_COUNT

  public void log() {
    dynamic_area.log();
    static_area.log();
    for(int i = 0; i < threads.size(); i++)
      ((ThreadInfo)threads.get(i)).log();
    Debug.println(Debug.MESSAGE);
  }  
//#endif NO_COMPRESSION

  // Adds a new thread to the thread list
  public void newThread(iThreadInfo ti) {
    ((ThreadInfo)ti).setThreadReference(threads.size());
    threads.add(ti);
  }  
// ifdef NO_COMPRESSION
  // This function revert changes moving back to a previous state
  public void revertTo(int[] data) {
    int sal = data[0];              // static area size
    int[] sa = new int[sal];
    System.arraycopy(data, 1, sa, 0, sal);  // static area
    static_area.revertTo(sa);

    int dal = data[1 + sal];            // dynamic area size
    int[] da = new int[dal];
    System.arraycopy(data, 1 + sal + 1, da, 0, dal);
    dynamic_area.revertTo(da);          // dynamic area

    int tl = data[1 + sal + 1 + dal];       // number of threads
    int[][] ts = new int[tl][];
    for(int idx = 0, pos = 1 + sal + 1 + dal + 1; idx < tl; idx++) {
      int tsl = data[pos++];            // length of the thread info
      ts[idx] = new int[tsl];
      System.arraycopy(data, pos, ts[idx], 0, tsl);
                            // thread info
      
      // skips the positions used by the thread information
      pos += tsl;
    }

    // Now we reconstract the list. For the entry that are already present
    // we just try to revert them to the right value, if there are more
    // we build them from scratch, if there are less we remove the others.
    int ctl = threads.size();

    if(ctl == tl)
      for(int idx = 0; idx < tl; idx++)
    ((ThreadInfo)threads.get(idx)).revertTo(this, ts[idx]);
    else if(ctl < tl) {
      for(int idx = 0; idx < ctl; idx++)
    ((ThreadInfo)threads.get(idx)).revertTo(this, ts[idx]);
      for(int idx = ctl; idx < tl; idx++) {
    ThreadInfo th = new ThreadInfo(this, ts[idx]);

    threads.add(th);
    th.setThreadReference(idx);
      }
    } else {
      for(int idx = 0; idx < tl; idx++)
    ((ThreadInfo)threads.get(idx)).revertTo(this, ts[idx]);
      for(int idx = tl; idx < ctl; idx++)
    threads.remove(tl);
    }
  }  
}

---