---

BIRCTraceManager.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.lang.reflect.Method;
import javax.swing.*;
import javax.swing.tree.*;
import ca.mcgill.sable.soot.*;
import ca.mcgill.sable.soot.jimple.*;
import edu.ksu.cis.bandera.jjjc.*;
import edu.ksu.cis.bandera.annotation.*;
import edu.ksu.cis.bandera.birc.*;
import edu.ksu.cis.bandera.jext.*;
import java.util.*;
import edu.ksu.cis.bandera.abstraction.*;
import edu.ksu.cis.bandera.abstraction.typeinference.*;
public class BIRCTraceManager implements TraceManager {
    private static Jimple jimple = Jimple.v();
    private TypeTable typeTable;
    private AnnotationManager am = CompilationManager.getAnnotationManager();
    private SootClassManager scm = CompilationManager.getSootClassManager();
    private Vector threadAnnotations = new Vector();
    private Vector threadTreeModels = new Vector();
    private Vector annotationTrace = new Vector();
    private Vector stmtIndexTrace = new Vector();
    private Hashtable valueNodeValueTable;
    private JimpleTrace trace;
    private int traceLength;
    private Stmt[] stmts;
    private JimpleStore currentStore;
    private Vector threads;
    private int currentStep = 0;
/**
 * BIRCTraceManager constructor comment.
 */
public BIRCTraceManager(JimpleTrace trace, TypeTable typeTable) {
    this.trace = trace;
    this.am = CompilationManager.getAnnotationManager();
    this.scm = CompilationManager.getSootClassManager();
    this.typeTable = typeTable;
    stmts = trace.getStatements();
    for (int i = 0; i < stmts.length; i++) {
        try {
            Annotation a = am.getContainingAnnotation((Stmt) stmts[i]);
            if ("edu.ksu.cis.bandera.annotation.SequentialAnnotation".equals(a.getClass().getName())) continue;
            if (annotationTrace.size() > 0) {
                if (a != annotationTrace.lastElement()) {
                    stmtIndexTrace.add(new Integer(i));
                    annotationTrace.add(a);
                    System.out.println(a.getClass().getName() + ":" + a);
                }
            } else {
                stmtIndexTrace.add(new Integer(i));
                annotationTrace.add(a);
                System.out.println(a.getClass().getName() + ":" + a);
            }
        } catch (Exception e) {
            System.out.println("Couldn't find annotation for " + stmts[i]);
        }
    }
    traceLength = annotationTrace.size();
    currentStore = trace.getStore(0);
    threads = currentStore.getThreads();
    threadTreeModels.setSize(threads.size());
    threadAnnotations.setSize(threads.size());
    reset();
}
/**
 * back method comment.
 */
public void back() {
    int index = ((Integer) stmtIndexTrace.elementAt(--currentStep)).intValue();
    Annotation a = (Annotation) annotationTrace.elementAt(currentStep);
    currentStore = trace.getStore(index);
    currentStore.print();
    int tid = 0;
    for (Iterator i = threads.iterator(); i.hasNext(); tid++) {
        SootMethod sm = (SootMethod) i.next();
        if (((JimpleBody) sm.getBody(jimple)).getStmtList().indexOf(stmts[index]) >= 0) {
            threadAnnotations.setElementAt(a, tid);
            break;
        }
    }
}
/**
 * cleanup method comment.
 */
public void cleanup() {}
/**
 * forward method comment.
 */
public void forward() {
    if (currentStep == traceLength-1) {
        currentStore = trace.getLastStore();
        currentStore.print();
        currentStep++;
        return;
    }
    int index = ((Integer) stmtIndexTrace.elementAt(++currentStep)).intValue();
    currentStore = trace.getStore(index);
    currentStore.print();
    Annotation a = (Annotation) annotationTrace.elementAt(currentStep);
    int tid = 0;
    for (Iterator i = threads.iterator(); i.hasNext(); tid++) {
        SootMethod sm = (SootMethod) i.next();
        if (((JimpleBody) sm.getBody(jimple)).getStmtList().indexOf(stmts[index]) >= 0) {
            System.out.println("ThID: " + tid + ", annotation: " + a);
            threadAnnotations.setElementAt(a, tid);
            break;
        }
    }
}
/**
 * 
 * @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() {
    if (currentStep == traceLength) return (Annotation) annotationTrace.elementAt(currentStep - 1);
    return (Annotation) annotationTrace.elementAt(currentStep);
}
/**
 * getAnnotation method comment.
 */
public edu.ksu.cis.bandera.annotation.Annotation getAnnotation(int threadID) {
    return (Annotation) threadAnnotations.elementAt(threadID);
}
/**
 * 
 * @return edu.ksu.cis.bandera.birc.JimpleLiteral
 * @param topMethod ca.mcgill.sable.soot.SootMethod
 * @param realMethod ca.mcgill.sable.soot.SootMethod
 * @param local ca.mcgill.sable.soot.jimple.Local
 */
private JimpleLiteral getLocalValue(SootMethod topMethod, SootMethod realMethod, Local local) {
    System.out.println(topMethod + ";" + realMethod + ";" + local);
    if (topMethod == realMethod) return currentStore.getLocalValue(topMethod, local);
    Vector v = new Vector();
    HashSet inlinedLocal = am.getInlinedLocal(new LocalExpr(realMethod, local));
    if (inlinedLocal != null) {
        for (Iterator i = inlinedLocal.iterator(); i.hasNext();) {
            LocalExpr le = (LocalExpr) i.next();
            if (le.getMethod() == topMethod) {
                v.add(le.getLocal());
            }
        }
    }
    if ((v.size() == 0) || (v.size() > 1)) {
        System.out.println("Unable to find value for <" + realMethod + ", " + local + ">, default to null");
        return null;
    } else {
        return currentStore.getLocalValue(topMethod, (Local) v.firstElement());
    }
}
/**
 * getNumOfSteps method comment.
 */
public int getNumOfSteps() {
    return traceLength;
}
/**
 * getThreadTreeModels method comment.
 */
public java.util.Vector getThreadTreeModels() {
    return threadTreeModels;
}
/**
 * getValueText method comment.
 */
public String getValueText(javax.swing.tree.DefaultTreeModel model, javax.swing.tree.DefaultMutableTreeNode node) {
    if (!(node.getUserObject() instanceof ValueNode))
        return "";
    ValueNode vn = (ValueNode) node.getUserObject();
    Object literal = valueNodeValueTable.get(vn);
    if (literal == null)
        return "";
    if (literal instanceof ReferenceLiteral) {
        if (((ReferenceLiteral) literal).value == null)
            return "null";
        literal = ((ReferenceLiteral) literal).value;
        if (literal instanceof ArrayLiteral) {
            ArrayLiteral arrayLiteral = (ArrayLiteral) literal;
            if (node.getChildCount() == 0) {
                int size = arrayLiteral.length;
                for (int i = 0; i < size; i++) {
                    ValueNode vNode = new ValueNode(arrayLiteral, i);
                    model.insertNodeInto(new DefaultMutableTreeNode(vNode), node, node.getChildCount());
                    valueNodeValueTable.put(vNode, arrayLiteral.contents[i]);
                }
            }
            return "#" + arrayLiteral.getId();
        } else {
                ClassLiteral classLiteral = (ClassLiteral) literal;
                if (node.getChildCount() == 0) {
                    SootClass sc = classLiteral.getSource();
                    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, classLiteral.getFieldValue(sf));
                    }
                }
                String result = "#" + classLiteral.getId() + "\nHolding: ";
                LockLiteral lockLiteral = classLiteral.getLockValue();
                if (threads.indexOf(lockLiteral.getHoldingThread()) != -1)
                    result += "Thread ID" + threads.indexOf(lockLiteral.getHoldingThread());
                result += "\nWaiting: ";
                for (int i = 0; i < lockLiteral.getNumWaiting(); i++) {
                    if (i == (lockLiteral.getNumWaiting() - 1)) {
                        result += ("ThreadID:" + threads.indexOf(lockLiteral.getWaitingThread(i)));
                    } else {
                        result += ("ThreadID:" + threads.indexOf(lockLiteral.getWaitingThread(i)) + ", ");
                    }
                }
                return result;
            }
    } else if (literal instanceof BooleanLiteral) {
        return "" + ((BooleanLiteral) literal).value;
    } else if (literal instanceof IntegerLiteral) {
        return "" + ((IntegerLiteral) literal).value;
    } else {
        return literal.toString();
    }
}
/**
 * getVariableTreeModel method comment.
 */
