---

VirtualMachine.java

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

import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.ErrorTrailInterface;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.JPF;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.jpf.Path;
import gov.nasa.arc.ase.jpf.Status;
import gov.nasa.arc.ase.jpf.TransitionResult;
import gov.nasa.arc.ase.jpf.iStore;
import gov.nasa.arc.ase.jpf.iScheduler;
import gov.nasa.arc.ase.jpf.iSystemState;
import gov.nasa.arc.ase.jpf.iThreadInfo;
import gov.nasa.arc.ase.jpf.iTrailInfo;
import gov.nasa.arc.ase.jpf.iVirtualMachine;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.util.Comma;
import gov.nasa.arc.ase.util.Counter;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.Right;
import java.io.BufferedReader;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.io.LineNumberReader;
import java.io.OutputStreamWriter;
import java.io.PrintStream;
import java.io.PrintWriter;
import java.lang.reflect.InvocationTargetException;
import java.lang.reflect.Method;
import java.util.Stack;
import java.util.StringTokenizer;
import java.util.Vector;
//#ifdef BANDERA
import edu.ksu.cis.bandera.jjjc.decompiler.FilenameLinePair;
//#endif BANDERA
//#ifdef DISTRIBUTED || PARALLEL

//#endif DISTRIBUTED || PARALLEL
//#ifdef JDK11

//#else JDK11
import java.util.LinkedList;
//#endif JDK11
//#ifdef BUCHI
import gov.nasa.arc.ase.jpf.BuchiSet;
//#ifdef JDK11

//#else JDK11
import java.util.HashSet;
//#endif JDK11
//#endif BUCHI
//#ifdef JDK11

//#endif JDK11

/**
 * This class represents the virtual machine. The virtual machine is able to
 * move backward and forward one step at a time.
 */
public class VirtualMachine implements iVirtualMachine {
  /**
   * The state of the system.
   */
  private SystemState ss;

  /**
   * State storing information stack.
   */
  private Stack stateStoringStack;

  /**
   * State backtrack information stack.
   */
  private Stack stateBacktrackStack;

  /**
   * Backtrack stack.
   */
  private Stack backtrackStack;

  /**
   * Used to print the max stack depth reached message only once.
   */
  private boolean maxDepthReached;

  /**
   * The name of the main class.
   */
  private String classname;

  /**
   * The arguments to the main class.
   */
  private String[] args;

  /**
   * The path to the error.
   */
  private JVMPath errorPath;

  /**
   * The current position in the error path.
   */
  private int posInErrorPath;

  /**
   * Set to true during path execution.
   */
  private boolean executingPath;

  /**
   * Path to the current position.
   */
  private LinkedList path;

//#ifdef BUCHI

  /**
   * Set to true at the initial state. Used to simulate
   * a transition into the initial state itself.
   */
  private boolean initialState;

  /**
   * Contains the list of the positions which are observable.
   */
  public static HashSet observablePositions = new HashSet();

  /**
   * Contains the list of the labels which are observable.
   */
  public static HashSet observableLabels = new HashSet();

  /**
   * Contains the list of invoke instructions which are observable.
   */
  public static HashSet observableInvokes = new HashSet();

  /**
   * Contains the list of methods whose return instruction are observable.
   */
  public static HashSet observableReturns = new HashSet();

//#endif BUCHI


  /**
   * A way to access the options specific to the JVM
   * without using a cast.
   */
  public static JVMOptions options;

  /**
   * Thread local version of the system state.
   */
//#ifdef BANDERA
  private static SystemState xss;
//#else BANDERA
//#ifdef JDK11

//#else JDK11

//#endif JDK11
//#endif BANDERA

  /**
   * Set of packages where to look for partition
   * classes. The first entry is null and it is
   * set as the package the main class is defined
   * in at run time.
   */
  private static String[] partitionPath = {
    null,
    "gov.nasa.arc.ase.jpf.partition",
    "gov.nasa.arc.ase.jpf.jvm.partition",
  };

