---

KernelState.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import java.io.*;
//#ifdef JDK11



//#else JDK11
import java.util.*;
//#endif JDK11
//#ifdef COVERAGE

//#endif COVERAGE

/**
 * This class represents the stack of the JVM.
 */
public class KernelState implements Storable {
  /**
   * The area containing the classes.
   */
  public StaticArea  sa;

  /**
   * The area containing the objects.
   */
  public DynamicArea da;
  
  /**
   * The list of the threads.
   */
  public ThreadList  tl;

  /**
   * Link to the system state.
   */
  public SystemState ss;

  /**
   * Number of nested atomic blocks.
   */
  public int atomicLevel;

  /**
   * True if the last was an intermediate step.
   */
  private boolean intermediateStep;

  /**
   * Thread that made stopped at an intermediate step.
   */
  private int intermediateThread;

  /**
   * The data returned by last get data.
   */
  public int[] data;

  private KernelState(KernelState ks) {
    sa = (StaticArea)ks.sa.clone();
    sa.ks = this;
    da = (DynamicArea)ks.da.clone();
    da.ks = this;
    tl = (ThreadList)ks.tl.clone();
    tl.ks = this;
    ss = null;
    atomicLevel = ks.atomicLevel;
    intermediateThread = ks.intermediateThread;
    data = ks.data;
  }  
  /**
   * Creates a new kernel state object.
   */
  public KernelState(SystemState system_state) {
    sa = new StaticArea(this);
    da = new DynamicArea(this);
    tl = new ThreadList(this);
    ss = system_state;
    atomicLevel = 0;
    intermediateStep = false;
    intermediateThread = -1;
    data = null;
  }  
  public void backtrackTo(ArrayOffset storing, Object backtrack) {
    sa.backtrackTo(storing, ((Object[])backtrack)[0]);
    da.backtrackTo(storing, ((Object[])backtrack)[1]);
    tl.backtrackTo(storing, ((Object[])backtrack)[2]);
    atomicLevel = ((Integer)((Object[])backtrack)[3]).intValue();
    intermediateStep = ((Boolean)((Object[])backtrack)[4]).booleanValue();
    intermediateThread = ((Integer)((Object[])backtrack)[5]).intValue();

    data = storing.data;
  }  
  public void clearAtomic() {
    atomicLevel--;
  }  
  public void clearIntermediate() {
    intermediateStep = false;
    intermediateThread = -1;
  }  
  public Object clone() {
    return new KernelState(this);
  }  
//#ifdef MARK_N_SWEEP
  public void gc() {
    Engine.getJPF().status.GCRuns++;
    da.gc();
  }  
  public Object getBacktrackData() {
    Object[] data = new Object[6];

    data[0] = sa.getBacktrackData();
    data[1] = da.getBacktrackData();
    data[2] = tl.getBacktrackData();
    data[3] = new Integer(atomicLevel);
    data[4] = new Boolean(intermediateStep);
    data[5] = new Integer(intermediateThread);
    
    return data;
  }  
  public int getIntermediateThread() {
    return intermediateThread;
  }  
  public int[] getStoringData() {
    if(data != null) return data;

    int[] saData = sa.getStoringData();
    int[] daData = da.getStoringData();
    int[] tlData = tl.getStoringData();

    int sal = saData.length;
    int dal = daData.length;
    int tll = tlData.length;

    data = new int[sal + dal + tll];

    System.arraycopy(saData, 0, data, 0, sal);
    System.arraycopy(daData, 0, data, sal, dal);
    System.arraycopy(tlData, 0, data, sal + dal, tll);

    return data;
  }  
  public int getThreadCount() {
    return tl.length();
  }  
  public iThreadInfo getThreadInfo(int index) {
    return tl.get(index);
  }  
  public void hash(HashData hd) {
    da.hash(hd);
    sa.hash(hd);

    for(int i = 0, l = tl.length(); i < l; i++)
      tl.get(i).hash(hd);
  }  
  /**
   * Hash an array of integers.
   */
  private static 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();
  }  
  /**
   * Hash an array of integers again. This time
   * uses the elements backward to have an independent
   * value.
   */
  private static 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();

    hash(hd);

    return hd.getValue();
  }  
  public boolean isIntermediate() {
    return intermediateStep;
  }  
  /**
   * The program is terminated if there are no alive threads.
   */
  public boolean isTerminated() {
    return !tl.anyAliveThread();
  }  
  public void jvmError(Exception e, ThreadInfo th) {
    log();
    e.printStackTrace();
    if(th != null) th.printInternalErrorTrace(e);
    Engine.getJPF().vm.getErrorTrail().print();
    Engine.getJPF().vm.getErrorTrail_to_file();
    System.exit(1);
  }  
//#endif MARK_N_SWEEP

  public void log() {
    da.log();
    sa.log();
    for(int i = 0; i < tl.length(); i++)
      tl.get(i).log();
    Debug.println(Debug.MESSAGE);
  }  
  /**
   * Creates a new thread.
   */
  public ThreadInfo newThread(int objref) {
    ThreadInfo th = new ThreadInfo(objref);

    tl.add(tl.length(), th);
//#ifdef COVERAGE

//#endif COVERAGE
    return th;
  }  
  public void setAtomic() {
    atomicLevel++;
  }  
  public void setIntermediate() {
    intermediateStep = true;
    intermediateThread = ss.sch.getThread();
  }  
}

---