---

ClassInfo.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.jpf.jvm.reflection.Reflection;
import gov.nasa.arc.ase.util.Debug;
import java.io.*;
import java.util.*;
// ifdef RACE
import gov.nasa.arc.ase.jpf.jvm.runtime.*;
//#endif RACE

public class ClassInfo {
  // from JavaClass
  private JavaClass       classData;
  // Used for constant pool resolution (from JavaClass)
  private ConstantPoolGen classConstantPool;
  // List of all methods in class
  private Hashtable       methodList = new Hashtable();
  // List of all dynamic fields in object
  private Field[]     dynamicFields;
  // List of all static fields in object
  private Field[]     staticFields;
  // Safe Blocks for this Class
  private SafeBlocks      safeBlocks;
  // unique id (not private)
  //  int id;
  // ClassInfo for its superClass
  private ClassInfo       superClass;

  private static String[] reflectionPath = {
    "gov.nasa.arc.ase.jpf.jvm.reflection", ""
  };

  Hashtable fieldNames = new Hashtable();

  Reflection reflection = null;

  private static String[] classPath = null;

  // creates a new class info object
  public ClassInfo(JavaClass cd) {
//    id = IDS.class_id++;

    classData = cd;

    if(Engine.options.po_reduction)
      loadSafeBlocks(cd);
    else
      safeBlocks = null;

    classConstantPool =  new ConstantPoolGen(cd.getConstantPool());

    // init fields
    int nsfields = 0;
    int ndfields = 0;
    Field[] fields = classData.getFields();
    for(int i = 0, l = fields.length; i < l; i++)
      if(fields[i].isStatic())
    nsfields++;
      else
    ndfields++;

    JavaClass jc = JPFVM.getJPFVM().loadClassData(classData.getSuperclassName());
    while(!jc.getClassName().equals("java.lang.Object")) {
      fields = jc.getFields();
      for(int i = 0, l = fields.length; i < l; i++)
    if(!fields[i].isStatic())
      ndfields++;
      jc = JPFVM.getJPFVM().loadClassData(jc.getSuperclassName());
    }

    staticFields = new Field[nsfields];
    dynamicFields = new Field[ndfields];

    int sfc = 0;
    int dfc = 0;
    
    fields = classData.getFields();
    for(int i = 0, l = fields.length; i < l; i++)
      if(fields[i].isStatic())
    staticFields[sfc++] = fields[i];
      else
    dynamicFields[dfc++] = fields[i];

    jc = JPFVM.getJPFVM().loadClassData(classData.getSuperclassName());
    while(!jc.getClassName().equals("java.lang.Object")) {
      fields = jc.getFields();
      for(int i = 0, l = fields.length; i < l; i++)
    if(!fields[i].isStatic())
      dynamicFields[dfc++] = fields[i];
      jc = JPFVM.getJPFVM().loadClassData(jc.getSuperclassName());
    }

    // init methods 
    Method[] methods = cd.getMethods();
    for(int i = 0, s = methods.length; i < s; i++) {
      Method m = methods[i];
      MethodInfo mi = new MethodInfo(m, this, classConstantPool);
      methodList.put(mi.getMethodName()+m.getSignature(), mi);
    }

    String superName = cd.getSuperclassName();

    if (cd.getClassName().equals("java.lang.Object")) {
// ifdef DEBUG

//#endif DEBUG
      superClass = null;      
    } else {
// ifdef DEBUG


//#endif DEBUG
      superClass = JPFVM.getJPFVM().getClass(superName);            
    }

    initFields();

    setReflection(cd.getClassName());
  }  
  public long callMethod(SystemState ss, KernelState ks, ThreadInfo th, String name, int[] args) {
    Reflection r = (Reflection)reflection.clone();
    r.setState(ss, ks, th);
    r.setObjectReference(args[0]);

    return r.callMethod(name, args);
  }  
  public long callStaticMethod(SystemState ss, KernelState ks, ThreadInfo th, String name, int[] args) {
    reflection.setState(ss, ks, th);

    return reflection.callStaticMethod(name, args);
  }  
  public Fields createFields() {
    Field[] fs = dynamicFields;
    Fields f = new Fields(this, fs.length);
    for(int i = 0, l = fs.length; i < l; i++) {
      f.setValue(i, Types.newValue(fs[i].getSignature()));
// ifdef MARK_N_SWEEP
      if(Types.isReference(fs[i].getSignature()))
    f.setValueRef(i);
//#endif MARK_N_SWEEP
    }

    return f;
  }  
  public Fields createStaticFields() {
    Field[] fs = staticFields;
    Fields f = new Fields(this, fs.length);
    for(int i = 0, l = fs.length; i < l; i++) {
      f.setValue(i, Types.newValue(fs[i].getSignature()));
// ifdef MARK_N_SWEEP
      if(Types.isReference(fs[i].getSignature()))
    f.setValueRef(i);
//#endif MARK_N_SWEEP
    }

    return f;
  }  
// ifdef RACE
  private void DEPEND_ExecuteMainMethod(ThreadInfo th){
    if (Depend.on()){
      Depend.addMain(th);
    }
  }  
//#endif RACE

