---

StackFrame.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.PoolObject;
import java.io.*;
import java.util.*;
import java.util.Random;

public class StackFrame extends PoolObject implements Constants {
  static private Random random = new Random();
                // static random number generator

  Stack operands;       // operand stack of each method
  int[] locals;

  InstructionHandle pc;     // program counter
  ClassInfo ci;         // class and method called
  MethodInfo mi;
  ConstantPoolGen cpg;      // used to look up constants
  LocalVariableGen[] localInfo; // table that links name and types of
                // local variables
// ifdef MARK_N_SWEEP
  BitSet localrefs = new BitSet();
  BitSet operandrefs = new BitSet();
  // EXTRA
  private int upto = 0;
  // EXTRA
  public StackFrame(ClassInfo c, MethodInfo m, int[] ls, Stack os, InstructionHandle p) {
    ci = c;
    mi = m;
    locals = ls;
    operands = os;
    pc = p;
    cpg = mi.getConstantPool();
    localInfo = mi.getMethodGen().getLocalVariables();
  }  
//#endif MARK_N_SWEEP

  // creates a new stack frame
  public StackFrame(MethodInfo m, ClassInfo c) {
    mi = m;
    ci  = c;

    operands = new Stack();
    cpg = mi.getConstantPool();     // loads the constant pool
    localInfo = mi.getMethodGen().getLocalVariables();
                    // gets the information about the variables

    if (localInfo == null)
      Debug.println(Debug.WARNING, "No local Variable information: use javac -g");

    // creates space for local variables
    pc = mi.getFirstInstruction();

    int nlocals = mi.getMethodGen().getMaxLocals();
    if(pc == null) nlocals = mi.getArgumentSize();

    locals = new int[nlocals];
  }  
  // stack operations
  public void clearOperandStack() {
    operands.removeAllElements();
  }  
  // creates a clone of the stack frame
  public Object clone(){
    try{
      // first clone of the other information
      StackFrame sf = (StackFrame)super.clone();

      // creates a new operand stack
      sf.operands = (Stack)operands.clone();

      // creates a copy of the local variables
      int nlocals = locals.length;
      sf.locals = new int[nlocals];
      System.arraycopy(locals, 0, sf.locals, 0, nlocals);

      // clones the list of which local variables are references
// ifdef MARK_N_SWEEP
      sf.localrefs = (BitSet)localrefs.clone();
      sf.operandrefs = (BitSet)operandrefs.clone();
//#endif MARK_N_SWEEP

      // implicit: sf.pc = pc;
      // implicit: sf.ci = ci;
      // implicit: sf.mi = mi;
      // implicit: sf.cpg = cpg;
      // implicit: sf.localInfo = localInfo;

      // returns back the clone
      return sf;
    } catch(CloneNotSupportedException e){
      throw new InternalError(e.toString());
    }
  }  
  // functions to handle exceptions

