package accrue.analysis.pointer;

import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.Iterator;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.concurrent.ConcurrentHashMap;
import java.util.concurrent.ConcurrentMap;

import polyglot.ast.Call;
import polyglot.ast.ClassLit;
import polyglot.ast.CodeNode;
import polyglot.ast.Expr;
import polyglot.ast.FieldDecl;
import polyglot.ast.Formal;
import polyglot.ast.Initializer;
import polyglot.ast.Local;
import polyglot.ast.ProcedureDecl;
import polyglot.ast.Term;
import polyglot.frontend.ExtensionInfo;
import polyglot.main.Report;
import polyglot.types.ArrayType;
import polyglot.types.ClassType;
import polyglot.types.CodeInstance;
import polyglot.types.ConstructorInstance;
import polyglot.types.FieldInstance;
import polyglot.types.InitializerInstance;
import polyglot.types.LocalInstance;
import polyglot.types.MemberInstance;
import polyglot.types.MethodInstance;
import polyglot.types.ProcedureInstance;
import polyglot.types.ReferenceType;
import polyglot.types.SemanticException;
import polyglot.types.Type;
import polyglot.types.TypeSystem;
import polyglot.util.ErrorInfo;
import polyglot.util.InternalCompilerError;
import polyglot.util.Position;
import accrue.AccrueExtensionInfo;
import accrue.AccrueOptions;
import accrue.analysis.AnalysisTopics;
import accrue.analysis.ext.AccrueExt_c;
import accrue.analysis.ext.ExtAlloc;
import accrue.analysis.ext.ExtCall;
import accrue.analysis.ext.ExtExpr;
import accrue.analysis.ext.ExtFormal;
import accrue.analysis.ext.ExtProcedureCall;
import accrue.analysis.ext.ExtProcedureDecl;
import accrue.analysis.interprocanalysis.Registrar;
import accrue.analysis.interprocvarcontext.SignatureRepository;
import accrue.analysis.pointer.PointsToEngine.StmtAndContext;
import accrue.analysis.pointer.StmtProcedureCall.ExceptionHandlerPointsToGraphNode;
import accrue.analysis.pointer.analyses.HeapAbstractionFactory;
import accrue.analysis.signatures.AnalysisSignatures;

public class StmtRegistrar {
    /**
     * A register of ReferenceVariables that map to LocalInstances in CodeInstances
     * (and, if the code instance is an instance initializer, it also
     * requires a constructor instance that it is associated with.)
     */
    private Map<LICI, ReferenceVariable> localDecls =
            new LinkedHashMap<LICI, ReferenceVariable>();

    private Map<FieldInstance, ReferenceVariable> staticFields =
            new LinkedHashMap<FieldInstance, ReferenceVariable>();

    private Map<ProcedureInstance, CodeInfo> codeDecls =
            new LinkedHashMap<ProcedureInstance, CodeInfo>();
    private Map<CodeNode, CodeInfo> staticInitializerDecls =
            new LinkedHashMap<CodeNode, CodeInfo>();
    private Map<ClassType, List<CodeNode>> instanceInitializerDecls =
            new LinkedHashMap<ClassType, List<CodeNode>>();
    private Set<ProcedureDecl> startProcs = new LinkedHashSet<ProcedureDecl>();

    private ConcurrentMap<ProcedureInstance, ErrorInfo> missingCode =
            new ConcurrentHashMap<ProcedureInstance, ErrorInfo>();
    private ConcurrentMap<ProcedureInstance, LibraryPointsToSignature> missingCodeSignatures =
            new ConcurrentHashMap<ProcedureInstance, LibraryPointsToSignature>();

    private List<PointsToStmt> stmts = new ArrayList<PointsToStmt>();
    private Map<CodeInstance, List<PointsToStmt>> codeToStmts =
            new LinkedHashMap<CodeInstance, List<PointsToStmt>>();

    private Map<ClassType, ReferenceVariable> classLiterals =
            new LinkedHashMap<ClassType, ReferenceVariable>();

    /**
     * This reference variable represents an abstract Error object that may be thrown
     * implicitly by any statement. Think of it as like an exception object stored
     * in a static field, and when there is a "catch (Error e) { ... }" or a 
     * "catch (Throwable e) { ... }" handler, then e may point to whatever is pointed
     * to by programWideError.
     */
    private ReferenceVariable programWideError;

    private final AccrueExtensionInfo extInfo;

    protected static Map<ExtensionInfo, Map<ClassType, ReferenceVariable>> generatedExceptionNodes =
            new LinkedHashMap<ExtensionInfo, Map<ClassType, ReferenceVariable>>();

    protected static final boolean USE_SINGLE_ALLOC_NODE_FOR_GENERATED_EXCEPTIONS =
            false;

    public static String ARRAY_CONTENTS = "[contents]";

    public StmtRegistrar(ExtensionInfo extInfo) {
        this.extInfo = (AccrueExtensionInfo) extInfo;
    }

    public Collection<PointsToStmt> stmts() {
        return this.stmts;
    }

    public Collection<PointsToStmt> stmtsForCode(CodeInstance ci) {
        List<PointsToStmt> ret = this.codeToStmts.get(ci);
        if (ret == null) return Collections.emptySet();
        return ret;
    }

    public Collection<ErrorInfo> missingCode() {
        return missingCode.values();
    }