  private static BufferedReader br = new BufferedReader(
      new InputStreamReader(System.in));

  /**
   * Creates a new Virtual Machine.
   */  
  public VirtualMachine() {
  }  
  /**
   * Moves one step backward.
   */
  public boolean Backtrack() {
    // cannot backtrack if the stack is empty
    if(stateStoringStack.empty())
      return false;

    // Removes the state from the stack.
    Engine.getJPF().store.offStack(ss);

    // restore the state and the system
    popState();
    popSystem();

//    System.err.println("Backtrack done");
//    ss.ks.log();

    return true;
  }  
  public boolean BuchiBacktrack() {
    return Backtrack();
  }  
  public boolean BuchiEvaluate(Method method) {
    Object[] args = new Object[1];
    args[0] = ss;

    try {
      return ((Boolean)method.invoke(null, args)).booleanValue();
    } catch(InvocationTargetException e) {
      e.printStackTrace();
      throw new JPFErrorException("Internal exeception in " + method.getDeclaringClass().getName());
    } catch(IllegalAccessException e) {
      throw new JPFErrorException("Illegal access to " + method.getDeclaringClass().getName());
    }
  }  
  public boolean BuchiEvaluate(Method method, Object[] arg) {
    Object[] args = new Object[arg.length+1];

    args[0] = ss;
    for(int i = 0; i < arg.length; i++) {
      if(arg[i] instanceof ReferenceWrapper) {
    args[i+1] = getReference(arg[i].toString());
      } else
    args[i+1] = arg[i];
    }

    try {
      return ((Boolean)method.invoke(null, args)).booleanValue();
    } catch(InvocationTargetException e) {
      e.printStackTrace();
      throw new JPFErrorException("Internal exeception in " + method.getDeclaringClass().getName());
    } catch(IllegalAccessException e) {
      throw new JPFErrorException("Illegal access to " + method.getDeclaringClass().getName());
    }
  }  
//#ifdef BUCHI
  public int BuchiForward() {
    boolean sys_move;
    int sd = options.search_depth;

    if(sd != -1
    && stateStoringStack.size() >= sd) {
      if(!maxDepthReached) {
    maxDepthReached = true;
    Debug.println(Debug.WARNING, "Max search depth reached");
      }

      return TransitionResult.END;
    }

    JPF jpf = Engine.getJPF();
    Status status = jpf.status;

    if(status.maxStackDepth < path.size())
      status.maxStackDepth = path.size();

    pushState();

    if(initialState) {
      initialState = false;
    } else
      if(!ss.nextSuccessor()) {
    removeState();

    return TransitionResult.END;
      }

    ss.sch.next();
    pushSystem();
    ss.sch.initialize(ss);

//#ifdef MARK_N_SWEEP

    if(options.garbage_collection && ss.GCNeeded) {
      ss.ks.gc();
      ss.GCNeeded = false;
    }

//#endif MARK_N_SWEEP

    if(ss.violatedAssertion || ss.uncaughtException) {
      return TransitionResult.NEW | TransitionResult.ERROR;
    } else {
      return TransitionResult.NEW;
    }
  }  
  public BuchiSet BuchiGet() {
    return Engine.getJPF().store.BuchiGet(ss);
  }  
  public void BuchiInitSch() {
    ss.sch.initialize(ss);
  }  
  public void BuchiObservable(String observable) {
    if(observable.startsWith("invoke.")) {
      synchronized(observableInvokes) {
    observableInvokes.add(observable.substring(7));
      }
    } else if(observable.startsWith("return.")) {
      synchronized(observableReturns) {
    observableReturns.add(observable.substring(7));
      }
    } else if(observable.startsWith("position.")) {
      synchronized(observablePositions) {
    observablePositions.add(observable.substring(9));
      }
    } else if(observable.startsWith("label.")) {
      synchronized(observableLabels) {
    observableLabels.add(observable.substring(6));
      }
    } else
      Debug.println(Debug.ERROR, "Unknown observable: " + observable);
  }  
  public void BuchiSetState(int buchi_state) {
    ((TrailInfo)path.getLast()).setBuchiState(buchi_state);
  }  
  /**
   * Creates a path to the current state.
   */
  public Path buildPath() {
    int s = path.size();

    JVMPath p  = new JVMPath(s);

    for(int index = 0; index < s; index++)
      p.set(index, ((TrailInfo)path.get(index)).getEntry());

    return p;
  }  
  /**
   * Moves backward in the error path.
   */
  public FilenameLinePair ErrorBackward() {
    Backtrack();

    posInErrorPath--;

    JVMPathEntry e = errorPath.get(posInErrorPath);

    return new FilenameLinePair(e.file, e.line);
  }  
  /**
   * Moves forward in the simulation.
   */
  public FilenameLinePair ErrorForward() {
    if (posInErrorPath >= errorPath.size())
      return null;

    JVMPathEntry e = errorPath.get(posInErrorPath);

    Forward();

    posInErrorPath++;

    if (posInErrorPath >= errorPath.size())
      return null;

    e = errorPath.get(posInErrorPath);

    return new FilenameLinePair(e.file, e.line);
  }  
  /**
   * Initializes error simulation.
   */
  public FilenameLinePair ErrorInit() {
    reinit();

    posInErrorPath = 0;

    ss.sch = new PathScheduler(ss, errorPath);

    JVMPathEntry e = errorPath.get(posInErrorPath);

    return new FilenameLinePair(e.file, e.line);
  }  
  /**
   * Length of the erro path.
   */
  public int ErrorPathLength() {
    return errorPath.size();
  }  
  public boolean executePath(Path p) {
    // first_max_stack_reached we need to backtrack to the initial state
    int backtrack = p.upCount();
    for(int i = 0; i < backtrack; i++)
      Backtrack();

    // now we have to execute all the steps in the p
    executingPath = true;

    ss.sch = new PathScheduler(ss, (JVMPath)p);

    for(int i = 0; i < p.size(); i++)
      Forward();

    executingPath = false;
    ss.newScheduler();

    int result = Engine.getJPF().store.put(this);

    return result == iStore.NEW;
  }  
  public boolean executePath(Path p, Object state) {
    // first_max_stack_reached we need to backtrack to the initial state
    int backtrack = p.upCount();
    for(int i = 0; i < backtrack; i++)
      Backtrack();

    // now we have to execute all the steps in the p
    executingPath = true;

    ss.sch = new PathScheduler(ss, (JVMPath)p);

    for(int i = 0; i < p.size(); i++)
      Forward();

    executingPath = false;
    ss.newScheduler();

    int result = Engine.getJPF().store.put(this);

    return result == iStore.NEW;
  }  
  /**
   * Moves one step forward.
   */
  public int Forward() {
    int sd = options.search_depth;

    // checks if the limited depth has been reached.
    if(sd != -1
    && stateStoringStack.size() >= sd) {
      if(!maxDepthReached) {
    maxDepthReached = true;
    Debug.println(Debug.WARNING, "Max search depth reached");
      }

      return TransitionResult.END;
    }

    JPF jpf = Engine.getJPF();
    Status status = jpf.status;

    if(status.maxStackDepth < path.size())
      status.maxStackDepth = path.size();

//#ifdef STACK_STATS

//#endif STACK_STATS
    

    // saves the current state.
    pushState();

    // generated next successor.
    if(!ss.nextSuccessor()) {
      // saves the backtrack information
      removeState();

      // if there is no successors we can be in an exit state,
      // in a deadlock, or there are not more executable threads.
      return TransitionResult.END;
    } else {
//#ifdef MARK_N_SWEEP

      // runs the garbage collector if necessary
      if (options.garbage_collection && ss.GCNeeded) {
    ss.ks.gc();
    ss.GCNeeded = false;
      }
      
//#endif MARK_N_SWEEP
      
      // moves the scheduler to the next position
      ss.sch.next();

      if(!executingPath && Engine.options.po_reduction) {
    int result = jpf.store.check(ss);

    // in stack check proviso
    if(ss.sch instanceof POScheduler) {
      if(result == iStore.ONSTACK)
        ((POScheduler)ss.sch).failedProviso();
    }
      }
      
      // saves the backtrack information
      pushSystem();

      // clears the scheduler for the new state
      ss.sch.initialize(ss);
      
      if(ss.ks.isIntermediate()) jpf.status.intermediateTransitions++;

      if(ss.violatedAssertion || ss.uncaughtException) {
    if(options.no_storing || executingPath || ss.ks.isIntermediate() || jpf.store.put(this) == iStore.NEW)
      return TransitionResult.NEW | TransitionResult.ERROR;
    else
      return TransitionResult.OLD | TransitionResult.ERROR;
      } else {
    if(options.no_storing || executingPath || ss.ks.isIntermediate() || jpf.store.put(this) == iStore.NEW) {
      return TransitionResult.NEW;
    }
    else
      return TransitionResult.OLD;
      }
    }
  }  
  public Reference getClassReference(String name) {
    if(ClassInfo.exists(name))
      return ss.ks.sa.get(name);

    return null;
  }  
  public String getErrorMessage() {
    if(ss.violatedAssertion) return "Assertion violated";
    if(ss.uncaughtException) return "Uncaught exception: " + ss.exceptionName;

    return "No error found";
  }  
  /**
   * Create a new error trace.
   */
  public ErrorTrailInterface getErrorTrail() {
    Vector v = new Vector();

    v.addElement("========================");
    v.addElement(" *** Path to error: ***");
    v.addElement("========================");
    
    int length = path.size();

    v.addElement("Steps to error: " + length);

    for(int index = 0; index < length; index++)
      try {
    v.addElement("Step #" + index + " " +
        ((TrailInfo)path.get(index)).toString());
      } catch(NullPointerException e) {
    v.addElement("Step #" + index);
      }

    ErrorTrail e = new ErrorTrail(v.size());

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

    return e;
  }  
  /**
   * Read the error trail and returns a path that can be simulated.
   */
  public Path getErrorTrail_from_file() {
    JVMPath path = null;
    String filename = classname + ".error.path";

    try {
      LineNumberReader in = new LineNumberReader(
      new FileReader(filename));

      StringTokenizer t;
      String ln = in.readLine();
      if(ln != null) {
    t = new StringTokenizer(ln, " :\t\r\n");

    // Size
    t.nextToken();
    int size = Integer.parseInt(t.nextToken());

    path = new JVMPath(size);

    for(int index = 0; index < size; index++) {
      ln = in.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());

      path.set(index, new JVMPathEntry(line, classname, thread, random));
    }
      }
      in.close();
    } catch (Exception e) {
      throw new JPFErrorException("error reading " + filename);
    }