  // creates an exception of the given class and throws it
  public InstructionHandle createAndThrowException(String classname,
      SystemState ss, KernelState ks, ThreadInfo th) {
    // lets check that the class is loaded or load it otherwise
    JPFVM jpfvm = JPFVM.getJPFVM();
    ClassInfo ci = jpfvm.getClass(classname);
    if (!ks.static_area.hasClass(classname)) {
      ks.static_area.addClass(ci);
      return ci.initialize(ss, ks, th);
    }

    // creates the new exception object
    int objref = ks.dynamic_area.newObject(ci, th);

    // puts the value on the stack
    push(objref);
// ifdef MARK_N_SWEEP
    setOperandRef();
//#endif MARK_N_SWEEP

// ifdef DEBUG

//#endif DEBUG

    // executes an implicit ATHROW instruction
    return new ATHROW().execute(ss, ks, th);
  }  
  // execute a random choice (actually execute all of them when verifying)
  public int doRandom(int max, Scheduler sch) {
    // different behavior depending if we are simulating or verifying
    if (((JPFOptions)Engine.options).verify){
      // gets the current random value
      int randomValue = sch.getCurrentRandom();

      // if this is the lat random value (max - 1) then we just
      // have clear the random flag so that next time we will
      // not execute the random anymore
      if ((randomValue+1) < max) {
// ifdef DEBUG

//#endif DEBUG
    TransitionResult.setRandom();
      } else {
// ifdef DEBUG

//#endif DEBUG
    TransitionResult.clearRandom();
      }
      return randomValue;
    } else {
      // code executed during simulation
      // since this is a random simulation just peek one at random
      // java.util.Random random = new java.util.Random();
      return Math.abs(random.nextInt() % max);
    }
  }  
  public void dup() {
// ifdef MARK_N_SWEEP
    boolean ref = isOperandRef();
    operands.push(operands.peek());
    if(ref) setOperandRef();
//#else MARK_N_SWEEP

//#endif MARK_N_SWEEP
  }  
  public void dup_x1() {
    // what it does on the stack is:
    // (top) A B ... => (top) B A B ...
    // often used to translate post increment/decremente operators
// ifdef MARK_N_SWEEP
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(b); if(bref) setOperandRef();
    push(a); if(aref) xSetOperandRef();
    push(b); if(bref) xSetOperandRef();
//#else MARK_N_SWEEP





//#endif MARK_N_SWEEP
  }  
  public void dup_x2() {
    // what it does on the stack is:
    // (top) A B C ... => (top) C A B C ...
    // often used to translate post increment/decremente operators
// ifdef MARK_N_SWEEP
    boolean cref = isOperandRef(); int c = xpop();
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(c); if(cref) setOperandRef();
    push(a); if(aref) xSetOperandRef();
    push(b); if(bref) xSetOperandRef();
    push(c); if(cref) xSetOperandRef();
//#else MARK_N_SWEEP







//#endif MARK_N_SWEEP
  }  
  public void dup2() {
// ifdef MARK_N_SWEEP
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(a); if(aref) xSetOperandRef();
    push(b); if(bref) xSetOperandRef();
    push(a); if(aref) setOperandRef();
    push(b); if(bref) setOperandRef();
//#else MARK_N_SWEEP

//#endif MARK_N_SWEEP
  }  
  public void dup2_x1() {
    // what it does on the stack is:
    // (top) A B C ... => (top) B C A B C ...
    // often used to translate post increment/decremente operators
// ifdef MARK_N_SWEEP
    boolean cref = isOperandRef(); int c = xpop();
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(b); if(bref) setOperandRef();
    push(c); if(cref) setOperandRef();
    push(a); if(aref) xSetOperandRef();
    push(b); if(bref) xSetOperandRef();
    push(c); if(cref) xSetOperandRef();
//#else MARK_N_SWEEP








//#endif MARK_N_SWEEP
  }  
  public void dup2_x2() {
    // what it does on the stack is:
    // (top) A B C D ... => (top) C D A B C D ...
    // often used to translate post increment/decremente operators
// ifdef MARK_N_SWEEP
    boolean dref = isOperandRef(); int d = xpop();
    boolean cref = isOperandRef(); int c = xpop();
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(c); if(cref) setOperandRef();
    push(d); if(dref) setOperandRef();
    push(a); if(aref) xSetOperandRef();
    push(b); if(bref) xSetOperandRef();
    push(c); if(cref) xSetOperandRef();
    push(d); if(dref) xSetOperandRef();
//#else MARK_N_SWEEP










//#endif MARK_N_SWEEP
  }  
  public boolean equals(Object object) {
    // casts to stack frame
    StackFrame sf = (StackFrame)object;

    // compares the program counter REFERENCES
    // the code is statically read into the vm so the same
    // chunk of code means the same reference
    if (pc != sf.pc) return false;
    if (!mi.getFullName().equals(sf.mi.getFullName())) return false;
    
// ifdef MARK_N_SWEEP
    if (!localrefs.equals(sf.localrefs)) return false;
    if (!operandrefs.equals(sf.operandrefs)) return false;
//#endif MARK_N_SWEEP

    // we are going to compare
    // the local variables and the operand stack
    int[] l = sf.locals;
    int nlocals = locals.length;

    if (nlocals != l.length) return false;
    for (int idx = 0; idx < nlocals; idx++)
      if(locals[idx] != l[idx]) return false;

    Stack o = sf.operands;
    int noperands = operands.size();

    if (noperands != o.size()) return false;
    for (int idx = 0; idx < noperands; idx++)
      if (!operands.get(idx).equals(o.get(idx)))
    return false;

    return true;
  }  
  // operations on local variables
  public int getCalleeThis(int locals) {
    return ((Integer)operands.get(operands.size() - locals)).intValue();
  }  
  public ClassInfo getClassInfo() {
    return ci;
  }  
  public ConstantPoolGen getConstantPool() {
    return cpg;
  }  
  // gets and sets some derived information
  public int getCurrentLine() {
    return mi.getLineNumbers().getSourceLine(pc.getPosition());
  }  
  public int getLocalVariable(int i) {
    return locals[i];
  }  
  // return the value of a variable given the name
  public long getLocalVariable(String name) {
    for(int idx = 0; idx < localInfo.length; idx++)
      if (name.equals(localInfo[idx].getName())) {
    switch(localInfo[idx].getType().getType()) {
      case T_BOOLEAN:
      case T_BYTE:
      case T_CHAR:
      case T_FLOAT:
      case T_INT:
      case T_REFERENCE:
      case T_ARRAY:
      case T_SHORT:
        return (long)getLocalVariable(localInfo[idx].getIndex());

      case T_DOUBLE:
      case T_LONG:
        return getLongLocalVariable(localInfo[idx].getIndex());
    }

    Debug.println(Debug.ERROR, "unknown local type - " + localInfo[idx].getType().getType());
    return -1;
      }

    // this should actually never happen
    Debug.println(Debug.ERROR, "unknown local variable - " + name);
    return -1;
  }  
  public int[] getLocalVariables() {
    return locals;
  }  
  public long getLongLocalVariable(int i) {
    return Types.intsToLong(locals[i], locals[i+1]);
  }  
  public MethodInfo getMethodInfo() {
    return mi;
  }  
  public String getMethodName() {
    return mi.getMethodName();
  }  
  public Stack getOperandStack() {
    return operands;
  }  
  public InstructionHandle getPC() {
    return pc;
  }  
  public int getThis() {
    if(locals.length == 0) return -1;

    return locals[0];
  }  
//#endif MARK_N_SWEEP

