---

ClassInfo.java

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

import de.fub.bytecode.Repository;
import de.fub.bytecode.classfile.Field;
import de.fub.bytecode.classfile.JavaClass;
import de.fub.bytecode.classfile.Method;
import gov.nasa.arc.ase.jpf.Engine;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import gov.nasa.arc.ase.jpf.JPFErrorException;
import gov.nasa.arc.ase.jpf.SafeBlocks;
import gov.nasa.arc.ase.jpf.jvm.bytecode.Instruction;
import gov.nasa.arc.ase.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.util.Debug;
import java.io.BufferedReader;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileReader;
import java.util.Hashtable;
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT
import gov.nasa.arc.ase.util.BSet;
import gov.nasa.arc.ase.util.ArrayBSet;
//#endif MARK_N_SWEEP || REFERENCE_COUNT
//#ifdef RACE

//#endif RACE

public class ClassInfo {
  /**
   * Map of the loaded classes.
   */
  private static Hashtable loadedClasses = new Hashtable();

  /**
   * Map of the loaded safe blocks.
   */
  private static Hashtable safeBlocksPool = new Hashtable();

  /**
   * Name of the class.
   */
  private String name;

  /**
   * List of static methods.
   */
  private MethodInfo[] staticMethods;

  /**
   * List of dynamic methods.
   */
  private MethodInfo[] dynamicMethods;

  /**
   * List of static fields.
   */
  private FieldInfo[] staticFields;

  /**
   * List of dynamic fields.
   */
  private FieldInfo[] dynamicFields;

  /**
   * Information about safe blocks in the code.
   */
  private SafeBlocks safeBlocks;

  /**
   * Reference to the super class.
   */
  private ClassInfo superClass;

  /**
   * Interfaces implemented by the class.
   */
  private String[] interfaces;

  /**
   * Name of the package.
   */
  private String packageName;

  /**
   * Name of the file which contains the source of this class.
   */
  private String sourceFileName;

  /**
   * Reflection object for this class.
   */
  private Reflection reflection;

  /**
   * Source file associated with the class.
   */
  private Source source;

//#ifdef MARK_N_SWEEP || REFERENCE_COUNT

  /**
   * Which fields are references.
   */
  private BSet dRefs;

  /**
   * Which static fields are references.
   */
  private BSet sRefs;

//#endif MARK_N_SWEEP || REFERENCE_COUNT
//#endif MARK_N_SWEEP || REFERENCE_COUNT