    return path;
  }  
  public Path getErrorTrail_to_file() {
    int length = path.size();

    try {
      PrintWriter out = new PrintWriter(
      new OutputStreamWriter(
        new  FileOutputStream(classname + ".error.path")));

      out.println("Size:" + length);

      for(int i = 0; i < length; i++) {
    TrailInfo ti = (TrailInfo)path.get(i);


    out.println("Thread:" + ti.getThread() + "\t Line:" + ti.getStep(0).line +
        "\t Class:" + ti.getStep(0).classname + "\t Random:" + ti.getRandom());
      }

      out.close();
    } catch (IOException e) {
    }

    return getErrorTrail1();
  }  
  /**
   * Returns an error trail.
   */
  public Path getErrorTrail1() {
    int length = path.size();

    errorPath = new JVMPath(length);

    for(int i = 0; i < length; i++) {
      TrailInfo ti = (TrailInfo)path.get(i);
      errorPath.set(i, ti.getEntry());
    }

    return errorPath;
  }  
  public Path getPath(byte[] p) {
    return new JVMPath(p);
  }  
  public Reference getReference(String name) {
    // first of all I have to get to a class
    StringTokenizer st = new StringTokenizer(name,  ".");
    StringBuffer sb = new StringBuffer();
    Reference r = null;

    while(st.hasMoreTokens()) {
      sb.append(st.nextToken());
      if((r = getClassReference(sb.toString())) != null)
    break;
      sb.append('.');
    }

    if(r == null)
      throw new JPFErrorException("invalid argument: " + name);

    // now walk thought the fields
    while(st.hasMoreTokens()) {
      r = r.getObjectField(st.nextToken());
    }

    return r;
  }  
  /**
   * Gets the thread local system state.
   */
  public static SystemState getSS() {
//#ifdef BANDERA
    return xss;
//#else BANDERA

//#endif BANDERA
  }  
  public Object getState() {
    return ss.clone();
  }  
  /**
   * Gets the system state.
   */
  public iSystemState getSystemState() {
    return ss;
  }  
  /**
   * Initialize the virtual machine. Creates the main thread, passes
   * the arguments to the main function and store the initial state.
   *
   * @param arguments the argument strings
   */ 
  public void init(String[] arguments) {
    if(arguments.length == 0)
      throw new JPFErrorException("missing class name");

    classname = arguments[0];
    args = new String[arguments.length-1];
    System.arraycopy(arguments, 1, args, 0, args.length);
    stateStoringStack = new Stack();
    stateBacktrackStack = new Stack();
    backtrackStack = new Stack();
    setSS(ss = new SystemState(this));
    maxDepthReached = false;
    errorPath = null;
    posInErrorPath = 0;
    executingPath = false;
    path = new LinkedList();

    // load the class information for the main class
    ClassInfo ci = ClassInfo.getClassInfo(classname);

    //create static fields and monitor for the class
    //also initializes class??
    ss.ks.sa.newClass(ci);

    // create the thread for the main class
    try {
    ci.createMainThread(ss, args);
    } catch(RuntimeException e) {
      ss.ks.jvmError(e, ss.getRunningThread());
    }
    
    // initializes the classes loaded, including main class
    // for which there was already an attempt for initializatio
    // above, that was probably not required
    ss.ks.sa.initializeClasses();

    // this method is empty, to be used later I guess?
    Engine.getJPF().initialized();

//#ifdef BUCHI

    if(options.buchi == null)

//#endif BUCHI

      // store the initial state in the hashtable
      Engine.getJPF().store.initial(this);

//#ifdef BUCHI

    else
      initialState = true;

//#endif BUCHI
  }  
  public boolean isDeadlocked() {
    int length = ss.getThreadCount();
    boolean result = false;

    for(int i = 0; i < length; i++) {
      ThreadInfo th = (ThreadInfo)ss.getThreadInfo(i);
      if(th.isRunnable())
    return false;
      if(th.countStackFrames() != 0)
    result = true;
    }

    return result;
  }  
  public boolean isTerminated() {
    return ss.ks.isTerminated();
  }  
  /**
   * Returns the identifier of the next thread to be executed.
   */
  public int nextThreadToExecute() {
    if (posInErrorPath >= errorPath.size())
      return -1;
    
    JVMPathEntry e = errorPath.get(posInErrorPath);

    return e.thread;
  }  
