package accrue;

import java.io.File;
import java.lang.reflect.Constructor;
import java.lang.reflect.InvocationTargetException;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
import java.util.StringTokenizer;

import polyglot.main.Main.TerminationException;
import polyglot.main.OptFlag;
import polyglot.main.OptFlag.Arg;
import polyglot.main.OptFlag.IntFlag;
import polyglot.main.OptFlag.PathFlag;
import polyglot.main.OptFlag.Switch;
import polyglot.main.UsageError;
import polyglot.util.CollectionUtil;
import accrue.analysis.interprocvarcontext.VarContextDataFlow;
import accrue.analysis.pointer.PointsToEngine;
import accrue.analysis.pointer.analyses.CallSiteContextSensitiveAnalysis;
import accrue.analysis.pointer.analyses.CrossProductAnalysis;
import accrue.analysis.pointer.analyses.DistinguishClass;
import accrue.analysis.pointer.analyses.FullObjSensitiveAnalysis;
import accrue.analysis.pointer.analyses.HeapAbstractionFactory;
import accrue.analysis.pointer.analyses.StaticCallSiteContextSensitiveAnalysis;
import accrue.analysis.pointer.analyses.TypeSensitive_nTmH_Analysis;

/**
 * Polyglot options for an object sensitive analysis
 */
public class AccrueOptionsHelper {
    public String startProcClass = null;
    public String pointsToEngineClass = null;
    public Integer pointsToTimeout = null;
    private String heapAbstractionFactoryString = null;
    public boolean emptysetsigs = false;
    public boolean noWemptysetsigs = false;
    public boolean flattenExpressions = false;
    public Collection<File> signatureSourcePath = null;

    public OptFlag<String> startOptFlag =
            new OptFlag<String>(new String[] { "-start", "--start" },
                                "<classname>",
                                "Start analysis from the main method of class") {
                @Override
                public Arg<String> handle(String[] args, int index)
                        throws UsageError {
                    return createArg(index + 1, args[index]);
                }

            };
    public OptFlag<String> pointsToEngineClassOptFlag =
            new OptFlag<String>(new String[] { "-pointsToEngineClass",
                                        "--pointsToEngineClass" },
                                "<classname>",
                                "Use an instance of <classname> for the pointer analysis engine.",
                                "accrue.analysis.pointer.PointsToEngineMultiThread") {
                @Override
                public Arg<String> handle(String[] args, int index)
                        throws UsageError {
                    return createArg(index + 1, args[index]);
                }

                @Override
                public Arg<String> defaultArg() {
                    return createDefault(this.defaultValue);
                }

            };

    IntFlag pointsToTimeoutOptFlag =
            new IntFlag(new String[] { "-pointstotimeout", "--pointstotimeout" },
                        "<timeout_secs>",
                        "Limit the time of execution of the pointer analysis engine.");

    public Switch noWarnMissingEdgesOptFlag =
            new Switch(new String[] { "-nowarnmissingedges",
                               "--nowarnmissingedges" },
                       "Suppress warnings about missing edges");
    public Switch emptySetSigsOptFlag =
            new Switch(new String[] { "-emptysetsigs", "--emptysetsigs" },
                       "Ensure all points to sets are non-empty (unsound)");

    public Switch flattenExpressionOptFlag =
            new Switch(new String[] { "-flattenExpressions",
                               "--flattenExpressions" },
                       "Flatten expressions before performing processing");

    public Switch warnEmptySetSigsOptFlag =
            new Switch(new String[] { "-noWemptysetsigs", "--noWemptysetsigs" },
                       "Don't warn when using -emptysetsigs");

    public PathFlag<File> sigSrcPathOptFlag =
            new PathFlag<File>(new String[] { "-sigsourcepath", "--sigsrcpath" },
                               "<path>",
                               "Look for signature files in path. Output will not be produced for signature files") {

                @Override
                public File handlePathEntry(String entry) {
                    return new File(entry);
                }

            };