  // return the type of a variable
  public int getType(String name) {
    for(int idx = 0; idx < localInfo.length; idx++)
      if (name.equals(localInfo[idx].getName()))
    return localInfo[idx].getType().getType();

    // this should actually never happen
    Debug.println(Debug.ERROR, "local variable name mismatch");

    return Constants.T_VOID;
  }  
// ifdef MARK_N_SWEEP
  public boolean hasAnyRef() {
    for(int i = 0, l = operandrefs.length(); i < l; i++)
      if(operandrefs.get(i)) return true;
    for(int i = 0, l = localrefs.length(); i < l; i++)
      if(localrefs.get(i)) return true;

    return false;
  }  
  public void hash(HashData hd) {
    for(int i = 0, l = locals.length; i < l; i++)
      hd.add(locals[i]);

    for(int i = 0, l = operands.size(); i < l; i++)
      hd.add(((Integer)operands.get(i)).intValue());
  }  
  // computes an hash code for the hash table
  // the default hash code is different for each object
  // we need to redifine it to make the hash table work
  public int hashCode() {
    HashData hd = new HashData();

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

    for(int i = 0, l = operands.size(); i < l; i++)
      hd.add(((Integer)operands.get(i)).intValue());

    return hd.getValue();
  }  
  // increments a local variable
  public void incIntLocalVariable(int index, int number) {
    locals[index] += number;
  }  
  public boolean isOperandRef() {
    return operandrefs.get(operands.size()-1);
  }  
  public boolean isOperandRef(int idx) {
    return operandrefs.get(operands.size()-idx-1);
  }  
  public boolean isSafe() {
    return ci.isSafe(getCurrentLine());
  }  
  public void local2stack(int index) {
    push(locals[index]);
  }  
  public void local2stack2(int index) {
    push(locals[index]);
    push(locals[index+1]);
  }  
//#endif MARK_N_SWEEP

// ifdef REFERENCE_COUNT












//#endif REFERENCE_COUNT

