package accrue.analysis.defuse;

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.Block;
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.FieldInstance;
import polyglot.types.LocalInstance;
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.DefUseAnalysisUtil.Mode;
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 dataflow finds reaching definitions for each local and field use.
 */
public class DefUseDataFlow extends VarContextDataFlow<DefUseAbsVal> {
    /**
     * 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 final DefUseAnalysisUtil autil;
    protected final Set<EdgeIdentifier> aUnitUses;
    protected final Set<AbstractLocation> aUnitObs;
    protected final Set<AbstractLocation> aUnitDefs;

    /**
     * Treat heap assignments as uses of the left-hand side.
     */
    protected final boolean heap_assign_is_use = true;

    protected final String data_dep_results_key;
    protected Map<DataFlowNodeIdentifier, Integer> nodePostordering;

    public DefUseDataFlow(DefUseAnalysisUtil autil,
            WorkQueue<VarContext<DefUseAbsVal>> workQueue, Job job,
            TypeSystem ts, NodeFactory nf) {
        super(autil, workQueue, job, ts, nf, true, false, false);
        this.autil = autil;
        aUnitObs = new HashSet<AbstractLocation>();
        aUnitDefs = new HashSet<AbstractLocation>();
        aUnitUses = new HashSet<EdgeIdentifier>();
        data_dep_results_key =
                (autil.mode() == Mode.INTER_EDGES) ? DefUseAnalysisFactory.DATA_DEPENDENCIES
                        : DefUseAnalysisFactory.INTRA_DATA_DEPENDENCIES;

    }

    protected int postorderNodeIDs(Peer<VarContext<DefUseAbsVal>> 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<DefUseAbsVal>> e : p.succs()) {
            count = postorderNodeIDs(e.getTarget(), count, visited);
        }

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

