---

JPFTraceManager.java

package edu.ksu.cis.bandera.bui.counterexample;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 2000   Robby (robby@cis.ksu.edu)                    *
 * All rights reserved.                                              *
 *                                                                   *
 * This work was done as a project in the SAnToS Laboratory,         *
 * Department of Computing and Information Sciences, Kansas State    *
 * University, USA (http://www.cis.ksu.edu/santos).                  *
 * It is understood that any modification not identified as such is  *
 * not covered by the preceding statement.                           *
 *                                                                   *
 * This work is free software; you can redistribute it and/or        *
 * modify it under the terms of the GNU Library General Public       *
 * License as published by the Free Software Foundation; either      *
 * version 2 of the License, or (at your option) any later version.  *
 *                                                                   *
 * This work is distributed in the hope that it will be useful,      *
 * but WITHOUT ANY WARRANTY; without even the implied warranty of    *
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU *
 * Library General Public License for more details.                  *
 *                                                                   *
 * You should have received a copy of the GNU Library General Public *
 * License along with this toolkit; if not, write to the             *
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,      *
 * Boston, MA  02111-1307, USA.                                      *
 *                                                                   *
 * Java is a trademark of Sun Microsystems, Inc.                     *
 *                                                                   *
 * To submit a bug report, send a comment, or get the latest news on *
 * this project and other SAnToS projects, please visit the web-site *
 *                http://www.cis.ksu.edu/santos                      *
 * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * */
import java.io.*;
import ca.mcgill.sable.soot.jimple.*;
import edu.ksu.cis.bandera.jext.*;
import ca.mcgill.sable.soot.*;
import edu.ksu.cis.bandera.jjjc.decompiler.*;
import edu.ksu.cis.bandera.annotation.*;
import javax.swing.*;
import javax.swing.tree.*;
import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.*;
import edu.ksu.cis.bandera.jjjc.*;
import gov.nasa.arc.ase.jpf.jvm.examine.*;
import java.util.*;
import java.lang.reflect.Method;
import edu.ksu.cis.bandera.abstraction.*;
import edu.ksu.cis.bandera.abstraction.typeinference.*;
public class JPFTraceManager implements TraceManager {
    private iVirtualMachine vm;
    private TypeTable typeTable;
    private AnnotationManager am = CompilationManager.getAnnotationManager();
    private Hashtable compiledClasses = CompilationManager.getCompiledClasses();
    private SootClassManager scm = CompilationManager.getSootClassManager();
    private Annotation a;
    private Vector threadAnnotations = new Vector();
    private Vector threadTreeModels = new Vector();
    private gov.nasa.arc.ase.jpf.jvm.examine.State state;
    private Hashtable valueNodeValueTable;
    private edu.ksu.cis.bandera.annotation.Annotation lastAnn;
/**
 * JPFTraceManager constructor comment.
 */
public JPFTraceManager(iVirtualMachine vm, TypeTable typeTable) {
    this.vm = vm;
    this.typeTable = typeTable;
    reset();
}
/**
 * back method comment.
 */
public void back() {
    FilenameLinePair flp = vm.ErrorBackward();
    int tid = vm.nextThreadToExecute();
    try {
        a = am.getAnnotation(flp);
    } catch (Exception e) {
        a = null;
    }
    System.out.println(flp + ": " + a);
    state.newState();
    threadAnnotations.setSize(state.numOfThreads());
    threadTreeModels.setSize(state.numOfThreads());
    threadAnnotations.setElementAt(a, tid);
}
/**
 * 
 */
public void cleanup() {
    /*
    File tempDir = new File(System.getProperty("user.dir") + File.separator + "$temp");
    if (!tempDir.exists()) return;
    try {
        if (!deleteDirectory(tempDir))
            System.out.println("Can't remove temporary directory '" + tempDir.getAbsolutePath() + "'");
        if (!tempDir.delete())
            System.out.println("Can't remove temporary directory '" + tempDir.getAbsolutePath() + "'");
    } catch (Exception e) {
        System.out.println("Can't remove temporary directory '" + tempDir.getAbsolutePath() + "'");
    }
    */
}
/**
 * 
 */
private boolean deleteDirectory(File dir) {
    File[] files = dir.listFiles();
    for (int i = 0; i < files.length; i++) {
        if (files[i].isDirectory()) {
            if (!deleteDirectory(files[i])) return false;
        }
        if (!files[i].delete()) return false;
    }
    return true;
}
/**
 * forward method comment.
 */
public void forward() {
    lastAnn = a;
    FilenameLinePair flp = vm.ErrorForward();
    int tid = vm.nextThreadToExecute();
    try {
        a = am.getAnnotation(flp);
    } catch (Exception e) {
        a = null;
    }
    System.out.println(flp + ": " + a);
    state.newState();
    threadAnnotations.setSize(state.numOfThreads());
    threadTreeModels.setSize(state.numOfThreads());
    if (tid != -1) 
        threadAnnotations.setElementAt(a, tid);
}
/**
 * 
 * @return java.lang.String
 * @param type java.lang.Object
 * @param value int
 */
private String getAbstractToken(Object type, int value) {
    String className = type.getClass().getName();
    String methodName = "getToken";
    try {
        Class cls = Class.forName(className);
        Method mtd = cls.getMethod(methodName, new Class[] {int.class});
        return (String) mtd.invoke(null, new Object[] {new Integer(value)});
    } catch (Exception e) {
        return "" + value;
    }
}
/**
 * getAnnotation method comment.
 */
public edu.ksu.cis.bandera.annotation.Annotation getAnnotation() {
    return a;
}
/**
 * 
 * @return edu.ksu.cis.bandera.annotation.Annotation
 * @param threadID int
 */
public Annotation getAnnotation(int threadID) {
    return (Annotation) threadAnnotations.elementAt(threadID);
}
/**
 * 
 * @return int
 */
public int getNumOfSteps() {
    return vm.ErrorPathLength();
}
/**
 * 
 * @return java.util.Vector
 */
public Vector getThreadTreeModels() {
    return threadTreeModels;
}
/**
 * 
 * @return java.lang.String
 * @param model javax.swing.tree.DefaultTreeModel
 * @param node javax.swing.tree.DefaultMutableTreeNode
 */
public String getValueText(DefaultTreeModel model, DefaultMutableTreeNode node) {
    if (!(node.getUserObject() instanceof ValueNode)) return "";

    ValueNode vn = (ValueNode) node.getUserObject();
    Object iv = valueNodeValueTable.get(vn);
    if (iv == null) return "null";
  if ("null".equals("" + iv)) return "null";
    if ((iv instanceof ArrayValue) && (node.getChildCount() == 0)) {
        ArrayValue v = (ArrayValue) iv;
        int size = v.getSize();
        for (int i = 0; i < size; i++) {
            ValueNode vNode = new ValueNode(v, i);
            model.insertNodeInto(new DefaultMutableTreeNode(vNode), node, node.getChildCount());
            valueNodeValueTable.put(vNode, v.getElementValue(i));
        }
    } else if ((iv instanceof ObjectValue) && (node.getChildCount() == 0)) {
        ObjectValue v = (ObjectValue) iv;
        SootClass sc = scm.getClass(v.getTypeName());
        for (ca.mcgill.sable.util.Iterator i = sc.getFields().iterator(); i.hasNext();) {
            SootField sf = (SootField) i.next();
            ValueNode vNode = new ValueNode(sf);
            model.insertNodeInto(new DefaultMutableTreeNode(vNode), node, node.getChildCount());
            valueNodeValueTable.put(vNode, v.getFieldValue(sf.getName()));
        }
    }
    
    return iv.toString();
}
/**
 * getVariableTreeModel method comment.
 */
public javax.swing.tree.TreeModel getVariableTreeModel() {
    valueNodeValueTable = new Hashtable();
    
    DefaultMutableTreeNode root = new DefaultMutableTreeNode("Store");

    for (Enumeration e = compiledClasses.elements(); e.hasMoreElements();) {
        SootClass sc = (SootClass) e.nextElement();
        if (!state.isLoaded(sc.getName())) continue;
        for (ca.mcgill.sable.util.Iterator i = sc.getFields().iterator(); i.hasNext();) {
            SootField sf = (SootField) i.next();
            if (Modifier.isStatic(sf.getModifiers())) {
                ValueNode vn = new ValueNode(sf);
                Object o = state.getStaticFieldValue(sf.getDeclaringClass().getName(), sf.getName());
                Object t = typeTable.get(sf);
                if ((t != null) && (t instanceof IntegralAbstraction) && !(t instanceof ConcreteIntegralAbstraction)) {
                    if (o instanceof IntValue) {
                        o = getAbstractToken(typeTable.get(sf), ((IntValue) o).getValue());
                    } else if (o instanceof ShortValue) {
                        o = getAbstractToken(typeTable.get(sf), ((ShortValue) o).getValue());
                    }
                }
                valueNodeValueTable.put(vn, o);
                root.add(new DefaultMutableTreeNode(vn));
            }
        }
    }

    Jimple jimple = Jimple.v();
    
    for (int i = 0; i < threadAnnotations.size(); i++) {
        threadTreeModels.setElementAt(null, i);
        if (!state.isActive(i)) continue;
        Annotation a = (Annotation) threadAnnotations.elementAt(i);
        if (a == null) continue;
        Annotation ta = am.getMethodAnnotationContainingAnnotation(a);
        if ((a instanceof MethodDeclarationAnnotation)
                || (a instanceof ConstructorDeclarationAnnotation)
                || (a instanceof FieldDeclarationAnnotation)
                || (a instanceof ClassDeclarationAnnotation))
            ta = a;
        Hashtable locals = a.getDeclaredLocalVariables();
        SootMethod sm;
        if (ta instanceof MethodDeclarationAnnotation) {
            sm = ((MethodDeclarationAnnotation) ta).getSootMethod();
            Hashtable parameters = ((MethodDeclarationAnnotation) ta).getParameterLocals();
            for (Enumeration e = parameters.keys(); e.hasMoreElements();) {
                Object key = e.nextElement();
                locals.put(key, parameters.get(key));
            }
        } else if (ta instanceof ConstructorDeclarationAnnotation) {
            sm = ((ConstructorDeclarationAnnotation) ta).getSootMethod();
            Hashtable parameters = ((ConstructorDeclarationAnnotation) ta).getParameterLocals();
            for (Enumeration e = parameters.keys(); e.hasMoreElements();) {
                Object key = e.nextElement();
                locals.put(key, parameters.get(key));
            }
        } else {
            DefaultMutableTreeNode node = new DefaultMutableTreeNode("Thread<no information available>, ID: " + i);
            root.add(node);
            threadTreeModels.setElementAt(new DefaultTreeModel(node), i);
            continue;
        }
        /*
        System.out.println("Thread #: " + i + ", " + a);
        System.out.println("=============");
        iMethodState ms = state.getMethodState(i);
        for (Enumeration e = locals.keys(); e.hasMoreElements();) {
            String localName = (String) e.nextElement();
            System.out.println(localName + ": " + ms.getLocalValue(localName));
        }
        System.out.println("");
        */
        iMethodState ms = state.getMethodState(i);
        DefaultMutableTreeNode mNode = new DefaultMutableTreeNode(new ValueNode(sm, i));
        if (!Modifier.isStatic(sm.getModifiers())) {
            ValueNode vn = new ValueNode(((JimpleBody) sm.getBody(jimple)).getLocal("JJJCTEMP$0"));
            mNode.add(new DefaultMutableTreeNode(vn));
            valueNodeValueTable.put(vn, ms.getLocalValue("this"));
        }
        for (Enumeration e = locals.elements(); e.hasMoreElements();) {
            Local lcl = (Local) e.nextElement();
            try {
                ValueNode vn = new ValueNode(lcl);
                mNode.add(new DefaultMutableTreeNode(vn));
                Object o = ms.getLocalValue(lcl.getName());
                Object t = typeTable.get(lcl);
                if ((t != null) && (t instanceof IntegralAbstraction) && !(t instanceof ConcreteIntegralAbstraction)) {
                    if (o instanceof IntValue) {
                        o = getAbstractToken(typeTable.get(lcl), ((IntValue) o).getValue());
                    } else if (o instanceof ShortValue) {
                        o = getAbstractToken(typeTable.get(lcl), ((ShortValue) o).getValue());
                    }
                }
                valueNodeValueTable.put(vn, o);
            } catch (Exception ex) {
                ex.printStackTrace();
            }
        }
        root.add(mNode);
        threadTreeModels.setElementAt(new DefaultTreeModel(mNode), i);
    }

    return new DefaultTreeModel(root);
}
/**
 * 
 * @return boolean
 * @param threadID int
 */
public boolean isAlive(int threadID) {
    return state.isActive(threadID);
}
/**
 * reset method comment.
 */
public void reset() {
    FilenameLinePair flp = vm.ErrorInit();
    try {
        a = am.getAnnotation(flp);
    } catch (Exception e) {
        a = null;
    }
    System.out.println(flp + ": " + a);

    if (state == null)
        state = new gov.nasa.arc.ase.jpf.jvm.examine.State();
    else
        state.newState();
    threadAnnotations.setSize(state.numOfThreads());
    threadTreeModels.setSize(state.numOfThreads());
    threadAnnotations.setElementAt(a, 0);
}
}

---