  /**
   * Creates a new class from the JavaClass information.
   */
  private ClassInfo(JavaClass jc) {
    name = jc.getClassName();

    loadedClasses.put(name, this);

    superClass = loadSuperClass(jc);
    staticMethods = loadStaticMethods(jc);
    dynamicMethods = loadDynamicMethods(jc);
    staticFields = loadStaticFields(jc);
    dynamicFields = loadDynamicFields(jc);
    interfaces = loadInterfaces(jc);
    packageName = jc.getPackageName();
    sourceFileName = jc.getSourceFileName();

    safeBlocks = loadSafeBlocks();
    reflection = loadReflection();
    reflection.setClassInfo(this);
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT
    dRefs = loadRefs(dynamicFields);
    sRefs = loadRefs(staticFields);
//#endif MARK_N_SWEEP || REFERENCE_COUNT

    source = null;
  }  
  /**
   * Creates the fields for a class.
   */
  public Fields createClassFields() {
    FieldInfo[] fs = staticFields;
    int size = fs.length;
    int length = 0;
    for(int i = 0; i < size; i++)
      if(fs[i] != null)
    length++;

    Fields f = new Fields(getType(), this, size, length, true
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT
    , sRefs
//#endif MARK_N_SWEEP || REFERENCE_COUNT
    );
    for(int i = 0; i < length; ) {
      String t = fs[i].getType();
      switch(Types.getBaseType(t)) {
    case Types.T_BYTE:
    case Types.T_CHAR:
    case Types.T_FLOAT:
    case Types.T_INT:
    case Types.T_SHORT:
    case Types.T_BOOLEAN:
      f.setField(i, 0);
      break;

    case Types.T_DOUBLE:
    case Types.T_LONG:
      f.setLongField(i, 0);
      break;

    case Types.T_REFERENCE:
    case Types.T_ARRAY:
      f.setField(i, -1);
      break;

    default:
      throw new InternalErrorException("invalid type");
      }
      i += Types.getTypeSize(t);
    }

    return f;
  }  
  /**
   * Creates the environment to execute the main method.
   */
  public ThreadInfo createMainThread(SystemState ss, String[] args) {
    int tObjref = ss.ks.da.newObject(
    ClassInfo.getClassInfo("java/lang/Thread"),
    null);
    ThreadInfo th = ss.ks.newThread(tObjref);

    MethodInfo mi = getStaticMethod("main([Ljava/lang/String;)V");

    if(mi == null)
      throw new JPFErrorException("main method not defined in " + name);

    th.newFrame(mi);

    int argsObjref = ss.ks.da.newArray(
    "Ljava/lang/String;",
    args.length,
    null);
    ElementInfo argsElement = ss.ks.da.get(argsObjref);

    for(int i = 0; i < args.length; i++) {
      int stringObjref = ss.ks.da.newString(args[i], null);
      argsElement.setField(i, stringObjref);
    }

    th.setLocalVariable(0, argsObjref, true);

    th.setStatus(ThreadInfo.RUNNING);

//#ifdef RACE


//#endif RACE

    return th;
  }  
  /**
   * Creates the fields for an object.
   */
  public Fields createObjectFields() {
    FieldInfo[] fs = dynamicFields;
    int size = fs.length;
    int length = 0;
    for(int i = 0; i < size; i++)
      if(fs[i] != null)
    length++;

    Fields f = new Fields(getType(), this, size, length, false
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT
    , dRefs
//#endif MARK_N_SWEEP || REFERENCE_COUNT
    );
    for(int i = 0; i < length; i++) {
      if(fs[i] != null) {
    switch(Types.getBaseType(fs[i].getType())) {
      case Types.T_BYTE:
      case Types.T_CHAR:
      case Types.T_FLOAT:
      case Types.T_INT:
      case Types.T_SHORT:
      case Types.T_BOOLEAN:
        f.setField(i, 0);
        break;

      case Types.T_DOUBLE:
      case Types.T_LONG:
        f.setLongField(i, 0);
        break;

      case Types.T_REFERENCE:
      case Types.T_ARRAY:
        f.setField(i, -1);
        break;

      default:
        throw new InternalErrorException("invalid type");
    }
      }
    }

    return f;
  }  
  /**
   * Returns the index for a dynamic field.
   */
  public int dynamicFieldIndex(String fname) {
    int length = dynamicFields.length;

    for(int i = 0; i < length; i++)
      if(dynamicFields[i] != null && dynamicFields[i].getName().equals(fname))
    return i;

    throw new InternalErrorException("class " + getName() + "does not have field `" + fname + "'");
  }  
  /**
   * Executes a method.
   */
  public Instruction executeMethod(ThreadInfo th, String mname) {
    MethodInfo mi = getDynamicMethod(mname);

    Reflection r = reflection.instantiate(th.getCalleeThis(mi));
    th.createMethodStackFrame(mi);

    return r.executeMethod(th, mi);
  }  
  /**
   * Executes a static method.
   */
  public Instruction executeStaticMethod(ThreadInfo th, String mname) {
    MethodInfo mi = getStaticMethod(mname);

    Reflection r = reflection.instantiate();
    th.createMethodStackFrame(mi);

    return r.executeStaticMethod(th, mi);
  }  
  public static boolean exists(String cname) {
    return Repository.lookupClass(cname) != null;
  }  
  /**
   * Loads a class.
   */
  public static synchronized ClassInfo getClassInfo(String cname) {
    if(cname == null) return null;

    cname = cname.replace('/', '.');
    
    ClassInfo ci = (ClassInfo)loadedClasses.get(cname);

    if(ci == null) {
      JavaClass jc = Repository.lookupClass(cname);

      if(jc == null)
    throw new JPFErrorException("could not load class " + cname);

      Repository.clearCache();

      ci = new ClassInfo(jc);
    }

    return ci;
  }  
  /**
   * Returns the information about a dynamic field.
   */
  public FieldInfo getDynamicField(int index) {
    return dynamicFields[index];
  }  
  /**
   * Returns the name of a dynamic field.
   */
  public String getDynamicFieldName(int index) {
    return dynamicFields[index].getName();
  }  
  /**
   * Returns the method info a given dynamic method.
   */
  public MethodInfo getDynamicMethod(String mname) {
    for(int i = 0, l = dynamicMethods.length; i < l; i++)
      if(dynamicMethods[i].getFullName().equals(mname))
    return dynamicMethods[i];

    if(superClass != null)
      return superClass.getDynamicMethod(mname);

    return null;
  }  
  /**
   * Returns the name of the class.
   */
  public String getName() {
    return name;
  }  
  /**
   * Returns the reflection object associated with the class.
   */
  public Reflection getReflection() {
    return reflection;
  }  
  public Source getSource() {
    if(source == null)
      source = loadSource();

    return source;
  }  
  public String getSourceFileName() {
    return sourceFileName;
  }  
  /**
   * Returns the information about a static field.
   */
  public FieldInfo getStaticField(int index) {
    return staticFields[index];
  }  
  /**
   * Returns the name of a static field.
   */
  public String getStaticFieldName(int index) {
    return staticFields[index].getName();
  }  
  /**
   * Returns the method info for a given static method.
   */
  public MethodInfo getStaticMethod(String mname) {
    for(int i = 0, l = staticMethods.length; i < l; i++)
      if(staticMethods[i].getFullName().equals(mname))
    return staticMethods[i];

    // class init is never inherited from super class
    if(mname.equals("<clinit>()V"))
      return null;

    if(superClass != null)
      return superClass.getStaticMethod(mname);

    return null;
  }  
  /**
   * Return the super class.
   */
  public ClassInfo getSuperClass() {
    return superClass;
  }  
  /**
   * Returns the type of a class.
   */
  public String getType() {
    return "L" + name.replace('.', '/') + ";";
  }  
  /**
   * Returns true if this class is an instance of the given class.
   */
  public boolean instanceOf(ClassInfo ci) {
    if(this == ci) return true;

    if(superClass != null)
      return superClass.instanceOf(ci);

    return false;
  }  
  /**
   * Returns true if the given class is an instance of the class
   * or interface specified.
   */
  public boolean instanceOf(String cname) {
    cname = cname.replace('/', '.');

    if(name.equals(cname)) return true;

    for(int i = 0, l = interfaces.length; i < l; i++)
      if(interfaces[i].equals(cname))
    return true;

    if(superClass != null)
      return superClass.instanceOf(cname);

    return false;
  }  
  /**
   * Checks if a method call is deterministic.
   */
  public boolean isMethodDeterministic(ThreadInfo th, String mname) {
    MethodInfo mi = getDynamicMethod(mname);

    Reflection r = reflection.instantiate(th.getCalleeThis(mi));

    return r.isMethodDeterministic(th, mi);
  }  
  /**
   * Checks if a method is executable.
   */
  public boolean isMethodExecutable(ThreadInfo th, String mname) {
    MethodInfo mi = getDynamicMethod(mname);

    Reflection r = reflection.instantiate(th.getCalleeThis(mi));

    return r.isMethodExecutable(th, mi);
  }  
  /**
   * Returns true if a line is defined as safe.
   */
  public boolean isSafe(int line) {
    if (safeBlocks == null)
      return false;
    else
      return safeBlocks.isSafe(line);
  }  
  /**
   * Checks if a static method call is deterministic.
   */
  public boolean isStaticMethodDeterministic(ThreadInfo th, String mname) {
    MethodInfo mi = getStaticMethod(mname);

    Reflection r = reflection.instantiate();

    return r.isStaticMethodDeterministic(th, mi);
  }  
  /**
   * Checks if a static method is executable.
   */
  public boolean isStaticMethodExecutable(ThreadInfo th, String mname) {
    MethodInfo mi = getStaticMethod(mname);

    Reflection r = reflection.instantiate();

    return r.isStaticMethodExecutable(th, mi);
  }  
  /**
   * Returns true if the class is a system class.
   */
  public boolean isSystemClass() {
    return name.startsWith("java.lang.") || name.startsWith("java.util.");
  }  
  /**
   * Loads the dynamic fields of a class.
   */
  private FieldInfo[] loadDynamicFields(JavaClass jc) {
    Field[] fields = jc.getFields();

    int counter = 0;

    for(int i = 0, l = fields.length; i < l; i++)
      if(!fields[i].isStatic())
    counter += Types.getTypeSize(fields[i].getSignature().toString());

    if(superClass != null)
      counter += superClass.dynamicFields.length;

    FieldInfo[] dFields = new FieldInfo[counter];

    if(superClass != null) {
      counter = superClass.dynamicFields.length;
      System.arraycopy(superClass.dynamicFields, 0, dFields, 0, counter);
    } else
      counter = 0;

    for(int i = 0, l = fields.length; i < l; i++)
      if(!fields[i].isStatic()) {
    dFields[counter] = new FieldInfo(fields[i], this);
    counter += Types.getTypeSize(fields[i].getSignature().toString());
      }

    return dFields;
  }  
  /**
   * Loads the dynamic methods of a class.
   */
  private MethodInfo[] loadDynamicMethods(JavaClass jc) {
    Method[] methods = jc.getMethods();

    int counter = 0;
    for(int i = 0, l = methods.length; i < l; i++)
      if(!methods[i].isStatic())
    counter++;

    MethodInfo[] dMethods = new MethodInfo[counter];
    
    counter = 0;
    for(int i = 0, l = methods.length; i < l; i++)
      if(!methods[i].isStatic())
    dMethods[counter++] = new MethodInfo(methods[i], this);

    return dMethods;
  }  
  /**
   * Loads the interfaces of a class.
   */
  private static String[] loadInterfaces(JavaClass jc) {
    int[] intInterfaces = jc.getInterfaces();

    String[] stringInterfaces = new String[intInterfaces.length];

    for(int i = 0, l = intInterfaces.length; i < l; i++)
      stringInterfaces[i] =
    jc.getConstantPool().getConstant(
        intInterfaces[i]
                    ).toString().replace('/', '.');

    return stringInterfaces;
  }  
  /**
   * Loads the reflection class.
   */
  private Reflection loadReflection() {
    return Reflection.load(name);
  }  
//#ifdef MARK_N_SWEEP || REFERENCE_COUNT

