---

BirState.java

package edu.ksu.cis.bandera.bir;

/* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
 * Bandera, a Java(TM) analysis and transformation toolkit           *
 * Copyright (C) 1998, 1999   James Corbett (corbett@hawaii.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 ca.mcgill.sable.util.*;

import java.util.*;

/**
 * A BirState represents a state of a BIR transition system in a trace.
 * <p>
 * The main parts of the state are:
 * <ul>
 * <li> A "state vector": 
 *    a Literal array storing the value of all state variables 
 *    which are laid out as they might be in a compiler.
 * <li> A Location array storing the current location of each thread.
 * <li> A boolean array indicating whether each thread is active.
 * </ul>
 * The interface Literal is implemented by a collection of classes
 * that represent values of non-composite types (BoolLit, IntLit,
 * LockLit, RefLit).  These objects are the contents of the state
 * vector.
 * <p>
 * This class is a BIR expression switch---it translates a BIR expression
 * into either a Literal value (the r-value of the expression in this state)
 * or an Integer (the address in the state vector of the l-value of
 * the expression in this state).   The rules are:
 * <ul>
 * <li> Any expression with an array or record value always evaluates
 *   to the Integer address of that object in the state vector.
 * <li> If the LHS flag is set, then any expression will evaluate
 *  to the Integer address of that entity in the state vector
 *  (in this case, it is an error if the expression is not an l-value).
 *  This flag is set to true only while evaluating the left-hand-side of
 *  an assignment (since we want the address to update).
 * <li> Otherwise, the expression evaluates to a Literal representing
 *  the r-value of the expression in this state.
 * </ul>
 */

