package accrue.analysis.interprocvarcontext;

import java.lang.ref.SoftReference;
import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.WeakHashMap;

import polyglot.ast.Block;
import polyglot.ast.Node;
import polyglot.ast.Term;
import polyglot.types.Type;
import polyglot.util.InternalCompilerError;
import polyglot.visit.DataFlow.Item;
import polyglot.visit.FlowGraph.EdgeKey;
import accrue.analysis.interprocanalysis.AbstractLocation;
import accrue.analysis.interprocanalysis.ExitMap;
import accrue.analysis.interprocanalysis.ExitMap.Key;
import accrue.analysis.interprocanalysis.Ordered;

/**
 * A VarContext keeps track of abstract values for local variables and heap
 * locations. It also tracks abstract values for the expression stack,
 * the return value (either exceptional return or normal return value).
 * It is also used tracks suspended execution contexts appropriate, i.e., when
 * control flow enters a finally block, due to, say, an exception being thrown,
 * if the finally block terminates normally, then the VarContext for the exception
 * needs to be restored (since the exception value will be held in the 
 * suspended returnResult field). See VarContextDataFlow for more details. 
 */
public class VarContext<T extends AbstractValue<T>> extends Item implements
        Cloneable, Ordered<VarContext<T>> {
    // These fields are all final. They are marked as non-final to allow the copy pattern
    private Map<String, T> locals;
    protected Map<AbstractLocation, T> locations;

    /**
     * Analyses can choose to lose precision for speed, and not track data flow to heap locations.
     * If so, then they need to provide a default policy for heap locations, which will
     * be used when a value is read from the heap. For soundness, this should be the top value.
     */
    private final boolean TRACK_HEAP_LOCATIONS;
    private final T DEFAULT_HEAP_LOCATION_VALUE;

    /**
     * The exprResultStack represents the stack of expression results computed so far. 
     * For example, with expression e1 + e2, the result of e1
     * will be pushed on to the stack, then the result of e2 will be pushed on
     * to the stack, and then, when + is evaluated, the top two results will be
     * popped.
     * When flow leaves anything other than an expression, this should be empty.
     */
    private Stack<T> exprResultStack;

    /**
     * Record how big the exprResultStack was when we enter a given node.
     * This is useful to help determine how many arguments are on the stack
     * for a given expression. This map is cleared whenever the exprResultStack
     * is cleared.
     */
    private Map<Term, Integer> exprResultStackNodeEntry;

    /**
     * The returnResult represents the abstract value either for a result returned by a return statement, or for
     * the exception object. Which it represents depends on whether this VarContext is for an exception edge
     * or a return edge. The returnResult may be null, if there is no result to return. 
     */
    private T returnResult;

    /**
     * The suspendedExecutionStack contains mappings from incoming CFG edge key to dataflow value for each
     * finally block
     */
    private SuspendedExecutionStack<T> suspendedExecutionStack = null;

    private final T bottomAbsVal;

    private final String analysisName;

    protected int hashCode = 0;
    protected boolean needsHashCode = true;

    /**
     * Create a variable context
     * 
     * @param analysisName
     *            name of the current analysis
     * @param bottomAbsVal
     *            bottom value of the abstract value lattice
     */
    public VarContext(String analysisName, T bottomAbsVal) {
        this(analysisName, bottomAbsVal, true, null);
    }

    /**
     * Create a new variable context
     * 
     * @param analysisName
     *            name of the current analysis
     * @param bottomAbsVal
     *            bottom value of the abstract value lattice
     * @param trackHeapLocations
     *            Analyses can choose to lose precision for speed, and not track
     *            data flow to heap locations. If so, then they need to provide
     *            a default policy for heap locations, which will be used when a
     *            value is read from the heap. For soundness, this should be the
     *            top value.
     * @param defaultHeapLocationValue
     *            Default value for heap locations
     */
    public VarContext(String analysisName, T bottomAbsVal,
            boolean trackHeapLocations, T defaultHeapLocationValue) {
        this.locals = Collections.emptyMap();
        this.locations = Collections.emptyMap();
        this.exprResultStack = Stack.emptyStack();
        this.suspendedExecutionStack = null;
        this.exprResultStackNodeEntry = null;
        this.returnResult = null;
        this.bottomAbsVal = bottomAbsVal;
        this.TRACK_HEAP_LOCATIONS = trackHeapLocations;
        this.DEFAULT_HEAP_LOCATION_VALUE = defaultHeapLocationValue;
        this.analysisName = analysisName;
    }

    /**
     * Create a variable context
     * 
     * @param analysisName
     *            name of the current analysis
     * @param locals
     *            Map from local variable names to abstract values
     * @param locations
     *            Map from abstract locations to abstract values
     * @param exprResultStack
     *            stack of values containing the results of the analyses of
     *            previous expressions
     * @param exprResultStackNodeEntry
     *            Map describing the depth of the stack when flow for various nodes
     *            was entered.
     * @param suspendedExecutionStack
     *            Stack of maps from finally block entry edge to abstract value used 
     *            to pass values through a finally block 
     * @param returnResult
     *            abstract value for the return result
     * @param bottomAbsVal
     *            bottom value of the abstract value lattice
     * @param trackHeapLocations
     *            Analyses can choose to lose precision for speed, and not track
     *            data flow to heap locations. If so, then they need to provide
     *            a default policy for heap locations, which will be used when a
     *            value is read from the heap. For soundness, this should be the
     *            top value.
     * @param defaultHeapLocationValue
     *            Default value for heap locations
     */
    protected VarContext(String analysisName, Map<String, T> locals,
            Map<AbstractLocation, T> locations, Stack<T> exprResultStack,
            Map<Term, Integer> exprResultStackNodeEntry,
            SuspendedExecutionStack<T> suspendedExecutionStack, T returnResult,
            T bottomAbsVal, boolean trackHeapLocations,
            T defaultHeapLocationValue) {
        this.locals = locals;
        this.locations = locations;
        this.exprResultStack = exprResultStack;
        this.exprResultStackNodeEntry = exprResultStackNodeEntry;
        this.suspendedExecutionStack = suspendedExecutionStack;
        this.returnResult = returnResult;
        this.bottomAbsVal = bottomAbsVal;
        this.TRACK_HEAP_LOCATIONS = trackHeapLocations;
        this.DEFAULT_HEAP_LOCATION_VALUE = defaultHeapLocationValue;
        this.analysisName = analysisName;
    }

    /**
     * @return a copy of <code>this</code>
     */
    protected VarContext<T> copy() {
        try {
            @SuppressWarnings("unchecked")
            VarContext<T> copy = (VarContext<T>) this.clone();
            copy.needsHashCode = true;
            return copy;
        }
        catch (CloneNotSupportedException e) {
            throw new InternalCompilerError("Clone weirdness");
        }
    }

    @Override
    public final boolean leq(VarContext<T> that) {
        return leq(this, that, this.locations.keySet());
    }

    /**
     * Check leq, but limiting the locations of domains to the specified set.
     * 
     * @param that
     *            {@link VarContext} to compare to
     * @param locationDomain
     *            restrict leq to these locations
     */
    public boolean leq(VarContext<T> that, Set<AbstractLocation> locationDomain) {
        if (that == null) return false;

        for (String l : this.locals.keySet()) {
            T thatAbsVal = that.locals.get(l);
            if (thatAbsVal == null || !this.locals.get(l).leq(thatAbsVal)) {
                return false;
            }
        }
        if (this.TRACK_HEAP_LOCATIONS != that.TRACK_HEAP_LOCATIONS) {
            throw new InternalCompilerError("Inconsistent VarContexts on TRACK_HEAP_LOCATIONS. Should be same for all VarContexts in an analysis");
        }
        if (this.TRACK_HEAP_LOCATIONS) {
            for (AbstractLocation l : locationDomain) {
                if (this.locations.get(l) == null) {
                    // this location is null, which is always regarded as the lowest AbsVal
                    continue;
                }
                T thatAbsVal = that.locations.get(l);
                if (thatAbsVal == null
                        || !this.locations.get(l).leq(thatAbsVal)) {
                    return false;
                }
            }
        }
        if (this.returnResult != null
                && (that.returnResult == null || !this.returnResult.leq(that.returnResult))) {
            return false;
        }
        if (this.suspendedExecutionStack != null
                && that.suspendedExecutionStack == null) {
            return false;
        }
        if (this.suspendedExecutionStack != null
                && !this.suspendedExecutionStack.leq(that.suspendedExecutionStack)) {
            return false;
        }
        return this.exprResultStack.leq(that.exprResultStack);
    }

    /**
     * Return a new VarContext that is an upper bound of <code>this</code> and
     * <code>that</code>, i.e., this.leq(this.uppperBound(that)) and
     * that.leq(this.upperBound(that)).
     * 
     * @param that
     *            compute the upper bound of <code>this</code> and
     *            <code>that</code>
     * @param widen
     *            if true use the widening operator
     * 
     * @return {@link VarContext} that is the upper bound of <code>this</code>
     *         and <code>that</code>
     */
    public VarContext<T> wideningUpperBound(VarContext<T> that, boolean widen) {
        if (that == null) {
            return this;
        }

        boolean changed =
                !(this.locals.keySet().equals(that.locals.keySet()))
                        || !(this.locations.keySet().equals(that.locations.keySet()));

        Map<String, T> locals = new LinkedHashMap<String, T>();
        Set<String> localsDomains =
                new LinkedHashSet<String>(this.locals.keySet());
        localsDomains.addAll(that.locals.keySet());
        for (String l : localsDomains) {
            T ub = valUpperBound(this.locals.get(l), that.locals.get(l), widen);
            if (ub == null) {
                throw new InternalCompilerError("Null AbsVal: "
                        + this.locals.get(l) + " " + that.locals.get(l));
            }
            locals.put(l, ub);
            changed = changed || ub != this.locals.get(l);
        }

        Map<AbstractLocation, T> locations =
                new LinkedHashMap<AbstractLocation, T>();
        Set<AbstractLocation> locationDomains =
                new LinkedHashSet<AbstractLocation>(this.locations.keySet());
        locationDomains.addAll(that.locations.keySet());
        for (AbstractLocation l : locationDomains) {
            T ub =
                    valUpperBound(this.locations.get(l),
                                  that.locations.get(l),
                                  widen);
            locations.put(l, ub);
            if (ub == null) {
                throw new InternalCompilerError("Null AbsVal: "
                        + this.locations.get(l) + " " + that.locations.get(l));
            }
            changed = changed || ub != this.locations.get(l);
        }

        T resReturnResult =
                this.returnResult == null ? that.returnResult
                        : (widen ? this.returnResult.widen(that.returnResult)
                                : this.returnResult.upperBound(that.returnResult));
        changed = changed || this.returnResult != resReturnResult;

        if (this.exprResultStack.size() != that.exprResultStack.size()) {
            System.err.println("Wrong sizes with \n  " + this.exprResultStack
                    + " \n  " + that.exprResultStack);
        }

        Stack<T> resUB =
                widen ? this.exprResultStack.widen(that.exprResultStack)
                        : this.exprResultStack.upperBound(that.exprResultStack);
        changed = changed || (resUB != this.exprResultStack);

        Map<Term, Integer> nodeEntry;
        Map<Term, Integer> thisExprRSNE = this.exprResultStackNodeEntry;
        Map<Term, Integer> thatExprRSNE = that.exprResultStackNodeEntry;
        if (thisExprRSNE == null) {
            thisExprRSNE = Collections.emptyMap();
        }
        if (thatExprRSNE == null) {
            thatExprRSNE = Collections.emptyMap();
        }
        if (thisExprRSNE.keySet().equals(thatExprRSNE.keySet())) {
            // the domains of the two maps are the same.
            // Good enough
            nodeEntry = this.exprResultStackNodeEntry;
        }
        else {
            // domains differ
            // keep the nodes that are in common.
            changed = true;
            if (thisExprRSNE.isEmpty()) {
                // use that
                nodeEntry = that.exprResultStackNodeEntry;
            }
            else if (thatExprRSNE.isEmpty()) {
                nodeEntry = this.exprResultStackNodeEntry;
            }
            else {
                nodeEntry = new LinkedHashMap<Term, Integer>(thisExprRSNE);
                nodeEntry.keySet().retainAll(thatExprRSNE.keySet());
            }
        }

        SuspendedExecutionStack<T> newSusStack;
        if (this.suspendedExecutionStack == null) {
            newSusStack = that.suspendedExecutionStack;
        }
        else if (that.suspendedExecutionStack == null) {
            newSusStack = this.suspendedExecutionStack;
        }
        else {
            newSusStack =
                    widen ? this.suspendedExecutionStack.widen(that.suspendedExecutionStack)
                            : this.suspendedExecutionStack.upperBound(that.suspendedExecutionStack);
        }
        changed = changed || (newSusStack != this.suspendedExecutionStack);

        if (!changed) return this;

        VarContext<T> copy = this.copy();
        copy.locals = locals;
        copy.locations = locations;
        copy.returnResult = resReturnResult;
        copy.exprResultStack = resUB;
        copy.exprResultStackNodeEntry = nodeEntry;
        copy.suspendedExecutionStack = newSusStack;
        return copy;
    }

    @Override
    public VarContext<T> upperBound(VarContext<T> that) {
        return wideningUpperBound(that, false);
    }

    @Override
    public VarContext<T> widen(VarContext<T> that) {
        return wideningUpperBound(that, true);
    }

    /**
     * Compute the upper bound of <code>a</code> and <code>b</code>
     * 
     * @param a
     *            value
     * @param b
     *            value
     * @param widen
     *            if true use the widening operator
     * @return the upper bound of <code>a</code> and <code>b</code>
     */
    protected T valUpperBound(T a, T b, boolean widen) {
        if (a == null) return b;
        if (b == null) return a;
        if (widen) {
            return a.widen(b);
        }
        else {
            return a.upperBound(b);
        }
    }

    /**
     * @return Map of names to abstract values
     */
    public Map<String, T> locals() {
        return this.locals;
    }

    /**
     * Copy this variable context and swap the locals for <code>newLocals</code>
     * @param newLocals new map of names of local variables to abstract values
     * @return copy of <code>this</code> with the new local variable map
     */
    public VarContext<T> locals(Map<String, T> newLocals) {
        VarContext<T> copy = this.copy();
        copy.locals = newLocals;
        return hashCons(copy);
    }

    /**
     * @return The stack of abstract values that are the results of the previous
     *         expression analyses
     */
    public Stack<T> exprResultStack() {
        return exprResultStack;
    }

    public Map<Term, Integer> exprResultStackNodeEntry() {
        return this.exprResultStackNodeEntry;
    }

    /**
     * Pop <code>i</code> results off the result stack.
     * 
     * @param i
     *            number of results to pop
     * @return the expression results with the first <code>i</code> results
     *         popped off
     */
    public VarContext<T> popExprResults(int i) {
        if (i <= 0) return this;
        Stack<T> s = this.exprResultStack;
        for (int j = 0; j < i; j++) {
            s = s.pop();
        }
        return this.exprResultStack(s);
    }

    /**
     * Pop i results off the result stack, and push one
     * 
     * @param i
     *            number of results to pop
     * @param v
     *            value to push
     * @param source
     *            AST node that resulted in the newly pushed value
     * @return an expression result stack with i results popped off and
     *         <code>v</code> pushed on
     */
    public VarContext<T> popAndPushExprResults(int i, T v, Node source) {
        Stack<T> s = this.exprResultStack;
        for (int j = 0; j < i; j++) {
            s = s.pop();
        }
        return this.exprResultStack(s.push(v, source));
    }

    /**
     * Pop first result off the result stack.
     * 
     * @return the expression results with the first result popped off
     */
    public VarContext<T> popExprResult() {
        return this.popExprResults(1);
    }

    /**
     * Push result
     * 
     * @param v
     *            value to push
     * @param source
     *            object associated with the value being pushed
     * 
     * @return the expression results with <code>v</code> pushed on
     */
    public VarContext<T> pushExprResult(T v, Object source) {
        return this.exprResultStack(this.exprResultStack.push(v, source));
    }

    /**
     * Push results
     * 
     * @param v
     *            values to push
     * @param source
     *            object associated with the values being pushed
     * 
     * @return the expression results with the elements of <code>vs</code>
     *         pushed on
     */
    public VarContext<T> pushExprResults(List<T> vs, Object source) {
        Stack<T> s = this.exprResultStack;
        for (int i = vs.size() - 1; i >= 0; i--) {
            s = s.push(vs.get(i), source);
        }
        return this.exprResultStack(s);
    }

    /**
     * @return a list of the first <code>i</code> results on the expression
     *         results stack
     */
    public List<T> peekExprResults(int i) {
        List<T> r = new ArrayList<T>(i);
        Stack<T> s = this.exprResultStack;
        for (int j = 0; j < i; j++) {
            r.add(s.peek());
            s = s.pop();
        }
        return r;
    }

    /**
     * @return the first result on the expression results stack
     */
    public T peekExprResult() {
        return this.exprResultStack.peek();
    }

    /**
     * Swap the expression result stack in this with <code>s</code>
     * 
     * @param s
     *            stack to be converted
     * @return copy of this {@link VarContext} with <code>s</code> as its
     *         expression result stack
     */
    public VarContext<T> exprResultStack(Stack<T> s,
            Map<Term, Integer> nodeEntry) {
        if (s == null) throw new InternalCompilerError("null stack");
        if (nodeEntry != null && nodeEntry.isEmpty()) {
            nodeEntry = null;
        }

        if ((s == this.exprResultStack || (s != null && s.equals(this.exprResultStack)))
                && (nodeEntry == this.exprResultStackNodeEntry || (nodeEntry != null && nodeEntry.equals(this.exprResultStackNodeEntry)))) {
            return this;
        }

        VarContext<T> copy = this.copy();
        copy.exprResultStack = s;
        copy.exprResultStackNodeEntry = nodeEntry;
        return hashCons(copy);
    }

    private VarContext<T> exprResultStack(Stack<T> s) {
        if (s == null) throw new InternalCompilerError("null stack");
        if (s == this.exprResultStack
                || (s != null && s.equals(this.exprResultStack))) {
            return this;
        }
        VarContext<T> copy = this.copy();
        copy.exprResultStack = s;
        return hashCons(copy);
    }

    /**
     * Clear the stack of expression results
     * 
     * @return a copy of <code>this</code> with an empty expression result stack
     */
    public VarContext<T> clearExprResultStack() {
        if (this.exprResultStack.isEmpty() && exprResultStackNodeEntry == null) {
            return this;
        }
        VarContext<T> copy = this.copy();
        copy.exprResultStack = Stack.emptyStack();
        copy.exprResultStackNodeEntry = null;
        return hashCons(copy);
    }

    /**
     * Get the abstract value for the return result (could be null)
     * 
     * @return abstract value for the return result
     */
    public T returnResult() {
        return returnResult;
    }

    /**
     * Swap the return result in <code>this</code> for <code>returnResult</code>
     * 
     * @param returnResult
     *            new return result
     * @return copy of <code>this</code> with the return result swapped out
     */
    public VarContext<T> returnResult(T returnResult) {
        if (this.returnResult == returnResult
                || (this.returnResult != null && this.returnResult.equals(returnResult))) {
            return this;
        }
        VarContext<T> copy = this.copy();
        copy.returnResult = returnResult;
        return hashCons(copy);
    }

    /**
     * Clear the return result in <code>this</code>
     * 
     * @return A copy of <code>this</code> with the return result cleared
     */
    public VarContext<T> clearReturnResult() {
        // this.returnResult will perform a functional update
        // i.e., will return a new VarContext that is identical to
        // this one, but with the return result equal to null.
        return this.returnResult(null);
    }

    /**
     * Get a new {@link VarContext} identical to <code>this</code> with the 
     * suspended execution stack replaced with the specified one
     * 
     * @param stack stack of maps from finally block entry edge key to abstract value
     * 
     * @return new {@link VarContext} with the existing suspended execution stack 
     * swapped out for the specified one.
     */
    public VarContext<T> suspendedExecutionStack(
            SuspendedExecutionStack<T> stack) {
        if (this.suspendedExecutionStack == stack
                || (this.suspendedExecutionStack != null && this.suspendedExecutionStack.equals(stack))) {
            return this;
        }
        VarContext<T> copy = this.copy();
        copy.suspendedExecutionStack = stack;
        return hashCons(copy);
    }

    /**
     * Restore the appropriate elements of the caller context after analyzing 
     * the callee. <code>this</code> is the callee context. <code>toRestore</code> 
     * is the caller context to restore.
     * 
     * @param toRestore
     *          Context to restore from
     * @param restoreLocalsAndStack
     *          If true then the local variables and expression stack will be 
     *          restored         
     * @param edgeKey
     *          exit key we are restoring for
     * @return new context with certain elements restored
     */
    public VarContext<T> restoreCallerContext(VarContext<T> toRestore,
            boolean restoreLocalsAndStack, Key edgeKey) {
        VarContext<T> c =
                this.suspendedExecutionStack(toRestore.suspendedExecutionStack());

        if (restoreLocalsAndStack) {
            c = c.locals(toRestore.locals());
            if (edgeKey == ExitMap.KEY_NORM_TERM) {
                // restore the result stack on the normal termination only.
                c =
                        c.exprResultStack(toRestore.exprResultStack(),
                                          toRestore.exprResultStackNodeEntry());
            }
        }
        return c;
    }

    /**
     * Get the stack of maps from finally entry edge keys to abstract values.
     * 
     * @return the stack of maps from finally entry edge keys to abstract values.
     */
    public SuspendedExecutionStack<T> suspendedExecutionStack() {
        return suspendedExecutionStack;
    }

    /**
     * Pop first result off the suspended execution stack.
     * 
     * @return Var context with one suspended execution popped off
     */
    public VarContext<T> popSuspendedExecutionStack() {
        return suspendedExecutionStack(suspendedExecutionStack.pop());
    }

    /**
     * Pop results off the suspended execution stack until the size
     * is no more than <code>depth</code>
     * 
     * @return Var context with depth no greater than depth.
     */
    public VarContext<T> popSuspendedExecutionStackToDepth(int depth) {
        if (depth < 0) {
            throw new IllegalArgumentException("Depth must be non-negative: "
                    + depth);
        }
        if (depth == 0) {
            return suspendedExecutionStack(SuspendedExecutionStack.<T> emptyStack());
        }
        if (this.suspendedExecutionStack == null) {
            // nothing to pop, and don't complain
            return this;
        }
        if (depth >= this.suspendedExecutionStack().size()) {
            if (depth > this.suspendedExecutionStack().size()) {
                throw new InternalCompilerError("Stack not deep enough! should be "
                        + depth
                        + " but is "
                        + this.suspendedExecutionStack().size());
            }
            return this;
        }
        return popSuspendedExecutionStack().popSuspendedExecutionStackToDepth(depth);
    }

    /**
     * Push suspended execution map
     * 
     * @param m
     *            value to push
     * @param fb
     *            finally block associated with the value being pushed
     * 
     * @return Var context with the suspended execution map pushed onto the stack
     */
    public VarContext<T> pushSuspendedExecutionStack(Map<EdgeKey, T> m, Block fb) {
        return suspendedExecutionStack(suspendedExecutionStack.push(m, fb));
    }

    /**
     * @return the first result on the suspended execution stack
     */
    public Map<EdgeKey, T> peekSuspendedExecutionStack() {
        return suspendedExecutionStack.peek();
    }

    /**
     * Add a new local variable to the context
     * 
     * @param name
     *            name of the local
     * @param absVal
     *            abstract value for the local
     * @return Copy of <code>this</code> with the new local variable added
     */
    public VarContext<T> addLocal(String name, T absVal) {
        if (absVal == null) throw new InternalCompilerError("null AbsVal");
        if (this.locals.containsKey(name)
                && absVal.equals(this.locals.get(name))) {
            return this;
        }
        Map<String, T> newLocals = new LinkedHashMap<String, T>(this.locals);
        newLocals.put(name, absVal);
        VarContext<T> copy = this.copy();
        copy.locals = newLocals;
        return hashCons(copy);
    }

    /**
     * Only call this through AnalysisUtil.addLocations
     * 
     * AbsVal for abstract locations only increase, they never get replaced...
     * 
     * @param abstractLocations
     *            locations to add
     * @param absVal
     *            abstract value for each element of the set of locations
     */
    protected final VarContext<T> addLocations(
            Set<AbstractLocation> abstractLocations, T absVal) {
        if (absVal == null) throw new InternalCompilerError("null AbsVal");
        if (!TRACK_HEAP_LOCATIONS) {
            return this;
        }
        return addLocations(this, abstractLocations, absVal);
    }

    /**
     * Add the locations with the upper bound of the existing abstract value (if
     * any) and <code>absVal</code>
     * 
     * @param abstractLocations
     *            locations to add
     * @param absVal
     *            abstract value for each element of the set of locations
     */
    protected VarContext<T> addLocationsImpl(
            Set<AbstractLocation> abstractLocations, T absVal) {
        if (VarContextDataFlow.DONT_TRACK_BOTTOM && absVal.isBottom()) {
            // the policy is bottom, so there is no change.
            return this;
        }
        Map<AbstractLocation, T> newLocations =
                new LinkedHashMap<AbstractLocation, T>(this.locations);
        for (AbstractLocation al : abstractLocations) {
            newLocations.put(al,
                             valUpperBound(newLocations.get(al), absVal, false));
        }
        VarContext<T> copy = this.copy();
        copy.locations = newLocations;
        return copy;
    }

    /**
     * Swap the locations in <code>this</code> for the given
     * 
     * @param newLocations
     *            Map of abstract locations to abstract values to set into
     *            <code>this</code>
     * @return copy of <code>this</code> with the new abstract locations and
     *         values
     */
    public VarContext<T> locations(Map<AbstractLocation, T> newLocations) {
        if (!TRACK_HEAP_LOCATIONS) {
            return this;
        }
        VarContext<T> copy = this.copy();
        copy.locations = newLocations;
        return hashCons(copy);
    }

    /**
     * @return map of abstract locations to values
     */
    public Map<AbstractLocation, T> locations() {
        return this.locations;
    }

    @Override
    public boolean equals(Object o) {
        if (this == o) return true;
        if (o instanceof VarContext<?>) {
            @SuppressWarnings("unchecked")
            // cannot check instanceof for generics at runtime
            VarContext<T> that = (VarContext<T>) o;

            if (this.TRACK_HEAP_LOCATIONS != that.TRACK_HEAP_LOCATIONS) {
                throw new InternalCompilerError("Inconsistent VarContexts on TRACK_HEAP_LOCATIONS. Should be same for all VarContexts in an analysis");
            }

            return this.locals.equals(that.locals)
                    && this.locations.equals(that.locations)
                    && (this.returnResult == that.returnResult || (this.returnResult != null && this.returnResult.equals(that.returnResult)))
                    && (this.exprResultStack == that.exprResultStack || (this.exprResultStack != null && this.exprResultStack.equals(that.exprResultStack)))
                    && (this.suspendedExecutionStack == that.suspendedExecutionStack || (this.suspendedExecutionStack != null && this.suspendedExecutionStack.equals(that.suspendedExecutionStack)))
                    && (this.exprResultStackNodeEntry == that.exprResultStackNodeEntry || (this.exprResultStackNodeEntry != null && this.exprResultStackNodeEntry.equals(that.exprResultStackNodeEntry)));
        }
        return false;
    }

    @Override
    public int hashCode() {
        if (needsHashCode) {
            hashCode =
                    this.locals.hashCode()
                            ^ this.locations.hashCode()
                            ^ (this.returnResult == null ? 842
                                    : this.returnResult.hashCode())
                            ^ (this.exprResultStack == null ? 4898
                                    : this.exprResultStack.hashCode())
                            ^ (this.exprResultStackNodeEntry == null ? 4898
                                    : this.exprResultStackNodeEntry.hashCode())
                            ^ (this.suspendedExecutionStack == null ? 4898
                                    : this.suspendedExecutionStack.hashCode());
            needsHashCode = false;
        }
        return hashCode;
    }

    /**
     * Print the argument as an {@link Object}
     * @param o object to print
     * @return String for the given object
     */
    protected static String printAsObj(Object o) {
        if (o == null) {
            return "JAVA_NULL";
        }
        else {
            return o.toString();
        }
    }

    @Override
    public String toString() {
        return printAsObj(this.locals) + " "
                + (this.TRACK_HEAP_LOCATIONS ? printAsObj(this.locations) : "")
                + " retResult:" + printAsObj(this.returnResult)
                + " exprResultStack:" + printAsObj(this.exprResultStack)
                + " suspendedExceptionStack: "
                + printAsObj(this.suspendedExecutionStack);
    }

    /**
     * Get the abstract value for the given location
     * 
     * @param l
     *            abstract location to get the value for
     * @return abstract value for <code>l</code>
     */
    public T getLocationAbsVal(AbstractLocation l) {
        if (!this.TRACK_HEAP_LOCATIONS) {
            return this.DEFAULT_HEAP_LOCATION_VALUE;
        }
        return locations.get(l);
    }

    /**
     * Get the upper bound of the values for a set of locations. Only call this
     * via AnalaysisUtil.getLocationAbsVal.
     * 
     * @param abstractLocations
     *            set of abstract location to get the upper bound for
     *            
     * @return the upper bound of the values for <code>abstractLocations</code>
     */
    T getLocationAbsValBounded(Set<AbstractLocation> abstractLocations) {
        if (!this.TRACK_HEAP_LOCATIONS) {
            return this.DEFAULT_HEAP_LOCATION_VALUE;
        }
        T absVal = null;
        for (AbstractLocation al : abstractLocations) {
            absVal = valUpperBound(absVal, getLocationAbsVal(al), false);
        }
        return absVal;
    }

    /**
     * Check whether a local with <code>localName</code> is in the variable context
     * @param localName name of the local to check for
     * @return true if the local exists in <code>this</code>
     */
    public boolean hasLocalAbsVal(String localName) {
        return locals.containsKey(localName);
    }

    /**
     * Get the value for the local name
     * 
     * @param localName
     *            name of the local
     * @param localType
     *            {@link Type} of the local
     * @return The abstract value for the local
     */
    public T getLocalAbsVal(String localName, Type localType) {
        if (locals.containsKey(localName)) {
            return locals.get(localName);
        }
        // there is no local by that name.
        // This may not be a bug, due to the possibility of dead code
        return getDefaultLocalAbsVal(localName, localType);
    }

    /**
     * Get the default value for local variables
     * 
     * @param localName
     *            name of the local
     * @param localType
     *            {@link Type} of the local
     * @return The abstract value for the local
     */
    protected T getDefaultLocalAbsVal(String localName, Type localType) {
        // SC: hack to get through test cases.
        return this.bottomAbsVal;
        // SC: throw new InternalCompilerError("No local " + localName + " varContext is " + this);
    }

    /**
     * Compute the {@link VarContext} that is the join of all the elements of
     * <code>items</code>
     * 
     * @param items
     *            list of {@link VarContext} to join
     * @return join of all the elements of <code>items</code>
     */
    public static <T extends AbstractValue<T>> VarContext<T> join(
            List<VarContext<T>> items) {
        return join(items, false, false, false);
    }

    /**
     * Compute the {@link VarContext} that is the join of all the elements of
     * <code>items</code>
     * 
     * @param items
     *            list of {@link VarContext} to join
     * @param extendByOneIfNeeded
     *            if true can add a bottom value to the expression stack
     * @param clearExprStacks
     *            clear all expression stacks before computing the join
     * @return join of all the elements of <code>items</code>
     */
    public static <T extends AbstractValue<T>> VarContext<T> join(
            List<VarContext<T>> items, boolean extendByOneIfNeeded,
            boolean clearExprStacks, boolean clearSuspendedExecutionContexts) {
        // join all the AbsVals
        VarContext<T> output = null;
        for (VarContext<T> absVal : items) {
            if (absVal == null) continue;
            if (clearExprStacks) {
                absVal = absVal.clearExprResultStack();
            }
            if (clearSuspendedExecutionContexts) {
                absVal = absVal.popSuspendedExecutionStackToDepth(0);
            }
            if (output == null) {
                output = absVal;
            }
            else {
                if (extendByOneIfNeeded
                        && absVal.exprResultStack().size() < output.exprResultStack()
                                                                   .size()) {
                    absVal =
                            absVal.pushExprResult(absVal.bottomAbsVal,
                                                  "extendStackAsNeeded");
                }
                if (extendByOneIfNeeded
                        && output.exprResultStack().size() < absVal.exprResultStack()
                                                                   .size()) {
                    output =
                            output.pushExprResult(absVal.bottomAbsVal,
                                                  "extendStackAsNeeded");
                }
                output = VarContext.upperBound(output, absVal);
            }
        }

        return output;

    }

    /* **********************
     * Memoization methods
     */

    private static final boolean HASH_CONS_VARCONTEXTS = true;
    @SuppressWarnings("rawtypes")
    // static = no generics
    private static Map<String, Map<VarContext, SoftReference<VarContext>>> hashCons =
            new HashMap<String, Map<VarContext, SoftReference<VarContext>>>();
    @SuppressWarnings("rawtypes")
    // static = no generics
    private static Map<LeqInput, Boolean> memoizedLeqResults =
            new HashMap<VarContext.LeqInput, Boolean>();
    @SuppressWarnings("rawtypes")
    // static = no generics
    private static Map<UpperBoundInput, VarContext> memoizedUpperBoundResults =
            new HashMap<VarContext.UpperBoundInput, VarContext>();
    @SuppressWarnings("rawtypes")
    // static = no generics
    private static Map<AddLocationsInput, VarContext> memoizedAddLocationsResults =
            new HashMap<VarContext.AddLocationsInput, VarContext>();

    /**
     * Check the memo and return that copy if it exists or add <code>c</code>
     * and return it
     * 
     * @param c
     *            var context to memoize
     * @return an equivalent var context
     */
    @SuppressWarnings({ "rawtypes", "unchecked" })
    // static = no generics
    protected static <T extends AbstractValue<T>> VarContext<T> hashCons(
            VarContext<T> c) {
        if (!HASH_CONS_VARCONTEXTS) return c;
        if (c == null) return c;
        Map<VarContext, SoftReference<VarContext>> m =
                hashCons.get(c.analysisName);
        if (m == null) {
            m = new WeakHashMap<VarContext, SoftReference<VarContext>>();
            hashCons.put(c.analysisName, m);
        }
        SoftReference<VarContext> ret = m.get(c);
        if (ret == null) {
            ret = new SoftReference<VarContext>(c);
            m.put(c, ret);
        }
        return ret.get();
    }

    /**
     * Clear all values for the given analysis
     * 
     * @param analysisName name of analysis
     */
    public static void clearHashCons(String analysisName) {
        hashCons.remove(analysisName);
    }

    /**
     * Class used to memoize leq computations
     * 
     * @param <T>
     *            type of abstract value
     */
    private static class LeqInput<T extends AbstractValue<T>> {

        /**
         * context to test less than or equal to
         */
        final VarContext<T> c1;
        /**
         * context to test less than or equal to
         */
        final VarContext<T> c2;
        /**
         * domain to compute leq over
         */
        final Set<AbstractLocation> domain;

        /**
         * Create a class representing <code>c1</code> leq <code>c2</code>
         * 
         * @param domain
         *            domain to compute leq over
         */
        public LeqInput(VarContext<T> c1, VarContext<T> c2,
                Set<AbstractLocation> domain) {
            this.c1 = c1;
            this.c2 = c2;
            this.domain = domain;
        }

        @Override
        public int hashCode() {
            return c1.hashCode() ^ c2.hashCode() ^ domain.hashCode();
        }

        @Override
        public boolean equals(Object obj) {
            if (this == obj) return true;
            if (obj == null) return false;
            if (!(obj instanceof LeqInput)) return false;
            LeqInput<?> other = (LeqInput<?>) obj;
            return this.c1 == other.c1 && this.c2 == other.c2
                    && domain.equals(other.domain);
        }
    }

    /**
     * Compute <code>c1</code> leq <code>c2</code> over the given locations
     * 
     * @param c1
     *            var context
     * @param c2
     *            var context
     * @param locationDomain
     *            Only compute leq over these locations
     * @return true if <code>c1</code> <= <code>c2</code> on the given domain
     */
    @SuppressWarnings("unused")
    public static <T extends AbstractValue<T>> boolean leq(VarContext<T> c1,
            VarContext<T> c2, Set<AbstractLocation> locationDomain) {
        if (c2 == null) return false;
        if (c1 == null) return true;
        if (HASH_CONS_VARCONTEXTS) {
            LeqInput<T> leqInput =
                    new LeqInput<T>(hashCons(c1), hashCons(c2), locationDomain);
            Boolean res = memoizedLeqResults.get(leqInput);
            if (res != null) {
                return res;
            }
            res = c1.leq(c2, locationDomain);
            memoizedLeqResults.put(leqInput, res);
            return res;
        }

        // Could change the static HASH_CONS_VARCONTEXTS so leave this
        return c1.leq(c2, locationDomain);
    }

    /**
     * Add locations to the given context
     * 
     * @param c
     *            context to add to
     * @param abstractLocations
     *            locations to add
     * @param absVal
     *            value for the added locations
     * @return A var context with the locations added
     */
    @SuppressWarnings("unused")
    private static <T extends AbstractValue<T>> VarContext<T> addLocations(
            VarContext<T> c, Set<AbstractLocation> abstractLocations, T absVal) {
        if (HASH_CONS_VARCONTEXTS) {
            AddLocationsInput ubInput =
                    new AddLocationsInput(hashCons(c),
                                          abstractLocations,
                                          absVal);
            @SuppressWarnings("unchecked")
            // static = no generics
            VarContext<T> res = memoizedAddLocationsResults.get(ubInput);
            if (res != null) {
                return res;
            }
            res = hashCons(c.addLocationsImpl(abstractLocations, absVal));
            memoizedAddLocationsResults.put(ubInput, res);
            return res;
        }

        // Could change the static HASH_CONS_VARCONTEXTS so leave this
        return c.addLocationsImpl(abstractLocations, absVal);
    }

    /**
     * Class to memoize abstract locations
     */
    private static class AddLocationsInput {
        /**
         * variable context to add the locations to
         */
        final VarContext<?> ctxt;
        /**
         * locations to add
         */
        final Set<AbstractLocation> abstractLocations;
        /**
         * value for each element of the added location set
         */
        final AbstractValue<?> absVal;
        /**
         * only compute the hash code once
         */
        final int memoizedHashCode;

        /**
         * Construct a class representing the memoization of the added locations
         * 
         * @param c1
         *            context to add to
         * @param abstractLocations
         *            locations to add
         * @param absVal
         *            value to add for the locations
         */
        public AddLocationsInput(VarContext<?> c1,
                Set<AbstractLocation> abstractLocations, AbstractValue<?> absVal) {
            this.ctxt = c1;
            this.abstractLocations = abstractLocations;
            this.absVal = absVal;
            this.memoizedHashCode =
                    ctxt.hashCode() ^ abstractLocations.hashCode()
                            ^ absVal.hashCode();
        }

        @Override
        public int hashCode() {
            return memoizedHashCode;
        }

        @Override
        public boolean equals(Object obj) {
            if (this == obj) return true;
            if (obj == null) return false;
            if (!(obj instanceof AddLocationsInput)) return false;
            AddLocationsInput other = (AddLocationsInput) obj;
            if (this.ctxt != other.ctxt) return false;
            if (this.memoizedHashCode != other.memoizedHashCode) return false;

            if (abstractLocations == null) {
                if (other.abstractLocations != null) return false;
            }
            else if (!abstractLocations.equals(other.abstractLocations))
                return false;
            if (ctxt == null) {
                if (other.ctxt != null) return false;
            }
            else if (!ctxt.equals(other.ctxt)) return false;
            if (absVal == null) {
                if (other.absVal != null) return false;
            }
            else if (!absVal.equals(other.absVal)) return false;
            return true;
        }

    }

    /**
     * Compute the upper bound of <code>c1</code> and <code>c2</code>
     * 
     * @param c1
     *            variable context
     * @param c2
     *            variable context
     * @return the upper bound of <code>c1</code> and <code>c2</code>
     */
    @SuppressWarnings("unused")
    public static <T extends AbstractValue<T>> VarContext<T> upperBound(
            VarContext<T> c1, VarContext<T> c2) {
        if (c1 == null) return c2;
        if (c2 == null) return c1;
        if (HASH_CONS_VARCONTEXTS) {
            UpperBoundInput<T> ubInput =
                    new UpperBoundInput<T>(hashCons(c1), hashCons(c2));

            @SuppressWarnings("unchecked")
            // static = no generics
            VarContext<T> res = memoizedUpperBoundResults.get(ubInput);
            if (res != null) {
                return res;
            }
            res = hashCons(c1.upperBound(c2));
            memoizedUpperBoundResults.put(ubInput, res);
            return res;
        }

        // Could change the static HASH_CONS_VARCONTEXTS so leave this
        return c1.upperBound(c2);
    }

    /**
     * Class used to memoize upper bound computations
     * 
     * @param <T> abstract value type
     */
    private static class UpperBoundInput<T extends AbstractValue<T>> {
        final VarContext<T> c1;
        final VarContext<T> c2;

        /**
         * Create a class representing the upper bound of <code>c1</code> and <code>c2</code>
         */
        public UpperBoundInput(VarContext<T> c1, VarContext<T> c2) {
            this.c1 = c1;
            this.c2 = c2;
        }

        @Override
        public int hashCode() {
            final int prime = 31;
            int result = 1;
            result = prime * result + ((c1 == null) ? 0 : c1.hashCode());
            result = prime * result + ((c2 == null) ? 0 : c2.hashCode());
            return result;
        }

        @Override
        public boolean equals(Object obj) {
            if (this == obj) return true;
            if (obj == null) return false;
            if (!(obj instanceof UpperBoundInput)) return false;
            UpperBoundInput<?> other = (UpperBoundInput<?>) obj;
            return this.c1 == other.c1 && this.c2 == other.c2;
        }
    }

    /**
     * Record the fact that analysis has entered this node
     */
    public VarContext<T> recordNodeEntry(Term node) {
        int size = exprResultStack.size();
        Map<Term, Integer> m = this.exprResultStackNodeEntry;
        if (m == null) {
            m = new LinkedHashMap<Term, Integer>();
            m.put(node, size);
        }
        else if (m.containsKey(node) && m.get(node) == size) {
            // no change!
            return this;
        }
        else {
            //  we need to record the node entry
            m = new LinkedHashMap<Term, Integer>(m);
            m.put(node, size);
        }
        return this.exprResultStack(this.exprResultStack, m);
    }

    /**
     * Record the fact that analysis has entered this node
     */
    public VarContext<T> recordNodeExit(Term node) {
        if (this.exprResultStackNodeEntry == null
                || !this.exprResultStackNodeEntry.containsKey(node)) {
            return this;
        }
        Map<Term, Integer> m =
                new LinkedHashMap<Term, Integer>(this.exprResultStackNodeEntry);
        m.remove(node);
        return this.exprResultStack(this.exprResultStack, m);
    }

    /**
     * Return number of elements on stack since entry to node was recorded.
     */
    public Integer depthToNodeEntry(Term node) {
        if (this.exprResultStackNodeEntry != null) {
            if (this.exprResultStackNodeEntry.containsKey(node)) {
                int n = this.exprResultStackNodeEntry.get(node);
                return this.exprResultStack.size() - n;
            }
        }
        return null;
    }

}