    public ReferenceVariable registerLocalDecl(LocalInstance li,
            CodeInfo containingCode, ConstructorContext constructorContext) {
        LICI key =
                new LICI(li, containingCode.codeInstance, constructorContext);
        ReferenceVariable ln =
                freshReferenceVariable(li.name(),
                                       false,
                                       li.type(),
                                       li.position());
        localDecls.put(key, ln);
        return ln;
    }

    public boolean hasReferenceVariable(LocalInstance li,
            CodeInfo containingCode, ConstructorContext constructorContext) {
        LICI key =
                new LICI(li, containingCode.codeInstance, constructorContext);
        return localDecls.containsKey(key);
    }

    public Local updateReferenceVariable(Local e, CodeInfo containingCode,
            ConstructorContext constructorContext) {
        LICI key =
                new LICI(e.localInstance(),
                         containingCode.codeInstance,
                         constructorContext);
        if (localDecls.containsKey(key)) {
            return (Local) setReferenceVariable(e,
                                                localDecls.get(key),
                                                constructorContext);
        }
        throw new InternalCompilerError("Screwed up the local decl stuff, there should be a defining instance");
    }

    public Expr createFreshReferenceVariable(Expr e,
            ConstructorContext constructorContext) {
        return createFreshReferenceVariable(e, e.toString(), constructorContext);
    }

    public Expr createFreshReferenceVariable(Expr e, String debugString,
            ConstructorContext constructorContext) {
        if (e instanceof Local) {
            throw new InternalCompilerError("Should only be called on non-locals");
        }

        return setReferenceVariable(e,
                                    freshReferenceVariable(debugString,
                                                           false,
                                                           e.type(),
                                                           e.position()),
                                    constructorContext);

    }

    public void registerArrayClone(Call c, CodeInfo codeInfo,
            ConstructorContext constructorContext) {
        if (!(c.target().type().isArray()
                && c.methodInstance().name().equals("clone") && c.methodInstance()
                                                                 .formalTypes()
                                                                 .isEmpty())) {
            throw new InternalCompilerError("Wrong method...");
        }
        ExtCall extClone = (ExtCall) AccrueExt_c.ext(c);

        CallSiteNode callSiteNode =
                freshCallSiteNode(c.methodInstance(),
                                  "array clone call",
                                  c.position());
        extClone.setCallSiteNode(callSiteNode);

        ArrayType type = (ArrayType) c.target().type();

        // "c = new"
        ClassType container =
                ((MemberInstance) codeInfo.codeInstance).container().toClass();
        this.addStmt(new StmtAllocToLocal(extClone.getReferenceVariable(constructorContext),
                                          freshAllocNode(type,
                                                         container,
                                                         true,
                                                         c.toString(),
                                                         c.position()),
                                          c.position(),
                                          codeInfo.codeInstance));

        // add assignments so that the contents of the clone point to the same things as the contents
        // of the original
        ExtExpr extArray = (ExtExpr) AccrueExt_c.ext(c.target());

        ReferenceVariable temp =
                freshReferenceVariable("Clone temp",
                                       false,
                                       type.base(),
                                       c.position());

        // temp = array.contents
        // c.contents = temp
        addAssignment(temp,
                      extArray.getReferenceVariable(constructorContext),
                      ARRAY_CONTENTS,
                      type.base(),
                      c.position(),
                      codeInfo);
        addAssignmentToField(extClone.getReferenceVariable(constructorContext),
                             ARRAY_CONTENTS,
                             type.base(),
                             temp,
                             c.position(),
                             codeInfo);
    }

    public void registerAlloc(ExtExpr ext, Type allocatedType,
            CodeInfo codeInfo, ConstructorContext constructorContext) {
        String name = allocatedType.toString();
        if (allocatedType.isClass()) name = allocatedType.toClass().name();
        registerAlloc(ext, allocatedType, name, codeInfo, constructorContext);
    }

    public void registerAlloc(ExtExpr ext, Type allocatedType,
            String debugString, CodeInfo codeInfo,
            ConstructorContext constructorContext) {
        ClassType container =
                ((MemberInstance) codeInfo.codeInstance).container().toClass();
        ExtAlloc extAlloc = (ExtAlloc) ext;
        extAlloc.setAllocNode(freshAllocNode(allocatedType,
                                             container,
                                             true,
                                             debugString,
                                             ext.node().position()),
                              constructorContext);
        this.addStmt(new StmtAllocToLocal(ext.getReferenceVariable(constructorContext),
                                          extAlloc.getAllocNode(constructorContext),
                                          ext.node().position(),
                                          codeInfo.codeInstance));
    }

    public void registerStringLiteral(Expr e, CodeInfo codeInfo,
            ConstructorContext constructorContext) {

        ClassType container =
                ((MemberInstance) codeInfo.codeInstance).container().toClass();
        ExtExpr ext = (ExtExpr) AccrueExt_c.ext(e);
        AllocSiteNode sln =
                freshAllocNode(e.type().toClass(),
                               container,
                               true,
                               e.toString(),
                               e.position());
        this.addStmt(new StmtAllocToLocal(ext.getReferenceVariable(constructorContext),
                                          sln,
                                          e.position(),
                                          codeInfo.codeInstance));
    }

