---

VirtualMachine.java

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

import de.fub.bytecode.*;
import edu.ksu.cis.bandera.jjjc.decompiler.*;
import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.util.Counter;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.Comma;
// ifdef NO_COMPRESSION
import gov.nasa.arc.ase.util.HashPool;
//#endif NO_COMPRESSION
import java.io.*;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.*;

public class VirtualMachine implements iVirtualMachine {
  private SystemState system_state;
// ifdef REFERENCE_COUNT

//#else REFERENCE_COUNT
  private KernelState kernel_state;
//#endif REFERENCE_COUNT
  private StateStack  stack = new StateStack();
  private boolean     first_max_stack_reached = true;
  // used by bandera error trail
  private String      mainClass;
  private JVMPath     errorPath;
  private int         pos_in_errorPath;
  private Counter     matching_states;

// ifdef NO_COMPRESSION
  public static HashPool fieldsPool = new HashPool();
  public static HashPool framePool = new HashPool();
  public static HashPool objectInfoPool = new HashPool();
  public static HashPool threadPool = new HashPool();
//#endif NO_COMPRESSION

// ifdef MARK_N_SWEEP
  private static boolean gc_needed = false;
//#endif MARK_N_SWEEP

  public static JVMOptions options;

  private static boolean initial_state = true;

// ifdef REFERENCE_COUNT







//#endif REFERENCE_COUNT
  public VirtualMachine(String classname) {
    new JPFVM();
    mainClass = classname;
    stack.setMaxDepth(VirtualMachine.options.search_depth);
    system_state = new SystemState();
    kernel_state = new KernelState();
// ifdef DISTRIBUTED



//#endif DISTRIBUTED

    ClassInfo ci = JPFVM.getJPFVM().getClass(classname);
    int mainclass = kernel_state.static_area.addClass(ci);

    ThreadInfo th = ci.executeMain(kernel_state, mainclass);
    ci.initialize(system_state, kernel_state, th);

    pushInitialSystemState();
    Engine.store.initial(kernel_state);
  }
  public static void activateGC() { gc_needed = true; }
  public boolean Backtrack() {
// ifdef DEBUG_SEARCH

//#endif DEBUG_SEARCH
    if (stack.isEmpty()) return false;

// ifdef DEBUG

//#endif DEBUG

    SystemState ss = (SystemState)stack.Pop();
    if (ss == null) return false;

    system_state = (SystemState)ss.clone();

// ifdef NO_COMPRESSION
    int[] data;
//#endif NO_COMPRESSION

    // Last system state on the stack
// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK
    data = system_state.getBacktrackData();
    kernel_state.revertTo(data);
//#endif NO_FASTBACKTRACK
// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT
// ifdef DEBUG


// ifdef REFERENCE_COUNT




//#endif REFERENCE_COUNT
//#endif DEBUG
    system_state.restoreAtomicData(kernel_state);
    TransitionResult.atomicLevel = system_state.atomicLevel;

    return true;
  }
  public Path buildPath() {
    int s = stack.size();
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD

//#else CHILDREN_LOOKAHEAD

//#endif CHILDREN_LOOKAHEAD
//#else DISTRIBUTED
    JVMPath p  = new JVMPath(s == 0 ? s : s - 1, 0);
//#endif DISTRIBUTED

    for(int index = 1; index < s; index++)
      p.set(index-1,
      ((SystemState)stack.get(index)).getTrailInfo().getThread());

    return p;
  }
  public boolean CheckInvariant(iProperty p) {
    return p.property(kernel_state);
  }
  public FilenameLinePair ErrorBackward() {
    Backtrack();
    pos_in_errorPath--;
    JVMPathEntry e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath);
    return new FilenameLinePair(e.file, e.line);
  }
  public FilenameLinePair ErrorForward() {
    if (pos_in_errorPath >= errorPath.size())
      return null;
    JVMPathEntry e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath);
    Scheduler sch = system_state.getScheduler();
    sch.setCurrentThread(e.thread);
    Forward();
    pos_in_errorPath++;
    if (pos_in_errorPath >= errorPath.size())
      return null;
    e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath);
    return new FilenameLinePair(e.file, e.line);
  }
  public FilenameLinePair ErrorInit() {
    ((JPFOptions)Engine.options).po_reduction = false;
    reinit(mainClass);
    pos_in_errorPath = 0;
    JVMPathEntry e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath);
    return new FilenameLinePair(e.file, e.line);
  }
  public int ErrorPathLength() {
    return errorPath.size();
  }
  public int Forward() {
// ifdef DEBUG_SEARCH

//#endif DEBUG_SEARCH
    boolean result;

    if (stack.Full(system_state.getScheduler().getSafeMoves())) {
      if (first_max_stack_reached) {
// ifdef DEBUG





//#endif DEBUG
    first_max_stack_reached = false;
      }
      return RESULT.EXIT;
    }
    //Debug.println(Debug.DEBUG, "\n---> Forward");
    result = system_state.nextSuccessor(kernel_state);
    if (!result) {
      if(system_state.handleIntermediate(kernel_state))
    return Forward();
      if (kernel_state.isTerminated()) {
// ifdef DEBUG

//#endif DEBUG
    return RESULT.EXIT;
      } else {
// ifdef DEBUG

//#endif DEBUG
    return RESULT.END;
      }
    } else {
// ifdef DEBUG

//#endif DEBUG
// ifdef MARK_N_SWEEP
      if (VirtualMachine.options.garbage_collection && gc_needed) {
    kernel_state.gc();
    gc_needed = false;
      }
//#endif MARK_N_SWEEP
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD




//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED
      pushSystemState();
// ifdef DISTRIBUTED

//#endif DISTRIBUTED
    result = Engine.store.put(kernel_state);
    if (result)
      return RESULT.NEW;
    else
      return RESULT.OLD;
// ifdef DISTRIBUTED


//#endif DISTRIBUTED
    }
  }
  public ErrorTrailInterface getErrorTrail() {
    Vector v = new Vector();
    v.addElement("");
    v.addElement("");
    v.addElement("========================");
    v.addElement(" *** Path to error: ***");
    v.addElement("========================");
    int Elements_in_trail = stack.size();
    v.addElement("Steps to error: " + (Elements_in_trail-1));
    for(int index = 1; index < Elements_in_trail; index++)
      try {
    v.add(index + ": " + ((SystemState)stack.get(index)).getTrailInfo().toString());
      } catch(NullPointerException e) {
    v.add(index + ":");
      }

    ErrorTrail e = new ErrorTrail(v.size());
    for(int index = 0; index < v.size(); index++)
      e.add((String)v.elementAt(index));

    return e;
  }
  /*********************************************************************/

  /*********************************************************************/
  // read errorFile into ePath; only in path-simulation mode
  /*********************************************************************/
  public Path getErrorTrail_from_file() {
    JVMPath ePath = null;
    try {
      String filename = mainClass + ".error.path";
      FileReader fr = new FileReader(filename);
      LineNumberReader ifr = new LineNumberReader(fr);
      String ln = ifr.readLine();
      StringTokenizer t;

      if(ln !=null) {
    t = new StringTokenizer(ln, " :\t\r\n");
    // Size
    t.nextToken();
    int size = Integer.parseInt(t.nextToken());
    ePath = new JVMPath(size);


    for(int index = 0; index < size; index++) {//??good size
      ln = ifr.readLine();
      t = new StringTokenizer(ln, " :\t\r\n");

      // Thread #
      t.nextToken();
      int thread = Integer.parseInt(t.nextToken());

      // Line #
      t.nextToken();
      int line = Integer.parseInt(t.nextToken());

      // Class name
      t.nextToken();
      String classname = t.nextToken();

      // Random #
      t.nextToken();
      int random = Integer.parseInt(t.nextToken());

      ePath.setErrorMove(index, line, classname, thread, random);

    }
      }
      fr.close();

    } catch (Exception e) {
      e.printStackTrace();
    }
    return ePath;
  }
  // read errorFile into errorPath

  /*/\/\/\/\/\/\/\/\/\/\ for path simulation ... */
  /*************************************************************************/
  // when getErrorTrail_to_file is invoked, the error file should be created
  /*************************************************************************/
  public Path getErrorTrail_to_file() {
    int s = stack.size();
    int size =   (s == 0 ? s : s - 1);

    // dump the error trace
    try {
      PrintWriter out = new PrintWriter(new OutputStreamWriter(
        new  FileOutputStream(mainClass + ".error.path")));

      out.print("Size:"+ size +"\n"); // size of error path

      for(int index = 1; index < s; index++) {
    int line = ((SystemState)stack.get(index)).getTrailInfo().getLine();
    String classname = ((SystemState)stack.get(index)).getTrailInfo().getClassname();
    int thread = ((SystemState)stack.get(index)).getTrailInfo().getThread();
    int random = ((SystemState)stack.get(index)).getTrailInfo().getRandom();

    out.print("Thread:"+ thread +"\t Line:"+ line +"\t Class:"+ classname +"\t Random:"+random +"\n");
      }
      out.close();
    } catch (Exception e) {
      /* do cleanup here - - possibly rethrow e */
      e.printStackTrace();
    }
    return null;
  }
