package accrue.analysis.antidep;

import java.util.Collection;
import java.util.Collections;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import polyglot.ast.ArrayAccess;
import polyglot.ast.ArrayAccessAssign;
import polyglot.ast.ArrayInit;
import polyglot.ast.Binary;
import polyglot.ast.Call;
import polyglot.ast.Cast;
import polyglot.ast.Catch;
import polyglot.ast.CodeDecl;
import polyglot.ast.ConstructorCall;
import polyglot.ast.Expr;
import polyglot.ast.Field;
import polyglot.ast.FieldAssign;
import polyglot.ast.FieldDecl;
import polyglot.ast.Formal;
import polyglot.ast.If;
import polyglot.ast.Instanceof;
import polyglot.ast.Lit;
import polyglot.ast.Local;
import polyglot.ast.LocalAssign;
import polyglot.ast.LocalDecl;
import polyglot.ast.New;
import polyglot.ast.NewArray;
import polyglot.ast.Node;
import polyglot.ast.NodeFactory;
import polyglot.ast.ProcedureCall;
import polyglot.ast.Return;
import polyglot.ast.Special;
import polyglot.ast.Stmt;
import polyglot.ast.Term;
import polyglot.ast.Throw;
import polyglot.ast.Try;
import polyglot.ast.TypeNode;
import polyglot.ast.Unary;
import polyglot.frontend.Job;
import polyglot.main.Report;
import polyglot.types.ClassType;
import polyglot.types.ConstructorInstance;
import polyglot.types.MethodInstance;
import polyglot.types.SemanticException;
import polyglot.types.TypeSystem;
import polyglot.util.InternalCompilerError;
import polyglot.visit.FlowGraph;
import polyglot.visit.FlowGraph.Edge;
import polyglot.visit.FlowGraph.EdgeKey;
import polyglot.visit.FlowGraph.ExceptionEdgeKey;
import polyglot.visit.FlowGraph.Peer;
import accrue.analysis.defuse.DefUseAnalysisFactory;
import accrue.analysis.ext.AccrueExt;
import accrue.analysis.ext.AccrueExt_c;
import accrue.analysis.ext.ExtArrayAccess;
import accrue.analysis.ext.ExtBinary;
import accrue.analysis.ext.ExtExpr;
import accrue.analysis.ext.ExtFormal;
import accrue.analysis.ext.ExtNewArray;
import accrue.analysis.ext.ExtTerm;
import accrue.analysis.interprocanalysis.AbstractLocation;
import accrue.analysis.interprocanalysis.AnalysisContext;
import accrue.analysis.interprocanalysis.DataFlowNodeIdentifier;
import accrue.analysis.interprocanalysis.EdgeIdentifier;
import accrue.analysis.interprocanalysis.EdgeIdentifier.HeapUseKey;
import accrue.analysis.interprocanalysis.EdgeIdentifier.LocalUseKey;
import accrue.analysis.interprocanalysis.EdgeIdentifier_c;
import accrue.analysis.interprocanalysis.ExitMap;
import accrue.analysis.interprocanalysis.ExitMap.Key;
import accrue.analysis.interprocanalysis.NodeIdentifier;
import accrue.analysis.interprocanalysis.WorkQueue;
import accrue.analysis.interprocvarcontext.FinalVarContext;
import accrue.analysis.interprocvarcontext.VarContext;
import accrue.analysis.interprocvarcontext.VarContextDataFlow;
import accrue.analysis.pointer.HContext;
import accrue.analysis.preciseExceptions.ThrowableType;

/**
 * This analysis works as follows: At every use, an edge is created for the
 * reference and associated with the locations referenced. The edge is only
 * propagated along forward edges.
 * 
 * Each use that "flows" to an assignment that may define a referenced location
 * has (may have) an anti-dependency on that assignment
 */
public class AntiDepDataFlow extends VarContextDataFlow<AntiDepAbsVal> {
    /**
     * Adds a set of results to the current set
     * 
     * @param resultKey
     *            The key of the analysis result to record.
     * @param rec
     *            The extension object to record these results on.
     * @param ctx
     *            The AnalysisContext to associate these results with.
     * @param results
     */
    public static <T> void addResults(String resultKey, AccrueExt rec,
            AnalysisContext ctx, Set<T> results) {
        // Get all the control dependencies of this dep
        Set<T> cur_results = rec.getAnalysisResult(resultKey, ctx);
        // If none exists, create a new one
        if (cur_results == null) {
            cur_results = new HashSet<T>();
            rec.recordAnalysisResult(resultKey, ctx, cur_results);
        }
        cur_results.addAll(results);
    }

