package accrue.analysis.notnulldataflow;

import java.util.Collections;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.List;
import java.util.Map;
import java.util.Set;

import polyglot.ast.ArrayAccess;
import polyglot.ast.ArrayInit;
import polyglot.ast.Assign;
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.Conditional;
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.Instanceof;
import polyglot.ast.Lit;
import polyglot.ast.Local;
import polyglot.ast.LocalDecl;
import polyglot.ast.New;
import polyglot.ast.NewArray;
import polyglot.ast.NodeFactory;
import polyglot.ast.NullLit;
import polyglot.ast.Receiver;
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.ext.jl5.ast.EnumConstant;
import polyglot.ext.jl5.ast.EnumConstantDecl;
import polyglot.ext.jl5.ast.ExtendedFor;
import polyglot.ext.jl5.ast.ParamTypeNode;
import polyglot.frontend.Job;
import polyglot.main.Report;
import polyglot.types.SemanticException;
import polyglot.types.TypeSystem;
import polyglot.util.CollectionUtil;
import polyglot.util.InternalCompilerError;
import polyglot.visit.FlowGraph;
import polyglot.visit.FlowGraph.EdgeKey;
import polyglot.visit.FlowGraph.ExceptionEdgeKey;
import polyglot.visit.FlowGraph.Peer;
import accrue.analysis.ext.AccrueExt_c;
import accrue.analysis.ext.ExtCast;
import accrue.analysis.ext.ExtExpr;
import accrue.analysis.ext.ExtFormal;
import accrue.analysis.ext.ExtTerm;
import accrue.analysis.interprocanalysis.DataFlowNodeIdentifier;
import accrue.analysis.interprocanalysis.ExitMap;
import accrue.analysis.interprocanalysis.ExitMap.ExceptionKey;
import accrue.analysis.interprocanalysis.WorkQueue;
import accrue.analysis.interprocvarcontext.FinalVarContext;
import accrue.analysis.interprocvarcontext.VarContext;
import accrue.analysis.interprocvarcontext.VarContextDataFlow;
import accrue.jl5.JL5DataFlowDispatch;

/**
 * Interprocedural dataflow analysis to determine which local variables and locations
 * cannot be null. This information is stored in the appropriate extension objects,
 * and is then used in subsequent analyses to improve the precision of analysis,
 * since various NullPointerExceptions can be determined not to be thrown. 
 */