    OptFlag<String> heapAbstractionOptFlag =
            new OptFlag<String>(new String[] { "-heapabstraction",
                                        "--heapabstraction" },
                                "<classname>",
                                "Use an instance of <classname> for the pointer heap abstraction factory. For convenience, can also specify one of \"full\" or \"2T1H\"") {
                @Override
                public Arg<String> handle(String[] args, int index)
                        throws UsageError {
                    return createArg(index + 1, args[index]);
                }

            };

    public void populateFlags(Set<OptFlag<?>> flags) {
        flags.add(startOptFlag);
        flags.add(pointsToEngineClassOptFlag);
        flags.add(pointsToTimeoutOptFlag);
        flags.add(noWarnMissingEdgesOptFlag);
        flags.add(emptySetSigsOptFlag);
        flags.add(flattenExpressionOptFlag);
        flags.add(warnEmptySetSigsOptFlag);
        flags.add(sigSrcPathOptFlag);
        flags.add(heapAbstractionOptFlag);
    }

    public boolean handleArg(Arg<?> arg) throws UsageError {
        if (arg.flag().ids().contains("-start")) {
            this.startProcClass = (String) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-nowarnmissingedges")) {
            VarContextDataFlow.WARN_ON_MISSING_EDGES = (Boolean) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-pointsToEngineClass")) {
            this.pointsToEngineClass = (String) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-pointstotimeout")) {
            this.pointsToTimeout = (Integer) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-emptysetsigs")) {
            this.emptysetsigs = (Boolean) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-flattenExpressions")) {
            this.flattenExpressions = (Boolean) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-noWemptysetsigs")) {
            this.noWemptysetsigs = (Boolean) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-sigsourcepath")) {
            this.signatureSourcePath = (List<File>) arg.value();
            return true;
        }
        else if (arg.flag().ids().contains("-heapabstraction")) {
            this.heapAbstractionFactoryString = (String) arg.value();
            return true;
        }
        return false;
    }