    public void registerClassLiteral(ClassLit lit, CodeInfo codeInfo,
            ConstructorContext constructorContext) {
        ClassType type = lit.typeNode().type().toClass();

        ReferenceVariable classLit = classLiterals.get(type);
        ;
        if (classLit == null) {
            TypeSystem ts = type.typeSystem();
            classLit =
                    registerStaticAlloc(ts.Class(), true, "class-literal-"
                            + type.fullName(), Position.COMPILER_GENERATED);

            classLiterals.put(type, classLit);
        }

        ExtExpr ext = (ExtExpr) AccrueExt_c.ext(lit);
        this.addStmt(new StmtLocalToLocal(ext.getReferenceVariable(constructorContext),
                                          classLit,
                                          lit.position(),
                                          codeInfo.codeInstance));
    }

    public ReferenceVariable registerAlloc(ReferenceType type, Position origin,
            String debugString, CodeInfo codeInfo) {
        ClassType container =
                ((MemberInstance) codeInfo.codeInstance).container().toClass();
        AllocSiteNode asn =
                freshAllocNode(type, container, true, debugString, origin);
        ReferenceVariable ln =
                freshReferenceVariable(debugString + "'", false, type, origin);
        this.addStmt(new StmtAllocToLocal(ln,
                                          asn,
                                          origin,
                                          codeInfo.codeInstance));
        return ln;
    }

    public ReferenceVariable registerStaticAlloc(Type type,
            boolean isPreciseType, String debugString, Position pos) {
        ReferenceVariable ln =
                freshReferenceVariable(debugString + "'", true, type, pos);
        MethodInstance main = null;
        for (ProcedureDecl pd : this.getStartProcs()) {
            if (pd.codeInstance() instanceof MethodInstance) {
                main = (MethodInstance) pd.codeInstance();
                break;
            }
        }

        if (main == null) {
            // we don't have a main method yet.
            queueStaticAlloc(ln, type, isPreciseType, debugString, pos);
        }
        else {
            processStaticAlloc(ln, type, isPreciseType, debugString, pos, main);
        }

        return ln;
    }

    private void processStaticAlloc(ReferenceVariable left, Type type,
            boolean isPreciseType, String debugString, Position pos,
            MethodInstance main) {
        ClassType container = (ClassType) main.container();
        AllocSiteNode asn =
                freshAllocNode(type, container, isPreciseType, debugString, pos);

        this.addStmt(new StmtAllocToLocal(left, asn, null, main));
    }

    /**
     * left = right
     */
    public void addAssignment(ReferenceVariable left, ReferenceVariable right,
            Position origin, CodeInfo codeInfo) {
        if (left == null) throw new InternalCompilerError("Null left", origin);
        if (right == null)
            throw new InternalCompilerError("Null right", origin);
        this.addStmt(new StmtLocalToLocal(left,
                                          right,
                                          origin,
                                          codeInfo.codeInstance));
    }

    /**
     * left = right, and only allow left to point to objects that are subtypes of t and
     * not subtypes of any element of notT.
     */
    public void addFilteredAssignment(ReferenceVariable left,
            ReferenceVariable right, Type t, Set<Type> notT, Position origin,
            CodeInfo codeInfo) {
        this.addStmt(new StmtFilteredLocalToLocal(left,
                                                  right,
                                                  t,
                                                  new LinkedHashSet<Type>(notT),
                                                  origin,
                                                  codeInfo.codeInstance));
    }

    /**
     * left = right.fi
     */
    public void addAssignment(ReferenceVariable left, ReferenceVariable right,
            FieldInstance fi, Position origin, CodeInfo codeInfo) {
        this.addStmt(new StmtFieldToLocal(left,
                                          right,
                                          fi,
                                          origin,
                                          codeInfo.codeInstance));
    }

    /**
     * left = right.fi
     */
    public void addAssignment(ReferenceVariable left, ReferenceVariable right,
            String field, Type expectedFieldType, Position origin,
            CodeInfo codeInfo) {
        this.addStmt(new StmtFieldToLocal(left,
                                          right,
                                          field,
                                          expectedFieldType,
                                          origin,
                                          codeInfo.codeInstance));
    }

    /**
     * left.fi = right
     */
    public void addAssignmentToField(ReferenceVariable left, FieldInstance fi,
            ReferenceVariable right, Position origin, CodeInfo codeInfo) {
        if (fi.flags().isStatic()) {
            throw new InternalCompilerError("static field");
        }
        if (right == null) {
            throw new InternalCompilerError("no right", origin);
        }
        this.addStmt(new StmtLocalToField(left,
                                          fi,
                                          right,
                                          origin,
                                          codeInfo.codeInstance));
    }

    /**
     * left.fi = right
     */
    public void addAssignmentToField(ReferenceVariable left, String fi,
            Type expectedFieldType, ReferenceVariable right, Position origin,
            CodeInfo codeInfo) {
        this.addStmt(new StmtLocalToField(left,
                                          fi,
                                          expectedFieldType,
                                          right,
                                          origin,
                                          codeInfo.codeInstance));
    }

    public void addStaticCall(ReferenceVariable result, MethodInstance mi,
            ExtProcedureCall ext, List<ReferenceVariable> actuals,
            List<ExceptionHandlerReferenceVariable> exceptionHandlers,
            Map<Type, ReferenceVariable> procedureThrows, Position origin,
            CodeInfo codeInfo) {
        CallSiteNode callSiteNode =
                freshCallSiteNode(mi, "static call", origin);
        ext.setCallSiteNode(callSiteNode);
        this.addStmt(new StmtStaticMethodCall(result,
                                              callSiteNode,
                                              mi,
                                              actuals,
                                              exceptionHandlers,
                                              procedureThrows,
                                              origin,
                                              codeInfo.codeInstance));
    }