  // executes the main method (just puts the frame on the stack)
  public ThreadInfo executeMain(KernelState ks, int classref) {
    ThreadInfo th = new ThreadInfo();
    ks.newThread(th);

    th.setStatus(STATUS.RUNNING);
    th.setClassInfo(this);
    th.setReference(new ClassRef(classref));
    th.newFrame(getMethodInfo("main([Ljava/lang/String;)V"));

    //** missing: we do not consider command line arguments yet **//
    th.setLocalVariable(0, (int)Types.newValue("[Ljava/lang/String;"));
// ifdef MARK_N_SWEEP
    th.setLocalVariableRef(0);
//#endif MARK_N_SWEEP

// ifdef DEBUG

//#endif DEBUG

// ifdef RACE
    DEPEND_ExecuteMainMethod(th);
//#endif RACE

    return th;
  }  
  public InstructionHandle executeMethod(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);
    boolean atomic = TransitionResult.isAtomic();
    String cn = classData.getClassName();

    if(cn.startsWith("java.lang.") || cn.startsWith("java.util."))
      atomic = true;

    Reflection r = (Reflection)reflection.clone();
    r.setState(ss, ks, th);
    r.setObjectReference(th.getCalleeThis(mi.getArgumentSize()));

    th.createMethodStackFrame(mi);