//#ifdef HEURISTIC
//#ifdef HEURISTIC_DEBUG



//#endif HEURISTIC_DEBUG









































//#endif HEURISTIC

  /**
   * Restore the state and backtracking information.
   */
  public void popState() {
    int[] storing = (int[])stateStoringStack.pop();
    ss.ks.backtrackTo(new ArrayOffset(storing),
    stateBacktrackStack.pop());
  }  
  public void popSystem() {
    ss.backtrackTo(null, backtrackStack.pop());
    path.removeLast();
  }  
  /**
   * Returns the identified of the thread that just executed.
   */
  public int previousThreadToExecute() {
    if (posInErrorPath < 1)
      return -1;

    JVMPathEntry e = errorPath.get(posInErrorPath-1);

    return e.thread;
  }  
//#endif BANDERA

  /**
   * Prints the current stack trace.
   */
  public void printStackTrace() {
    ss.getRunningThread().printStackTrace();
  }  
  /**
   * Saves the state of the system.
   */
  public void pushState() {
    stateStoringStack.push(ss.ks.getStoringData());
    stateBacktrackStack.push(ss.ks.getBacktrackData());
  }  
  /**
   * Saves the backtracking information.
   */
  public void pushSystem() {
    backtrackStack.push(ss.getBacktrackData());
    path.addLast(ss.ti);
    ss.ti = null;
  }  
  /**
   * Reinitializes the virtual machine.
   */
  public void reinit() {
//#ifdef RACE

//#endif RACE
//#ifdef !NO_STATIC_SYMMETRY
    StaticMap.reset();
//#endif !NO_STATIC_SYMMETRY
//#ifdef !NO_DYNAMIC_SYMMETRY
    DynamicMap.reset();
//#endif !NO_DYNAMIC_SYMMETRY

    stateStoringStack = new Stack();
    stateBacktrackStack = new Stack();
    backtrackStack = new Stack();
    setSS(ss = new SystemState(this));
    maxDepthReached = false;
    posInErrorPath = 0;
    executingPath = false;
    path = new LinkedList();

    ClassInfo ci = ClassInfo.getClassInfo(classname);
    ss.ks.sa.newClass(ci);
    ci.createMainThread(ss, args);
    ss.ks.sa.initializeClasses();

//#ifdef BUCHI

    if(options.buchi == null)

//#endif BUCHI

      Engine.getJPF().store.initial(this);

//#ifdef BUCHI

    else
      initialState = true;

//#endif BUCHI
  }  
  public void removeState() {
    stateStoringStack.pop();
    stateBacktrackStack.pop();
  }  