    public void addSpecialCall(ReferenceVariable result,
            ReferenceVariable receiver, MethodInstance mi,
            ExtProcedureCall ext, List<ReferenceVariable> actuals,
            List<ExceptionHandlerReferenceVariable> exceptionHandlers,
            Map<Type, ReferenceVariable> procedureThrows, Position origin,
            CodeInfo codeInfo) {
        CallSiteNode callSiteNode =
                freshCallSiteNode(mi, "super method call", origin);
        ext.setCallSiteNode(callSiteNode);
        this.addStmt(new StmtSpecialMethodCall(result,
                                               receiver,
                                               callSiteNode,
                                               mi,
                                               actuals,
                                               exceptionHandlers,
                                               procedureThrows,
                                               origin,
                                               codeInfo.codeInstance));
    }

    public void addConstructorCall(ReferenceVariable receiver,
            ConstructorInstance ci, ExtProcedureCall ext,
            List<ReferenceVariable> actuals,
            List<ExceptionHandlerReferenceVariable> exceptionHandlers,
            Map<Type, ReferenceVariable> procedureThrows, Position origin,
            CodeInfo codeInfo) {

        CallSiteNode callSiteNode =
                freshCallSiteNode(ci, "constructor call", origin);
        ext.setCallSiteNode(callSiteNode);
        this.addStmt(new StmtConstructorCall(receiver,
                                             callSiteNode,
                                             ci,
                                             actuals,
                                             exceptionHandlers,
                                             procedureThrows,
                                             origin,
                                             codeInfo.codeInstance));
    }

    public void addVirtualCall(ReferenceVariable result,
            ReferenceVariable receiver, MethodInstance pi,
            ExtProcedureCall ext, List<ReferenceVariable> actuals,
            List<ExceptionHandlerReferenceVariable> exceptionHandlers,
            Map<Type, ReferenceVariable> procedureThrows, Position origin,
            CodeInfo codeInfo) {
        CallSiteNode callSiteNode =
                freshCallSiteNode(pi, "virtual call", origin);
        ext.setCallSiteNode(callSiteNode);
        this.addStmt(new StmtVirtualMethodCall(result,
                                               receiver,
                                               callSiteNode,
                                               pi,
                                               actuals,
                                               exceptionHandlers,
                                               procedureThrows,
                                               origin,
                                               codeInfo.codeInstance));
    }

    /**
     * catch (T e) { ... } 
     * where T is either a subtype of Error, or a supertype of Error.
     */
    public void addCatchImplicitError(ReferenceVariable catchFormal,
            Position origin, CodeInfo codeInfo) {

        if (programWideError == null) {
            TypeSystem ts = codeInfo.codeInstance.typeSystem();

            programWideError =
                    registerStaticAlloc(ts.Error(),
                                        false,
                                        "program-wide-error",
                                        Position.COMPILER_GENERATED);

        }

        this.addStmt(new StmtLocalToLocal(catchFormal,
                                          programWideError,
                                          origin,
                                          codeInfo.codeInstance));
    }

    protected void addStmt(PointsToStmt s) {
        this.stmts.add(s);
        CodeInstance ci = s.codeInstance;
        List<PointsToStmt> stmts = codeToStmts.get(ci);
        if (stmts == null) {
            stmts = new ArrayList<PointsToStmt>();
            codeToStmts.put(ci, stmts);
        }
        stmts.add(s);
    }

    /**
     * Record the existence of a procedure decl.
     */
    public CodeInfo recordProcedureDecl(ProcedureDecl pd,
            ConstructorContext constructorContext) {
        ProcedureInstance pi = pd.procedureInstance();

        ReferenceVariable thisNode = null;
        if (!pi.flags().isStatic()) {
            Type container = null;
            if (pi instanceof MethodInstance) {
                container = ((MethodInstance) pi).container();
            }
            else {
                container = ((ConstructorInstance) pi).container();
            }
            thisNode =
                    freshReferenceVariable(usableName(pi) + ".this",
                                           false,
                                           container,
                                           pd.position());
            ExtProcedureDecl ext = (ExtProcedureDecl) AccrueExt_c.ext(pd);
            ext.setThisNode(thisNode);
        }
        else if (Registrar.isStartProc(pi)) {
            this.addStartProc(pd);
        }

        List<ReferenceVariable> formals =
                new ArrayList<ReferenceVariable>(pd.formals().size());
        for (Formal f : pd.formals()) {
            if (f.type().type().isReference()) {
                ReferenceVariable ln =
                        freshReferenceVariable(pd.name() + "." + f.name(),
                                               false,
                                               f.type().type(),
                                               f.position());
                formals.add(ln);
                ((ExtFormal) AccrueExt_c.ext(f)).setReferenceVariable(ln,
                                                                      constructorContext);
                // add formals to the set
                this.localDecls.put(new LICI(f.localInstance(),
                                             pd.codeInstance(),
                                             constructorContext),
                                    ln);
            }
        }

        ReferenceVariable retValue = null;
        if (pi instanceof MethodInstance
                && ((MethodInstance) pi).returnType().isReference()) {
            retValue =
                    freshReferenceVariable(pd.name() + ".RET",
                                           false,
                                           ((MethodInstance) pi).returnType(),
                                           pd.position());
        }

        Map<Type, ReferenceVariable> exceptionRets =
                new LinkedHashMap<Type, ReferenceVariable>();
        for (Type exType : pi.throwTypes()) {
            exceptionRets.put(exType,
                              freshReferenceVariable(pd.name()
                                                             + "-throw-"
                                                             + exType.toClass()
                                                                     .name(),
                                                     false,
                                                     exType,
                                                     pd.position()));
        }
        // make sure that there are exceptionRets for common RuntimeExceptions
        TypeSystem ts = pi.typeSystem();
        if (!pi.throwTypes().contains(ts.RuntimeException())) {
            exceptionRets.put(ts.RuntimeException(),
                              freshReferenceVariable(pd.name()
                                                             + "-throw-RuntimeException",
                                                     false,
                                                     ts.RuntimeException(),
                                                     pd.position()));
        }
        if (!pi.throwTypes().contains(ts.Error())) {
            exceptionRets.put(ts.Error(),
                              freshReferenceVariable(pd.name() + "-throw-Error",
                                                     false,
                                                     ts.Error(),
                                                     pd.position()));
        }

        CodeInfo codeInfo =
                new CodeInfo(pd.codeInstance(),
                             thisNode,
                             formals,
                             retValue,
                             exceptionRets);

        if (this.codeDecls.containsKey(pi)) {
            throw new InternalCompilerError("same pi registered twice");
        }

        this.codeDecls.put(pi, codeInfo);
        return codeInfo;
    }