public class BirState extends AbstractExprSwitch 
    implements Cloneable, BirConstants {

    TransSystem system;
    Literal [] store;            // StateVar values
    Location [] location;        // Thread Locations
    boolean [] threadActive;     // Thread status (active or inactive)

    boolean lhs = false;         // Translating LHS of assign
    int choice;                  // choice for nondeterministic actions
    String output = "";          // Output from Bandera.print() stamenets

    BirState(TransSystem system) {
    this.system = system;
    }
    public void applyAction(Action action, int choice) {
    this.choice = choice;
    action.apply(this);
    }
    public void caseAddExpr(AddExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new IntLit(op1.getValue() + op2.getValue()));
    }
    public void caseAndExpr(AndExpr expr)
    {
    expr.getOp1().apply(this);
    BoolLit op1 = (BoolLit) getResult();
    expr.getOp2().apply(this);
    BoolLit op2 = (BoolLit) getResult();
    setResult(new BoolLit(op1.getValue() && op2.getValue()));
    }
    public void caseArrayExpr(ArrayExpr expr)
    {
    boolean saveLhs = lhs;
    // Even if we're in LHS mode, eval index in normal mode
    // (the index could be a constant, which doesn't have an address)
    lhs = false;  
    expr.getIndex().apply(this);
    ConstExpr index = (ConstExpr) getResult();
    lhs = saveLhs;                           // restore mode
    expr.getArray().apply(this);
    Integer offset = (Integer) getResult();
    int address = offset.intValue() + index.getValue() + 1; 
    // add 1 to address for length (which is stored in first slot)
    if (lhs || expr.getType().isKind(ARRAY|RECORD)) 
        setResult(new Integer(address));
    else
        setResult(store[address]);  
    }
    public void caseAssertAction(AssertAction assertAction) {
    // Assertions do not modify the state
    }
    /**
     * Execute assignment.
     */

    public void caseAssignAction(AssignAction assign) 
    {
    assign.getRhs().apply(this);
    Literal val = (Literal) getResult();
    lhs = true;
    assign.getLhs().apply(this);
    Integer index = (Integer) getResult();
    lhs = false;
    store[index.intValue()] = val;
    }
    public void caseBoolLit(BoolLit expr)
    {
        setResult(expr);
    }
    public void caseChooseExpr(ChooseExpr expr)
    {
    // Use choice from trace to compute value 
    setResult(expr.getChoice(choice));
    }
    public void caseConstant(Constant expr)
    {
        setResult(expr);
    }
    public void caseDerefExpr(DerefExpr expr)
    {
    // Even if we're in LHS mode, eval ref expr in normal mode
    // (it could be null, which has no address)
    boolean saveLhs = lhs;
    lhs = false;
    expr.getTarget().apply(this);
    RefLit ref = (RefLit) getResult();
    lhs = saveLhs;
    int address = ref.getCollection().getOffset();
    if (ref.getCollection().getType().isKind(COLLECTION)) 
        address += ref.getIndex() * expr.getType().getExtent();
    if (lhs || expr.getType().isKind(ARRAY|RECORD)) 
        setResult(new Integer(address));
    else
        setResult(store[address]);  
    }
    public void caseDivExpr(DivExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new IntLit(op1.getValue() / op2.getValue()));
    }
    public void caseEqExpr(EqExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new BoolLit(op1.getValue() == op2.getValue()));
    }
    public void caseInstanceOfExpr(InstanceOfExpr expr)
    {
    expr.getRefExpr().apply(this);
    if (getResult() instanceof NullExpr)
        // null is an instanceof any ref type
        setResult(new BoolLit(true));
    else {
        StateVar collection = ((RefLit)getResult()).getCollection();
        StateVarVector targets = expr.getRefType().getTargets();
        setResult(new BoolLit(targets.indexOf(collection) >= 0));
    }
    }
    public void caseIntLit(IntLit expr)
    {
        setResult(expr);
    }
    public void caseLeExpr(LeExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new BoolLit(op1.getValue() <= op2.getValue()));
    }
    public void caseLengthExpr(LengthExpr expr)
    {
    expr.getArray().apply(this);
    Integer offset = (Integer) getResult();
    setResult(store[offset.intValue()]);
    }
    public void caseLockAction(LockAction lockAction) 
    {
    lhs = true;
    lockAction.getLockExpr().apply(this);
    Integer index = (Integer) getResult();
    lhs = false;
    LockLit lock = (LockLit) store[index.intValue()];
    int operation = lockAction.getOperation();
    BirThread thread = lockAction.getThread();
    store[index.intValue()] = lock.nextState(operation,thread,choice);
    }
    public void caseLockTest(LockTest lockTest) 
    {
    lockTest.getLockExpr().apply(this);
    LockLit lock = (LockLit) getResult();
    setResult(new BoolLit(lock.queryState(lockTest.getOperation(),
                          lockTest.getThread())));
    }
    public void caseLtExpr(LtExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new BoolLit(op1.getValue() < op2.getValue()));
    }
    public void caseMulExpr(MulExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new IntLit(op1.getValue() * op2.getValue()));
    }
    public void caseNeExpr(NeExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new BoolLit(op1.getValue() != op2.getValue()));
    }
    public void caseNewArrayExpr(NewArrayExpr expr)
    {
    StateVar target = expr.getCollection();
    Type type = ((Collection)target.getType()).getBaseType();
    BirTypeInit initializer = new BirTypeInit(this);
    // Use length computed from trace
    int length = target.getActualBaseTypeSize();
    int address = target.getOffset() + choice * length;
    // Set length field
    store[address] = new IntLit(length);
    type.apply(initializer,new Integer(address));
    setResult(new RefLit(target,choice));
    }
    public void caseNewExpr(NewExpr expr)
    {
    StateVar target = expr.getCollection();
    Type type = ((Collection)target.getType()).getBaseType();
    // Make sure to initialize new object
    BirTypeInit initializer = new BirTypeInit(this);
    int address = target.getOffset() + choice * type.getExtent();
    type.apply(initializer,new Integer(address));
    setResult(new RefLit(target,choice));
    }
    public void caseNotExpr(NotExpr expr)
    {
    expr.getOp().apply(this);
    BoolLit op = (BoolLit) getResult();
    setResult(new BoolLit(! op.getValue()));
    }
    public void caseNullExpr(NullExpr expr)
    {
    setResult(expr);
    }
    public void caseOrExpr(OrExpr expr)
    {
    expr.getOp1().apply(this);
    BoolLit op1 = (BoolLit) getResult();
    expr.getOp2().apply(this);
    BoolLit op2 = (BoolLit) getResult();
    setResult(new BoolLit(op1.getValue() || op2.getValue()));
    }
    public void casePrintAction(PrintAction printAction) 
    {
    // Dump the output of Bandera.print() to the 'output' string
    Vector printItems = printAction.getPrintItems();
    for (int i = 0; i < printItems.size(); i++) {
        Object item = printItems.elementAt(i);
        if (item instanceof String)
        output += item;
        else {
        ((Expr)item).apply(this);
        output += getResult().toString();
        }
    }
    output += "\n";
    }
    public void caseRecordExpr(RecordExpr expr)
    {
    expr.getRecord().apply(this);
    Integer offset = (Integer) getResult();
    int address = offset.intValue() + expr.getField().getOffset();
    if (lhs || expr.getType().isKind(ARRAY|RECORD)) 
        setResult(new Integer(address));
    else
        setResult(store[address]);  
    }
    public void caseRefExpr(RefExpr expr)
    {
    setResult(new RefLit(expr.getTarget(),0));
    }
    public void caseRemExpr(RemExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new IntLit(op1.getValue() % op2.getValue()));
    }
    public void caseStateVar(StateVar expr)
    {
    if (lhs || expr.getType().isKind(ARRAY|RECORD|COLLECTION)) 
        setResult(new Integer(expr.getOffset()));
    else
        setResult(store[expr.getOffset()]);
    }
    public void caseSubExpr(SubExpr expr)
    {
    expr.getOp1().apply(this);
    ConstExpr op1 = (ConstExpr) getResult();
    expr.getOp2().apply(this);
    ConstExpr op2 = (ConstExpr) getResult();
    setResult(new IntLit(op1.getValue() - op2.getValue()));
    }
    public void caseThreadAction(ThreadAction threadAction) 
    {
    if (threadAction.isStart()) 
        threadActive[threadAction.getThreadArg().getId()] = true;
    else if (threadAction.isExit())
        threadActive[threadAction.getThread().getId()] = false;
    }
    public void caseThreadLocTest(ThreadLocTest threadLocTest) 
    {
    setResult(new BoolLit(location[threadLocTest.getThread().getId()]
                  == threadLocTest.getLocation()));
    }
    public void caseThreadTest(ThreadTest threadTest) 
    {
    boolean done = ! threadActive[threadTest.getThreadArg().getId()];
    setResult(new BoolLit(done));
    }
    /**
     * Update thread location once all transformation actions have completed.
     */

    public void completeTrans(Transformation trans) {
    Location toLoc = trans.getToLoc();
    location[toLoc.getThread().getId()] = toLoc;
    }
    /**
     * Make a copy of this state
     */

    public BirState copy() {
    BirState result = new BirState(system);
    result.store = (Literal []) store.clone();
    result.location = (Location []) location.clone();
    result.threadActive = (boolean []) threadActive.clone();
    result.output = output;
    return result;
    }
    public void defaultCase(Object obj)
    {
    throw new RuntimeException("Forgot to handle case: " + obj);
    }
    public String exprValue(Expr expr) {
    expr.apply(this);
    if (expr.getType().isKind(ARRAY|RECORD))
        return "Object";
    else 
        return getResult().toString();
    }
    public String getOutput() { return output; }
    public Literal [] getStore() { return store; }
    public TransSystem getSystem() { return system; }
    /**
     * Build the initial state of a BIR transition system.
     */

    public static BirState initialState(TransSystem system, 
                    TransVector transVector,
                    Vector choiceVector) {
    int stateSize = 
        setActualSizesFromTrace(system,transVector,choiceVector);
    BirState state = new BirState(system);
    state.location = new Location[system.getThreads().size()];
    state.threadActive = new boolean[system.getThreads().size()];
    state.store = new Literal[stateSize];

    // Initialize each state variable using BIR type initializer
    BirTypeInit initializer = new BirTypeInit(state);
    StateVarVector vars = system.getStateVars();
    for (int i = 0; i < vars.size(); i++) {
        StateVar var = vars.elementAt(i);
        var.getType().apply(initializer,var);
    }

    // Initialize thread loc and active vars
    ThreadVector threads = system.getThreads();
    for (int i = 0; i < threads.size(); i++) {
        BirThread thread = threads.elementAt(i);
        state.location[thread.getId()] = thread.getStartLoc();
        state.threadActive[thread.getId()] = thread.isMain();
    }

    return state;
    }
    public boolean isActive(BirThread thread) { 
    return threadActive[thread.getId()];
    }
    public void print() {
    System.out.println("STATE");
    for (int i = 0; i < store.length; i++)
        System.out.print(store[i] + " ");
    System.out.println();
    ThreadVector threads = system.getThreads();
    for (int i = 0; i < threads.size(); i++) {
        BirThread thread = threads.elementAt(i);
        if (threadActive[thread.getId()])
        System.out.println("    " + thread.getName() + " at " +
                   location[thread.getId()].getLabel());
    }
    BirTypePrint printer = new BirTypePrint(this);
    StateVarVector vars = system.getStateVars();
    for (int i = 0; i < vars.size(); i++) {
        StateVar var = vars.elementAt(i);
        System.out.print("    " + var.getName() + " = ");
        var.getType().apply(printer,var);
        System.out.println();
    }   
    }
    /**
     * Given the trace, compute the size of the state vector (which
     * holds the values of all state variables).
     * <p>
     * This used to be done statically given the collection
     * bounds in the BIR, but with dynamic verifiers like dSPIN
     * (which ignore these bounds), we don't know how many
     * collection elements are allocated until we see the trace.
     * <p>
     * We also set the choice for each Allocator action to indicate
     * the index into the collection of the instance that was allocated 
     * (this is just a count of the number allocated so far).  
     * Note that for NewArrayExpr, the choice that comes in is
     * the actual length---we reset it to the instance index
     * (the max length for the collection is computed and stored
     * in the collection).
     */
    public static int setActualSizesFromTrace(TransSystem system, 
                          TransVector transVector,
                          Vector choiceVector) {
    // Count number of allocator calls in trace for each collection
    // Also, for arrays, calculate max size of array in each collection
    StateVarVector vars = system.getStateVars();
    StateVarVector targets = system.refAnyType().getTargets();
    int numAlloc [] = new int[targets.size()]; 
    int maxArrayLength [] = new int[targets.size()]; 

    for (int i = 0; i < transVector.size(); i++) {
        ActionVector actions = transVector.elementAt(i).getActions();
        int choices [] = (int []) choiceVector.elementAt(i);
        for (int j = 0; j < actions.size(); j++) {
        Action action = actions.elementAt(j);
        if (action.isAssignAction()) {
            Expr rhs = ((AssignAction)action).getRhs();

            // When we see an allocator, find the target and
            // update the instance count.  For arrays,
            // also update the max array size.
            if (rhs instanceof Allocator) {
            int targetNum = 
                targets.indexOf(((Allocator)rhs).getCollection());
            if (rhs instanceof NewArrayExpr) {
                int arrayLength = choices[j];
                if (arrayLength > maxArrayLength[targetNum])
                maxArrayLength[targetNum] = arrayLength;
            }
            // Set choice for alloc action to # of instance alloced
            choices[j] = numAlloc[targetNum];
            numAlloc[targetNum] += 1;
            }
        }
        }
    }

    // Now assign each variable an offset, using the allocator counts
    // to determine the size of collections.  Note that we use the 
    // term "extent" to denote the number of memory slots needed
    // by a variable, while "size" denotes the number of components
    // (e.g., array or collection elements).
    int currentStateSize = 0;
    for (int i = 0; i < vars.size(); i++) {
        StateVar var = vars.elementAt(i);
        var.setOffset(currentStateSize);
        int varExtent = 0;
        if (var.getType().isKind(COLLECTION)) {
        int targetNum = targets.indexOf(var);
        int numItems = numAlloc[targetNum];
        var.setActualSize(numItems);
        Type baseType = ((Collection)var.getType()).getBaseType();
        int itemExtent = baseType.getExtent();
        if (baseType.isKind(ARRAY)) {
            int elementExtent = 
            ((Array)baseType).getBaseType().getExtent();
            int arraySize = maxArrayLength[targetNum];
            var.setActualBaseTypeSize(arraySize);
            itemExtent = 1 + arraySize * elementExtent;
            // Extra 1 for length field  
        }
        var.setActualBaseTypeExtent(itemExtent);
        // Extent of collection depends on # items and their extent
        varExtent = numItems * itemExtent;
        }
        else  // Extent of normal variable is just extent of its type
        varExtent = var.getType().getExtent();
        currentStateSize += varExtent;
        System.out.println(" Var " + var + " extent = " + varExtent);
    }
    return currentStateSize;
    }
}

---