    protected AntiDepAnalysisUtil autil;

    public AntiDepDataFlow(AntiDepAnalysisUtil autil,
            WorkQueue<VarContext<AntiDepAbsVal>> workQueue, Job job,
            TypeSystem ts, NodeFactory nf) {
        super(autil, workQueue, job, ts, nf, true, false, false);
        this.autil = autil;
    }

    protected Map<DataFlowNodeIdentifier, Integer> nodePostordering;

    protected int postorderNodeIDs(Peer<VarContext<AntiDepAbsVal>> p,
            int count, Set<NodeIdentifier> visited) {
        DataFlowNodeIdentifier nid = dataFlowNodeIdentifierForPeer(p);
        if (visited.contains(nid)) return count;

        // visit p
        visited.add(nid);

        // visit all the successors of p
        for (Edge<VarContext<AntiDepAbsVal>> e : p.succs()) {
            count = postorderNodeIDs(e.getTarget(), count, visited);
        }

        // number p
        this.nodePostordering.put(nid, Integer.valueOf(count++));

        return count;
    }

    @Override
    protected void check(FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> p) throws SemanticException {
        if (p.isEntry()) return;
        Term n = p.node();
        // Anti-deps
        VarContext<AntiDepAbsVal> dfIn = p.inItem();
        AntiDepAbsVal uses = null;
        if (n instanceof LocalAssign) {
            LocalAssign la = (LocalAssign) n;
            Local l = la.left();
            uses = dfIn.getLocalAbsVal(l.name(), l.type());
        }
        else if (n instanceof FieldAssign) {
            FieldAssign fa = (FieldAssign) n;
            Field f = fa.left();
            Set<AbstractLocation> locs;
            if (f.target() instanceof Term) {
                AntiDepAbsVal targetDFI = dfIn.peekExprResult();
                locs = autil.abstractLocations(targetDFI, f);
            }
            else locs = autil.abstractLocations(f);

            uses = autil.getLocationAbsVal(dfIn, locs);
        }
        else if (n instanceof ArrayAccessAssign) {
            ArrayAccessAssign aaa = (ArrayAccessAssign) n;
            ArrayAccess aa = aaa.left();
            int numArgs = 2;
            AntiDepAbsVal arrayDFI = dfIn.peekExprResults(numArgs).get(1);
            Set<AbstractLocation> locs = autil.abstractLocations(arrayDFI, aa);
            uses = autil.getLocationAbsVal(dfIn, locs);
        }
        else if (n instanceof ProcedureCall) {
            AccrueExt ext = AccrueExt_c.ext(n);
            Set<AbstractLocation> locs =
                    ext.getAnalysisResult(DefUseAnalysisFactory.MODIFIED_LOCATIONS,
                                          currentContext());
            uses = autil.getLocationAbsVal(dfIn, locs);
        }

        if (uses != null && !uses.reachingUses().isEmpty()) {
            AccrueExt ext = AccrueExt_c.ext(n);
            addResults(AntiDepAnalysisFactory.INTRA_ANTI_DEPENDENCIES,
                       ext,
                       autil.currentContext(),
                       uses.reachingUses());
        }
    }

    @Override
    protected void check(FlowGraph<VarContext<AntiDepAbsVal>> graph, Term n,
            boolean entry, VarContext<AntiDepAbsVal> inItem,
            Map<EdgeKey, VarContext<AntiDepAbsVal>> outItems) {
        throw new InternalCompilerError("Unsupported");
    }