    return r.executeMethod(mi, atomic);
  }  
  public InstructionHandle executeStaticMethod(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);
    boolean atomic = TransitionResult.isAtomic();
    String cn = classData.getClassName();

    if(cn.startsWith("java.lang.") || cn.startsWith("java.util."))
      atomic = true;

    if(name.equals("<clinit>()V") && VirtualMachine.options.atomic_init)
      atomic = true;

    reflection.setState(ss, ks, th);

    th.createMethodStackFrame(mi);

    return reflection.executeStaticMethod(mi, atomic);
  }  
  public JavaClass getClassData() {
    return classData;
  }  
  public String getClassName() {
    return classData.getClassName();
  }  
  public ConstantPoolGen getCPG() {
    return classConstantPool;
  }  
  public Field[] getDynamicFields() {
    return dynamicFields;
  }  
  public String getFieldName(int index) {
    return (String)fieldNames.get(new Integer(index));
  }  
  public int getFieldType(int index) {
    return Type.getType(dynamicFields[index].getSignature()).getType();
  }  
  public int getFieldType(String fname) {
    int index = ((Integer)fieldNames.get(fname)).intValue();

    return Type.getType(dynamicFields[index].getSignature()).getType();
  }  
  public MethodInfo getMethodInfo(String name) {
    MethodInfo mi = (MethodInfo) methodList.get(name);
    if (mi == null) {
      if (name.equals("<clinit>()V")) // special case: don't look
    return null;                    // further if it is class init
// ifdef DEBUG


//#endif DEBUG
      if (superClass == null) {
    Debug.println(Debug.ERROR, "Method not found: " + name);
    System.exit(0);
      }
      return superClass.getMethodInfo(name);
    }
    else 
      return mi;
  }  
  public Field[] getStaticFields() {
    return staticFields;
  }  
  public int getStaticFieldType(int index) {
    return Type.getType(staticFields[index].getSignature()).getType();
  }  
  public int getStaticFieldType(String fname) {
    int index = ((Integer)fieldNames.get(fname)).intValue();

    return Type.getType(staticFields[index].getSignature()).getType();
  }  
  public ClassInfo getSuperClassInfo() {
    return superClass;
  }  
  private void initFields() {
    Field[] fs = dynamicFields;
    for(int i = 0, s = fs.length; i < s; i++)
      fieldNames.put(fs[i].getName(), new Integer(i));
    
    fs = getStaticFields();
    for(int i = 0, s = fs.length; i < s; i++)
      fieldNames.put(fs[i].getName(), new Integer(i));
  }  
  // executes the class init for the specific class.
  public InstructionHandle initialize(SystemState ss, KernelState ks, ThreadInfo th) {
    if(methodList.get("<clinit>()V") == null) return th.getPC();

    return executeStaticMethod(ss, ks, th, "<clinit>()V");
  }  
  public boolean isMethodDeterministic(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);

    Reflection r = (Reflection)reflection.clone();
    r.setState(ss, ks, th);
    r.setObjectReference(th.getCalleeThis(mi.getArgumentSize()));

    return r.isMethodDeterministic(mi);
  }  
  public boolean isMethodExecutable(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);

    Reflection r = (Reflection)reflection.clone();
    r.setState(ss, ks, th);
    r.setObjectReference(th.getCalleeThis(mi.getArgumentSize()));

    int stacksize = th.size();
    return r.isMethodExecutable(mi);
  }  
  public boolean isSafe(int line) {
    if (safeBlocks == null)
      return false;
    else
      return safeBlocks.isSafe(line);
  }  
  public boolean isStaticMethodDeterministic(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);

    reflection.setState(ss, ks, th);

    return reflection.isStaticMethodDeterministic(mi);
  }  
  public boolean isStaticMethodExecutable(SystemState ss, KernelState ks, ThreadInfo th, String name) {
    MethodInfo mi = getMethodInfo(name);

    reflection.setState(ss, ks, th);

    return reflection.isStaticMethodExecutable(mi);
  }  
  public boolean isThread() {
    ClassInfo ci = this;

    while (ci != null) {
      if (ci.getClassName().equals("java.lang.Thread"))
    return true;
      ci = ci.superClass;
    }

    return false;
  }  
  private void loadSafeBlocks(JavaClass cd) {
    if(classPath == null) setClassPath();

    // read in safe blocks if they exist
    String name = cd.getClassName().replace('.', '/');

    for(int i = 0; i < classPath.length; i++)
      try {
    String filename = classPath[i] + "/" + name + ".safe";
    BufferedReader in = new BufferedReader(new FileReader(filename));       
    Debug.println(Debug.WARNING, "Loading " + filename);
    safeBlocks = new SafeBlocks(in);

    return;
      } catch (FileNotFoundException e) {
      }

    safeBlocks = null;
  }  
  public String reflectionClassName(String name) {
    int index = 0;
    int last = 0;
    StringBuffer sb = new StringBuffer();

    while((index = name.indexOf(".", last)) != -1) {
      sb.append(Character.toUpperCase(name.charAt(last)));
      sb.append(name.substring(last + 1, index));
      last = index + 1;
    }
    sb.append(name.substring(last));

    return sb.toString();
  }  
  private static void setClassPath() {
    StringTokenizer st = new StringTokenizer(System.getProperty("java.class.path"), ":");
    classPath = new String[st.countTokens()];
    for(int i = 0; st.hasMoreTokens(); i++)
      classPath[i] = st.nextToken();
  }  
  private void setReflection(String name) {
    int l = reflectionPath.length;

    for(int i = 0; i < l && reflection == null; i++) {
      String cn;

      if(reflectionPath[i].equals(""))
    cn = name + "Reflection";
      else
    cn = reflectionPath[i] + "." + name + "Reflection";
      try {
    Class clazz = Class.forName(cn);
    reflection = (Reflection)clazz.newInstance();
    Debug.println(Debug.WARNING, "Loading class " + cn);
      } catch(InstantiationException e) {
    Debug.println(Debug.ERROR, "Can't instantiate " + cn);
    System.exit(1);
      } catch(IllegalAccessException e) {
    Debug.println(Debug.ERROR, "Can't instantiate " + cn);
    System.exit(1);
      } catch(ClassNotFoundException e) {
      }
    }

    for(int i = 0; i < l && reflection == null; i++) {
      String cn;
      if(reflectionPath[i].equals(""))
    cn = reflectionClassName(name) + "Reflection";
      else
    cn = reflectionPath[i] + "." + reflectionClassName(name) + "Reflection";
      try {
    Class clazz = Class.forName(cn);
    reflection = (Reflection)clazz.newInstance();
    Debug.println(Debug.WARNING, "Loading class " + cn);
      } catch(InstantiationException e) {
    Debug.println(Debug.ERROR, "Can't instantiate " + cn);
    System.exit(1);
      } catch(IllegalAccessException e) {
    Debug.println(Debug.ERROR, "Can't instantiate " + cn);
    System.exit(1);
      } catch(ClassNotFoundException e) {
      }
    }

    if(reflection == null)
      reflection = new Reflection();

    reflection.setClassInfo(this);
  }  
}

---