    private static class QueuedStaticAlloc {
        final ReferenceVariable ln;
        final Type type;
        final boolean isPreciseType;
        final String debugString;
        final Position pos;

        QueuedStaticAlloc(ReferenceVariable ln, Type type,
                boolean isPreciseType, String debugString, Position pos) {
            this.ln = ln;
            this.type = type;
            this.isPreciseType = isPreciseType;
            this.debugString = debugString;
            this.pos = pos;
        }

    }

    private List<QueuedStaticAlloc> queuedStaticAllocs =
            new LinkedList<StmtRegistrar.QueuedStaticAlloc>();

    private void queueStaticAlloc(ReferenceVariable ln, Type type,
            boolean isPreciseType, String debugString, Position pos) {
        queuedStaticAllocs.add(new QueuedStaticAlloc(ln,
                                                     type,
                                                     isPreciseType,
                                                     debugString,
                                                     pos));
    }

    private void addStartProc(ProcedureDecl pd) {
        this.startProcs.add(pd);
        if (!queuedStaticAllocs.isEmpty()) {
            MethodInstance main = null;
            for (ProcedureDecl spd : this.getStartProcs()) {
                if (spd.codeInstance() instanceof MethodInstance) {
                    main = (MethodInstance) spd.codeInstance();
                    break;
                }
            }

            if (main != null) {
                // we now have a main method!
                Iterator<QueuedStaticAlloc> iter =
                        queuedStaticAllocs.iterator();
                while (iter.hasNext()) {
                    QueuedStaticAlloc qsa = iter.next();
                    processStaticAlloc(qsa.ln,
                                       qsa.type,
                                       qsa.isPreciseType,
                                       qsa.debugString,
                                       qsa.pos,
                                       main);
                    iter.remove();
                }
            }
        }

    }

    /**
     * Record the existence of an initializer
     */
    public void recordInitializer(Initializer init) {
        recordInitializerOrFieldDecl(init);
    }

    /**
     * Record the existence of a field decl
     */
    public void recordFieldDecl(FieldDecl fd) {
        recordInitializerOrFieldDecl(fd);
    }

    /**
     * Internal method that factors out the common functionality for
     * recording the existence of an initializer or field decl
     */
    protected void recordInitializerOrFieldDecl(CodeNode cn) {
        InitializerInstance ii = (InitializerInstance) cn.codeInstance();
        if (ii == null) {
            // no initializer instance
            if (cn.codeBody() != null) {
                throw new InternalCompilerError("CodeNode has a non-null code body, but no instance initializer. Is that right?");
            }
            // No initializer instance, and no code body. Probably a field decl
            // with no initializer. Nothing to do here.
            return;
        }
        if (ii.flags().isStatic()) {
            Map<Type, ReferenceVariable> exceptionRets =
                    new LinkedHashMap<Type, ReferenceVariable>();

            TypeSystem ts = ii.typeSystem();

            exceptionRets.put(ii.typeSystem().RuntimeException(),
                              freshReferenceVariable("static-init-throw-RuntimeException",
                                                     false,
                                                     ts.RuntimeException(),
                                                     cn.position()));
            exceptionRets.put(ii.typeSystem().Error(),
                              freshReferenceVariable("static-init-throw-Error",
                                                     false,
                                                     ts.Error(),
                                                     cn.position()));
            CodeInfo codeInfo =
                    new CodeInfo(cn.codeInstance(),
                                 null,
                                 Collections.<ReferenceVariable> emptyList(),
                                 null,
                                 exceptionRets);
            this.staticInitializerDecls.put(cn, codeInfo);
            return;
        }
        ClassType container = ii.container().toClass();
        List<CodeNode> s = instanceInitializerDecls.get(container);
        if (s == null) {
            s = new ArrayList<CodeNode>();
            instanceInitializerDecls.put(container, s);
        }
        s.add(cn);
    }

    public CodeInfo getCodeInfo(ProcedureInstance pi) {
        return this.codeDecls.get(pi);
    }

    public CodeInfo getCodeInfo(Initializer staticInit) {
        if (!staticInit.initializerInstance().flags().isStatic()) {
            throw new InternalCompilerError("Instance initializer used!");
        }
        return this.staticInitializerDecls.get(staticInit);
    }

