package accrue.analysis.interprocanalysis;

import java.util.Collection;
import java.util.Collections;

import polyglot.ast.Block;
import polyglot.ast.Catch;
import polyglot.ast.CodeNode;
import polyglot.ast.CompoundStmt;
import polyglot.ast.JLang;
import polyglot.ast.NodeFactory;
import polyglot.ast.Stmt;
import polyglot.ast.Term;
import polyglot.ast.Try;
import polyglot.frontend.Job;
import polyglot.types.ClassType;
import polyglot.types.TypeSystem;
import polyglot.visit.CFGBuilder;
import polyglot.visit.DataFlow;
import polyglot.visit.FlowGraph;
import polyglot.visit.FlowGraph.Peer;
import accrue.analysis.ext.AccrueExt_c;
import accrue.analysis.ext.ExtTerm;
import accrue.analysis.preciseExceptions.ThrowableType;

/**
 * Uses the results of precise exceptions analysis to create a more accurate
 * control flow graph.
 * 
 * Any analysis pass that uses PreciseDataFlow to perform analysis should have as a 
 * prerequisite the goal AnalysisScheduler.PreciseExceptionAnalysis(2). This will
 * run 2 passes of the PreciseExceptions pass, as well as a NotNullAnalysisPass, and 
 * use the results to produce a more accurate control flow graph.
 * 
 * @param <FlowItem>
 *            The DataFlow.Item that the dataflow propagates 
 */