    @Override
    protected Map<EdgeKey, VarContext<AntiDepAbsVal>> flowImpl(
            VarContext<AntiDepAbsVal> trueItem,
            VarContext<AntiDepAbsVal> falseItem,
            VarContext<AntiDepAbsVal> otherItem,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        Term node = peer.node();
        if (Report.should_report(this.autil.workQueue()
                                           .factory()
                                           .reportTopics(), 3)) {
            Report.report(3,
                          "AntiDepDataFlow:      "
                                  + peer
                                  + "     T result stack is "
                                  + ((trueItem == null) ? "null"
                                          : trueItem.exprResultStack()));
            Report.report(3,
                          "AntiDepDataFlow:      "
                                  + peer
                                  + "     F result stack is "
                                  + ((falseItem == null) ? "null"
                                          : falseItem.exprResultStack()));
            Report.report(3,
                          "AntiDepDataFlow:      "
                                  + peer
                                  + "     O result stack is "
                                  + ((otherItem == null) ? "null"
                                          : otherItem.exprResultStack()));
        }
        VarContext<AntiDepAbsVal> dfIn =
                safeConfluence(trueItem,
                               FlowGraph.EDGE_KEY_TRUE,
                               falseItem,
                               FlowGraph.EDGE_KEY_FALSE,
                               otherItem,
                               FlowGraph.EDGE_KEY_OTHER,
                               peer,
                               graph);

        if (peer.isEntry()) {
            if (node instanceof Stmt || node instanceof LocalDecl) {
                return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                                     peer.succEdgeKeys());
            }
            else if (node instanceof Expr) {
                return itemToMapWithExceptionResults(dfIn.clearReturnResult(),
                                                     peer.succEdgeKeys());
            }
            else {
                return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
            }

        }

        if (peer.node() instanceof Stmt
                && Report.should_report(this.autil.workQueue()
                                                  .factory()
                                                  .reportTopics(), 3)) {
            Report.report(3, "AntiDepDataFlow: Starting processing of node "
                    + node);
            Report.report(3, "AntiDepDataFlow:           result stack is "
                    + dfIn.exprResultStack());
            Report.report(3,
                          "AntiDepDataFlow:           locals are "
                                  + dfIn.locals());
            Report.report(3,
                          "AntiDepDataFlow:           locations are "
                                  + dfIn.locations());

        }

