---

MethodInfo.java

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

import de.fub.bytecode.classfile.Code;
import de.fub.bytecode.classfile.CodeException;
import de.fub.bytecode.classfile.ConstantPool;
import de.fub.bytecode.classfile.ExceptionTable;
import de.fub.bytecode.classfile.LineNumberTable;
import de.fub.bytecode.classfile.LocalVariable;
import de.fub.bytecode.classfile.LocalVariableTable;
import de.fub.bytecode.classfile.Method;
import de.fub.bytecode.Constants;
import de.fub.bytecode.generic.InstructionHandle;
import de.fub.bytecode.generic.InstructionList;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.util.Debug;

/**
 * Represents the information associated with a method.
 */
public class MethodInfo {
  /**
   * Name of the method.
   */
  private String name;

  /**
   * Signature of the method.
   */
  private String signature;

  /**
   * Class the method belongs to.
   */
  private ClassInfo ci;

  /**
   * Instructions associated with the method.
   */
  private Instruction[] code;
  
  /**
   * Exception handlers.
   */
  private ExceptionHandler[] exceptions;

  /**
   * Table used for line numbers.
   */
  private int[] lineNumbers;

  /**
   * Local variables names.
   */
  private String[] localVariableNames;

  /**
   * Local variables types.
   */
  private String[] localVariableTypes;

  /**
   * Static method.
   */
  private boolean isStatic;

  /**
   * Synchronized method.
   */
  private boolean isSynchronized;

  /**
   * Native method.
   */
  private boolean isNative;

  /**
   * Maximum number of local variables.
   */
  private int maxLocals;

  /**
   * Maximum number of elements on the stack.
   */
  private int maxStack;

  /**
   * Used to warn about local variable information.
   */
  private static boolean warnedLocalInfo = false;