public class NotNullDataFlow extends VarContextDataFlow<NotNullAbsVal>
        implements JL5DataFlowDispatch<VarContext<NotNullAbsVal>> {
    public NotNullDataFlow(NotNullAnalysisUtil autil,
            WorkQueue<VarContext<NotNullAbsVal>> wq, Job job, TypeSystem ts,
            NodeFactory nf) {
        super(autil, wq, job, ts, nf, true /* forward analysis */);
        setWarnOnEdgesMissingData(false);
    }

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

        VarContext<NotNullAbsVal> dfIn =
                safeConfluence(trueItem,
                               FlowGraph.EDGE_KEY_TRUE,
                               falseItem,
                               FlowGraph.EDGE_KEY_FALSE,
                               otherItem,
                               FlowGraph.EDGE_KEY_OTHER,
                               peer,
                               graph);
        Set<EdgeKey> succEdgeKeys = peer.succEdgeKeys();
        if (peer.isEntry()) {
            if (n instanceof Stmt) {
                return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                                     succEdgeKeys,
                                                     peer);
            }
            else if (n instanceof Expr) {
                return itemToMapWithExceptionResults(dfIn.clearReturnResult(),
                                                     succEdgeKeys,
                                                     peer);
            }
            else {
                return itemToMapWithExceptionResults(dfIn, succEdgeKeys, peer);
            }
        }

        if (Report.should_report(this.autil()
                                     .workQueue()
                                     .factory()
                                     .reportTopics(), 3)) {
            Report.report(3, "NotNullDataFlow: Starting processing of node "
                    + n + " " + n.getClass() + " " + n.position());
            Report.report(3, "NotNullDataFlow:           result stack is "
                    + dfIn.exprResultStack());
            Report.report(3,
                          "NotNullDataFlow:           locals are "
                                  + dfIn.locals());
            Report.report(3, "NotNullDataFlow:           returnResult is "
                    + dfIn.returnResult());
            Report.report(3,
                          "NotNullDataFlow:           suspended execution stack size is "
                                  + (dfIn.suspendedExecutionStack() == null ? "null"
                                          : dfIn.suspendedExecutionStack()
                                                .size()));
        }

        Map<EdgeKey, VarContext<NotNullAbsVal>> r =
                ((ExtTerm) AccrueExt_c.ext(n)).flowDispatch(this,
                                                            dfIn,
                                                            trueItem,
                                                            falseItem,
                                                            graph,
                                                            peer);
        if (Report.should_report(this.autil()
                                     .workQueue()
                                     .factory()
                                     .reportTopics(), 3)) {
            Report.report(3, "NotNullDataFlow: finished processing of node "
                    + n);
        }
        return r;
    }

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

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowCatch(Catch n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {

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

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowFinally(Block n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {

        // Just set up the normal termination and ERROR edges, the exceptions edges et al. 
        // will be handled by the framework in InterProcDataFlow
        Map<EdgeKey, VarContext<NotNullAbsVal>> m =
                new LinkedHashMap<EdgeKey, VarContext<NotNullAbsVal>>();
        m.put(FlowGraph.EDGE_KEY_OTHER, dfIn);

        EdgeKey errorKey = new ExceptionEdgeKey(ts.Error());
        if (peer.succEdgeKeys().contains(errorKey)) {
            m.put(errorKey,
                  dfIn.clearExprResultStack()
                      .returnResult(NotNullAbsVal.NOT_NULL));
        }
        return m;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowExpr(Expr n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        return itemToMapWithExceptionResults(dfIn.popAndPushExprResults(numArgs,
                                                                        exprIsNotNull(n,
                                                                                      dfIn),
                                                                        n),
                                             peer.succEdgeKeys(),
                                             peer);
    }

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowField(Field n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        if (n.target() instanceof Term) {
            dfIn.exprResultStack().peek();
            dfIn = dfIn.popExprResult();
        }
        Map<EdgeKey, VarContext<NotNullAbsVal>> m =
                itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);

        // if we successfully called the field, then there is a result on the stack,
        // and we know the receiver is non-null
        dfIn = dfIn.pushExprResult(exprIsNotNull(n, dfIn), n);
        if (n.target() instanceof Expr) {
            dfIn = addNotNull(dfIn, (Expr) n.target());
        }
        for (EdgeKey ek : CollectionUtil.list(FlowGraph.EDGE_KEY_OTHER,
                                              FlowGraph.EDGE_KEY_TRUE,
                                              FlowGraph.EDGE_KEY_FALSE)) {
            if (m.containsKey(ek)) {
                m.put(ek, dfIn);
            }
        }
        return m;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowReturn(Return n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // If we return a value, then we pop the result off the stack, and push it straight back on for the return.
        // If we do not return a value, then we do not change the result stack at all.
        if (n.expr() != null) {
            dfIn = dfIn.returnResult(dfIn.peekExprResult());
        }
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys(),
                                             peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowThrow(Throw n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // At the top of the stack is the exception value.
        // Get it, and set the return result ot it.
        dfIn = dfIn.returnResult(dfIn.peekExprResult());
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys(),
                                             peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowConditional(
            Conditional n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // there are two results on the stack, one from the test, and the other from the branches
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<NotNullAbsVal> res = dfIn.peekExprResults(numArgs);
        dfIn = dfIn.popAndPushExprResults(numArgs, res.get(0), n);
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowLit(Lit n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        dfIn = dfIn.popAndPushExprResults(numArgs, exprIsNotNull(n, dfIn), n);
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowCall(Call n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        FinalVarContext<NotNullAbsVal> callResult;
        try {
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);
            callResult = this.autil().call(n.methodInstance(), dfIn, callSite);
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }

        // add in the possible null pointer exception.
        dfIn = dfIn.popExprResults(n.methodInstance().formalTypes().size());
        NotNullAbsVal receiverDFI = dfIn.peekExprResult();
        dfIn = dfIn.popExprResult();

        if (receiverDFI.isMaybeNull()) {
            ExceptionKey npe = ExitMap.exceptionKey(ts.NullPointerException());
            VarContext<NotNullAbsVal> npeItem =
                    dfIn.returnResult(NotNullAbsVal.NOT_NULL)
                        .clearExprResultStack();
            callResult =
                    (FinalVarContext<NotNullAbsVal>) callResult.addKey(npe,
                                                                       VarContext.upperBound(npeItem,
                                                                                             callResult.get(npe)));
        }

        Map<EdgeKey, VarContext<NotNullAbsVal>> callResultMap =
                finalVarContextToDataFlowMap(callResult,
                                             peer.succEdgeKeys(),
                                             peer);

        // if we successfully called the method, then we know the receiver is non-null        
        if (n.target() instanceof Expr) {
            for (EdgeKey ek : CollectionUtil.list(FlowGraph.EDGE_KEY_OTHER,
                                                  FlowGraph.EDGE_KEY_TRUE,
                                                  FlowGraph.EDGE_KEY_FALSE)) {
                if (callResultMap.containsKey(ek)) {
                    callResultMap.put(ek,
                                      addNotNull(callResultMap.get(ek),
                                                 (Expr) n.target()));
                }
            }
        }

        return callResultMap;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowNew(New n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // get the arguments.                
        FinalVarContext<NotNullAbsVal> callResult;
        try {
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);
            callResult =
                    autil().callFromNew(n.constructorInstance(),
                                        dfIn,
                                        NotNullAbsVal.NOT_NULL,
                                        callSite);
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }
//        System.err.println("#### just called " + n);
//        System.err.println("      the succEdgeKeys are " + peer.succEdgeKeys());
//        System.err.println("      the keys in the final var context are "
//                + callResult.allKeys());
//        System.err.println("      the input result stack was "
//                + dfIn.exprResultStack());
//        System.err.println("      the callResult normal term is "
//                + callResult.get(ItemMap.KEY_NORM_TERM).exprResultStack());

        Map<EdgeKey, VarContext<NotNullAbsVal>> callResultMap =
                finalVarContextToDataFlowMap(callResult,
                                             peer.succEdgeKeys(),
                                             peer);

        // if we successfully called the constructor, then there is a new, non-null object on the stack!
        VarContext<NotNullAbsVal> normalTermination =
                callResultMap.get(FlowGraph.EDGE_KEY_OTHER);
        if (normalTermination == null) {
            // the constructor cannot return normally!
        }
        else {
            normalTermination =
                    normalTermination.pushExprResult(NotNullAbsVal.NOT_NULL, n);
            for (EdgeKey ek : CollectionUtil.list(FlowGraph.EDGE_KEY_OTHER,
                                                  FlowGraph.EDGE_KEY_TRUE,
                                                  FlowGraph.EDGE_KEY_FALSE)) {
                if (callResultMap.containsKey(ek)) {
                    callResultMap.put(ek, normalTermination);
                }
            }
        }
        return callResultMap;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowNewArray(NewArray n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        if (n.init() != null) {
            // pop off the initializer. 
            dfIn = dfIn.popExprResult();
        }
        // pop off the dimensions, if any
        dfIn = dfIn.popExprResults(n.dims().size());

        // pop off the base type 
        dfIn = dfIn.popExprResult();

        // pus the result on
        dfIn = dfIn.pushExprResult(NotNullAbsVal.NOT_NULL, n);

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowArrayAccess(
            ArrayAccess n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // pop off the index and the array.
        dfIn = dfIn.popExprResults(2);

        Map<EdgeKey, VarContext<NotNullAbsVal>> m =
                itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);

        // if we successfully access the array, then there is a result on the stack,
        // and we know the array is non-null
        VarContext<NotNullAbsVal> successful =
                dfIn.pushExprResult(exprIsNotNull(n, dfIn), n);
        successful = addNotNull(successful, n.array());

        for (EdgeKey k : m.keySet()) {
            if (!(k instanceof FlowGraph.ExceptionEdgeKey)) {
                m.put(k, successful);
            }
        }
        return m;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowConstructorCall(
            ConstructorCall n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        FinalVarContext<NotNullAbsVal> callResult;
        try {
            DataFlowNodeIdentifier callSite =
                    dataFlowNodeIdentifierForPeer(peer);
            callResult =
                    autil().constructorCallFromConstructor(n.constructorInstance(),
                                                           dfIn,
                                                           callSite);
        }
        catch (SemanticException ex) {
            throw new InternalCompilerError(ex);
        }
//        System.err.println("#### just did constructor call " + n);
//        System.err.println("      the succEdgeKeys are " + peer.succEdgeKeys());
//        System.err.println("      the current result has keys "
//                + callResult.allKeys());
//        System.err.println("      the input result stack was " + dfIn.exprResultStack());
//        System.err.println("      the callResult normal term is " + callResult.get(ItemMap.KEY_NORM_TERM).exprResultStack());

        Map<EdgeKey, VarContext<NotNullAbsVal>> callResultMap =
                finalVarContextToDataFlowMap(callResult,
                                             peer.succEdgeKeys(),
                                             peer);
//        System.err.println("      the current result now has keys "
//                + callResultMap.keySet());

        return callResultMap;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowUnary(Unary n,
            VarContext<NotNullAbsVal> dfIn, VarContext<NotNullAbsVal> trueItem,
            VarContext<NotNullAbsVal> falseItem,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // we pop one result and push one result.
        // but these unary operations are all on primitives, so it is always non-null, so the net effect is no change to the result stack.

        if (n.type().isBoolean()) {
            if (trueItem == null) trueItem = dfIn;
            if (falseItem == null) falseItem = dfIn;

            Map<EdgeKey, VarContext<NotNullAbsVal>> ret =
                    flowBooleanConditions(trueItem,
                                          falseItem,
                                          dfIn,
                                          graph,
                                          peer);
            if (ret != null) {
                return ret;
            }
        }
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowBinary(Binary n,
            VarContext<NotNullAbsVal> dfIn, VarContext<NotNullAbsVal> trueItem,
            VarContext<NotNullAbsVal> falseItem,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // we pop some number of results (normally 2) and push one, which is always non-null
        int numArgs = argumentsOnResultStack(n, dfIn);
        dfIn = dfIn.popAndPushExprResults(numArgs, NotNullAbsVal.NOT_NULL, n);

        if ((Binary.EQ.equals(n.operator()) || Binary.NE.equals(n.operator()))) {
            // n is an == or != expression
            if (n.left() instanceof NullLit || n.right() instanceof NullLit) {
                // n is a comparison to null                
                // e is the expression being compared with null.
                Expr e = (n.left() instanceof NullLit) ? n.right() : n.left();

                return comparisonToNull(e,
                                        Binary.EQ.equals(n.operator()),
                                        dfIn,
                                        peer.succEdgeKeys());
            }
        }
        if (n.type().isBoolean()) {
            if (trueItem == null) {
                trueItem = dfIn;
            }
            else {
                trueItem =
                        trueItem.popAndPushExprResults(numArgs,
                                                       NotNullAbsVal.NOT_NULL,
                                                       n);
            }
            if (falseItem == null) {
                falseItem = dfIn;
            }
            else {
                falseItem =
                        falseItem.popAndPushExprResults(numArgs,
                                                        NotNullAbsVal.NOT_NULL,
                                                        n);
            }

            Map<EdgeKey, VarContext<NotNullAbsVal>> ret =
                    flowBooleanConditions(trueItem,
                                          falseItem,
                                          dfIn,
                                          graph,
                                          peer);
            if (ret != null) {
                return ret;
            }
        }
        return itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowAssign(Assign n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // the number of arguments on the stack depend on the kind of assignment...
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<NotNullAbsVal> results = dfIn.peekExprResults(numArgs);
        dfIn =
                kill(dfIn.popAndPushExprResults(numArgs, results.get(0), n),
                     n.left());

        if (n.operator() != Assign.ASSIGN || results.get(0).isNotNull()) {
            dfIn = addNotNull(dfIn, n.left());
        }

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowInstanceof(Instanceof n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        int numArgs = argumentsOnResultStack(n, dfIn);
        dfIn = dfIn.popAndPushExprResults(numArgs, NotNullAbsVal.NOT_NULL, n); // the result of the instanceof is a primitive

        // on the true branch of an instanceof, we know that expression is not null
        VarContext<NotNullAbsVal> trueBranch = addNotNull(dfIn, n.expr());
        return itemsToMap(trueBranch, dfIn, dfIn, peer.succEdgeKeys());
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowCast(Cast n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // we pop two results expression and the cast type, and push the expression (index 1).
        int numArgs = argumentsOnResultStack(n, dfIn);
        List<NotNullAbsVal> res = dfIn.peekExprResults(numArgs);
        dfIn = dfIn.popAndPushExprResults(numArgs, res.get(1), n);

        // Interestingly, if we get a class cast exception, then we know that the expression being cast is non null 
        Map<EdgeKey, VarContext<NotNullAbsVal>> m =
                itemToMapWithExceptionResults(dfIn, peer.succEdgeKeys(), peer);
        ExceptionEdgeKey cce =
                new ExceptionEdgeKey(this.typeSystem().ClassCastException());
        if (m.containsKey(cce)) {
            m.put(cce, addNotNull(m.get(cce), n.expr()));
        }
        return m;
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowLocalDecl(LocalDecl n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        if (n.init() != null) {
            NotNullAbsVal initRes = dfIn.peekExprResult();
            dfIn = dfIn.addLocal(n.name(), initRes);
        }

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

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowFieldDecl(FieldDecl n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        if (n.init() != null) {
            NotNullAbsVal initRes = dfIn.peekExprResult();
            // well, at the moment, we don't really track non-null fields,
            // since we can only do weak updates. But this would be a good
            // place to modify code if/when we can do strong updates.
        }

        // Make sure to *not* rely on peer.succEdgeKeys() for the contents of the map.
        return Collections.singletonMap(FlowGraph.EDGE_KEY_OTHER,
                                        dfIn.clearExprResultStack());
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowFormal(Formal n,
            VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // if it is a catch formal, it cannot be null...
        ExtFormal ef = (ExtFormal) AccrueExt_c.ext(n);
        if (ef.isCatchFormal()) {
            dfIn = dfIn.addLocal(n.name(), NotNullAbsVal.NOT_NULL);
        }
        return itemToMapWithExceptionResults(dfIn.clearExprResultStack(),
                                             peer.succEdgeKeys(),
                                             peer);
    }

    private NotNullAbsVal exprIsNotNull(Expr e, VarContext<NotNullAbsVal> dfIn) {
        if (e instanceof New) return NotNullAbsVal.NOT_NULL;
        if (e instanceof Special) return NotNullAbsVal.NOT_NULL;
        if (e.type().isNull()) return NotNullAbsVal.MAYBE_NULL;
        if (!e.type().isReference()) return NotNullAbsVal.NOT_NULL;

        if (e instanceof Lit) {
            if (e.constantValue() == null) return NotNullAbsVal.MAYBE_NULL;
            return NotNullAbsVal.NOT_NULL;
        }

        if (e instanceof Local) {
            NotNullAbsVal nn =
                    dfIn.getLocalAbsVal(((Local) e).name(), e.type());
            if (nn == null) return NotNullAbsVal.MAYBE_NULL;
            return nn;
        }
        if (e instanceof Field) {
            NotNullAbsVal nn =
                    autil().getLocationAbsVal(dfIn,
                                              autil().abstractLocations((Field) e));
            if (nn == null) return NotNullAbsVal.MAYBE_NULL;
            return nn;
        }
        if (e instanceof ArrayAccess) {
            NotNullAbsVal nn =
                    autil().getLocationAbsVal(dfIn,
                                              autil().abstractLocations((ArrayAccess) e));
            if (nn == null) return NotNullAbsVal.MAYBE_NULL;
            return nn;
        }
        if (e instanceof ArrayInit) {
            return NotNullAbsVal.MAYBE_NULL;
        }

        return NotNullAbsVal.MAYBE_NULL;
    }

    private static VarContext<NotNullAbsVal> addNotNull(
            VarContext<NotNullAbsVal> dfIn, Expr e) {
        if (e instanceof Local) {
            dfIn = dfIn.addLocal(((Local) e).name(), NotNullAbsVal.NOT_NULL);
        }
        // that's all we track at the moment... Maybe we'll add more things that can be strongly updated later
        return dfIn;
    }

    private static VarContext<NotNullAbsVal> kill(
            VarContext<NotNullAbsVal> dfIn, Expr e) {
        if (e instanceof Local) {
            dfIn = dfIn.addLocal(((Local) e).name(), NotNullAbsVal.MAYBE_NULL);
        }
        return dfIn;
    }

    /**
     * Utility method used to produce appropriate
     * DataFlowItems when expressions that compare local variables to null
     * are evaluated to true and false.
     */
    private static Map<EdgeKey, VarContext<NotNullAbsVal>> comparisonToNull(
            Expr expr, boolean equalsEquals, VarContext<NotNullAbsVal> in,
            Set<EdgeKey> edgeKeys) {
        VarContext<NotNullAbsVal> eq = kill(in, expr);
        VarContext<NotNullAbsVal> neq = addNotNull(in, expr);

        if (equalsEquals) {
            return itemsToMap(eq, neq, in, edgeKeys);
        }
        else {
            return itemsToMap(neq, eq, in, edgeKeys);
        }
    }

    @Override
    protected Object clone() throws CloneNotSupportedException {
        // TODO Auto-generated method stub
        return super.clone();
    }

    /**
     * "Check" the nodes of the graph for the not null analysis. This actually
     * consists of setting various "not null" flags in the extensions.
     */
    @Override
    protected void check(FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> p) throws SemanticException {
        if (p.isEntry()) {
            return;
        }

        if (p.node() instanceof Expr) {
            Expr e = (Expr) p.node();

            if (!e.type().isPrimitive()) {
                VarContext<NotNullAbsVal> normTerm =
                        p.outItem(FlowGraph.EDGE_KEY_OTHER);
                if (normTerm != null) {
                    ExtExpr ext = (ExtExpr) AccrueExt_c.ext(e);
                    if (normTerm.exprResultStack().isEmpty()) {
                        // this code is unreachable, e.g., a.foo() where a is always null. 
                        ext.recordNullAnalysisResult(autil().currentContext(),
                                                     p.peerKey(),
                                                     false);
                        System.err.println("**** warning, empty expression result stack for "
                                + p.node());
                        //throw new InternalCompilerError("Empty expr result stack for " + e);
                    }
                    else {
                        ext.recordNullAnalysisResult(autil().currentContext(),
                                                     p.peerKey(),
                                                     normTerm.exprResultStack()
                                                             .peek()
                                                             .isMaybeNull());
                    }

                    // OK, it maybe doesn't belong here, but we'll do it anyway.
                    if (e instanceof Cast) {
                        ((ExtCast) ext).recordClassCastAnalysisResult(autil());
                    }
                }
                else {
                    // it's possible that the expression doesn't have a normal termination, e.g., if it is a call
                    // that cannot terminate normally.
                }
            }
        }
//        VarContext<NotNullAbsVal> dfIn = (VarContext<NotNullAbsVal>)p.inItem();
        if (p.node() instanceof Field) {
            //System.out.println("*** Field " + p.node() + " target " + dfIn.exprResultStack().peek());            
        }
        else if (p.node() instanceof Call
                && ((Call) p.node()).target() instanceof Expr) {
//            boolean maybeNull = ((ExtExpr)AccrueExt_c.ext(((Call)p.node()).target())).mayBeNull(autil.currentContext());
            //System.out.println("*** Call " + p.node() + " target is " + (maybeNull?"MAYBE NULL" : "NOT NULL"));
            //System.out.println("     locals are " + ((DFIContext<NotNullDFI>)p.outItem(FlowGraph.EDGE_KEY_OTHER)).locals());
        }
        else if (p.node() instanceof FieldAssign) {
            FieldAssign fa = (FieldAssign) p.node();
            Receiver target = fa.left().target();
            if (target instanceof Expr) {
//                boolean maybeNull = ((ExtExpr)AccrueExt_c.ext(target)).mayBeNull(autil.currentContext());
                //System.out.println("*** Field assign " + p.node() + " target " + (maybeNull?"MAYBE NULL" : "NOT NULL"));            
            }
        }

    }

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

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

    @Override
    protected VarContext<NotNullAbsVal> constructMissingContextForEdgeKey(
            EdgeKey ek, FinalVarContext<NotNullAbsVal> f,
            Peer<VarContext<NotNullAbsVal>> peer) {
        VarContext<NotNullAbsVal> ret = null;
        if (ek instanceof ExceptionEdgeKey) {
            // we have an exception!
            ExceptionEdgeKey eek = (ExceptionEdgeKey) ek;
            if (eek.type().isSubtype(ts.Error())) {
                // use the normal termination, since it could be a real Error 
                ret = f.normalTermination();
            }
            if (ret == null) {
                ret =
                        new VarContext<NotNullAbsVal>(this.autil()
                                                          .analysisName(),
                                                      this.autil()
                                                          .bottomAbstractValue());

            }
            // the exception itself cannot be null.
            ret =
                    ret.returnResult(NotNullAbsVal.NOT_NULL)
                       .clearExprResultStack();
        }
        return ret;
    }

    /*******************************************************
     * The following methods provide support for JL5 language features.
     * We include them here rather than in a subclass, since many (most?)
     * uses of Accrue will be for JL5 or above
     */

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowEnumConstantDecl(
            EnumConstantDecl n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // treat it like a field decl. That is
        // FOO(a, b) is kind of equivalent to 
        // static final MyEnumClass FOO = new MyEnumClass(a, b);

        // That said, we don't actually track non-nullity of fields very well...

        // Make sure to *not* rely on peer.succEdgeKeys() for the contents of the map.
        return Collections.singletonMap(FlowGraph.EDGE_KEY_OTHER,
                                        dfIn.clearExprResultStack());

    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowEnumConstant(
            EnumConstant n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        // treat an enum constant like a field
        return flowField(n, dfIn, graph, peer);
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowExtendedFor(
            ExtendedFor n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        throw new UnsupportedOperationException("This analysis does not support "
                + "ExtendedFor AST nodes. Run the SimplifyExpressions pass first "
                + "to desugar them into other AST nodes.");
    }

    @Override
    public Map<EdgeKey, VarContext<NotNullAbsVal>> flowParamTypeNode(
            ParamTypeNode n, VarContext<NotNullAbsVal> dfIn,
            FlowGraph<VarContext<NotNullAbsVal>> graph,
            Peer<VarContext<NotNullAbsVal>> peer) {
        return flowTypeNode(n, dfIn, graph, peer);
    }
}