        return count;
    }

    @SuppressWarnings("unused")
    @Override
    protected void check(FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> p) throws SemanticException {
        if (p.isEntry()) return;

        Term n = p.node();
        // First, update other analyses with refined results
        if (n instanceof Expr && ((Expr) n).type().isReference()) {
            Expr expr = (Expr) n;
            ExtExpr ext = (ExtExpr) AccrueExt_c.ext(n);

            VarContext<DefUseAbsVal> ctx = p.outItem(FlowGraph.EDGE_KEY_OTHER);

            if (ctx != null) {
                if (!ctx.exprResultStack().isEmpty()) {
                    boolean fsMaybeNull =
                            autil.mayBeNull(ctx.peekExprResult(), expr, p);
                    ext.recordNullAnalysisResult(autil.currentContext(),
                                                 p.peerKey(),
                                                 fsMaybeNull);
                }
                else throw new InternalCompilerError("Expression " + n
                        + " has empty expression result stack");
            }
        }

        // USES
        VarContext<DefUseAbsVal> dfIn = p.inItem();
        if (dfIn == null && n instanceof Expr) {
            if (Report.should_report(this.autil.workQueue()
                                               .factory()
                                               .reportTopics(), 3)) {
                Report.report(3,
                              "DefUseDataFlow:      Ignoring Peer<VarContext<DefUseAbsVal>> with null inItem (cannot be reached):"
                                      + p);
            }
            return;
        }

        Set<AbstractLocation> observed_locs = null;
        Set<EdgeIdentifier> uses = null;
        if (n instanceof Local) {
            Local l = (Local) n;
            DefUseAbsVal val = dfIn.getLocalAbsVal(l.name(), l.type());
            if (val != null) uses = val.reachingDefinitions();
        }
        else if (n instanceof Field) {
            Field f = (Field) n;
            if (!f.flags().isStatic()) {
                DefUseAbsVal targetDFI = dfIn.peekExprResult();
                observed_locs = autil.abstractLocations(targetDFI, f);
            }
            else observed_locs = autil.abstractLocations(f);

            DefUseAbsVal val = autil.getLocationAbsVal(dfIn, observed_locs);
            if (val != null) uses = val.reachingDefinitions();

        }
        else if (n instanceof ArrayAccess) {
            ArrayAccess aa = (ArrayAccess) n;
            int numArgs = 2;
            DefUseAbsVal arrayDFI = dfIn.peekExprResults(numArgs).get(1);
            observed_locs = autil.abstractLocations(arrayDFI, aa);
            DefUseAbsVal val = autil.getLocationAbsVal(dfIn, observed_locs);
            if (val != null) uses = val.reachingDefinitions();
        }
        else if (autil.trackStrings() && n instanceof Binary
                && ((Binary) n).type().equals(ts.String())) {
            Binary b = (Binary) n;
            int numArgs = argumentsOnResultStack(n, dfIn);
            List<DefUseAbsVal> args = dfIn.peekExprResults(numArgs);

            DefUseAbsVal rightDFI = args.get(0);
            DefUseAbsVal leftDFI = args.get(1);
            observed_locs = new HashSet<AbstractLocation>();
            uses = new HashSet<EdgeIdentifier>();
            if (b.right().type().equals(ts.String())) {
                Set<AbstractLocation> locs =
                        autil.stringLocations(rightDFI, b.right());
                observed_locs.addAll(locs);

                DefUseAbsVal stringDFI = autil.getLocationAbsVal(dfIn, locs);
                if (stringDFI != null)
                    uses.addAll(stringDFI.reachingDefinitions());
            }
            if (b.left().type().equals(ts.String())) {
                Set<AbstractLocation> locs =
                        autil.stringLocations(leftDFI, b.left());
                observed_locs.addAll(locs);

                DefUseAbsVal stringDFI = autil.getLocationAbsVal(dfIn, locs);
                if (stringDFI != null)
                    uses.addAll(stringDFI.reachingDefinitions());
            }
        }
        else if (n instanceof ProcedureCall) {
            observed_locs =
                    autil.getCallResults(DefUseAnalysisFactory.OBSERVED_LOCATIONS,
                                         (ProcedureCall) n);
            uses =
                    new HashSet<EdgeIdentifier>(autil.<EdgeIdentifier> getCallResults(data_dep_results_key,
                                                                                      (ProcedureCall) n));
            // For INTRA_EDGES, create use edges at call site.
            if (autil.mode().equals(Mode.INTRA_EDGES)) {
                DefUseAbsVal callUses =
                        autil.getLocationAbsVal(dfIn, observed_locs);
                if (callUses != null)
                    uses.addAll(callUses.reachingDefinitions());
            }
        }

        // record uses
        if (n instanceof CodeDecl) {
            // record aggregate uses by this analysis unit.
            AccrueExt ext = AccrueExt_c.ext(n);
            addResults(data_dep_results_key,
                       ext,
                       autil.currentContext(),
                       aUnitUses);
            addResults(DefUseAnalysisFactory.OBSERVED_LOCATIONS,
                       ext,
                       autil.currentContext(),
                       aUnitObs);
        }
        else {
            if (uses != null && !uses.isEmpty()) {
                AccrueExt ext = AccrueExt_c.ext(n);
                addResults(data_dep_results_key,
                           ext,
                           autil.currentContext(),
                           uses);
                // Add heap uses to the method summary
                if (!(n instanceof Local)) aUnitUses.addAll(uses);
            }
            if (observed_locs != null && !observed_locs.isEmpty()) {
                AccrueExt ext = AccrueExt_c.ext(n);
                addResults(DefUseAnalysisFactory.OBSERVED_LOCATIONS,
                           ext,
                           autil.currentContext(),
                           observed_locs);
                aUnitObs.addAll(observed_locs);
            }
        }

        // DEFS
        Set<AbstractLocation> modified_locs = null;
        if (n instanceof FieldAssign) {
            FieldAssign fa = (FieldAssign) n;
            Field f = fa.left();
            // get the reaching definitions of the field
            modified_locs = autil.abstractLocations(f);
            if (modified_locs == null || modified_locs.isEmpty()) {
                throw new InternalCompilerError("Field assign " + n
                        + " modifies no locations!");
            }
            if (heap_assign_is_use || autil.mode() == Mode.INTRA_EDGES) {
                DefUseAbsVal val = autil.getLocationAbsVal(dfIn, modified_locs);
                if (val != null) {
                    uses = val.reachingDefinitions();
                    if (uses != null && !uses.isEmpty()) {
                        AccrueExt ext = AccrueExt_c.ext(n);
                        if (heap_assign_is_use) {
                            addResults(data_dep_results_key,
                                       ext,
                                       autil.currentContext(),
                                       uses);
                            aUnitUses.addAll(uses);
                        }
                        if (autil.mode() == Mode.INTRA_EDGES) {
                            // TODO: output dependency really only apply to field assigns
                            addResults(DefUseAnalysisFactory.INTRA_OUTPUT_DEPENDENCIES,
                                       ext,
                                       autil.currentContext(),
                                       uses);
                        }
                    }
                }
            }
        }
        else if (n instanceof ArrayAccessAssign) {
            ArrayAccessAssign aaa = (ArrayAccessAssign) n;
            ArrayAccess aa = aaa.left();
            // get the reaching definitions of the field
            // get DFI for target
            modified_locs = autil.abstractLocations(aa);
            if (modified_locs == null || modified_locs.isEmpty()) {
                throw new InternalCompilerError("Array access assign " + n
                        + " modifies no locations!");
            }

            if (heap_assign_is_use || autil.mode() == Mode.INTRA_EDGES) {
                DefUseAbsVal val = autil.getLocationAbsVal(dfIn, modified_locs);
                if (val != null) {
                    uses = val.reachingDefinitions();
                    if (uses != null && !uses.isEmpty()) {
                        AccrueExt ext = AccrueExt_c.ext(n);
                        if (heap_assign_is_use) {
                            addResults(data_dep_results_key,
                                       ext,
                                       autil.currentContext(),
                                       uses);
                            aUnitUses.addAll(uses);
                        }
                        if (autil.mode() == Mode.INTRA_EDGES) {
                            addResults(DefUseAnalysisFactory.INTRA_OUTPUT_DEPENDENCIES,
                                       ext,
                                       autil.currentContext(),
                                       uses);
                        }
                    }
                }
            }

        }
        else if (autil.mode() == Mode.INTRA_EDGES && n instanceof LocalAssign) {
            AccrueExt ext = AccrueExt_c.ext(n);
            Local l = ((LocalAssign) n).left();
            DefUseAbsVal defDFI = dfIn.getLocalAbsVal(l.name(), l.type());
            Set<EdgeIdentifier> outputDeps = defDFI.reachingDefinitions();
            addResults(DefUseAnalysisFactory.INTRA_OUTPUT_DEPENDENCIES,
                       ext,
                       autil.currentContext(),
                       outputDeps);

        }
        else if (n instanceof ProcedureCall) {
            modified_locs =
                    autil.getCallResults(DefUseAnalysisFactory.MODIFIED_LOCATIONS,
                                         (ProcedureCall) n);
        }

        // record defs
        if (n instanceof CodeDecl) {
            // record aggregate defs by this analysis unit
            AccrueExt ext = AccrueExt_c.ext(n);
            addResults(DefUseAnalysisFactory.MODIFIED_LOCATIONS,
                       ext,
                       autil.currentContext(),
                       aUnitDefs);
        }
        else if (modified_locs != null) {
            AccrueExt ext = AccrueExt_c.ext(n);
            addResults(DefUseAnalysisFactory.MODIFIED_LOCATIONS,
                       ext,
                       autil.currentContext(),
                       modified_locs);
            if (autil.mode() == Mode.INTRA_EDGES) {
                DefUseAbsVal defDFI =
                        autil.getLocationAbsVal(dfIn, modified_locs);
                if (defDFI == null) defDFI = autil.bottomAbstractValue();

                Set<EdgeIdentifier> outputDeps = defDFI.reachingDefinitions();
                addResults(DefUseAnalysisFactory.INTRA_OUTPUT_DEPENDENCIES,
                           ext,
                           autil.currentContext(),
                           outputDeps);
            }
            aUnitDefs.addAll(modified_locs);
        }

        // XXX: Should we record defs for ArrayInit or NewArray?
        // it seems uninteresting since there is never any ambiguity.
    }

    @Override
    protected Map<EdgeKey, VarContext<DefUseAbsVal>> flowImpl(
            VarContext<DefUseAbsVal> trueItem,
            VarContext<DefUseAbsVal> falseItem,
            VarContext<DefUseAbsVal> otherItem,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        Term node = peer.node();

//        long start = System.currentTimeMillis();
        if (Report.should_report(this.autil.workQueue()
                                           .factory()
                                           .reportTopics(), 3)) {
            Report.report(3,
                          "DefUseDataFlow:      "
                                  + peer
                                  + "     T result stack is "
                                  + ((trueItem == null) ? "null"
                                          : trueItem.exprResultStack()));
            Report.report(3,
                          "DefUseDataFlow:      "
                                  + peer
                                  + "     F result stack is "
                                  + ((falseItem == null) ? "null"
                                          : falseItem.exprResultStack()));
            Report.report(3,
                          "DefUseDataFlow:      "
                                  + peer
                                  + "     O result stack is "
                                  + ((otherItem == null) ? "null"
                                          : otherItem.exprResultStack()));
        }
        VarContext<DefUseAbsVal> dfIn =
                safeConfluence(trueItem,
                               FlowGraph.EDGE_KEY_TRUE,
                               falseItem,
                               FlowGraph.EDGE_KEY_FALSE,
                               otherItem,
                               FlowGraph.EDGE_KEY_OTHER,
                               peer,
                               graph);

        final Map<EdgeKey, VarContext<DefUseAbsVal>> ret;

        if (peer.isEntry()) {
            if (node instanceof Stmt || node instanceof LocalDecl) {
                ret =
                        itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                                      peer.succEdgeKeys());
            }
            else if (node instanceof Expr) {
                ret =
                        itemToMapWithExceptionResults(dfIn.clearReturnResult(),
                                                      peer.succEdgeKeys());
            }
            else {
                ret = itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
            }
//            long finish = System.currentTimeMillis();

            return ret;
        }

        if (peer.node() instanceof Stmt
                && Report.should_report(this.autil.workQueue()
                                                  .factory()
                                                  .reportTopics(), 3)) {
            Report.report(3, "DefUseDataFlow: Starting processing of node "
                    + node);
            Report.report(3, "DefUseDataFlow:           result stack is "
                    + dfIn.exprResultStack());
            Report.report(3,
                          "DefUseDataFlow:           locals are "
                                  + dfIn.locals());
            Report.report(3,
                          "DefUseDataFlow:           locations are "
                                  + dfIn.locations());
        }
        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, "DefUseDataFlow: Finished processing of node "
                    + node);
            Report.report(3, "DefUseDataFlow:           result stack is "
                    + dfIn.exprResultStack());
            Report.report(3,
                          "DefUseDataFlow:           locals are "
                                  + dfIn.locals());
            Report.report(3,
                          "DefUseDataFlow:           locations are "
                                  + dfIn.locations());

        }