//#endif BUCHI

//#ifdef DISTRIBUTED || PARALLEL






















































































//#endif DISTRIBUTED || PARALLEL

  /**
   * Sets the thread local system state.
   */
  private static void setSS(SystemState ss) {
//#ifdef BANDERA
    xss = ss;
//#else BANDERA

//#endif BANDERA
  }  
  /**
   * Restores the  machine to a state from the heuristic queue.
   */
  public void setState(Object state) {
    ss = (SystemState)((SystemState)state).clone();
    ss.vm = this;
    setSS(ss);
  }  
  /**
   * Prints and saves the error trace.
   */
  public void ShowErrorTrail() {
    ErrorTrailInterface et = getErrorTrail();

    et.print();

    try{
      et.print(new PrintStream(new FileOutputStream("error.trail")));
    } catch (IOException e) {
    }
  }  
//#ifdef BANDERA
  /**
   * Prints the content of an error trail.
   */
  public void ShowErrorTrail(Path path) {
    reinit();

    for(int i = 0; i < errorPath.size()-1; i++) {
      FilenameLinePair pair = ErrorForward();
      Debug.println(Debug.WARNING, pair.getFilename() + " " + pair.getLine());
    }
  }  
  public iScheduler xForward(iScheduler sch) {
    JPF jpf = Engine.getJPF();
    Status status = jpf.status;

    if(sch != null)
      ss.sch = (Scheduler)sch;
    else
      ss.sch.initialize(ss);

    if(!ss.nextSuccessor())
      return null;

//#ifdef MARK_N_SWEEP
    if (options.garbage_collection && ss.GCNeeded) {
      ss.ks.gc();
      ss.GCNeeded = false;
    }
//#endif MARK_N_SWEEP

    ss.sch.next();

    sch = (iScheduler)ss.sch.clone();

    ss.sch.initialize(ss);
      
    return sch;
  }  
}

---