public abstract class PreciseDataFlow<FlowItem extends DataFlow.Item> extends
        DataFlow<FlowItem> {

    /**
     * Analysis helper class
     */
    private final AnalysisUtil<?> autil;

    /**
     * Create a new dataflow visitor
     * 
     * @param autil
     *            Analysis helper class
     * @param job
     *            Polyglot compiler {@link Job}
     * @param ts
     *            Polyglot type system
     * @param nf
     *            factory for creating AST nodes
     * @param forward
     *            forward or backward dataflow
     */
    public PreciseDataFlow(AnalysisUtil<?> autil, Job job, TypeSystem ts,
            NodeFactory nf, boolean forward) {
        this(autil, job, ts, nf, forward, false);
    }

    /**
     * Create a new dataflow visitor
     * 
     * @param context
     *            Initial analysis context
     * @param autil
     *            Analysis helper class
     * @param job
     *            Polyglot compiler {@link Job}
     * @param ts
     *            Polyglot type system
     * @param nf
     *            factory for creating AST nodes
     * @param forward
     *            forward or backward dataflow
     * @param dataflowOnEntry
     * 			  true if we want to process the entry node
     */
    public PreciseDataFlow(AnalysisUtil<?> autil, Job job, TypeSystem ts,
            NodeFactory nf, boolean forward, boolean dataflowOnEntry) {
        this(autil, job, ts, nf, forward, dataflowOnEntry, false);
    }

    /**
     * Create a new dataflow visitor
     * 
     * @param autil
     *            Analysis helper class
     * @param job
     *            Polyglot compiler {@link Job}
     * @param ts
     *            Polyglot type system
     * @param nf
     *            factory for creating AST nodes
     * @param forward
     *            forward or backward dataflow
     * @param dataflowOnEntry
     * 			  true if we want to process the entry node
     * @param trackBackEdges 
     * 			  true if the dataflow tracks backward flowgraph edges
     */
    public PreciseDataFlow(AnalysisUtil<?> autil, Job job, TypeSystem ts,
            NodeFactory nf, boolean forward, boolean dataflowOnEntry,
            boolean trackBackEdges) {
        super(job, ts, nf, forward, dataflowOnEntry, trackBackEdges);
        this.autil = autil;
    }

    @Override
    protected CFGBuilder<FlowItem> createCFGBuilder(TypeSystem ts,
            FlowGraph<FlowItem> g) {
        return new PreciseCFGBuilder<FlowItem>(lang(), ts, g, this);
    }

    @Override
    protected FlowGraph<FlowItem> initGraph(CodeNode code, Term root) {
        return new FlowGraph<FlowItem>(root, this.forward, false); // don't always have succ edge keys
    }

    /**
     * @return current procedure analysis context
     */
    public AnalysisContext currentContext() {
        return autil.currentContext();
    }

    /**
     * @return the analysis helper class
     */
    protected AnalysisUtil<?> autil() {
        return autil;
    }

    /**
     * Get the dataflow identifier object for the given flowgraph peer
     * 
     * @param peer
     *            flowgraph peer
     * @return dataflow identifier
     */
    protected DataFlowNodeIdentifier dataFlowNodeIdentifierForPeer(
            Peer<FlowItem> peer) {
        return new DataFlowNodeIdentifier_c(this.currentContext(),
                                            peer.peerKey(),
                                            peer.node());
    }

    /**
     * Get the dataflow identifier object for the given flowgraph peer in the
     * given context
     * 
     * @param peer
     *            flowgraph peer
     * @param currentContext
     *            current analysis context
     * @return dataflow identifier
     */
    protected static <FlowItem extends DataFlow.Item> DataFlowNodeIdentifier dataFlowNodeIdentifierForPeer(
            Peer<FlowItem> peer, AnalysisContext currentContext) {
        return new DataFlowNodeIdentifier_c(currentContext,
                                            peer.peerKey(),
                                            peer.node());
    }

    /**
     * Get the flowgraph peer for the given dataflow identifier
     * 
     * @param bi
     *            dataflow identifier
     * @param graph
     *            dataflow graph
     * @return flowgraph peer
     */
    protected static <FlowItem extends DataFlow.Item> Peer<FlowItem> peerForDataFlowNodeIdentifier(
            DataFlowNodeIdentifier bi, FlowGraph<FlowItem> graph) {
        return graph.peer(bi.getNode(), bi.getPeerKey());
    }

    /**
     * A more precise CFG builder that adds Exception edges only for
     * exceptions that might actually be thrown.
     */
    public static class PreciseCFGBuilder<FlowItem extends DataFlow.Item>
            extends CFGBuilder<FlowItem> {

        /**
         * Exception types to suppress
         */
        private Collection<ClassType> suppressExceptions =
                Collections.emptySet();
        /**
         * AST node to suppress exceptions on
         */
        private Term suppressTarget = null;

        /**
         * Create a new CFG builder
         * 
         * @param ts Polyglot type system
         * @param graph dataflow graph
         * @param df dataflow visitor
         */
        public PreciseCFGBuilder(JLang lang, TypeSystem ts,
                FlowGraph<FlowItem> graph, PreciseDataFlow<FlowItem> df) {
            super(lang, ts, graph, df);
            // make sure we do not track errors.
            this.errorEdgesToExitNode = true;
            // add specific edges into finally blocks for exceptions
            this.exceptionEdgesToFinally = true;
        }

        /**
         * Swap out the exceptions and target
         * 
         * @param suppressExceptions
         *            new set of expression types to suppress
         * @param suppressTarget
         *            AST node to supress them on
         * @return new {@link PreciseCFGBuilder} with the given suppressed
         *         exceptions and targets
         */
        public PreciseCFGBuilder<FlowItem> push(
                Collection<ClassType> suppressExceptions, Term suppressTarget) {

            PreciseCFGBuilder<FlowItem> v =
                    (PreciseCFGBuilder<FlowItem>) this.copy();
            v.suppressExceptions = suppressExceptions;
            v.suppressTarget = suppressTarget;
            return v;
        }

        @Override
        public void visitThrow(Term a) {
            PreciseDataFlow<FlowItem> pdf =
                    (PreciseDataFlow<FlowItem>) dataflow();
            Collection<ThrowableType> mayBeThrown = approximateThrown(a, pdf);
            for (ThrowableType tk : mayBeThrown) {
                visitThrow(a, Term.EXIT, tk);
            }

            if (trackImplicitErrors) {
                // Every statement can throw an error.
                // This is probably too inefficient.
                if ((a instanceof Stmt && !(a instanceof CompoundStmt))
                        || (a instanceof Block && ((Block) a).statements()
                                                             .isEmpty())) {

                    visitThrow(a, Term.EXIT, ts.Error());
                }
            }
        }

        /**
         * Approximate the set of exceptions that may be thrown by the
         * term a as precisely as possible
         * 
         * @param a AST node to compute the exceptions for
         * @param pdf dataflow
         */
        protected Collection<ThrowableType> approximateThrown(Term a,
                PreciseDataFlow<FlowItem> pdf) {
            ExtTerm ea = (ExtTerm) AccrueExt_c.ext(a);
            return ea.throwTypes(ts, pdf.currentContext());
        }

        /**
         * Create edges for an exception thrown from term <code>t</code>.
         * 
         * @param t
         *            AST node
         * @param entry
         *            1 if we are looking at the entry of the term
         * @param tt
         *            exception type
         */
        public void visitThrow(Term t, int entry, ThrowableType tt) {
            Peer<FlowItem> last_peer =
                    this.graph.peer(t, this.path_to_finally, entry);
            for (PreciseCFGBuilder<FlowItem> v = this; v != null; v =
                    (PreciseCFGBuilder<FlowItem>) v.outer()) {
                boolean suppress = false;
                for (ClassType ct : this.suppressExceptions) {
                    if (tt.type().isSubtype(ct)) {
                        suppress = true;
                        break;
                    }
                }
                if (suppress) {
                    if (this.suppressTarget != null) {
                        edge(last_peer,
                             this.graph.peer(this.suppressTarget,
                                             this.path_to_finally,
                                             Term.EXIT),
                             new FlowGraph.ExceptionEdgeKey(tt.type()));
                    }
                    return;
                }

                Term c = v.innermostTarget();

                if (c instanceof Try) {
                    Try tr = (Try) c;

                    if (!v.skipInnermostCatches()) {
                        boolean definiteCatch = false;

                        // No generics in polyglot
                        for (Catch cb : tr.catchBlocks()) {
                            // definite catch
                            if (tt.type().isImplicitCastValid(cb.catchType())) {
                                edge(last_peer,
                                     this.graph.peer(cb,
                                                     this.path_to_finally,
                                                     Term.ENTRY),
                                     new FlowGraph.ExceptionEdgeKey(tt.type()));
                                definiteCatch = true;
                            }
                            // possible catch
                            else if (!tt.isExactType()
                                    && cb.catchType()
                                         .isImplicitCastValid(tt.type())) {
                                edge(last_peer,
                                     this.graph.peer(cb,
                                                     this.path_to_finally,
                                                     Term.ENTRY),
                                     new FlowGraph.ExceptionEdgeKey(cb.catchType()));
                            }
                        }
                        if (definiteCatch) {
                            // the exception has definitely been caught.
                            // we can stop recursing to outer try-catch blocks
                            return;
                        }
                    }

                    if (tr.finallyBlock() != null) {
                        if (exceptionEdgesToFinally) {
                            last_peer =
                                    tryFinally(v,
                                               last_peer,
                                               last_peer.node() == t,
                                               new FlowGraph.ExceptionEdgeKey(tt.type()),
                                               tr.finallyBlock());
                        }
                        else {
                            last_peer =
                                    tryFinally(v,
                                               last_peer,
                                               last_peer.node() == t,
                                               tr.finallyBlock());
                        }
                    }
                }
            }

            // If not caught, insert a node from the thrower to exit.
            if (errorEdgesToExitNode || !tt.type().isSubtype(ts.Error())) {
                edge(last_peer,
                     exitPeer(),
                     new FlowGraph.ExceptionEdgeKey(tt.type()));
            }
        }
    }

}