// ifdef DISTRIBUTED
// ifdef CHILDREN_LOOKAHEAD
























//#endif CHILDREN_LOOKAHEAD
//#endif DISTRIBUTED

  // new code for production of error trail for Bandera

  public Path getErrorTrail1() {
    int s = stack.size();
    errorPath = new JVMPath(s == 0 ? s : s - 1);
    for(int index = 1; index < s; index++)
      errorPath.setErrorMove(index-1,
      ((SystemState)stack.get(index)).getTrailInfo().getLine(),
      ((SystemState)stack.get(index)).getTrailInfo().getClassname(),
      ((SystemState)stack.get(index)).getTrailInfo().getThread(),
      ((SystemState)stack.get(index)).getTrailInfo().getRandom()
                );

    // dump errorPath to file

    return errorPath;
  }
  public iKernelState getKernelState(){
    return kernel_state;
  }
  public int getSafeMoves() {
    return system_state.getScheduler().getSafeMoves();
  }
  public static String getStatus() {
// ifdef NO_COMPRESSION

//#else NO_COMPRESSION
    return " fsp " + Comma.format(fieldsPool.size()) +
      " frp " + Comma.format(framePool.size()) +
      " tp " + Comma.format(threadPool.size()) +
      " oip " + Comma.format(objectInfoPool.size());
//#endif NO_COMPRESSION
  }
  public iSystemState getSystemState(){
    return system_state;
  }
  public int nextThreadToExecute() {
    if (pos_in_errorPath >= errorPath.size())
      return -1;
    JVMPathEntry e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath);
    return e.thread;
  }
  public int previousThreadToExecute() {
    if (pos_in_errorPath < 1)
      return -1;
    JVMPathEntry e = ((JVMPath)errorPath).getErrorMove(pos_in_errorPath-1);
    return e.thread;
  }
  public void printStackTrace() {
    ((ThreadInfo)kernel_state.getThreadInfo(system_state.getScheduler().getCurrentThread())).printStackTrace();
  }