  /**
   * Creates a new method info.
   */
  public MethodInfo(Method m, ClassInfo c) {
    name = m.getName();
    signature = m.getSignature();
    ci = c;
    code = loadCode(m);
    exceptions = loadExceptions(m);
    lineNumbers = loadLineNumbers(m);
    localVariableNames = loadLocalVariableNames(m);
    localVariableTypes = loadLocalVariableTypes(m);
    isStatic = m.isStatic();
    isSynchronized = m.isSynchronized();
    isNative = m.isNative();
    maxLocals = getMaxLocals(m);
    maxStack = getMaxStack(m);

  }  
  public boolean canEnter(ThreadInfo th) {
    if(isSynchronized)
      if(isStatic) 
    return th.list.ks.sa.get(ci.getName()).canLock(th);
      else
    return th.list.ks.da.get(th.getCalleeThis(this)).canLock(th);

    return true;
  }  
  public void enter(ThreadInfo th) {
    if(isSynchronized)
      if(isStatic)
    th.list.ks.sa.get(ci.getName()).lock(th);
      else
    th.list.ks.da.get(th.getThis()).lock(th);
  }  
  /**
   * Returns the size of the arguments.
   */
  public int getArgumentsSize() {
    if(isStatic) 
      return Types.getArgumentsSize(signature);
    else
      return Types.getArgumentsSize(signature) + 1;
  }  
  /**
   * Returns the class the method belongs to.
   */
  public ClassInfo getClassInfo() {
    return ci;
  }  
  /**
   * Return the complete name of the method, including the class name.
   */
  public String getCompleteName() {
    return ci.getName() + "." + name + signature;
  }  
  public ExceptionHandler[] getExceptions() {
    return exceptions;
  }  
  /**
   * Returns the full name of the method, name and signature.
   */
  public String getFullName() {
    return name + signature;
  }  
  /**
   * Returns a specific instruction.
   */
  public Instruction getInstruction(int i) {
    if(code == null) return null;

    if(i < 0 || i >= code.length) return null;

    return code[i];
  }  
  /**
   * Returns the instruction at a certain position.
   */
  public Instruction getInstructionAt(int position) {
    if(code == null) return null;

    for(int i = 0, l = code.length; i < l; i++)
      if(code[i] != null && code[i].getPosition() == position)
    return code[i];

    throw new InternalErrorException("instruction not found");
  }  
  /**
   * Returns the instructions of the method.
   */
  public Instruction[] getInstructions() {
    return code;
  }  
  /**
   * Returns the line number for a given position.
   */
  public int getLineNumber(Instruction pc) {
    if(lineNumbers == null)
      return pc.getPosition();

    return lineNumbers[pc.getOffset()];
  }  
  /**
   * Returns a table to translate positions into line numbers.
   */
  public int[] getLineNumbers() {
    return lineNumbers;
  }  
  public String[] getLocalVariableNames() {
    return localVariableNames;
  }  
  public String[] getLocalVariableTypes() {
    return localVariableTypes;
  }  
  public int getMaxLocals() {
    return maxLocals;
  }  
  public static int getMaxLocals(Method m) {
    Code c = m.getCode();

    if(c == null) return 0;

    return c.getMaxLocals();
  }  
  public int getMaxStack() {
    return maxStack;
  }  
  public static int getMaxStack(Method m) {
    Code c = m.getCode();

    if(c == null) return 0;

    return c.getMaxStack();
  }  
  /**
   * Returns the name of the method.
   */
  public String getName() {
    return name;
  }  
  /**
   * Returns the signature of the method.
   */
  public String getSignature() {
    return signature;
  }  
  /**
   * Returns true if the field is native.
   */
  public boolean isNative() {
    return isNative;
  }  
  /**
   * Returns true if the field is static.
   */
  public boolean isStatic() {
    return isStatic;
  }  
  /**
   * Returns true if the field is synchronized.
   */
  public boolean isSynchronized() {
    return isSynchronized;
  }  
  /**
   * Returns true if the method is a system method.
   */
  public boolean isSystemMethod() {
    if(name.equals("<clinit>") && signature.equals("()V")) {
      return true;
    }

    /************************************************************\
    if(VirtualMachine.options.atomic_init && name.equals("<init>")) {
      return true;
    }
    \************************************************************/

    if(ci.isSystemClass())
      return true;

    return false;
  }  
  public void leave(ThreadInfo th) {
    if(isSynchronized)
      if(isStatic)
    th.list.ks.sa.get(ci.getName()).unlock(th);
      else
    th.list.ks.da.get(th.getThis()).unlock(th);
  }  
  /**
   * Loads the code of the method.
   */
  private Instruction[] loadCode(Method m) {
    Code c = m.getCode();

    if(c == null) return null;

    InstructionList il = new InstructionList(c.getCode());

    InstructionHandle[] hs = il.getInstructionHandles();
    int length = hs.length;

    Instruction[] is = new Instruction[length];

    for(int i = 0; i < length; i++) {
      is[i] = Instruction.create(hs[i], i, this, m.getConstantPool());
//#ifdef COVERAGE




//#endif COVERAGE
    }
    return is;
  }  
  /**
   * Returns the exceptions of the method.
   */
  private ExceptionHandler[] loadExceptions(Method m) {
    Code c = m.getCode();
    if(c == null) return null;

    CodeException[] ce = c.getExceptionTable();
    if(ce.length == 0) return null;

    int length = ce.length;
    ExceptionHandler[] eh = new ExceptionHandler[length];

    ConstantPool cp = m.getConstantPool();

    for(int i = 0; i < length; i++) {
      int ct = ce[i].getCatchType();
      eh[i] = new ExceptionHandler(
      (ct == 0 ?
       null :
       cp.getConstantString(ct, Constants.CONSTANT_Class).replace('/', '.')
      ),
      ce[i].getStartPC(),
      ce[i].getEndPC(),
      ce[i].getHandlerPC());
    }

    return eh;
  }  
  /**
   * Loads the line numbers for the method.
   */
  private int[] loadLineNumbers(Method m) {
    Code c = m.getCode();

    if(c == null) return null;

    LineNumberTable lnt = c.getLineNumberTable();

    int length = code.length;
    int[] ln = new int[length];

    if(lnt == null)
      // no line information
      return null;
    else
      for(int i = 0; i < length; i++)
    ln[i] = lnt.getSourceLine(code[i].getPosition());

    return ln;
  }  
  /**
   * Loads the names of the local variables.
   */
  private String[] loadLocalVariableNames(Method m) {
    Code c = m.getCode();
    
    if(c == null) return null;

    LocalVariableTable lvt = c.getLocalVariableTable();

    if(lvt == null) {
      if(!warnedLocalInfo && !ci.isSystemClass()) {
    Debug.println(Debug.WARNING);
    Debug.println(Debug.WARNING, "No local variable information available");
    Debug.println(Debug.WARNING, "for " + getCompleteName());
    Debug.println(Debug.WARNING, "Recompile with -g to include this information");
    Debug.println(Debug.WARNING);
    warnedLocalInfo = true;
      }
      return null;
    }

    LocalVariable[] lv = lvt.getLocalVariableTable();

    int length = lv.length;
    String[] lvn = new String[length];

    for(int i = 0; i < length; i++)
      lvn[i] = lv[i].getName();

    return lvn;
  }  
  /**
   * Loads the types of the local variables.
   */
  private String[] loadLocalVariableTypes(Method m) {
    Code c = m.getCode();
    
    if(c == null) return null;

    LocalVariableTable lvt = c.getLocalVariableTable();

    if(lvt == null) {
      if(!warnedLocalInfo && !ci.isSystemClass()) {
    Debug.println(Debug.WARNING, "No local variable information available");
    Debug.println(Debug.WARNING, "for " + getCompleteName());
    Debug.println(Debug.WARNING, "Recompile with -g to include this information");
    Debug.println(Debug.WARNING);
    warnedLocalInfo = true;
      }
      return null;
    }

    LocalVariable[] lv = lvt.getLocalVariableTable();
    int length = lv.length;
    String[] lvn = new String[length];

    for(int i = 0; i < length; i++)
      lvn[i] = lv[i].getSignature();

    return lvn;
  }  
}

---