  public void log(int id) {
    Debug.print(Debug.MESSAGE, "  SF#" + id + " S(");
    for(int i = 0; i < operands.size(); i++) {
      int j = ((Integer)operands.get(i)).intValue();
      Debug.print(Debug.MESSAGE, " ");
// ifdef MARK_N_SWEEP
      if(operandrefs.get(i)) Debug.print(Debug.MESSAGE, "#");
//#endif MARK_N_SWEEP
      Debug.print(Debug.MESSAGE, j + "");
    }
    Debug.print(Debug.MESSAGE, " ) L(");
    for(int i = 0; i < locals.length; i++) {
      int j = locals[i];
      Debug.print(Debug.MESSAGE, " ");
// ifdef MARK_N_SWEEP
      if(localrefs.get(i)) Debug.print(Debug.MESSAGE, "#");
//#endif MARK_N_SWEEP
      Debug.print(Debug.MESSAGE, j + "");
    }
    Debug.println(Debug.MESSAGE, " )");
  }  
// ifdef MARK_N_SWEEP
  public void mark(DynamicArea da) {
    for(int i = 0, l = operands.size(); i < l; i++)
      if(operandrefs.get(i))
    da.mark(((Integer)operands.get(i)).intValue());

    for(int i = 0, l = locals.length; i < l; i++)
      if(localrefs.get(i))
    da.mark(locals[i]);
  }  
  public int pcs() { return upto + (pc == null ? 0 : pc.getPosition()); }  
  int peek() {
    return ((Integer)operands.peek()).intValue();
  }  
  int peek(int n) {
    return ((Integer)operands.get(operands.size() - 1 - n)).intValue();
  }  
  long peek2() {
    int lo = ((Integer)operands.peek()).intValue();
    int hi = ((Integer)operands.get(operands.size() - 2)).intValue();

    return Types.intsToLong(lo, hi);
  }  
  long peek2(int n) {
    int lo = ((Integer)operands.get(operands.size() - 1 - n)).intValue();
    int hi = ((Integer)operands.get(operands.size() - 2 - n)).intValue();

    return Types.intsToLong(lo, hi);
  }  
  int pop() {
// ifdef MARK_N_SWEEP
    if(isOperandRef()) {
      VirtualMachine.activateGC();
      operandrefs.clear(operands.size()-1);
    }
//#endif MARK_N_SWEEP
// ifdef REFERENCE_COUNT





//#endif REFERENCE_COUNT
    return ((Integer)operands.pop()).intValue();
  }  
  void pop(int n) {
    for(int i = 0; i < n; i++) {
// ifdef MARK_N_SWEEP
      if(isOperandRef()) {
    VirtualMachine.activateGC();
    operandrefs.clear(operands.size()-1);
      }
//#endif MARK_N_SWEEP
// ifdef REFERENCE_COUNT





//#endif REFERENCE_COUNT
      operands.pop();
    }
  }  
  long pop2() {
    int lo = ((Integer)operands.pop()).intValue();
    int hi = ((Integer)operands.pop()).intValue();

    return Types.intsToLong(lo, hi);
  }  
// ifdef DISTRIBUTED



//#endif DISTRIBUTED

