package accrue.analysis.pointer;

import polyglot.frontend.ExtensionInfo;
import polyglot.main.Main.TerminationException;
import polyglot.types.ProcedureInstance;
import polyglot.util.InternalCompilerError;
import accrue.analysis.pointer.analyses.HeapAbstractionFactory;

public abstract class PointsToEngine {
    /**
     * How long to run the engine before timing out, in milliseconds.
     * E.g., timeout_millisecs == 10000 means that we will run the
     * engine for at most about 10 seconds.
     */
    private Long timeout_millisecs = null;

    /**
     * The time at which the engine started
     */
    private Long startTime = null;

    /**
     * The time at which the engine should time out.
     * This is equal to startTime + timeout_millisecs
     */
    private Long timeoutTime = null;

    /**
     * The heap abstraction to use for this engine.
     */
    private final HeapAbstractionFactory haf;

    protected PointsToEngine() {
        this.haf = null;
    }

    public PointsToEngine(HeapAbstractionFactory haf) {
        this.haf = haf;
    }

    protected Long startTime() {
        return startTime;
    }

    protected Long timeoutTime() {
        return timeoutTime;
    }

    protected Long timeout() {
        return timeout_millisecs;
    }

    public void setTimeout(Long timeout_millisecs) {
        if (startTime != null) {
            throw new InternalCompilerError("Already started engine. Cannot set timeout now.");
        }
        this.timeout_millisecs = timeout_millisecs;
    }

    public HeapAbstractionFactory heapAbstractionFactory() {
        return haf;
    }

    protected void startSolution() {
        this.startTime = System.currentTimeMillis();
        if (timeout_millisecs != null) {
            timeoutTime = startTime + timeout_millisecs;
        }
    }

    protected void checkTimeout() {
        if (timeoutTime != null) {
            if (System.currentTimeMillis() > timeoutTime) {
                throw new PointsToTimeoutException();
            }
        }
    }

    public final PointsToGraph solve(StmtRegistrar registrar,
            ExtensionInfo extInfo) {
        startSolution();
        PointsToGraph g = solveImpl(registrar, extInfo);
        g.setSolved();
        return g;
    }

    protected abstract PointsToGraph solveImpl(StmtRegistrar registrar,
            ExtensionInfo extInfo);

    abstract void recordRead(StmtAndContext sac, PointsToGraphNode r);

    abstract void newContext(ProcedureInstance callee, CContext calleeContext);

    abstract void changedNode(PointsToGraphNode n);

    protected void checkReachedFixedpoint(StmtRegistrar registrar,
            PointsToGraph g) {
        // for safety, do a pass through again...
        //System.err.println("Checking correctness of points to graph engine...");
        for (PointsToStmt s : registrar.stmts()) {
            for (CContext context : g.getContexts(s.codeInstance)) {
                boolean thisChanged =
                        s.process(context,
                                  g,
                                  registrar,
                                  this.heapAbstractionFactory(),
                                  new StmtAndContext(s, context));
                if (thisChanged) {
                    throw new InternalCompilerError("Processed a statement that changed the points to graph: "
                            + s);
                }
            }
        }
//        System.err.println("  Checked a total of " + count + " statements");
    }

    @Override
    public String toString() {
        return this.getClass().getSimpleName() + " with abstraction "
                + this.heapAbstractionFactory();
    }

    public static class PointsToTimeoutException extends TerminationException {
        public PointsToTimeoutException() {
            super("Pointer analysis timed out");
        }

    }

    public static class StmtAndContext {
        final CContext context;
        final PointsToStmt stmt;

        public StmtAndContext(PointsToStmt stmt, CContext context) {
            this.stmt = stmt;
            this.context = context;
        }

        @Override
        public int hashCode() {
            return context.hashCode() ^ stmt.hashCode();
        }

        @Override
        public boolean equals(Object o) {
            if (this == o) return true;
            StmtAndContext that = (StmtAndContext) o;
            return this.context.equals(that.context)
                    && this.stmt.equals(that.stmt);
        }
    }

}