//        long finish = System.currentTimeMillis();
//		System.err.println("Flow impl finished: "+ (finish-start) + "ms ("  + node.getClass() + ")");
        return ret;
    }

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

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

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

    // TODO: how can points-to for formals could be refined w/ DefUse?
    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowFormal(Formal n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        ExtFormal ef = (ExtFormal) AccrueExt_c.ext(n);

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

        DefUseAbsVal rdef = createLocalDefinition(n.name(), peer);
        dfIn = dfIn.addLocal(n.name(), rdef);

        if (ef.isCatchFormal()) {
            DefUseAbsVal 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<DefUseAbsVal>> flowLocal(Local n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        // push the reaching definitions onto the stack
        DefUseAbsVal locDFI = dfIn.getLocalAbsVal(n.name(), n.type());

        dfIn = dfIn.pushExprResult(locDFI, n);
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowLocalAssign(
            LocalAssign n, VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        // the number of arguments on the stack depend on the kind of
        // assignment...
        int numArgs = argumentsOnResultStack(n, dfIn);

        LocalInstance li = n.left().localInstance();
        DefUseAbsVal rdef = createLocalDefinition(li.name(), peer);
        dfIn = dfIn.addLocal(li.name(), rdef);
        // there is a unique reaching def for uses of the value of this node.
        dfIn = dfIn.popAndPushExprResults(numArgs, rdef, n);

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

    //////////////////// Fields /////////////////////////	
    // For each use, we want to lookup the reaching definitions and push them
    // onto the result stack.

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowField(Field n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        DefUseAbsVal 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<DefUseAbsVal> 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 definitions of the receiver
        Set<AbstractLocation> locs = autil.abstractLocations(targetDFI, n);
        DefUseAbsVal fieldDFI = autil.getLocationAbsVal(dfIn, locs);
        if (fieldDFI == null) fieldDFI = autil.bottomAbstractValue();

        // push result for field access
        dfIn = dfIn.pushExprResult(fieldDFI, n);

        res = (FinalVarContext<DefUseAbsVal>) res.normalTermination(dfIn);

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

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowFieldDecl(FieldDecl n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        FieldInstance fi = n.fieldInstance();

        DefUseAbsVal targetDFI =
                fi.flags().isStatic() ? autil.bottomAbstractValue()
                        : new NewAllocAbsVal(autil.pointsToThis());

        // we update the location.
        Set<AbstractLocation> locs =
                autil.abstractLocationsImplicitTarget(targetDFI, fi);
        DefUseAbsVal rdef = createHeapDefinition(locs, peer);

        // XXX: Strong update for singleton sets :: FIXME -- must also check
        // that loc can only refer to a single concrete location.
        // if(locs.size() == 1) {
        // Map<AbstractLocation,DefUseAbsVal> newLocs =
        // new HashMap<AbstractLocation,DefUseAbsVal>();
        // newLocs.put(locs.iterator().next(),rdef);
        // dfIn = dfIn.locations(newLocs);
        // }
        // else
        dfIn = autil.addLocations(dfIn, locs, rdef);

        // 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<DefUseAbsVal>> flowFieldAssign(
            FieldAssign n, VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        // the number of arguments on the stack depend on the kind of
        // assignment...
        int numArgs = argumentsOnResultStack(n, dfIn);
        DefUseAbsVal targetDFI = dfIn.peekExprResults(numArgs).get(numArgs - 1);

        // at this point, there may be a NPE thrown...
        Field f = n.left();
        FinalVarContext<DefUseAbsVal> 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);
        DefUseAbsVal rdef = createHeapDefinition(locs, peer);

        // XXX: Strong update for singleton sets :: FIXME -- must also check
        // that loc can only refer to a single concrete location.
        // if(locs.size() == 1) {
        // Map<AbstractLocation,DefUseAbsVal> newLocs =
        // new HashMap<AbstractLocation,DefUseAbsVal>();
        // newLocs.put(locs.iterator().next(),rdef);
        // dfIn = dfIn.locations(newLocs);
        // }
        // else
        dfIn = autil.addLocations(dfIn, locs, rdef);
        // there is a unique reaching def for uses of the value of this node.
        dfIn = dfIn.popAndPushExprResults(numArgs, rdef, n);

        res = (FinalVarContext<DefUseAbsVal>) res.normalTermination(dfIn);

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

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

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

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

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

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

        DefUseAbsVal elementDFI = autil.getLocationAbsVal(dfIn, locs);
        if (elementDFI == null) elementDFI = autil.bottomAbstractValue();
        dfIn = dfIn.pushExprResult(elementDFI, n);

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

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

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

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

        FinalVarContext<DefUseAbsVal> oob =
                flowOutOfBoundsException(dfIn, aa, peer);
        dfIn = oob.normalTermination();
        oob = (FinalVarContext<DefUseAbsVal>) oob.removeNormalTermination();

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

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

        // if we do not throw an exception, then we update the location.
        Set<AbstractLocation> locs = autil.abstractLocations(arrayDFI, aa);
        DefUseAbsVal rdef = createHeapDefinition(locs, peer);

        dfIn = autil.addLocations(dfIn, locs, rdef);

        // there is a unique reaching def for uses of the value of this node.
        dfIn = dfIn.popAndPushExprResults(numArgs, rdef, n);

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

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

        // update the location.
        Set<AbstractLocation> locs = autil.abstractLocationsForArray(n);
        DefUseAbsVal rdef = createHeapDefinition(locs, peer);
        dfIn = autil.addLocations(dfIn, locs, rdef);
        dfIn = dfIn.pushExprResult(rdef, n);

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

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowNewArray(NewArray n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        DefUseAbsVal init = autil.bottomAbstractValue();
        if (n.init() != null) {
            init = dfIn.peekExprResult();
            dfIn = dfIn.popExprResult();
        }
        else {
            // create definitions for the default intialization
            Set<AbstractLocation> locs = autil.abstractLocationsForArray(n);
            init = createHeapDefinition(locs, peer);
            dfIn = autil.addLocations(dfIn, locs, init);
        }
        // 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<DefUseAbsVal> 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();
        DefUseAbsVal newArray = new NewAllocAbsVal(autil.pointsTo(n));
        dfIn = dfIn.pushExprResult(newArray, n);
        res = (FinalVarContext<DefUseAbsVal>) res.normalTermination(dfIn);

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

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

        FinalVarContext<DefUseAbsVal> call = null;
        // get the results of the call.
        try {
            if (!mi.flags().isStatic()) {
                DefUseAbsVal targetDFI =
                        dfIn.peekExprResults(mi.formalTypes().size() + 1)
                            .get(mi.formalTypes().size());
                // this is a virtual call, add in defs of target and args
                FinalVarContext<DefUseAbsVal> recv =
                        flowNullPointerException(dfIn,
                                                 n.target(),
                                                 targetDFI,
                                                 peer);
                call = autil.call(mi, dfIn, callSite);
                // now merge with exceptional edge
                call =
                        (FinalVarContext<DefUseAbsVal>) 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<DefUseAbsVal>> flowNew(New n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        try {
            ConstructorInstance ci = n.constructorInstance();

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

            call = (FinalVarContext<DefUseAbsVal>) 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<DefUseAbsVal>> flowConstructorCall(
            ConstructorCall n, VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        try {
            // clear procDFI before calling new procedure.
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);

            FinalVarContext<DefUseAbsVal> 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<DefUseAbsVal>> flowThrow(Throw n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        DefUseAbsVal excDFI = dfIn.peekExprResult();
        // XXX: can't throw NewAllocs since there aren't actual allocation sites
        // for all exceptions. Just flow the bottom value... this is probably bad.
        Set<HContext> excObjs = autil.pointsTo(excDFI, n.expr());
        if (excDFI instanceof NewAllocAbsVal) {
            excDFI = autil.bottomAbstractValue();
        }

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

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

        // Only add key if node has successors. 
        // Otherwise we are throwing a fatal error
        if (peer.succs().size() != 0) {
            // XXX: not totally confident about this part
            for (HContext on : excObjs) {
                Key k = ExitMap.exceptionKey(on.type().toClass());
                t =
                        (FinalVarContext<DefUseAbsVal>) t.addKey(k,
                                                                 dfIn.upperBound(t.get(k)));
            }
        }
        return finalVarContextToDataFlowMap(t, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowReturn(Return n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        DefUseAbsVal 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<DefUseAbsVal>> flowExpr(Expr n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        throw new InternalCompilerError("Not yet implemented: " + n + " "
                + n.getClass() + " for analysis " + this.getClass().getName());
    }

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

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowBinary(Binary n,
            VarContext<DefUseAbsVal> dfIn, VarContext<DefUseAbsVal> trueItem,
            VarContext<DefUseAbsVal> falseItem,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<DefUseAbsVal> args = dfIn.peekExprResults(numArgs);
        // right is at top of stack
        DefUseAbsVal argsDFI;
        if (autil.trackStrings() && n.operator() == Binary.ADD
                && n.type().equals(ts.String())) {
            ExtExpr extExpr = (ExtExpr) AccrueExt_c.ext(n);
            if (extExpr.getReferenceVariable(autil.currentContext()
                                                  .getConstructorContext()) != null) {
                Set<HContext> objects = autil.pointsTo(n);
                Set<AbstractLocation> locs =
                        new HashSet<AbstractLocation>(objects.size());
                for (HContext hc : objects) {
                    locs.add(AbstractLocation.create(hc,
                                                     DefUseAnalysisUtil.STRING_CONTENTS));
                }
                argsDFI = createHeapDefinition(locs, peer);
            }
            else {
                System.err.println("WARNING: String expression has no local node:"
                        + n);
                argsDFI = autil.bottomAbstractValue();
            }
        }
        else {
            argsDFI = upperBound(args);
        }

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

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

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

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowLit(Lit n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        DefUseAbsVal litDFI;
        if (n.type().isNull() || !n.type().isReference())
            litDFI = autil.bottomAbstractValue();
        else {
            // XXX: not all literals have local nodes
            ExtExpr extExpr = (ExtExpr) AccrueExt_c.ext(n);
            if (extExpr.getReferenceVariable(autil.currentContext()
                                                  .getConstructorContext()) != null) {
                Set<HContext> objects = autil.pointsTo(n);
                litDFI = new NewAllocAbsVal(objects);
            }
            else {
                litDFI = autil.bottomAbstractValue();
            }
        }
        return itemToMapWithExceptionResults(dfIn.pushExprResult(litDFI, n),
                                             peer.succEdgeKeys());
    }

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

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

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

    // statements

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

    // other terms

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowFinally(Block n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        return flowBlock(n, dfIn, graph, peer);
    }

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

    @Override
    public Map<EdgeKey, VarContext<DefUseAbsVal>> flowTry(Try n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> 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<DefUseAbsVal>> flowCatch(Catch n,
            VarContext<DefUseAbsVal> dfIn,
            FlowGraph<VarContext<DefUseAbsVal>> graph,
            Peer<VarContext<DefUseAbsVal>> peer) {
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys());
    }

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

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

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

    protected FinalVarContext<DefUseAbsVal> flowImpossibleException(
            FinalVarContext<DefUseAbsVal> res, ClassType exType, Node cause) {
        VarContext<DefUseAbsVal> empty = autil.createInitContext();
        return (FinalVarContext<DefUseAbsVal>) res.exception(exType,
                                                             empty.returnResult(autil.bottomAbstractValue()));
    }

    protected FinalVarContext<DefUseAbsVal> flowNullPointerException(
            VarContext<DefUseAbsVal> dfIn, Node cause, DefUseAbsVal causeDFI,
            Peer<VarContext<DefUseAbsVal>> peer) {
        if (cause instanceof Expr) {
            ExtExpr extTarg = (ExtExpr) AccrueExt_c.ext(cause);
            if (autil.mayBeNull(causeDFI, (Expr) cause, peer)) {
                if (!extTarg.mayBeNull(autil.currentContext())) {
                    throw new InternalCompilerError("DEFUSE DID NOT REFINE :"
                            + cause);
                }
                // 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);
    }

    protected FinalVarContext<DefUseAbsVal> flowArithmeticException(
            VarContext<DefUseAbsVal> dfIn, Binary cause,
            Peer<VarContext<DefUseAbsVal>> 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<DefUseAbsVal> flowOutOfBoundsException(
            VarContext<DefUseAbsVal> dfIn, Expr cause,
            Peer<VarContext<DefUseAbsVal>> 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<DefUseAbsVal> flowClassCastException(
            VarContext<DefUseAbsVal> dfIn, Cast cause, DefUseAbsVal causeDFI,
            Peer<VarContext<DefUseAbsVal>> peer) {
        if (autil.mayThrowClassCastException(causeDFI, cause, peer)) {
            return flowUncheckedException(dfIn,
                                          ts.ClassCastException(),
                                          cause,
                                          peer);
        }
        return autil.createFinalVarContext(dfIn);
    }

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

    protected DefUseAbsVal createLocalDefinition(String defined,
            Peer<VarContext<DefUseAbsVal>> peer) {
        NodeIdentifier ni = dataFlowNodeIdentifierForPeer(peer);
        LocalUseKey key =
                new LocalUseKey(defined, !(autil.mode() == Mode.INTER_EDGES));
        Set<EdgeIdentifier> def =
                Collections.<EdgeIdentifier> singleton(new EdgeIdentifier_c(key,
                                                                            ni));
        return new DefUseAbsVal(def);
    }

    protected DefUseAbsVal createHeapDefinition(Set<AbstractLocation> locs,
            Peer<VarContext<DefUseAbsVal>> peer) {
        NodeIdentifier ni = dataFlowNodeIdentifierForPeer(peer);
        HeapUseKey key =
                new HeapUseKey(locs, !(autil.mode() == Mode.INTER_EDGES));
        Set<EdgeIdentifier> def =
                Collections.<EdgeIdentifier> singleton(new EdgeIdentifier_c(key,
                                                                            ni));
        return new DefUseAbsVal(def);
    }

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

}