// ifdef BUCHI














// ifdef MARK_N_SWEEP




//#endif MARK_N_SWEEP





















// ifdef NO_COMPRESSION

//#endif NO_COMPRESSION
// ifdef NO_FASTBACKTRACK

//#endif NO_FASTBACKTRACK

// ifdef NO_FASTBACKTRACK


//#endif NO_FASTBACKTRACK
// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT





















// ifdef NO_FASTBACKTRACK

//#endif NO_FASTBACKTRACK

// ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT



// ifdef NO_COMPRESSION

//#endif NO_COMPRESSION

// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK


//#endif NO_FASTBACKTRACK

// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT










































































// ifdef NO_FASTBACKTRACK



























//#else NO_FASTBACKTRACK


































//#endif NO_FASTBACKTRACK





// ifdef NO_FASTBACKTRACK

//#endif NO_FASTBACKTRACK

// ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT



//#endif BUCHI

  public void pushInitialSystemState() {
// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK
    system_state.setBacktrackData(kernel_state.getBacktrackData());
//#endif NO_FASTBACKTRACK

// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT

// ifdef DEBUG


// ifdef REFERENCE_COUNT




//#endif REFERENCE_COUNT
//#endif DEBUG

    SystemState ss = (SystemState)system_state.clone();
    stack.Push(ss);
  }
  public void pushSystemState() {
    Scheduler sch = system_state.getScheduler();
    stack.UpdateTop(sch);
    sch.initialize();
    system_state.atomicLevel = TransitionResult.atomicLevel;
    TransitionResult.initialize();
    stack.UpdateTopExtra(system_state);
// ifdef NO_FASTBACKTRACK

//#else NO_FASTBACKTRACK
    system_state.setBacktrackData(kernel_state.getBacktrackData());
//#endif NO_FASTBACKTRACK

// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT

// ifdef DEBUG


// ifdef REFERENCE_COUNT




//#endif REFERENCE_COUNT
//#endif DEBUG

    SystemState ss = (SystemState)system_state.clone();
    stack.Push(ss);
  }
  public void reinit(String classname){
    new JPFVM();
// ifdef RACE
    Runner.race_conditions = 0;
//#endif RACE
    stack = new StateStack();
    stack.setMaxDepth(VirtualMachine.options.search_depth);

    Repository.clearCache();
// ifdef NO_STATIC_SYMMETRY
    StaticMap.reset();
//#endif NO_STATIC_SYMMETRY

    system_state = new SystemState();
    kernel_state = new KernelState();

    ClassInfo ci = JPFVM.getJPFVM().getClass(classname);
    int mainclass = kernel_state.static_area.addClass(ci);

    ThreadInfo th = ci.executeMain(kernel_state, mainclass);
    ci.initialize(system_state, kernel_state, th);

    pushInitialSystemState();
    Engine.store.initial(kernel_state);
  }
  public void ShowErrorTrail() {
    BufferedWriter out = null;

    Debug.println(Debug.WARNING, "\n");
    Debug.println(Debug.WARNING, "========================");
    Debug.println(Debug.WARNING, " *** Path to error: ***");
    Debug.println(Debug.WARNING, "========================");
    int Elements_in_trail = stack.size();
    Debug.println(Debug.WARNING, "Steps to error: " + (Elements_in_trail-1));
    try{
      out = new BufferedWriter(new FileWriter("error.trail"));
    } catch (IOException e) {};
    for(int index = 1; index < Elements_in_trail; index++) {
      Debug.print(Debug.WARNING, index + ": ");
      ((SystemState)stack.get(index)).getTrailInfo().print();
      ((SystemState)stack.get(index)).getTrailInfo().dump2file(out);
    }
    try {out.close();} catch (IOException e) {};
  }
  /*********************************************************************/
  /*/\/\/\/\/\/\/\/\/\/\ end ... */


  public void ShowErrorTrail(Path ePath) {
    reinit(mainClass);
    for(int i = 0; i < errorPath.size()-1; i++) {
      FilenameLinePair pair = ErrorForward();
      Debug.println(Debug.WARNING, pair.getFilename() + " " +
      pair.getLine());
    }
  }
