package accrue.analysis.interprocvarcontext;

import java.util.Collection;
import java.util.Collections;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import polyglot.ast.Call;
import polyglot.ast.ConstructorCall;
import polyglot.ast.ConstructorDecl;
import polyglot.ast.Expr;
import polyglot.ast.Formal;
import polyglot.ast.New;
import polyglot.ast.Node;
import polyglot.ast.ProcedureDecl;
import polyglot.ast.Special;
import polyglot.ast.Term;
import polyglot.main.Report;
import polyglot.types.ClassType;
import polyglot.types.ConstructorInstance;
import polyglot.types.MethodInstance;
import polyglot.types.ProcedureInstance;
import polyglot.types.SemanticException;
import polyglot.types.Type;
import polyglot.util.InternalCompilerError;
import accrue.AccrueExtensionInfo;
import accrue.analysis.ext.AccrueExt_c;
import accrue.analysis.ext.ExtCall;
import accrue.analysis.ext.ExtConstructorDecl;
import accrue.analysis.ext.ExtTerm;
import accrue.analysis.interprocanalysis.AbstractLocation;
import accrue.analysis.interprocanalysis.AnalysisContext;
import accrue.analysis.interprocanalysis.AnalysisUnit;
import accrue.analysis.interprocanalysis.AnalysisUtil;
import accrue.analysis.interprocanalysis.DataFlowNodeIdentifier;
import accrue.analysis.interprocanalysis.ExitMap;
import accrue.analysis.interprocanalysis.ExitMap.Key;
import accrue.analysis.interprocanalysis.Ordered;
import accrue.analysis.interprocanalysis.WorkQueue;
import accrue.analysis.pointer.HContext;
import accrue.analysis.preciseExceptions.ThrowableType;
import accrue.analysis.signatures.AnalysisSignatures;

/**
 * Abstract utility class for performing an interprocedural analysis with a
 * variable context.
 * 
 * @param <A>
 *            Type of analysis results
 * @param <T>
 *            Value type for analysis items in the context
 */