    public CodeInfo getCodeInfo(FieldDecl staticInit) {
        if (!staticInit.initializerInstance().flags().isStatic()) {
            throw new InternalCompilerError("Instance initializer used!");
        }
        return this.staticInitializerDecls.get(staticInit);
    }

    public CodeInfo getCodeInfo(CodeNode n) {
        if (n instanceof Initializer) {
            return getCodeInfo((Initializer) n);
        }
        if (n instanceof FieldDecl) {
            return getCodeInfo((FieldDecl) n);
        }
        if (n instanceof ProcedureDecl) {
            return getCodeInfo(((ProcedureDecl) n).procedureInstance());
        }
        throw new InternalCompilerError("Unknown decl " + n, n.position());
    }

    public Set<ProcedureDecl> getStartProcs() {
        return this.startProcs;
    }

    public Set<CodeNode> getStaticInitializers() {
        return this.staticInitializerDecls.keySet();
    }

    public List<CodeNode> getInstanceInitializers(ClassType container) {
        List<CodeNode> s = this.instanceInitializerDecls.get(container);
        if (s == null) return Collections.emptyList();
        return s;
    }

    private String usableName(ProcedureInstance pi) {
        if (pi instanceof ConstructorInstance) {
            ConstructorInstance ci = (ConstructorInstance) pi;
            return ci.container().toClass().name();
        }
        else if (pi instanceof MethodInstance) {
            MethodInstance mi = (MethodInstance) pi;
            return mi.name();
        }
        else {
            throw new InternalCompilerError("Unknown pi");
        }
    }

    private Expr setReferenceVariable(Expr e, ReferenceVariable localNode,
            ConstructorContext constructorContext) {
        ExtExpr ext = (ExtExpr) AccrueExt_c.ext(e);
        ext.setReferenceVariable(localNode, constructorContext);
        return e;
    }

    public ReferenceVariable getLocalNode(LocalInstance li,
            CodeInfo containingCode, ConstructorContext constructorContext) {
        LICI key =
                new LICI(li, containingCode.codeInstance, constructorContext);
        if (!localDecls.containsKey(key)) {
            throw new InternalCompilerError("No localnode!");
        }
        return localDecls.get(key);
    }

    public ReferenceVariable nodeForStaticField(FieldInstance fi) {
        if (!fi.flags().isStatic()) {
            throw new InternalCompilerError("Non static field");
        }
        ReferenceVariable ln = staticFields.get(fi);
        if (ln == null) {
            ln =
                    freshReferenceVariable("static-"
                                                   + fi.container()
                                                       .toClass()
                                                       .name() + "."
                                                   + fi.name(),
                                           true,
                                           fi.type(),
                                           fi.position()); // is a static local node
            staticFields.put(fi, ln);
        }
        return ln;
    }

    protected ReferenceVariable freshReferenceVariable(String debugString,
            boolean isSingleton, Type expectedType, Position pos) {
        return new ReferenceVariable(debugString,
                                     isSingleton,
                                     expectedType,
                                     pos);
    }

    protected AllocSiteNode freshAllocNode(Type type,
            ClassType containingClass, boolean isPreciseType,
            String debugString, Position pos) {
        return new AllocSiteNode(type,
                                 containingClass,
                                 isPreciseType,
                                 debugString,
                                 pos);
    }

    protected CallSiteNode freshCallSiteNode(ProcedureInstance callee,
            String debugString, Position pos) {
        return new CallSiteNode(callee, debugString, pos);
    }

    /**
     * A pair of a LocalInstance and CodeInstance, with a construct context
     * as needed.
     *
     */
    private static class LICI {
        final LocalInstance li;
        final CodeInstance codeInstance;
        final ConstructorContext constructorContext;

        LICI(LocalInstance li, CodeInstance ci,
                ConstructorContext constructorContext) {
            this.li = li;
            this.codeInstance = ci;
            this.constructorContext = constructorContext;
        }

        @Override
        public boolean equals(Object o) {
            if (o == this) return true;
            if (o instanceof LICI) {
                LICI that = (LICI) o;
                return (this.li == that.li /*|| this.li.equals(that.li)*/)
                        && (this.codeInstance == that.codeInstance)
                        && (this.constructorContext == that.constructorContext || this.constructorContext.equals(that.constructorContext));
            }
            return false;
        }

        @Override
        public int hashCode() {
            return li.hashCode()
                    ^ codeInstance.hashCode()
                    ^ (constructorContext == null ? 0
                            : constructorContext.hashCode());
        }
    }

    public static class CodeInfo {
        public CodeInfo(CodeInstance codeInstance, ReferenceVariable thisNode,
                List<ReferenceVariable> formals, ReferenceVariable retValue,
                Map<Type, ReferenceVariable> exceptionRets) {
            this.codeInstance = codeInstance;
            this.thisNode = thisNode;
            this.formals = formals;
            this.retValue = retValue;
            this.exceptionRets = exceptionRets;
        }

        public final CodeInstance codeInstance;
        public final ReferenceVariable thisNode;
        public final List<ReferenceVariable> formals;
        public final ReferenceVariable retValue;
        public final Map<Type, ReferenceVariable> exceptionRets;

        @Override
        public String toString() {
            return codeInstance.toString();
        }
    }

    public static class ExceptionHandlerReferenceVariable {
        public ExceptionHandlerReferenceVariable(Type exType,
                ReferenceVariable ln) {
            this.exType = exType;
            this.ln = ln;
        }