  private static BSet loadRefs(FieldInfo[] f) {
    int l = f.length;
    boolean[] refs = new boolean[l];

    for(int i = 0; i < l; i++)
      refs[i] = f[i] != null && Types.isReference(f[i].getType());

    return new ArrayBSet(refs);
  }  
  /**
   * Loads the safe blocks.
   */
  private SafeBlocks loadSafeBlocks() {
    if(!Engine.options.po_reduction) return null;

    String fname = packageName.replace('.', File.separatorChar) +
    File.separator + sourceFileName.substring(0, sourceFileName.length() - 5);

    for(int i = 0, l = ClassPath.length(); i < l; i++) {
      String filename = ClassPath.get(i) + File.separator + fname + ".safe";
      SafeBlocks s = loadSafeBlocks(filename);

      if(s != null) return s;
    }

    return null;
  }  
  private SafeBlocks loadSafeBlocks(String fname) {
    SafeBlocks s = (SafeBlocks)safeBlocksPool.get(fname);

    if(s == null) {
      try {
    BufferedReader in = new BufferedReader(new FileReader(fname));
    Debug.println(Debug.WARNING, "Loading " + fname);
    safeBlocksPool.put(fname, s = new SafeBlocks(in));
      } catch (FileNotFoundException e) {
      }
    }

    return s;
  }  
  private Source loadSource() {
    return Source.getSource(packageName.replace('.', File.separatorChar) +
    File.separator + sourceFileName);
  }  
  /**
   * Loads the static fields of a class.
   */
  private FieldInfo[] loadStaticFields(JavaClass jc) {
    Field[] fields = jc.getFields();

    int counter = 0;

    for(int i = 0, l = fields.length; i < l; i++)
      if(fields[i].isStatic())
    counter += Types.getTypeSize(fields[i].getSignature().toString());

    FieldInfo[] sFields = new FieldInfo[counter];

    counter = 0;
    for(int i = 0, l = fields.length; i < l; i++)
      if(fields[i].isStatic()) {
    sFields[counter] = new FieldInfo(fields[i], this);
    counter += Types.getTypeSize(fields[i].getSignature().toString());
      }

    return sFields;
  }  
  /**
   * Loads the static methods of a class.
   */
  private MethodInfo[] loadStaticMethods(JavaClass jc) {
    Method[] methods = jc.getMethods();

    int counter = 0;
    for(int i = 0, l = methods.length; i < l; i++)
      if(methods[i].isStatic())
    counter++;

    MethodInfo[] sMethods = new MethodInfo[counter];
    
    counter = 0;
    for(int i = 0, l = methods.length; i < l; i++)
      if(methods[i].isStatic())
    sMethods[counter++] = new MethodInfo(methods[i], this);

    return sMethods;
  }  
  /**
   * Loads the super class of a class.
   */
  private static ClassInfo loadSuperClass(JavaClass jc) {
    if(jc.getClassName().equals("java.lang.Object"))
      return null;

    return ClassInfo.getClassInfo(jc.getSuperclassName());
  }  
  /**
   * Returns the index for a static field.
   */
  public int staticFieldIndex(String fname) {
    int length = staticFields.length;

    for(int i = 0; i < length; i++)
      if(staticFields[i] != null && staticFields[i].getName().equals(fname))
    return i;

    throw new InternalErrorException("class " + getName() + " does not have static field `" + fname + "'");
  }  
}

---