    /**
     * Create the PointsToEngine for performing pointer analysis. The field 
     * this.pointToEngineClass is the fully qualified name of a
     * subclass of PointsToEngine. If the field this.heapAbstractionFactoryString
     * is non-null, then it is passed as an argument to the constructor of the
     * pointToEngineClass. (And thus, the pointToEngineClass must have a constructor that
     * takes a single String argument.)
     * 
     * If this.heapAbstractionFactoryString is null, then the constructor is passed
     * a HeapAbstractionFactory. (And thus, the pointsToEngineClass must
     * have a constructor that takes a single HeapAbstractionFactory argument.)
     * @return a PointsToEngine for performing pointer analysis.
     */
    public PointsToEngine createPointsToEngine() {

        HeapAbstractionFactory haf = createHeapAbstractionFactory();

        PointsToEngine eng;
        try {
            Constructor<?> c =
                    Class.forName(this.pointsToEngineClass)
                         .getConstructor(HeapAbstractionFactory.class);
            eng = (PointsToEngine) c.newInstance(haf);
        }
        catch (InstantiationException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass);
        }
        catch (IllegalAccessException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass
                    + ": no public default constructor");
        }
        catch (ClassNotFoundException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass + ": class not found");
        }
        catch (SecurityException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass + ": " + e.getMessage());
        }
        catch (NoSuchMethodException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass
                    + ": 1no appropriate constructor " + e.getMessage());
        }
        catch (IllegalArgumentException e) {
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass
                    + ": 2no appropriate constructor " + e.getMessage());
        }
        catch (InvocationTargetException e) {
            if (e.getCause() instanceof RuntimeException) {
                throw (RuntimeException) e.getCause();
            }
            throw new TerminationException("Cannot instantiate pointsToEngine "
                    + this.pointsToEngineClass + ": "
                    + e.getCause().getMessage());
        }
        if (this.pointsToTimeout != null) {
            eng.setTimeout(this.pointsToTimeout * 1000L);
        }
        return eng;

    }

    public HeapAbstractionFactory createHeapAbstractionFactory() {
        return createHeapAbstractionFactory(this.heapAbstractionFactoryString);
    }

    /**
     * create a HeapAbstractionFactory from a string. The format for the string is
     * <pre>
     *   facts ::= fact | "[" fact "|" fact "|" ... "]"
     *   fact  ::= classname ["(" arg "," arg "," ... ")"]
     *   arg   ::= int | string
     * </pre>
     * where classname is a fully qualified classname of a heap abstraction, and the 
     * optional "(arg1, arg2, ...)" are zero or more integer or string literal
     * arguments, which will be passed to the constructor for the heap abstraction.
     * 
     * For convenience, classname may be abbreviated for several of the pointer analyses 
     * that come with Accrue, described as follows.
     * 
     * Abbreviation :   Fully qualified class name/factory
     * full  :  accrue.analysis.pointer.analyses.FullObjSensitiveAnalysis
     * type  :  accrue.analysis.pointer.analyses.TypeSensitive_nTmH_Analysis
     * 2t1h  :  accrue.analysis.pointer.analyses.TypeSensitive_nTmH_Analysis(2,1)
     * scs   :  accrue.analysis.pointer.analyses.StaticCallSiteContextSensitiveAnalaysis
     * cs    :  accrue.analysis.pointer.analyses.CallSiteContextSensitiveAnalaysis
     * distinguish  :   accrue.analysis.pointer.analyses.DistinguishClass
     * 
     * Some example strings that are acceptable include:
     * "full"
     * "full(5)"
     * "type(2,1)"
     * "2t1h"
     * "accrue.analysis.pointer.analyses.FullObjSensitiveAnalysis(2)"
     * 
     * The following strings will create Cross product analyses
     * "[2t1h | scs(2)]"
     * "[2t1h | scs(2) | distinguish(mypackage.Foo)]"
     * 
     * @param hafString
     * @return
     */
    public static HeapAbstractionFactory createHeapAbstractionFactory(
            String hafString) {
        if (hafString == null) {
            return new CrossProductAnalysis(new TypeSensitive_nTmH_Analysis(),
                                            new StaticCallSiteContextSensitiveAnalysis());
        }
        StringTokenizer st = new StringTokenizer(hafString, "[]|");
        LinkedList<HeapAbstractionFactory> list =
                new LinkedList<HeapAbstractionFactory>();
        while (st.hasMoreTokens()) {
            list.addFirst(parseHeapAbstractionFactory(st.nextToken()));
        }
        HeapAbstractionFactory hf = null;
        for (HeapAbstractionFactory haf : list) {
            if (hf == null) {
                hf = haf;
            }
            else {
                hf = new CrossProductAnalysis(haf, hf);
            }
        }
        System.err.println("// HeapAbstractionFactory is " + hf);
        return hf;
    }

    /**
     * Parse heap abstraction factories.
     */
    private static ParseResult parseFactories(String hafString, int index) {
        if ("[".equals(nextToken(hafString, index))) {
            // parse a list
            index++;
            LinkedList<HeapAbstractionFactory> list =
                    new LinkedList<HeapAbstractionFactory>();
            while (true) {
                ParseResult r = parseFactory(hafString, index);
                index = r.endIndex;
                list.addFirst(r.haf);
                if ("]".equals(nextToken(hafString, index))) {
                    index++;
                    break;
                }
                else if (",".equals(nextToken(hafString, index))) {
                    // consume comma
                    index++;
                }
                else {
                    // uh oh error.
                    throw new TerminationException("Unparseable heap abstraction factory string: "
                            + hafString);

                }
            }
            if (list.isEmpty()) {
                return new ParseResult(null, index);
            }
            if (list.size() == 1) {
                return new ParseResult(list.get(0), index);
            }
            HeapAbstractionFactory hf = null;
            for (HeapAbstractionFactory haf : list) {
                if (hf == null) {
                    hf = haf;
                }
                else {
                    hf = new CrossProductAnalysis(haf, hf);
                }
            }

            return new ParseResult(hf, index);
        }
        else {
            return parseFactory(hafString, index);
        }
    }

    private static ParseResult parseFactory(String hafString, int index) {
        String hafClass = nextToken(hafString, index);
        index += hafClass.length();

        // are there arguments?
        List<Object> args = new ArrayList<Object>();
        if ("(".equals(nextToken(hafClass, index))) {
            // swallow the paren
            index++;
            while (true) {
                String arg = nextToken(hafClass, index);
                try {
                    args.add(Integer.parseInt(arg));
                }
                catch (NumberFormatException e) {
                    // nope, not a number
                    args.add(arg);
                }
                index += arg.length();
                if (")".equals(nextToken(hafClass, index))) {
                    // close paren
                    index++;
                    break;
                }
                else if (",".equals(nextToken(hafClass, index))) {
                    // comma
                    index++;
                    continue;
                }
                else {
                    // uh oh error.
                    throw new TerminationException("Unparseable heap abstraction factory string: "
                            + hafString);
                }
            }
        }

        if (hafClass.equalsIgnoreCase("full")) {
            hafClass = FullObjSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("type")) {
            hafClass = TypeSensitive_nTmH_Analysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("scs")) {
            hafClass =
                    StaticCallSiteContextSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("cs")) {
            hafClass =
                    CallSiteContextSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("distinguish")) {
            hafClass = DistinguishClass.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("2t1h")) {
            hafClass = TypeSensitive_nTmH_Analysis.class.getCanonicalName();
            args = CollectionUtil.<Object> list(2, 1);
        }
        try {
            Class<?> clazz;
            try {
                clazz = Class.forName(hafClass);
            }
            catch (ClassNotFoundException e) {
                // try again but prepend the analysis package
                clazz =
                        Class.forName("accrue.analysis.pointer.analyses."
                                + hafClass);
            }
            Class<?>[] argTypes = new Class[args.size()];
            for (int i = 0; i < argTypes.length; i++) {
                if (args.get(i) instanceof Integer) {
                    argTypes[i] = int.class;
                }
                else {
                    argTypes[i] = String.class;
                }
            }
            Constructor<?> cons = clazz.getConstructor(argTypes);
            HeapAbstractionFactory haf =
                    (HeapAbstractionFactory) cons.newInstance(args.toArray());
            return new ParseResult(haf, index);
        }
        catch (InstantiationException e) {
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafClass);
        }
        catch (IllegalAccessException e) {
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafClass + ": no public default constructor");
        }
        catch (ClassNotFoundException e) {
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafClass + ": class not found");
        }
        catch (ClassCastException e) {
            throw new TerminationException("Cannot instantiate " + hafClass
                    + ": it is not an instance of HeapAbstractionFactory");
        }
        catch (RuntimeException e) {
            throw new TerminationException("Cannot instantiate " + hafClass
                    + ": received exception " + e.getMessage());
        }
        catch (NoSuchMethodException e) {
            throw new TerminationException("Cannot instantiate " + hafClass
                    + ": no appropriate constructor");
        }
        catch (InvocationTargetException e) {
            if (e.getCause() instanceof RuntimeException) {
                throw (RuntimeException) e.getCause();
            }
            throw new TerminationException("Cannot instantiate " + hafClass
                    + ": " + e.getCause().getMessage());
        }
    }

    private static class ParseResult {
        final HeapAbstractionFactory haf;
        final int endIndex;

        public ParseResult(HeapAbstractionFactory haf, int endIndex) {
            this.haf = haf;
            this.endIndex = endIndex;
        }
    }

    private static List<Character> specialTokens =
            Arrays.<Character> asList('[', ']', '(', ')', '|', ',');

    private static String nextToken(String s, int index) {
        // skip initial whitespace
        while (index < s.length() && Character.isWhitespace(s.charAt(index))) {
            index++;
        }
        if (index >= s.length()) {
            // no next token.
            return null;
        }
        if (specialTokens.contains(s.charAt(index))) {
            return String.valueOf(s.charAt(index));
        }
        if (s.charAt(index) == '"') {
            // it's an open quote. Parse a string lit
            return parseStringLit(s, index);
        }
        // Otherwise, parse until we hit whitespace or a special character.
        int end = index + 1;
        while (end < s.length() && !Character.isWhitespace(s.charAt(end))
                && !specialTokens.contains(s.charAt(end))) {
            end++;
        }
        return s.substring(index, end);
    }

    private static String parseStringLit(String s, int index) {
        if (s.charAt(index) != '"') {
            return null;
        }
        boolean isEscape = false;
        int end = index + 1;
        while (end < s.length()) {
            char c = s.charAt(end++);
            if (c == '"' && !isEscape) {
                // end of the string literal
                return s.substring(index, end);
            }
            isEscape = false;
            if (c == '\\') {
                // we have a backslash. could be an escaped quotation
                // Set isEscape to true in case the next char is a quotation,
                // in which case we will not regard it as the end of the string literal
                isEscape = true;
            }
        }
        // The string literal wasn't terminated.
        return null;
    }

    private static HeapAbstractionFactory parseHeapAbstractionFactory(
            String hafString) {
        String hafClass = null;
        List<Object> args = new ArrayList<Object>();
        StringTokenizer st = new StringTokenizer(hafString, "(), ");
        while (st.hasMoreTokens()) {
            String token = st.nextToken();
            if (hafClass == null) {
                hafClass = token;
                continue;
            }
            Object a;
            try {
                a = Integer.parseInt(token);
            }
            catch (NumberFormatException e) {
                // nope, not a number
                a = token;
            }
            args.add(a);
        }
        if (hafClass.equalsIgnoreCase("full")) {
            hafClass = FullObjSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("type")) {
            hafClass = TypeSensitive_nTmH_Analysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("scs")) {
            hafClass =
                    StaticCallSiteContextSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("cs")) {
            hafClass =
                    CallSiteContextSensitiveAnalysis.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("distinguish")) {
            hafClass = DistinguishClass.class.getCanonicalName();
        }
        if (hafClass.equalsIgnoreCase("2t1h")) {
            hafClass = TypeSensitive_nTmH_Analysis.class.getCanonicalName();
            args = CollectionUtil.<Object> list(2, 1);
        }
        try {
            Class<?> clazz = Class.forName(hafClass);
            Class<?>[] argTypes = new Class[args.size()];
            for (int i = 0; i < argTypes.length; i++) {
                if (args.get(i) instanceof Integer) {
                    argTypes[i] = int.class;
                }
                else {
                    argTypes[i] = String.class;
                }
            }
            Constructor<?> cons = clazz.getConstructor(argTypes);
            return (HeapAbstractionFactory) cons.newInstance(args.toArray());
        }
        catch (InstantiationException e) {
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafString);
        }
        catch (IllegalAccessException e) {
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafString + ": no public default constructor");
        }
        catch (ClassNotFoundException e) {
            if (!hafClass.startsWith("accrue.analysis.pointer.analyses.")) {
                // try again but prepend the analysis package from Accrue
                return parseHeapAbstractionFactory("accrue.analysis.pointer.analyses."
                        + hafString);
            }
            throw new TerminationException("Cannot instantiate HeapAbstractionFactory "
                    + hafString + ": class not found");
        }
        catch (ClassCastException e) {
            throw new TerminationException("Cannot instantiate " + hafString
                    + ": it is not an instance of HeapAbstractionFactory");
        }
        catch (RuntimeException e) {
            throw new TerminationException("Cannot instantiate " + hafString
                    + ": received exception " + e.getMessage());
        }
        catch (NoSuchMethodException e) {
            throw new TerminationException("Cannot instantiate " + hafString
                    + ": no appropriate constructor");
        }
        catch (InvocationTargetException e) {
            if (e.getCause() instanceof RuntimeException) {
                throw (RuntimeException) e.getCause();
            }
            throw new TerminationException("Cannot instantiate " + hafString
                    + ": " + e.getCause().getMessage());
        }
    }
}