        final public Type exType;
        final public ReferenceVariable ln;

        @Override
        public String toString() {
            return exType + " -> " + ln;
        }
    }

    public void recordMissingCode(ProcedureInstance pi, Position pos) {
        String container = null;
        String procName = null;
        if (pi instanceof ConstructorInstance) {
            ConstructorInstance ci = (ConstructorInstance) pi;
            container = ci.container().toClass().fullName();
            procName = ci.container().toClass().name();
        }
        if (pi instanceof MethodInstance) {
            MethodInstance mi = (MethodInstance) pi;
            container = mi.container().toClass().fullName();
            procName = mi.name();
        }
        if (this.missingCode.containsKey(pi)) {
            return;
        }
        /*        this.missingCode.putIfAbsent(pi, new ErrorInfo(ErrorInfo.WARNING, 
                                                               "Missing code for " + container+"."+pi.signature() + " " + "in pointer analysis", 
                                                               pos));
                /*
                this.missingCode.replace(pi, new ErrorInfo(ErrorInfo.WARNING, 
                        "Missing code for " + container+"."+pi.signature() + " " + "in pointer analysis", 
                        pos));
                 */
    }

    public boolean processMissingCode(CodeInstance caller,
            CContext callerContext, CallSiteNode callSiteNode,
            MethodInstance mi, List<ReferenceVariableReplica> args,
            HContext receiver, ReferenceVariableReplica result,
            List<ExceptionHandlerPointsToGraphNode> handlers,
            Map<Type, ReferenceVariableReplica> procThrows, PointsToGraph g,
            Position origin, HeapAbstractionFactory af, StmtAndContext sac) {

        LibraryPointsToSignature sig = missingCodeSignatures.get(mi);
        if (sig == null) {
            SignatureRepository<LibraryPointsToSignature> r =
                    extInfo.getAnalysisSignatures()
                           .signatureRepository(PointerAnalysisPass.ANALYSIS_NAME);
            sig = r == null ? null : r.lookup(mi);
            if (sig != null) {
                missingCodeSignatures.putIfAbsent(mi, sig);
                //missingCodeSignatures.replace(mi, sig);
            }
        }
        if (sig != null) {
            if (Report.should_report(AnalysisTopics.POINTSTO, 3)) {
                Report.report(3,
                              "Using library signature for points to processing of "
                                      + mi);
            }
            try {
                return sig.process(caller,
                                   callerContext,
                                   callSiteNode,
                                   mi,
                                   args,
                                   receiver,
                                   result,
                                   handlers,
                                   procThrows,
                                   this,
                                   g,
                                   origin,
                                   af,
                                   sac);
            }
            catch (SemanticException e) {
                throw new InternalCompilerError(e);
            }
        }
        if (Report.should_report(AnalysisTopics.POINTSTO, 3)) {
            Report.report(3,
                          "No library signature for points to processing of "
                                  + mi);
        }
        recordMissingCode(mi, origin);

        if (mi.returnType().isReference()) {
            if (((AccrueOptions) this.extInfo.getOptions()).helper().emptysetsigs) {
                // XXX Wrong?
                LibraryPointsToSignature singleton =
                        new PointsToLibrarySigs.Singleton(mi.container() + "::"
                                + mi.signature(), mi.returnType(), false);
                LibraryPointsToSignature existing =
                        missingCodeSignatures.putIfAbsent(mi, singleton);
                if (existing != null) {
                    singleton = existing;
                }
                if (!(((AccrueOptions) this.extInfo.getOptions()).helper().noWemptysetsigs)) {
                    System.err.println("*** Generating unsound points to set for "
                            + mi.signature());
                }
                try {
                    return singleton.process(caller,
                                             callerContext,
                                             callSiteNode,
                                             mi,
                                             args,
                                             receiver,
                                             result,
                                             handlers,
                                             procThrows,
                                             this,
                                             g,
                                             origin,
                                             af,
                                             sac);
                }
                catch (SemanticException e) {
                    throw new InternalCompilerError(e);
                }
            }
        }

        return false;
    }