// ifdef DISTRIBUTED




// ifdef DEBUG_SEARCH

//#endif DEBUG_SEARCH





























// ifdef NO_FASTBACKTRACK

//#endif NO_FASTBACKTRACK
// ifdef REFERENCE_COUNT

//#endif REFERENCE_COUNT



// ifdef CHILDREN_LOOKAHEAD



//#endif CHILDREN_LOOKAHEAD
// ifdef DEBUG_SEARCH

//#endif DEBUG_SEARCH



//#endif DISTRIBUTED

  public int simForward() {
    boolean result;

    result = system_state.nextSuccessor(kernel_state);
    if (!result) {
      if (kernel_state.isTerminated()){
// ifdef DEBUG

//#endif DEBUG
    return RESULT.EXIT;
      }
      else{
// ifdef DEBUG

//#endif DEBUG
    return RESULT.END;
      }
    }
    else {
// ifdef DEBUG

//#endif DEBUG
// ifdef MARK_N_SWEEP
      if (VirtualMachine.options.garbage_collection && gc_needed) {
    kernel_state.gc();
    gc_needed = false;
      }
//#endif MARK_N_SWEEP
// ifdef RACE
      if (Runner.race_conditions >= VirtualMachine.options.race_level)
    return RESULT.EXIT;
//#endif RACE
      if (Reader.interrupt()){
    Debug.println(Debug.ERROR, "EXECUTION HAS BEEN INTERRUPTED !!");
    return RESULT.EXIT;
      }
      return RESULT.NEW;
    }
  }
  /*********************************************************************/

  /*********************************************************************/
  // used in path simulation mode: stuttering equivalence
  /*********************************************************************/
  public void SimulateErrorTrail(Path ePath) {
    JVMPathEntry e;
    Scheduler sch;
    int s; // stack size

    int old_line = 0; // for stuttering

    reinit(mainClass);
    pos_in_errorPath = 0;

    while(pos_in_errorPath < ePath.size()) {
      e = ((JVMPath)ePath).getErrorMove(pos_in_errorPath);
      // some e's should be ignored when interpreting abstract counterexamples on a concrete program
      sch = system_state.getScheduler();
      sch.setCurrentThread(e.thread);
      sch.setCurrentRandom(e.random);
      Forward();
      s = stack.size();

      int line_sim = ((SystemState)stack.get(s-1)).getTrailInfo().getLine();
      int random_sim = ((SystemState)stack.get(s-1)).getTrailInfo().getRandom();

      if(e.line != line_sim)  {

    while(e.line == old_line && pos_in_errorPath < ePath.size()-1) {//stuttering
      pos_in_errorPath++;
      e = ((JVMPath)ePath).getErrorMove(pos_in_errorPath);
    }

    if(e.line != line_sim)  { // Warning !!!
      Debug.println(Debug.ERROR, "!!!!! Warning: mismatch line numbers: program "+ line_sim +" ; error trail "+e.line);
      Debug.println(Debug.ERROR, "! This may not be a real counter-example !");

      pos_in_errorPath = ePath.size(); // exit while loop
    }
      }

      if(e.random != random_sim) // Warning !!!
    Debug.println(Debug.ERROR, "!!!!! Warning: mismatch random numbers: program "+ random_sim +" ; error trail "+e.random);

      old_line = e.line;
      pos_in_errorPath++;
    }
  }
}

---