        final Map<EdgeKey, VarContext<AntiDepAbsVal>> ret;
        ret =
                ((ExtTerm) AccrueExt_c.ext(node)).flowDispatch(this,
                                                               dfIn,
                                                               trueItem,
                                                               falseItem,
                                                               graph,
                                                               peer);
        if (peer.node() instanceof Stmt
                && Report.should_report(this.autil.workQueue()
                                                  .factory()
                                                  .reportTopics(), 3)) {
            Report.report(3, "AntiDepDataFlow: Finished processing of node "
                    + node);
            Report.report(3, "AntiDepDataFlow:           result stack is "
                    + dfIn.exprResultStack());
            Report.report(3,
                          "AntiDepDataFlow:           locals are "
                                  + dfIn.locals());
            Report.report(3,
                          "AntiDepDataFlow:           locations are "
                                  + dfIn.locations());

        }
        return ret;
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowCodeDecl(CodeDecl n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    // ////////////////// Locals /////////////////////////

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowLocalDecl(LocalDecl n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        if (n.init() != null) {
            dfIn = dfIn.popExprResult();
        }
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowFormal(Formal n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        ExtFormal ef = (ExtFormal) AccrueExt_c.ext(n);

        // pop off type from expression stack
        dfIn = dfIn.popExprResult();

        if (ef.isCatchFormal()) {
            AntiDepAbsVal exDefs = dfIn.returnResult();
            if (exDefs == null) {
                throw new InternalCompilerError("Was expecting a return result for the catch formal");
            }
            dfIn = dfIn.clearReturnResult();
        }
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowLocal(Local n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {

        AntiDepAbsVal cur = dfIn.getLocalAbsVal(n.name(), n.type());
        AntiDepAbsVal use = createLocalUse(n.name(), peer);
        dfIn = dfIn.addLocal(n.name(), use.upperBound(cur));
        dfIn = dfIn.pushExprResult(use, n);
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowLocalAssign(
            LocalAssign n, VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // the number of arguments on the stack depend on the kind of
        // assignment...
        int numArgs = argumentsOnResultStack(n, dfIn);
        Local l = n.left();
        // get the reaching uses
        AntiDepAbsVal locDFI = dfIn.getLocalAbsVal(l.name(), n.type());
        // there is a unique reaching def for uses of the value of this node

        //XXX: strong update: Sound to kill reaching uses here?.
        dfIn = dfIn.popAndPushExprResults(numArgs, locDFI, n);

        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    // ////////////////// Fields /////////////////////////

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowField(Field n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        AntiDepAbsVal targetDFI = autil.bottomAbstractValue();
        if (n.target() instanceof Term) {
            // we evaluated the receiver, and so it is on the stack.
            targetDFI = dfIn.peekExprResult();
            dfIn = dfIn.popExprResult();
        }

        // at this point, there may be a NPE thrown...
        FinalVarContext<AntiDepAbsVal> res =
                flowNullPointerException(dfIn, n.target(), targetDFI, peer);

        dfIn = res.normalTermination();

        // if we do not throw a NPE, then we use a location determined by the
        // reaching uses of the receiver
        Set<AbstractLocation> locs = autil.abstractLocations(targetDFI, n);
        AntiDepAbsVal use = createHeapUse(locs, peer);

        dfIn = autil.addLocations(dfIn, locs, use);
        // push result for field access
        dfIn = dfIn.pushExprResult(use, n);

        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);
        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowFieldDecl(FieldDecl n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {

        // Treat it like a field assignment.
        // But since we don't need to put anything on the expression stack,
        // it is essentially a no-op.

        // Since FieldDecls are "finish peers" of the dataflow, and
        // are dealt with specially by InterProcDataFlow, we ignore
        // peer.succEdgeKeys().
        return Collections.singletonMap(FlowGraph.EDGE_KEY_OTHER,
                                        dfIn.clearExprResultStack());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowFieldAssign(
            FieldAssign n, VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // the number of arguments on the stack depend on the kind of
        // assignment...
        int numArgs = argumentsOnResultStack(n, dfIn);
        AntiDepAbsVal targetDFI =
                dfIn.peekExprResults(numArgs).get(numArgs - 1);

        // at this point, there may be a NPE thrown...
        Field f = n.left();
        FinalVarContext<AntiDepAbsVal> res =
                flowNullPointerException(dfIn, f.target(), targetDFI, peer);
        dfIn = res.normalTermination();

        // if we do not throw a NPE, then we update the location.
        Set<AbstractLocation> locs = autil.abstractLocations(targetDFI, f);

        AntiDepAbsVal fieldDFI = autil.getLocationAbsVal(dfIn, locs);
        if (fieldDFI == null) fieldDFI = autil.bottomAbstractValue();

        dfIn = dfIn.popAndPushExprResults(numArgs, fieldDFI, n);
        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);
        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    // ////////////////// Arrays /////////////////////////

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowArrayAccess(
            ArrayAccess n, VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // Index
        dfIn = dfIn.popExprResult();
        // Array
        AntiDepAbsVal arrayDFI = dfIn.exprResultStack().peek();
        dfIn = dfIn.popExprResult();

        // at this point, there may be a NPE thrown...
        FinalVarContext<AntiDepAbsVal> npe =
                flowNullPointerException(dfIn, n.array(), arrayDFI, peer);
        npe = (FinalVarContext<AntiDepAbsVal>) npe.removeNormalTermination();

        // at this point, there may be a ArrayIndexOutOfBoundsException
        // thrown...
        FinalVarContext<AntiDepAbsVal> oob =
                flowOutOfBoundsException(dfIn, n, peer);
        oob = (FinalVarContext<AntiDepAbsVal>) oob.removeNormalTermination();

        // if no exceptions are thrown, then we push the DFI for the element
        Set<AbstractLocation> locs = autil.abstractLocations(arrayDFI, n);

        AntiDepAbsVal rdef = createHeapUse(locs, peer);
        dfIn = autil.addLocations(dfIn, locs, rdef);
        dfIn = dfIn.pushExprResult(rdef, n);

        FinalVarContext<AntiDepAbsVal> res =
                (FinalVarContext<AntiDepAbsVal>) oob.upperBound(npe);
        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);

        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowArrayAccessAssign(
            ArrayAccessAssign n, VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        AntiDepAbsVal arrayDFI = dfIn.peekExprResults(numArgs).get(numArgs - 1);

        ArrayAccess aa = n.left();
        FinalVarContext<AntiDepAbsVal> npe =
                flowNullPointerException(dfIn, aa.array(), arrayDFI, peer);
        dfIn = npe.normalTermination();
        npe = (FinalVarContext<AntiDepAbsVal>) npe.removeNormalTermination();

        FinalVarContext<AntiDepAbsVal> oob =
                flowUncheckedException(dfIn, ts.OutOfBoundsException(), n, peer);
        dfIn = oob.normalTermination();
        oob = (FinalVarContext<AntiDepAbsVal>) oob.removeNormalTermination();

        FinalVarContext<AntiDepAbsVal> res =
                (FinalVarContext<AntiDepAbsVal>) npe.upperBound(oob);

        // XXX: could refine this also
        if (lang().throwTypes(n, ts).contains(ts.ArrayStoreException())) {
            FinalVarContext<AntiDepAbsVal> ase =
                    flowUncheckedException(dfIn,
                                           ts.ArrayStoreException(),
                                           n,
                                           peer);
            dfIn = ase.normalTermination();
            ase =
                    (FinalVarContext<AntiDepAbsVal>) ase.removeNormalTermination();
            res = (FinalVarContext<AntiDepAbsVal>) res.upperBound(ase);
        }

        // if no exceptions are thrown, then we push the DFI for the element
        Set<AbstractLocation> locs = autil.abstractLocations(arrayDFI, aa);

        AntiDepAbsVal elementDFI = autil.getLocationAbsVal(dfIn, locs);
        if (elementDFI == null) elementDFI = autil.bottomAbstractValue();

        dfIn = dfIn.popAndPushExprResults(numArgs, elementDFI, n);

        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);
        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowArrayInit(ArrayInit n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        dfIn = dfIn.popExprResults(n.elements().size());
        dfIn = dfIn.pushExprResult(autil.bottomAbstractValue(), n);

        FinalVarContext<AntiDepAbsVal> res = autil.createFinalVarContext(dfIn);
        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowNewArray(NewArray n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // AntiDepAbsVal init = autil.bottomAbstractValue();
        if (n.init() != null) {
            // init = dfIn.peekExprResult();
            dfIn = dfIn.popExprResult();
        }
        // pop off the results for the dims
        dfIn = dfIn.popExprResults(n.dims().size());
        // pop off the result for the base type.
        dfIn = dfIn.popExprResult();

        FinalVarContext<AntiDepAbsVal> res = autil.createFinalVarContext(dfIn);
        try {
            ExtNewArray ext = (ExtNewArray) AccrueExt_c.ext(n);
            if (ext.mayThrowNegativeArraySizeException()) {
                res =
                        flowUncheckedException(res.normalTermination(),
                                               ts.typeForName("java.lang.NegativeArraySizeException")
                                                 .toClass(),
                                               n,
                                               peer);
            }
        }
        catch (SemanticException e) {
            throw new InternalCompilerError(e);
        }

        // if we do not throw an exception, we have a result on the stack
        dfIn = res.normalTermination();
        AntiDepAbsVal newArray = AntiDepAbsVal.EMPTY;
        dfIn = dfIn.pushExprResult(newArray, n);
        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);

        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    // ////////////////// Calls /////////////////////////
    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowCall(Call n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        MethodInstance mi = n.methodInstance();
        DataFlowNodeIdentifier callSite = dataFlowNodeIdentifierForPeer(peer);

        FinalVarContext<AntiDepAbsVal> call = null;
        // get the results of the call.
        try {
            if (!mi.flags().isStatic()) {
                AntiDepAbsVal targetDFI =
                        dfIn.peekExprResults(mi.formalTypes().size() + 1)
                            .get(mi.formalTypes().size());
                // this is a virtual call, add in defs of target and args
                FinalVarContext<AntiDepAbsVal> recv =
                        flowNullPointerException(dfIn,
                                                 n.target(),
                                                 targetDFI,
                                                 peer);
                call = autil.call(mi, dfIn, callSite);

                // now merge with exceptional edge
                call =
                        (FinalVarContext<AntiDepAbsVal>) call.upperBound(recv.removeNormalTermination());
            }
            else {
                call = autil.call(n.methodInstance(), dfIn, callSite);
            }
            for (EdgeKey k : peer.succEdgeKeys()) {
                if (k instanceof ExceptionEdgeKey) {
                    ExceptionEdgeKey ek = (ExceptionEdgeKey) k;
                    if (!call.exceptionTypes().contains(ek.type())) {
                        call =
                                flowImpossibleException(call,
                                                        (ClassType) ek.type(),
                                                        n);
                    }
                }
            }
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }
        return finalVarContextToDataFlowMap(call, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowNew(New n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        try {
            ConstructorInstance ci = n.constructorInstance();

            // clear procDFI before calling new procedure.
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);
            AntiDepAbsVal newObj = AntiDepAbsVal.EMPTY;
            FinalVarContext<AntiDepAbsVal> call =
                    autil.callFromNew(ci, dfIn, newObj, callSite);
            dfIn = call.normalTermination();
            // push "unique object"
            dfIn = dfIn.pushExprResult(newObj, n);

            call =
                    (FinalVarContext<AntiDepAbsVal>) call.normalTermination(dfIn);

            for (EdgeKey k : peer.succEdgeKeys()) {
                if (k instanceof ExceptionEdgeKey) {
                    ExceptionEdgeKey ek = (ExceptionEdgeKey) k;
                    if (!call.exceptionTypes().contains(ek.type())) {
                        call =
                                flowImpossibleException(call,
                                                        (ClassType) ek.type(),
                                                        n);
                    }
                }
            }
            return finalVarContextToDataFlowMap(call, peer.succEdgeKeys(), peer);
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }
    }

    // Other stmts

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowConstructorCall(
            ConstructorCall n, VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        try {
            // clear procDFI before calling new procedure.
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);

            FinalVarContext<AntiDepAbsVal> ccall =
                    autil.constructorCallFromConstructor(n.constructorInstance(),
                                                         dfIn,
                                                         callSite);

            for (EdgeKey k : peer.succEdgeKeys()) {
                if (k instanceof ExceptionEdgeKey) {
                    ExceptionEdgeKey ek = (ExceptionEdgeKey) k;
                    if (!ccall.exceptionTypes().contains(ek.type())) {
                        ccall =
                                flowImpossibleException(ccall,
                                                        (ClassType) ek.type(),
                                                        n);
                    }
                }
            }

            return finalVarContextToDataFlowMap(ccall,
                                                peer.succEdgeKeys(),
                                                peer);
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowThrow(Throw n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        AntiDepAbsVal excDFI = dfIn.peekExprResult();
        Set<HContext> excObjs = autil.pointsTo(excDFI, n.expr());

        dfIn = dfIn.popExprResult();
        FinalVarContext<AntiDepAbsVal> t =
                flowNullPointerException(dfIn, n.expr(), excDFI, peer);
        // add DFI for the exception we are throwing

        dfIn =
                t.normalTermination()
                 .clearExprResultStack()
                 .returnResult(excDFI);
        t = (FinalVarContext<AntiDepAbsVal>) t.removeNormalTermination();

        // Only add key if node has successors.
        // Otherwise we are throwing a fatal error
        if (peer.succs().size() != 0) {
            for (HContext on : excObjs) {
                if (!ts.descendsFrom(on.type(), ts.Throwable()))
                    throw new InternalCompilerError("Expected a descendant of java.lang.Exception, got "
                            + on.type());
                Key k = ExitMap.exceptionKey(on.type().toClass());
                t =
                        (FinalVarContext<AntiDepAbsVal>) t.addKey(k,
                                                                  VarContext.upperBound(dfIn,
                                                                                        t.get(k)));
            }
        }
        return finalVarContextToDataFlowMap(t, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowReturn(Return n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        AntiDepAbsVal retDFI = autil.bottomAbstractValue();
        if (n.expr() != null) {
            retDFI = dfIn.peekExprResult();
            dfIn = dfIn.popExprResult();
        }
        dfIn = dfIn.returnResult(retDFI);
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    // miscellaneous expressions
    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowExpr(Expr n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        throw new InternalCompilerError("Not yet implemented: " + n + " "
                + n.getClass() + " for analysis " + this.getClass().getName());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowCast(Cast n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<AntiDepAbsVal> args = dfIn.peekExprResults(numArgs);
        AntiDepAbsVal exprDFI = args.get(1);
        FinalVarContext<AntiDepAbsVal> res =
                flowClassCastException(dfIn, n, exprDFI, peer);
        dfIn = res.normalTermination();
        dfIn = dfIn.popAndPushExprResults(numArgs, args.get(1), n);
        res = (FinalVarContext<AntiDepAbsVal>) res.normalTermination(dfIn);
        return finalVarContextToDataFlowMap(res, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowBinary(Binary n,
            VarContext<AntiDepAbsVal> dfIn, VarContext<AntiDepAbsVal> trueItem,
            VarContext<AntiDepAbsVal> falseItem,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<AntiDepAbsVal> args = dfIn.peekExprResults(numArgs);
        AntiDepAbsVal join = upperBound(args);
        dfIn = dfIn.popAndPushExprResults(numArgs, join, n);

        // some binary operations cause an arithmetic exception
        FinalVarContext<AntiDepAbsVal> out =
                flowArithmeticException(dfIn, n, peer);
        return finalVarContextToDataFlowMap(out, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowSpecial(Special n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // XXX: Look into how "this" gets set
        dfIn = dfIn.pushExprResult(AntiDepAbsVal.EMPTY, n);
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowLit(Lit n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        AntiDepAbsVal litDFI = autil.bottomAbstractValue();
        return itemToMapWithExceptionResults(dfIn.pushExprResult(litDFI, n),
                                             peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowInstanceof(Instanceof n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        int numArgs = VarContextDataFlow.argumentsOnResultStack(n, dfIn);
        dfIn =
                dfIn.popAndPushExprResults(numArgs,
                                           autil.bottomAbstractValue(),
                                           n);

        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowUnary(Unary n,
            VarContext<AntiDepAbsVal> dfIn, VarContext<AntiDepAbsVal> trueItem,
            VarContext<AntiDepAbsVal> falseItem,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    // statements

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowStmt(Stmt n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    // other terms

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowTypeNode(TypeNode n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn.pushExprResult(autil.bottomAbstractValue(),
                                                                 n),
                                             peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowTry(Try n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        if (n.finallyBlock() != null) {
            throw new InternalCompilerError("Don't handle finally blocks yet",
                                            n.finallyBlock().position());
        }
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowCatch(Catch n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<AntiDepAbsVal>> flowIf(If n,
            VarContext<AntiDepAbsVal> dfIn,
            FlowGraph<VarContext<AntiDepAbsVal>> graph,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        super.flowIf(n, dfIn, graph, peer);
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

    // exceptions
    protected FinalVarContext<AntiDepAbsVal> flowUncheckedException(
            VarContext<AntiDepAbsVal> dfIn, ClassType exType, Node cause,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        FinalVarContext<AntiDepAbsVal> res = autil.createFinalVarContext(dfIn);
        dfIn = dfIn.clearExprResultStack();
        return (FinalVarContext<AntiDepAbsVal>) res.exception(exType,
                                                              dfIn.returnResult(autil.bottomAbstractValue()));
    }

    // exceptions
    protected FinalVarContext<AntiDepAbsVal> flowImpossibleException(
            VarContext<AntiDepAbsVal> dfIn, ClassType exType, Node cause,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        FinalVarContext<AntiDepAbsVal> res = autil.createFinalVarContext(dfIn);
        dfIn = dfIn.clearExprResultStack();
        return flowImpossibleException(res, exType, cause);
    }

    protected FinalVarContext<AntiDepAbsVal> flowImpossibleException(
            FinalVarContext<AntiDepAbsVal> res, ClassType exType, Node cause) {
        VarContext<AntiDepAbsVal> empty = autil.createInitContext();
        // System.out.println("REFINE EXCEPTIONS: " + cause + " can't throw "
        // + exType + " at " + cause.position()
        // + ", but a control flow edge exists. "
        // + "Flowing an empty context.");
        return (FinalVarContext<AntiDepAbsVal>) res.exception(exType,
                                                              empty.returnResult(autil.bottomAbstractValue()));
    }

    protected FinalVarContext<AntiDepAbsVal> flowNullPointerException(
            VarContext<AntiDepAbsVal> dfIn, Node cause, AntiDepAbsVal causeDFI,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        if (cause instanceof Expr) {
            ExtExpr extTarg = (ExtExpr) AccrueExt_c.ext(cause);
            if (autil.mayBeNull(causeDFI, (Expr) cause, peer)) {
                // Target can actually be null
                return flowUncheckedException(dfIn,
                                              ts.NullPointerException(),
                                              cause,
                                              peer);
            }
            else if (extTarg.mayBeNull(autil.currentContext())) {
                // we can't actually throw a null pointer exception, but the
                // control flow graph has an edge for a NPE
                // record an exception, but with bottom on the decision to
                return flowImpossibleException(dfIn,
                                               ts.NullPointerException(),
                                               cause,
                                               peer);
            }
            return autil.createFinalVarContext(dfIn);
        }
        return autil.createFinalVarContext(dfIn);
    }

    protected FinalVarContext<AntiDepAbsVal> flowArithmeticException(
            VarContext<AntiDepAbsVal> dfIn, Binary cause,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // if it throws an arithmetic exception, note that in the context
        Collection<ThrowableType> throwTypes =
                ((ExtBinary) AccrueExt_c.ext(cause)).throwTypes(this.ts,
                                                                autil.currentContext());
        if (throwTypes.contains(new ThrowableType(ts.ArithmeticException(),
                                                  true))) {
            return flowUncheckedException(dfIn,
                                          ts.ArithmeticException(),
                                          cause,
                                          peer);
        }
        return autil.createFinalVarContext(dfIn);
    }

    protected FinalVarContext<AntiDepAbsVal> flowOutOfBoundsException(
            VarContext<AntiDepAbsVal> dfIn, Expr cause,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        // if it throws an OOB exception, note that in the context
        Collection<ThrowableType> throwTypes =
                ((ExtArrayAccess) AccrueExt_c.ext(cause)).throwTypes(this.ts,
                                                                     autil.currentContext());
        if (throwTypes.contains(new ThrowableType(ts.OutOfBoundsException(),
                                                  true))) {
            return flowUncheckedException(dfIn,
                                          ts.OutOfBoundsException(),
                                          cause,
                                          peer);
        }
        return autil.createFinalVarContext(dfIn);
    }

    protected FinalVarContext<AntiDepAbsVal> flowClassCastException(
            VarContext<AntiDepAbsVal> dfIn, Cast cause, AntiDepAbsVal causeDFI,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        if (autil.mayThrowClassCastException(causeDFI, cause, peer)) {
            return flowUncheckedException(dfIn,
                                          ts.ClassCastException(),
                                          cause,
                                          peer);
        }
        return autil.createFinalVarContext(dfIn);
    }

    protected AntiDepAbsVal upperBound(Collection<AntiDepAbsVal> l) {
        AntiDepAbsVal ub = null;
        for (AntiDepAbsVal s : l) {
            if (ub == null) {
                ub = s;
            }
            else {
                ub = ub.upperBound(s);
            }
        }
        if (ub == null) return this.autil.bottomAbstractValue();
        return ub;
    }

    protected AntiDepAbsVal createLocalUse(String defined,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        NodeIdentifier ni = dataFlowNodeIdentifierForPeer(peer);
        LocalUseKey key = new LocalUseKey(defined, true);
        Set<EdgeIdentifier> def =
                Collections.<EdgeIdentifier> singleton(new EdgeIdentifier_c(key,
                                                                            ni));
        return new AntiDepAbsVal(def);
    }

    protected AntiDepAbsVal createHeapUse(Set<AbstractLocation> locs,
            Peer<VarContext<AntiDepAbsVal>> peer) {
        NodeIdentifier ni = dataFlowNodeIdentifierForPeer(peer);
        HeapUseKey key = new HeapUseKey(locs, true);
        Set<EdgeIdentifier> def =
                Collections.<EdgeIdentifier> singleton(new EdgeIdentifier_c(key,
                                                                            ni));
        return new AntiDepAbsVal(def);
    }

    protected static Map<EdgeKey, VarContext<AntiDepAbsVal>> itemToMapWithExceptionResults(
            VarContext<AntiDepAbsVal> dfIn, Set<EdgeKey> edgeKeys) {
        Map<EdgeKey, VarContext<AntiDepAbsVal>> m =
                new HashMap<EdgeKey, VarContext<AntiDepAbsVal>>();
        VarContext<AntiDepAbsVal> exceptional = null;
        for (EdgeKey ek : edgeKeys) {
            if (ek instanceof ExceptionEdgeKey) {
                if (exceptional == null) {
                    exceptional =
                            dfIn.clearExprResultStack()
                                .returnResult(AntiDepAbsVal.EMPTY); // XXX
                                                                    // should
                                                                    // be
                                                                    // an
                                                                    // exception
                                                                    // stack?
                }
                m.put(ek, exceptional);
            }
            else {
                m.put(ek, dfIn);
            }
        }
        return m;
    }

}