    public boolean processMissingCode(CodeInstance caller,
            CContext callerContext, CallSiteNode callSiteNode,
            ConstructorInstance ci,
            ReferenceVariableReplica newAllocatedObject,
            List<ReferenceVariableReplica> args,
            List<ExceptionHandlerPointsToGraphNode> handlers,
            Map<Type, ReferenceVariableReplica> procThrows, PointsToGraph g,
            Position origin, HeapAbstractionFactory af, StmtAndContext sac) {
        LibraryPointsToSignature sig = missingCodeSignatures.get(ci);
        if (sig == null) {
            AnalysisSignatures sigs = extInfo.getAnalysisSignatures();
            if (sigs != null) {
                SignatureRepository<LibraryPointsToSignature> r =
                        sigs.signatureRepository(PointerAnalysisPass.ANALYSIS_NAME);
                sig = r == null ? null : r.lookup(ci);
            }
            if (sig != null) {
                missingCodeSignatures.putIfAbsent(ci, sig);
                //missingCodeSignatures.replace(ci, sig);
            }
        }
        if (sig != null) {
            try {
                boolean changed = false;
                for (HContext o : g.pointsTo(sac, newAllocatedObject)) {
                    changed =
                            sig.process(caller,
                                        callerContext,
                                        callSiteNode,
                                        ci,
                                        args,
                                        o,
                                        null,
                                        handlers,
                                        procThrows,
                                        this,
                                        g,
                                        origin,
                                        af,
                                        sac) || changed;
                }
                return changed;
            }
            catch (SemanticException e) {
                throw new InternalCompilerError(e);
            }
        }
        recordMissingCode(ci, origin);

        if (((AccrueOptions) this.extInfo.getOptions()).helper().emptysetsigs) {
            // XXX Wrong?
            LibraryPointsToSignature singleton =
                    new PointsToLibrarySigs.Singleton(ci.container() + "::"
                            + ci.signature(), ci.container().toType(), false);
            LibraryPointsToSignature existing =
                    missingCodeSignatures.putIfAbsent(ci, singleton);
            if (existing != null) {
                singleton = existing;
            }
            if (!(((AccrueOptions) this.extInfo.getOptions()).helper().noWemptysetsigs)) {
                System.err.println("*** Generating unsound points to set for "
                        + ci.signature());
            }
            try {
                boolean changed = false;
                for (HContext o : g.pointsTo(sac, newAllocatedObject)) {
                    changed =
                            singleton.process(caller,
                                              callerContext,
                                              callSiteNode,
                                              ci,
                                              args,
                                              o,
                                              null,
                                              handlers,
                                              procThrows,
                                              this,
                                              g,
                                              origin,
                                              af,
                                              sac);
                }
                return changed;
            }
            catch (SemanticException e) {
                throw new InternalCompilerError(e);
            }
        }

        return false;
    }

    /**
     * Utility method for adding exceptions
     */
    public void addGeneratedExceptionAssignments(Set<ClassType> exceptionTypes,
            Term cause, RegisterPointerStmtsVisitor v) {
        Position origin = cause.position();

        for (ClassType exType : exceptionTypes) {
            ReferenceVariable ln;
            if (USE_SINGLE_ALLOC_NODE_FOR_GENERATED_EXCEPTIONS) {
                Map<ClassType, ReferenceVariable> gen =
                        generatedExceptionNodes.get(exType.typeSystem()
                                                          .extensionInfo());
                if (gen == null) {
                    gen = new LinkedHashMap<ClassType, ReferenceVariable>();
                    generatedExceptionNodes.put(exType.typeSystem()
                                                      .extensionInfo(), gen);
                }
                ln = gen.get(exType);
                if (ln == null) {
                    ln =
                            registerStaticAlloc(exType, true, "generated-"
                                    + exType.name(), origin);
                    gen.put(exType, ln);
                }
            }
            else {
                // The exception may be generated, so it is an allocation site
                ln =
                        registerAlloc(exType,
                                      origin,
                                      "generated-" + exType.name(),
                                      v.currentCode());
            }
            addExceptionAssignments(exType, ln, origin, v);
        }
    }

    /**
     * Utility method for adding exceptions
     */
    public void addExceptionAssignments(Type exceptionType,
            ReferenceVariable exceptionLocalNode, Position origin,
            RegisterPointerStmtsVisitor v) {
        TypeSystem ts = v.typeSystem();

        // walk up the handlers, assigning to appropriate variables
        boolean definitelyCaught = false;
        boolean maybeCaught = false;
        Set<Type> alreadyCaught = new LinkedHashSet<Type>();

        for (ExceptionHandlerReferenceVariable ehln : v.exceptionHandlers()) {
            if (ts.isSubtype(exceptionType, ehln.exType)) {
                // there is a catch block that definitely catches this exception
                addFilteredAssignment(ehln.ln,
                                      exceptionLocalNode,
                                      ehln.exType,
                                      alreadyCaught,
                                      origin,
                                      v.currentCode());
                definitelyCaught = true;
                maybeCaught = true;
                break;
            }
            else if (ts.isSubtype(ehln.exType, exceptionType)) {
                // may be caught
                addFilteredAssignment(ehln.ln,
                                      exceptionLocalNode,
                                      ehln.exType,
                                      alreadyCaught,
                                      origin,
                                      v.currentCode());
                maybeCaught = true;
                alreadyCaught.add(ehln.exType);
            }
        }
        if (!definitelyCaught) {
            // the exception may not have been caught, so it may go beyond the
            // scope of the method.
            for (Type methodThrowType : v.currentCode().exceptionRets.keySet()) {
                if (ts.isSubtype(methodThrowType, exceptionType)
                        || ts.isSubtype(exceptionType, methodThrowType)) {
                    // may fall under this throwtype.
                    addFilteredAssignment(v.currentCode().exceptionRets.get(methodThrowType),
                                          exceptionLocalNode,
                                          methodThrowType,
                                          alreadyCaught,
                                          origin,
                                          v.currentCode());
                    maybeCaught = true;
                }
                if (ts.isSubtype(exceptionType, methodThrowType)) {
                    definitelyCaught = true;
                }
            }
        }
        if (!definitelyCaught) {
            throw new InternalCompilerError("Seems like a (non-Error) exception may not be caught or declared");
        }
    }

    /**
     * Return the code instances that should be analyzed in the initial context.
     * This is typically the start prceodure(s), and static initializers.
     */
    public Collection<CodeInstance> getInitialCodeInstances() {
        ArrayList<CodeInstance> cis = new ArrayList<CodeInstance>();
        for (ProcedureDecl pd : this.getStartProcs()) {
            cis.add(pd.procedureInstance());
        }
        for (CodeNode init : this.getStaticInitializers()) {
            cis.add(init.codeInstance());
        }
        return cis;
    }
}