public abstract class AnalysisUtilVarContext<A extends Ordered<A>, T extends AbstractValue<T>>
        extends AnalysisUtil<A> {
    /*
     * Record the set of abstraction locations read and written during analysis 
     */
    private Set<AbstractLocation> readLocations;
    private Set<AbstractLocation> writeLocations;

    /**
     * Should we track java.lang.Error <code>ExitMap.key</code>s?
     */
    protected boolean trackErrors = true;

    /**
     * Create a new utility class
     * 
     * @param workQueue
     *            Queue of analysis units
     * @param currentAnalysisUnit
     *            Current analysis unit from the queue
     * @param extInfo
     *            compiler analysis unit
     */
    public AnalysisUtilVarContext(WorkQueue<A> workQueue,
            AnalysisUnit currentAnalysisUnit, AccrueExtensionInfo extInfo) {
        super(workQueue, currentAnalysisUnit, extInfo);
        this.readLocations = new LinkedHashSet<AbstractLocation>();
        this.writeLocations = new LinkedHashSet<AbstractLocation>();
    }

    /**
     * 
     * @return Abstract locations read during analysis
     */
    Set<AbstractLocation> readLocations() {
        return this.readLocations;
    }

    /**
     * @return Abstract locations written during analysis
     */
    Set<AbstractLocation> writeLocations() {
        return this.writeLocations;
    }

    /**
     * Process a call to <code>mi</code> with {@link VarContext}
     * <code>input</code>.
     * 
     * @param mi
     *            method to analyze
     * @param input
     *            variable context before analyzing the method
     * @param n
     *            the call to the method
     * @param callSite
     *            AST node (and context) for the call site
     * 
     * @return new map of variables to their values after the analysis
     * @throws SemanticException
     *             if analysis fails
     */
    public FinalVarContext<T> call(MethodInstance mi, VarContext<T> input,
            Call n, DataFlowNodeIdentifier callSiteNode)
            throws SemanticException {
        boolean isStaticCall = mi.flags().isStatic();
        if (isStaticCall) {
            return callNonVirtual(mi,
                                  workQueue.factory()
                                           .createAnalysisContext(this,
                                                                  mi,
                                                                  null,
                                                                  n),
                                  null,
                                  null,
                                  input,
                                  n);
        }
        else {
            // this is a non-static call (and may be
            // a virtual call, or a call to super.m())
            // loop over the possible receivers.
            Expr receiver = (Expr) n.target();
            Set<HContext> pointsTo = pointsTo(receiver);

            if (pointsTo == null) {
                throw new InternalCompilerError("No points to info for the receiver: "
                        + n);
            }

            // analyze all method implementations that may potentially be called, and
            // take an upper bound of the result.
            FinalVarContext<T> res = this.emptyFinalVarContext();
            for (HContext o : pointsTo) {
                // analyze the implementing method
                Type receiverType = o.type();
                MethodInstance omi = null;
                if (receiver instanceof Special
                        && ((Special) receiver).kind() == Special.SUPER) {
                    // it's a call to super.m(). Don't dynamically dispatch.
                    omi = mi;
                }
                else if (receiverType != null) {
                    // it's a virtual call, so find
                    // the appropriate implementing method.
                    omi =
                            extInfo.typeSystem()
                                   .findImplementingMethod(receiverType.toClass(),
                                                           mi);
                }
                else {
                    //System.err.println(" *** no receiver for virtual method invocation to " + mi + " " + n.position());
                    throw new InternalCompilerError("no receiver for virtual method invocation to "
                                                            + mi,
                                                    n.position());
                }
                if (omi == null) {
                    // no implementing method!
                    // we'll see if we have a signature for mi
                    omi = mi;
                }
                res =
                        (FinalVarContext<T>) res.upperBound(callNonVirtual(omi,
                                                                           workQueue.factory()
                                                                                    .createAnalysisContext(this,
                                                                                                           omi,
                                                                                                           o,
                                                                                                           n),
                                                                           o,
                                                                           null,
                                                                           input,
                                                                           n));
            }
            if (pointsTo.isEmpty()) {
                // XXX MISSING RECIEVER COMMENT
                // System.err.println(" *** Receiver doesn't point to anything! May be a bug in the program? ");
                // System.err.println("     " + n + " " + mi.container()+"."+ mi.name() + "  at " + n.position());
                res =
                        this.getAnalysisForMissingReceiver(mi,
                                                           input,
                                                           n,
                                                           callSiteNode);
            }

            return res;
        }
    }

    /**
     * Empty variable context
     */
    private FinalVarContext<T> BOTTOM =
            new FinalVarContext<T>(Collections.<Key, VarContext<T>> emptyMap(),
                                   Collections.<ClassType> emptySet());

    /**
     * @return an empty variable context
     */
    public FinalVarContext<T> emptyFinalVarContext() {
        return BOTTOM;
    }

    /**
     * Create a {@link FinalVarContext} context from the given
     * {@link VarContext} for normal termination
     * 
     * @param normalTermination {@link VarContext} for normal termination
     * @return {@link FinalVarContext} just containing the normal termination map
     */
    public FinalVarContext<T> createFinalVarContext(
            VarContext<T> normalTermination) {
        return (FinalVarContext<T>) emptyFinalVarContext().normalTermination(normalTermination);
    }

    /**
     * Process a call to <code>ci</code> created with <code>new</code> with {@link VarContext}
     * <code>input</code>.
     * 
     * @param ci
     *            constructor to analyze
     * @param input
     *            variable context before analyzing the method
     * @param receiverAbsVal
     *            The abstract value to use for the newly created object, i.e.,
     *            the abstract value that "this" will map to in the invoked constructor.            
     * @param n
     *            the call to the constructor
     * @param callSite
     *            AST node (and context) for the call site
     *            
     * @return new map of variables to their values after the analysis
     * @throws SemanticException
     *             if analysis fails
     */
    public FinalVarContext<T> call(ConstructorInstance ci, VarContext<T> input,
            T receiverAbsVal, New n, DataFlowNodeIdentifier callSiteNode)
            throws SemanticException {
        if (input == null) return this.emptyFinalVarContext();
        Set<HContext> pointsTo = pointsTo(n);
        if (pointsTo.size() == 1) {
            HContext receiver = pointsTo.iterator().next();

            return callNonVirtual(ci,
                                  workQueue.factory()
                                           .createAnalysisContext(this,
                                                                  ci,
                                                                  receiver,
                                                                  n),
                                  receiver,
                                  receiverAbsVal,
                                  input,
                                  n);
        }
        else if (pointsTo.isEmpty()) {
            // XXX MISSING RECIEVER COMMENT
            // System.err.println(" *** Receiver of new doesn't point to anything! May be a bug in the program? ");
            // System.err.println("     " + n + " " + ci.container()+"."+ ci.signature() + "  at " + n.position());
            return this.getAnalysisForMissingReceiver(ci,
                                                      input,
                                                      n,
                                                      callSiteNode);
        }
        else {
            throw new InternalCompilerError("Invocation to constructor does not have unique pointsto: "
                                                    + pointsTo,
                                            n.position());
        }
    }

    /**
     * Process a call to <code>ci</code> with {@link VarContext}
     * <code>input</code>. This is different from call(ConstructorInstance ci, 
     * VarContext<T> input, T receiverAbsVal, New n), which is used when a
     *  "new C(...)" expression is encountered. By contrast, this is used when
     *  a "this(...)" or "super(...)" constructor call is encountered.      
     * 
     * @param ci
     *            constructor to analyze
     * @param input
     *            variable context before analyzing the method
     * @param n
     *            the call to the constructor
     * @param callSite
     *            AST node (and context) for the call site
     *            
     * @return new map of variables to their values after the analysis
     * @throws SemanticException
     *             if analysis fails
     */
    public FinalVarContext<T> constructorCall(ConstructorInstance ci,
            VarContext<T> input, ConstructorCall n,
            DataFlowNodeIdentifier callSiteNode) throws SemanticException {
        if (input == null) return this.emptyFinalVarContext();
        ConstructorDecl cd =
                (ConstructorDecl) this.currentAnalysisUnit().codeNode();
        ExtConstructorDecl ext = (ExtConstructorDecl) AccrueExt_c.ext(cd);
        Set<HContext> pointsTo =
                pointsTo(ext.getThisNode(), this.currentContext(), this.extInfo);
        if (pointsTo.isEmpty()) {
            // XXX MISSING RECIEVER COMMENT
            // System.err.println(" *** Receiver of constructor doesn't point to anything! May be a bug in the program? ");
            // System.err.println("     " + n + " " + ci.container()+"."+ ci.signature() + "  at " + n.position());
            return this.getAnalysisForMissingReceiver(ci,
                                                      input,
                                                      n,
                                                      callSiteNode);
        }
        else {
            FinalVarContext<T> res = this.emptyFinalVarContext();
            for (HContext o : pointsTo) {

                res =
                        (FinalVarContext<T>) res.upperBound(callNonVirtual(ci,
                                                                           this.currentAnalysisUnit()
                                                                               .context(),
                                                                           o,
                                                                           input.getLocalAbsVal("this",
                                                                                                ci.container()),
                                                                           input,
                                                                           n));
            }
            return res;
        }
    }

    /**
     * Process a call to a non-virtual call to <code>pi</code> with
     * {@link VarContext} <code>input</code>.
     * 
     * @param pi
     *            call to analyze
     * @param calleeContext
     *            procedure analysis context
     * @param receiver
     *            abstract heap object for the callee
     * @param preCall
     *            variable context before analyzing the method
     * @param n
     *            the call to the procedure
     * 
     * @return new map of variables to their values after the analysis
     * @throws SemanticException
     *             if analysis fails
     */
    private FinalVarContext<T> callNonVirtual(ProcedureInstance pi,
            AnalysisContext calleeContext, HContext receiver, T receiverAbsVal,
            VarContext<T> preCall, Term n) throws SemanticException {
        if (Report.should_report(this.workQueue.factory().reportTopics(), 3)) {
            Report.report(2, this.workQueue.factory().analysisName()
                    + ": callNonVirtual " + pi);
        }

        if (preCall == null) {
            // no point in processing this...
            if (Report.should_report(this.workQueue.factory().reportTopics(), 4)) {
                Report.report(3, "Null input context, so skipping call to "
                        + pi);
            }

            return this.emptyFinalVarContext();
        }

        preCall = preCallNonVirtual(pi, calleeContext, preCall, n);

        int numArgs = pi.formalTypes().size();
        List<T> argAbsVals = preCall.peekExprResults(numArgs);
        // reverse the list of argDGFIs since they are given to us in stack order (i.e., last arg is at the top of the stack, and is in position 0).
        Collections.reverse(argAbsVals);
        preCall = preCall.popExprResults(numArgs);

        if (Report.should_report(this.workQueue.factory().reportTopics(), 4)) {
            Report.report(3, "   argAbsVals : " + argAbsVals);
        }

        if (pi instanceof MethodInstance) {
            // The receiver is on the expression stack.
            T t = preCall.peekExprResult();
            if (receiverAbsVal == null) {
                receiverAbsVal = t;
            }
            preCall = preCall.popExprResult();
        }
        else if (n instanceof New) {
            // the type node is on the expression stack.
            preCall = preCall.popExprResult();
        }

        SuspendedExecutionStack<T> precallSuspendedExecutionStack =
                preCall.suspendedExecutionStack();
        if (precallSuspendedExecutionStack == null) {
            precallSuspendedExecutionStack =
                    SuspendedExecutionStack.emptyStack();
        }
        VarContext<T> input = preCall.popSuspendedExecutionStackToDepth(0);

        // get the implementing method body to add the argument names...
        ProcedureDecl pd = (ProcedureDecl) workQueue.registrar().getCode(pi);
        AnalysisUnit callee = null;

        // compute the expected exits, in case the signature needs it.
        Set<ExitMap.Key> expectedExits = computeExpectedExits(n);

        boolean preparedCalleeContext = false;
        FinalVarContext<T> res;
        if (pd == null || pd.body() == null) {
            LibrarySignature<A, T> sig =
                    this.getSignatureForMissingCode(pi,
                                                    receiverAbsVal,
                                                    argAbsVals);
            if (sig != null) {
                res =
                        sig.process(pi,
                                    calleeContext,
                                    receiver,
                                    input,
                                    receiverAbsVal,
                                    argAbsVals,
                                    this,
                                    expectedExits,
                                    n);
                if (res == null)
                    throw new InternalCompilerError("Null returned by signature: "
                            + sig.getClass());
            }
            else {
                recordMissingCode(pi);
                res =
                        guessAnalysisForMissingCode(pi,
                                                    calleeContext,
                                                    receiver,
                                                    input,
                                                    receiverAbsVal,
                                                    argAbsVals,
                                                    expectedExits,
                                                    n);
                // restore caller context
                res = res.restoreContext(preCall, false);
                return res;
            }
        }
        else {
            // Create a new context appropriate for analyzing the method instance
            Map<String, T> newLocals = new LinkedHashMap<String, T>();
            if (receiverAbsVal != null && !pi.flags().isStatic()) {
                newLocals.put("this", receiverAbsVal);
            }

            if (pd.formals().size() != argAbsVals.size()) {
                throw new InternalCompilerError("Mismatched arguments");
            }
            for (int i = 0; i < argAbsVals.size(); i++) {
                Formal f = pd.formals().get(i);
                T arg = argAbsVals.get(i);
                newLocals.put(f.name(), arg);
            }
            VarContext<T> beforeCall =
                    input.locals(newLocals).clearExprResultStack();

            callee = new AnalysisUnit(pd, calleeContext);

            res = this.getAnalysisResultsFromWorkQueue(callee, beforeCall);

            if (maybeRecursiveCall(callee)) {
                res = this.handleRecursiveCall(res, beforeCall, callee);
            }
            preparedCalleeContext = true;

        }

        // join the return context and the normal termination context
        res =
                (FinalVarContext<T>) res.normalTermination(upperBound(res.normalTermination(),
                                                                      res.returnItem()));

        res = (FinalVarContext<T>) res.removeReturnItem();

        // restore caller context
        res = res.restoreContext(preCall, preparedCalleeContext);

        // restore the result stack on the normal termination only.
        if (res.normalTermination() != null) {
            VarContext<T> nt = res.normalTermination();

            // push the return value if there was one.
            if (pi instanceof MethodInstance) {
                MethodInstance mi = (MethodInstance) pi;
                if (!mi.returnType().isVoid()) {
                    // this method should have returned a result.
                    // it may not have, if we haven't actually got around to processing it yet.
                    T returnedResult = res.normalTermination().returnResult();
                    if (returnedResult == null) {
                        returnedResult = bottomAbstractValue();
                    }
                    nt = nt.pushExprResult(returnedResult, "returnX1-" + pi);
                }
            }

            nt = nt.clearReturnResult();

            res = (FinalVarContext<T>) res.normalTermination(nt);
        }

        return res;

    }

    /**
     * @param n
     *            {@link Term} on which to compute exit keys
     * @return Set of possible exit keys that can be reached from the given
     *         {@link Term}
     */
    protected Set<Key> computeExpectedExits(Term n) {
        Set<ExitMap.Key> expectedExits = new LinkedHashSet<ExitMap.Key>();
        expectedExits.add(ExitMap.KEY_NORM_TERM);
        ExtTerm extTerm = (ExtTerm) AccrueExt_c.ext(n);
        if (extTerm instanceof ExtCall) {
            ExtCall ex = (ExtCall) extTerm;
            if (!ex.canTerminateNormally(this.currentContext())) {
                // call cannot return normally, so set the expected exits correctly
                expectedExits.remove(ExitMap.KEY_NORM_TERM);
            }
        }
        for (ThrowableType tk : extTerm.throwTypes(typeSystem(),
                                                   this.currentContext())) {
            if (!trackErrors
                    && typeSystem().isSubtype(tk.type(), typeSystem().Error())) {
                // ignore Error
                continue;
            }
            expectedExits.add(ExitMap.exceptionKey(tk.type().toClass()));
        }
        return expectedExits;
    }

    /**
     * Get the analysis results for the given callee and variable context.
     * 
     * @param callee
     *            Code for a callee that is to be analyzed
     * @param beforeCall
     *            variable context before the call to the callee
     * @return new variable context after performing the analysis
     * @throws SemanticException
     *             thrown for an analysis error
     */
    protected abstract FinalVarContext<T> getAnalysisResultsFromWorkQueue(
            AnalysisUnit callee, VarContext<T> beforeCall)
            throws SemanticException;

    /**
     * Allow extensions a chance to modify the input before the analysis of a
     * non-virtual procedure call.
     * 
     * @param procedure
     *            to be called
     * @param calleeContext
     *            Procedure analysis context
     * @param input
     *            variable context before the call to the callee
     * @param n
     *            the call to the procedure
     */
    protected VarContext<T> preCallNonVirtual(ProcedureInstance pi,
            AnalysisContext calleeContext, VarContext<T> input, Term n) {
        return input;
    }

    /**
     * Subclasses can override to provide signature for missing code.
     * 
     * @param pi
     *            missing procedure instance
     * @param receiverAbsVal
     *            analyis context value for the receiver
     * @param argAbsVals
     *            list of values for the procedure arguments
     */
    protected LibrarySignature<A, T> getSignatureForMissingCode(
            ProcedureInstance pi, T receiverAbsVal, List<T> argAbsVals) {
        List<String> signatureAnalysisNames = this.signatureAnalysisNames();
        for (String analysisName : signatureAnalysisNames) {
            AnalysisSignatures sigs = extInfo.getAnalysisSignatures();
            if (sigs != null) {
                SignatureRepository<T> r =
                        sigs.signatureRepository(analysisName);
                if (r != null) {
                    @SuppressWarnings("unchecked")
                    LibrarySignature<A, T> ls =
                            (LibrarySignature<A, T>) r.lookup(pi);
                    if (ls != null) return ls;
                }
            }
        }
        return null;
    }

    /**
     * Subclasses can override as a stop gap measure before they have signature.
     * 
     * @param pi
     *            missing procedure
     * @param calleeContext
     *            procedure context
     * @param receiver
     *            receiver heap object
     * @param input
     *            variable context before analysis
     * @param receiverAbsVal
     *            value for the receiver
     * @param argAbsVals
     *            list of values for the procedure arguments
     * @param expectedExits
     *            set of expected exit keys
     * @param node
     *            calling node
     * @return New variable context updated from the input during analysis
     */
    protected FinalVarContext<T> guessAnalysisForMissingCode(
            ProcedureInstance pi, AnalysisContext calleeContext,
            HContext receiver, VarContext<T> input, T receiverAbsVal,
            List<T> argAbsVals, Set<ExitMap.Key> expectedExits, Node node) {
        System.err.println("sig for procedure = " + pi + "apparently not found");
        throw new UnsupportedOperationException("Subclass can override to guess analysis for missing code: "
                + this.getClass());
    }

    /**
     * Provide a hook for subclasses to implementation functionality when
     * procedure pi is called (e.g., "e.m()") but there is an empty points to
     * set for the receiver expression.
     * 
     * @param pi
     *            called procedure
     * @param input
     *            variable context before analysis
     * @param n
     *            calling term
     * @param callSite
     *            AST node (and context) for the call site
     */
    protected FinalVarContext<T> getAnalysisForMissingReceiver(
            ProcedureInstance pi, VarContext<T> input, Term n,
            DataFlowNodeIdentifier callSiteNode) {
        int numArgs = pi.formalTypes().size();
        List<T> argAbsVals = input.peekExprResults(numArgs);
        // reverse the list of argDGFIs since they are given to us in stack order (i.e., last arg is at the top of the stack, and is in position 0).
        Collections.reverse(argAbsVals);
        input = input.popExprResults(numArgs);

        T receiverAbsVal = this.bottomAbstractValue();
        if (pi instanceof MethodInstance || n instanceof New) {
            receiverAbsVal = input.peekExprResult();
            input = input.popExprResult();
        }

        Set<ExitMap.Key> expectedExits = computeExpectedExits(n);
//        System.out.println("expectedExits for missing receiver " + n + " :: "
//                + expectedExits);

        FinalVarContext<T> res =
                this.guessAnalysisForMissingReceiver(pi,
                                                     input,
                                                     receiverAbsVal,
                                                     argAbsVals,
                                                     expectedExits,
                                                     callSiteNode);

        VarContext<T> nt = res.normalTermination();
        // push the return value if there was one.
        if (pi instanceof MethodInstance) {
            MethodInstance mi = (MethodInstance) pi;
            if (!mi.returnType().isVoid()) {
                // this method should have returned a result.
                // it may not have, if we haven't actually got around to processing it yet.
                T returnedResult = res.normalTermination().returnResult();
                nt = nt.pushExprResult(returnedResult, "returnX1-" + pi);
            }
        }
        nt = nt.clearReturnResult();
        res = (FinalVarContext<T>) res.normalTermination(nt);
        return res;
    }

    /** 
     * Subclasses should override as a stop gap measure if the receiver is missing, 
     * i.e., if the points to set of the receiver expression is empty.
     *
     * @param pi
     *            missing procedure
     * @param input
     *            variable context before analysis   
     * @param receiverAbsVal
     *            abstract value for the receiver
     * @param argAbsVals
     *            list of abstract values for the procedure arguments
     * @param expectedExits
     *            set of expected exit keys
     * @param callSite
     *            AST node (and context) for the call site
     *            
     * @return New variable context updated from the input during analysis
     */
    protected abstract FinalVarContext<T> guessAnalysisForMissingReceiver(
            ProcedureInstance pi, VarContext<T> input, T receiverAbsVal,
            List<T> argAbsVals, Set<ExitMap.Key> expectedExits,
            DataFlowNodeIdentifier callSiteNode);

    /**
     * The call to callee is potentially recursive.
     * 
     * @param res
     *            Variable context resulting from calling the calles
     * @param beforeCall
     *            variable context before analysis
     * @param callee
     *            Recursive procedure
     */
    protected FinalVarContext<T> handleRecursiveCall(FinalVarContext<T> res,
            VarContext<T> beforeCall, AnalysisUnit callee) {
        // by default, do nothing
        return res;
    }

    @Override
    public String analysisName() {
        return workQueue().factory().analysisName();
    }

    /**
     * @return List containing the analysis names
     */
    protected List<String> signatureAnalysisNames() {
        return Collections.singletonList(this.analysisName());
    }

    /**
     * Compute the abstract values for the given abstract locations
     * @param c variable context
     * @param locs set of abstract locations
     * @return abstract values for the given abstract locations
     */
    public T getLocationAbsVal(VarContext<T> c, Set<AbstractLocation> locs) {
        recordReads(locs);
        if (c != null) {
            return c.getLocationAbsValBounded(locs);
        }
        return null;
    }

    /**
     * Record a location that has been read
     * 
     * @param loc
     *            location that was read
     */
    public void recordRead(AbstractLocation loc) {
        recordReads(Collections.singleton(loc));
    }

    public void recordReads(Collection<AbstractLocation> locs) {
        readLocations.addAll(locs);
    }

    /**
     * Record a location that has been written
     * 
     * @param loc
     *            location that was written
     */
    public void recordWrite(AbstractLocation loc) {
        recordWrites(Collections.singleton(loc));
    }

    public void recordWrites(Collection<AbstractLocation> locs) {
        writeLocations.addAll(locs);
        // track all writes as reads so that the work queue dependencies work out
        recordReads(locs);
    }

    /**
     * Add a set of locations at the given value.
     * 
     * @param c
     *            current context to add to
     * @param locs
     *            locations to add
     * @param absVal
     *            value for the locations
     * @return variable context with the locations added
     */
    public VarContext<T> addLocations(VarContext<T> c,
            Set<AbstractLocation> locs, T absVal) {
        recordWrites(locs);
        if (c != null) {
            return c.addLocations(locs, absVal);
        }
        return null;
    }

    /**
     * Given final context fpc, add an exception of type exType with policy p.
     * That is, the PolContext associated with any exType' that is a superclass
     * of exType in the resulting FinalPolContext will be at least as
     * restrictive as the normal termination PolContext of fpc, and the program
     * counter of the PolContext for both normal termination and exType' will be
     * at least policy p. There will be a PolContext associated with exType.
     * Additionally, if isExactException is false, then exception exType' such
     * that exType is a subclass of exType', the PolContext associated with any
     * exType' that is a subclass of exType in the resulting FinalPolContext
     * will be at least as restrictive as the normal termination PolContext of
     * fpc, and the program counter of the PolContext for exType' will be at
     * least policy p.
     * 
     * @param fpc
     *            final context to add to
     * @param exType
     *            exception type
     * @param pc
     *            Abstract value associated with the program counter, if appropriate.
     * @param exception
     *            abstract value for the exception
     * @param isExactException
     *            if isExactException is false, then exception exType' such that
     *            exType is a subclass of exType', the PolContext associated
     *            with any exType' that is a subclass of exType in the resulting
     *            FinalPolContext will be at least as restrictive as the normal
     *            termination PolContext of fpc, and the program counter of the
     *            PolContext for exType' will be at least policy p.
     * @return new variable context
     */
//    public FinalVarContext<T> addException(FinalVarContext<T> fpc,
//            ClassType exType, AbstractValue<?> pc, T exception, boolean isExactException) {
//        if (!isExactException) throw new InternalCompilerError("Can only accept exact exceptions...");
//        // increase the normal termination
//        VarContext<T> nt = fpc.normalTermination();
//
//        FinalVarContext<T> res = fpc;
//        VarContext<T> exContext;
//        if (nt != null) {
//            exContext = nt.exprResultStack(Stack.singleton(exception, null));
//        }
//        else {
//            exContext = this.createInitContext();
//            exContext = exContext.exprResultStack(Stack.singleton(exception, null));
//        }        
//        res = (FinalVarContext<T>)res.exception(exType, upperBound((VarContext<T>)exContext, res.exception(exType)));
//                 
//        return res;        
//    }

    /**
     * Create an initial variable context
     * 
     * @return initial variable context
     */
    public VarContext<T> createInitContext() {
        return new VarContext<T>(analysisName(), this.bottomAbstractValue());
    }

    /**
     * @return The bottom value in the abstract value lattice
     */
    public abstract T bottomAbstractValue();

}