  public void printStackContent() {
    Debug.print(Debug.ERROR, "\tat ");
    Debug.print(Debug.ERROR, mi.getFullName());
    if(pc != null)
      Debug.println(Debug.ERROR, ":" + pc.getPosition());
    else
      Debug.println(Debug.ERROR);
    Debug.println(Debug.ERROR, "\t  Operand stack is:");
    for(int i = 0, l = operands.size(); i < l; i++) {
      Debug.print(Debug.ERROR, "\t    ");
// ifdef MARK_N_SWEEP
      if(operandrefs.get(i))
    Debug.print(Debug.ERROR, "#");
//#endif MARK_N_SWEEP
      Debug.println(Debug.ERROR, operands.get(i));
    }
    Debug.println(Debug.ERROR, "\t  Local variables are:");
    for(int i = 0, l = locals.length; i < l; i++) {
      Debug.print(Debug.ERROR, "\t    ");
// ifdef MARK_N_SWEEP
      if(localrefs.get(i))
    Debug.print(Debug.ERROR, "#");
//#endif MARK_N_SWEEP
      Debug.println(Debug.ERROR, ""+locals[i]);
    }
  }  
  public void printStackTrace() {
    Debug.print(Debug.ERROR, "\tat ");
    Debug.print(Debug.ERROR, ci.getClassName());
    Debug.print(Debug.ERROR, ".");
    Debug.print(Debug.ERROR, mi.getMethodName());
    if(pc != null) {
      Debug.print(Debug.ERROR, "(");
      Debug.print(Debug.ERROR, Source.getSourceName(ci.getClassName()));
      Debug.print(Debug.ERROR, ":");
      Debug.println(Debug.ERROR, getCurrentLine() + ")");
    } else
      Debug.println(Debug.ERROR, "(Native Method)");
  }  
  void push(int v) {
    operands.push(new Integer(v));
  }  
  void push2(long v) {
    operands.push(new Integer(Types.hiLong(v)));
    operands.push(new Integer(Types.loLong(v)));
  }  
  public void setLocalVariable(int index, int v) {
// ifdef MARK_N_SWEEP
    if(localrefs.get(index)
    && locals[index] != -1
    && locals[index] != v)
      VirtualMachine.activateGC();
//#endif MARK_N_SWEEP
// ifdef REFERENCE_COUNT





//#endif REFERENCE_COUNT
    locals[index] = v;
  }  
//#endif MARK_N_SWEEP

// ifdef MARK_N_SWEEP
  public void setLocalVariableRef(int idx) {
// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT
    localrefs.set(idx);
  }  
  public void setLongLocalVariable(int index, long v) {
    locals[index] = Types.loLong(v);
    locals[index+1] = Types.hiLong(v);
  }  
  public void setOperandRef() {
    operandrefs.set(operands.size()-1);
// ifdef REFERENCE_COUNT


//#endif REFERENCE_COUNT
  }  
  public void setPC(InstructionHandle newpc) {
    pc = newpc;
  }  
  public void setUpto(int u) { upto = u; }  
  public void stack2local(int index) {
// ifdef MARK_N_SWEEP
    boolean aref = isOperandRef(); int a = peek();
//#endif MARK_N_SWEEP

// ifdef MARK_N_SWEEP
    if(localrefs.get(index)
    && locals[index] != -1
    && (locals[index] != a || !aref)) {
      VirtualMachine.activateGC();
    }
//#endif MARK_N_SWEEP

// ifdef REFERENCE_COUNT








//#endif REFERENCE_COUNT

// ifdef MARK_N_SWEEP
    if(aref)
      localrefs.set(index);
    else
      localrefs.clear(index);
//#endif MARK_N_SWEEP

    locals[index] = pop();
  }  
  public void stack2local2(int index) {
// ifdef MARK_N_SWEEP
    boolean aref = isOperandRef(); int a = peek();
    boolean bref = isOperandRef(); int b = peek();
//#endif MARK_N_SWEEP

// ifdef MARK_N_SWEEP
    if(localrefs.get(index)
    && locals[index] != -1
    && (locals[index] != a || !aref)) {
      VirtualMachine.activateGC();
    }
    if(localrefs.get(index+1)
    && locals[index+1] != -1
    && (locals[index+1] != b || !bref)) {
      VirtualMachine.activateGC();
    }
//#endif MARK_N_SWEEP

// ifdef REFERENCE_COUNT

















//#endif REFERENCE_COUNT

// ifdef MARK_N_SWEEP
    if(aref)
      localrefs.set(index);
    else
      localrefs.clear(index);

    if(bref)
      localrefs.set(index+1);
    else
      localrefs.clear(index+1);
//#endif MARK_N_SWEEP

    locals[index] = pop();
    locals[index+1] = pop();
  }  
  public void swap() {
    // what it does on the stack is:
    // (top) A B ... => (top) B A ...
// ifdef MARK_N_SWEEP
    boolean bref = isOperandRef(); int b = xpop();
    boolean aref = isOperandRef(); int a = xpop();
    push(b); if(bref) xSetOperandRef();
    push(a); if(aref) xSetOperandRef();
//#else MARK_N_SWEEP




//#endif MARK_N_SWEEP
  }  
  int xpop() {
// ifdef MARK_N_SWEEP
    operandrefs.clear(operands.size()-1);
//#endif MARK_N_SWEEP
    return ((Integer)operands.pop()).intValue();
  }  
  public void xSetLocalVariableRef(int idx) {
    localrefs.set(idx);
  }  
  public void xSetOperandRef() {
    operandrefs.set(operands.size()-1);
  }  
}

---