public javax.swing.tree.TreeModel getVariableTreeModel() {
    valueNodeValueTable = new Hashtable();
    
    DefaultMutableTreeNode root = new DefaultMutableTreeNode("Store");

    Hashtable compiledClasses = CompilationManager.getCompiledClasses();
    for (Enumeration e = compiledClasses.elements(); e.hasMoreElements();) {
        SootClass sc = (SootClass) e.nextElement();
        for (ca.mcgill.sable.util.Iterator i = sc.getFields().iterator(); i.hasNext();) {
            SootField sf = (SootField) i.next();
            if (Modifier.isStatic(sf.getModifiers())) {
                Object o = currentStore.getStaticFieldValue(sf);
                if (o != null) {
                    ValueNode vn = new ValueNode(sf);
                    Object t = typeTable.get(sf);
                    if ((t != null) && (t instanceof IntegralAbstraction) && !(t instanceof ConcreteIntegralAbstraction)) {
                        o = getAbstractToken(typeTable.get(sf), ((IntegerLiteral) o).value);
                    }
                    valueNodeValueTable.put(vn, o);
                    root.add(new DefaultMutableTreeNode(vn));
                }
            }
        }
    }

    for (int i = 0; i < threadAnnotations.size(); i++) {
        threadTreeModels.setElementAt(null, i);
        if (!isAlive(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;
        }
        DefaultMutableTreeNode mNode = new DefaultMutableTreeNode(new ValueNode(sm, i));
        if (!Modifier.isStatic(sm.getModifiers())) {
            Local lcl = ((JimpleBody) sm.getBody(jimple)).getLocal("JJJCTEMP$0");
            Object o = getLocalValue((SootMethod) threads.elementAt(i), sm, lcl);
            if (o != null) {
                ValueNode vn = new ValueNode(lcl);
                mNode.add(new DefaultMutableTreeNode(vn));
                valueNodeValueTable.put(vn, o);
            }
        }
        for (Enumeration e = locals.elements(); e.hasMoreElements();) {
            Local lcl = (Local) e.nextElement();
            Object o = getLocalValue((SootMethod) threads.elementAt(i), sm, lcl);
            if (o != null) {
                Object t = typeTable.get(lcl);
                if ((t != null) && (t instanceof IntegralAbstraction) && !(t instanceof ConcreteIntegralAbstraction)) {
                    o = getAbstractToken(typeTable.get(lcl), ((IntegerLiteral) o).value);
                }
                ValueNode vn = new ValueNode(lcl);
                mNode.add(new DefaultMutableTreeNode(vn));
                valueNodeValueTable.put(vn, o);
            }
        }
        root.add(mNode);
        threadTreeModels.setElementAt(new DefaultTreeModel(mNode), i);
    }

    return new DefaultTreeModel(root);
}
/**
 * isAlive method comment.
 */
public boolean isAlive(int threadID) {
    return currentStore.isActive((SootMethod) threads.elementAt(threadID));
}
/**
 * reset method comment.
 */
public void reset() {
    currentStep = 0;
    currentStore = trace.getStore(0);
    currentStore.print();
    Annotation a = (Annotation) annotationTrace.elementAt(0);
    int tid = 0;
    for (Iterator i = threads.iterator(); i.hasNext(); tid++) {
        SootMethod sm = (SootMethod) i.next();
        if (((JimpleBody) sm.getBody(jimple)).getStmtList().indexOf(stmts[0]) >= 0) {
            threadAnnotations.setElementAt(a, tid);
            break;
        }
    }
}
}

---