/* Java and Android Analysis Framework
 * Copyright (C) 2017 Jingbo Lu and Yulei Sui
 *
 * This library is free software; you can redistribute it and/or
 * modify it under the terms of the GNU Lesser General Public
 * License as published by the Free Software Foundation; either
 * version 2.1 of the License, or (at your option) any later version.
 *
 * This library is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
 * Lesser General Public License for more details.
 *
 * You should have received a copy of the GNU Lesser General Public
 * License along with this library; if not, write to the
 * Free Software Foundation, Inc., 59 Temple Place - Suite 330,
 * Boston, MA 02111-1307, USA.
 */

package util;

import java.io.BufferedReader;
import java.io.File;
import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.io.OutputStream;
import java.io.PrintStream;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.Collection;
import java.util.HashMap;
import java.util.Iterator;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Set;

import org.apache.commons.io.FileUtils;
import org.junit.Test;
import org.junit.runner.RunWith;
import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameters;

import driver.FakeMainFactory;
import driver.Main;
import driver.SootUtils;
import pag.node.var.ContextVar_Node;
import pag.node.var.Var_Node;
import pta.ContextSensPTA;
import pta.PTA;
import soot.Body;
import soot.Context;
import soot.G;
import soot.Local;
import soot.MethodOrMethodContext;
import soot.PointsToSet;
import soot.SootMethod;
import soot.Unit;
import soot.Value;
import soot.jimple.InvokeExpr;
import soot.jimple.NullConstant;
import soot.jimple.StaticInvokeExpr;
import soot.jimple.Stmt;
import soot.util.queue.QueueReader;

/**
 * for every testcase in pta run a single test
 * 
 * @author Ammonia
 */
@RunWith(Parameterized.class)
public class PTAValidator {
	static final ArrayList<String> additionalCMD = new ArrayList<String>();;
	static final String srcPath = "../tests/src/pta";
	static final List<String> mainOrPackList = new ArrayList<String>();

	@Parameters
	public static Collection<String> prepareData() {
		final List<String> mainList = new ArrayList<String>();
		for (String mainOrPack : mainOrPackList) {
			if (!isExlude(mainOrPack)) {
				if (isPack(mainOrPack))
					loadFromPath(packToPath(mainOrPack), mainList);
				else
					mainList.add(mainOrPack);
			}
		}
		if (mainList.isEmpty())
			loadFromPath(srcPath, mainList);
		
		for (String mainOrPack : mainOrPackList) {
			if (isExlude(mainOrPack)) {
				mainOrPack = mainOrPack.substring(1);
				if (isPack(mainOrPack))
					exludeFromPath(packToPath(mainOrPack), mainList);
				else
					mainList.remove(mainOrPack);
			}
		}
		for (String mainclass : mainList)
			System.out.println(mainclass);
		int size = mainList.size();
		final String mid = " testcase founded.", mids = " testcases founded.",
				tail = " Now start testing...\nLoading library...";
		String info;
		switch (size) {
		case 0:
			info = mid;
			break;
		case 1:
			info = mid + tail;
			break;
		default:
			info = mids + tail;
		}
		System.out.println(size + info);
		return mainList;
	}

	private static String packToPath(String mainOrPack) {
		return "../tests/src/" + mainOrPack.replace('.', '/');
	}

	private static boolean isExlude(String mainOrPack) {
		return mainOrPack.charAt(0)=='-';
	}
	private static boolean isPack(String mainOrPack) {
		return Character.isLowerCase(mainOrPack.charAt(mainOrPack.lastIndexOf('.') + 1));
	}

	private static void loadFromPath(String srcPath, List<String> mainList) {
		System.out.println(srcPath);
		for (File clazz : FileUtils.listFiles(new File(srcPath), new String[] { "java" }, true)) {
			String mainclass = SootUtils.fromFileToClass(clazz.toString().substring("../tests/src/".length()));
			if (!mainclass.startsWith("pta.utils"))
				mainList.add(mainclass);
		}
	}
	private static void exludeFromPath(String srcPath, List<String> mainList) {
		System.out.println(srcPath);
		for (File clazz : FileUtils.listFiles(new File(srcPath), new String[] { "java" }, true)) {
			String mainclass = SootUtils.fromFileToClass(clazz.toString().substring("../tests/src/".length()));
			if (!mainclass.startsWith("pta.utils"))
				mainList.remove(mainclass);
		}
	}

	private String mainClassName;
	static boolean result;
	static boolean resultcmp;
	static boolean bunch = true; //load all testcases in one time; recommended for testing rather than debugging.

	public PTAValidator(String mainClassName) {
		this.mainClassName = mainClassName;
	}

	@Test
	public void test() {
		PTATimer.start(mainClassName);
		
		if (!result)
			switchToDummyOut();
		List<String> args = (List<String>) additionalCMD.clone();
		if(mainClassName.startsWith("pta.reflog"))
			args.add("-reflog=../tests/src/pta/reflog/"+mainClassName.substring(mainClassName.lastIndexOf('.')+1)+".log");
		invokePTA(mainClassName, args.toArray(new String[0]));
		if (!result)
			switchToSystemOut();
		
		PTATimer.stop(mainClassName);
		
		if(resultcmp){
//			if(PTAComparator.count!=0)
//				System.out.println(mainClassName+" is not precise!: "+PTAComparator.count);
			if(PTAComparator.count2!=0)
				System.out.println(mainClassName+" is not sound!: "+PTAComparator.count2);
		}else
			checkAlias(mainClassName.substring(mainClassName.lastIndexOf('.') + 1) + ".java");
		// printCGEdges("<"+mainClassName+": void main(java.lang.String[])>",
		// 3);
		// printAppPts();
	}

	public static void main(String[] args) {
		if (args.length > 0 && (args[0].equals("-h") || args[0].equals("-help")))
			printUsage();
		else {
			int i = 0;
			while (i < args.length) {
				if (!args[i].contains(".")&&!(args[i].equals("pta") ))
					additionalCMD.add(args[i]);
				else
					mainOrPackList.add(args[i].trim());
				i++;
			}
			if (additionalCMD.contains("-check")) {
				List<String> checktests = new ArrayList<>(Arrays.asList("python", "checktests.py", "-mainclasses"));
				checktests.addAll(prepareData());
				invokeExternalPTA(checktests);
				return;
			}
			if (additionalCMD.contains("-result")) {
				result = true;
				additionalCMD.remove("-result");
			}
			if (additionalCMD.contains("-resultcmp")) {
				resultcmp = true;
				additionalCMD.remove("-resultcmp");
			}
			org.junit.runner.JUnitCore.main(new String[] { "util.PTAValidator" });
		}
	}

	private final static void printUsage() {
		System.out.println("Usage for PTAValidator:\n"
				+ option(CYAN, "-h" + RESET + "|" + CYAN + "-help", "\t\tprint this message")
				+ option(CYAN, RESET + "|" + CYAN + "<mainclass|package|OPTION>*",
						"run all the testcases in PTA or the testcases specified by <mainclass|package>*")
				+ "\te.g. the args \"-result\" will runtests for all testcases in package pta with result information printed.\n"
				+ "\te.g. the args \"pta.special pta.basic.Return\" will runtests for all testcases in package pta.special plus one testcase pta.basic.Return.\n"
				+ "Typical Options for runTests:\n"
				+ option(YELLOW, "-result", "\tprint analysis result for each testcase")
				+ option(YELLOW, "-pta <k>(c|o)+?(<h>h)?|insens",
						"specify pointer-analysis e.g. 2o1h or 2o -> 2obj+1heap (default value: insens; default h for o: k-1; default h for c: 0.)")
				+ option(YELLOW, "-originalname", "use original Java names in analysis")
				+ "and nearly all other druid options...(find them by \"python runJA -help\")\n" + "Invalid options:\n"
				+ "\tthe following options are compulsory for testcases thus have already been added:\n" + "\t"
				+ option(RED, "-jre", "\t") + "\t" + option(RED, "-apppath", "") + "\t" + option(RED, "-libpath", "")
				+ "\t" + option(RED, "-mainclass", "") + "\t" + option(RED, "-singleentry", "") + "\t"
				+ option(RED, "-bunch", "") + "\t"
				+ option(RED, "-debug", "")+ "\t(a few of others containing jni using may not be valid.)\n");

	}

	private final static String option(String color, String option, String description) {
		return "\t" + color + option + RESET + "\t" + description + ".\n";
	}

	// ==============================Validator===============================
	public static String RESET = "", BOLD = "", GREEN = "", YELLOW = "", CYAN = "", WHITE = "", RED = "";
	static {
		if (!System.getProperty("os.name").toLowerCase().contains("win")) {
			RESET = "\033[0m";
			BOLD = "\033[1m";
			GREEN = "\033[32m";
			YELLOW = "\033[33m";
			CYAN = "\033[36m";
			WHITE = "\033[37m";
			RED = "\033[91m";
		}
	}

	private static PTA pta;
	/// output settings
	public static PrintStream dummyPrintStream;
	public static PrintStream filePrintStream;
	public static PrintStream systemOutStream = System.out;

	public static void switchToDummyOut() {
		dummyPrintStream = new PrintStream(new OutputStream() {
			@Override
			public void write(int b) throws IOException {
			}
		});
		System.setOut(dummyPrintStream);
	}

	public static void switchToSystemOut() {
		dummyPrintStream.close();
		System.setOut(systemOutStream);
	}

	public static void switchToFileOut() {
		System.setOut(filePrintStream);
	}

	/// invokers
	public static void invokePTA(String mainClass) {
		invokePTA(mainClass, new String[0]);
	}

	public static void invokePTA(String mainClass, String[] additionalArgs) {
		String[] mainArgs = new String[] { "-mainclass", mainClass };// main
																		// class
		invokePTA(concat(mainArgs, additionalArgs));
	}

	private static String[] CPSRArgs = new String[] { "-jre=lib/jre/jre1.6.0_45",
			// "-libpath=aafe/android-lib",
			"-apppath=../tests/bin", "-singleentry"
//			,"-debug"
			};

	public static void invokePTA(String[] clientArgs) {
		String[] args = concat(CPSRArgs, clientArgs);
//		systemOutStream.println(Arrays.asList(args));
		if(bunch){
			args = concat(args, new String[]{"-bunch"});
		}else{
			G.reset();
		}
		FakeMainFactory.v=null;
		if(resultcmp){
			PTAComparator.main(args);
		}else{
			Main.main(args);
			pta = Main.pta;
		}
	}

	public static String[] concat(String[] a, String[] b) {
		String[] c = new String[a.length + b.length];
		System.arraycopy(a, 0, c, 0, a.length);
		System.arraycopy(b, 0, c, a.length, b.length);
		return c;
	}

	public static void invokeExternalPTA(List<String> cmd) {
		try {
			ProcessBuilder pbuilder = new ProcessBuilder(cmd);
			pbuilder.redirectErrorStream(true);
			Process process = pbuilder.start();
			InputStream inputStream = process.getInputStream();
			BufferedReader reader = new BufferedReader(new InputStreamReader(inputStream));
			String line;
			while ((line = reader.readLine()) != null)
				System.out.println(line);
		} catch (IOException e) {
			e.printStackTrace();
		}
	}

	/// checkers
	/**
	 * Are the two pointers an alias with context insensitive points-to
	 * information?
	 */
	private static boolean isMayAlias(Value value, Value value2) {
		if (value instanceof NullConstant || value2 instanceof NullConstant)
			return false;
		PointsToSet pts1 = pta.reachingObjects((Local) value);
		PointsToSet pts2 = pta.reachingObjects((Local) value2);
		return soot.jimple.toolkits.pointer.Union.hasNonEmptyIntersection(pts1, pts2);
	}

	private static void checkAlias(String fileName) {
		String mayAliasSig = "<pta.utils.Dummy: void mayAlias(java.lang.Object,java.lang.Object)>";
		String notAliasSig = "<pta.utils.Dummy: void notAlias(java.lang.Object,java.lang.Object)>";

		QueueReader<MethodOrMethodContext> worklist = pta.getCgb().getReachableMethods().listener();
		Set<SootMethod> reachableMethods = new LinkedHashSet<SootMethod>();
		while (worklist.hasNext()) {
			SootMethod method = worklist.next().method();
			if (reachableMethods.add(method)) {
				if (method.isNative() || method.isPhantom())
					continue;
				Body b = method.retrieveActiveBody();
				for (Iterator<Unit> sIt = b.getUnits().iterator(); sIt.hasNext();) {
					final Stmt s = (Stmt) sIt.next();
					if (s.containsInvokeExpr()) {
						InvokeExpr ie = s.getInvokeExpr();
						if (ie instanceof StaticInvokeExpr) {
							final String methRefSig = ie.getMethodRef().getSignature();
							if (methRefSig.equals(mayAliasSig) || methRefSig.equals(notAliasSig)) {
								Value arg0 = ie.getArg(0);
								Value arg1 = ie.getArg(1);
								String args = "(" + arg0 + ", " + arg1 + ") " + " " + getId(arg0) + ", " + getId(arg1);
								String invokeInfo = RESET + "%s" + args + " " + YELLOW + fileName + RESET + ": "
										+ s.getTag("LineNumberTag") + "\n";
								String seccessInfo = GREEN + "\tSUCCESS: " + invokeInfo;
								String failInfo = RED + "\tFAIL:    " + invokeInfo;
								if (methRefSig.equals(mayAliasSig)) {
									if (isMayAlias(arg0, arg1))
										System.out.printf(seccessInfo, "mayAlias");
									else
										System.out.printf(failInfo, "mayAlias");
								} else {
									if (isMayAlias(arg0, arg1))
										System.out.printf(failInfo, "notAlias");
									else
										System.out.printf(seccessInfo, "notAlias");
								}
							}
						}
					}
				}
			}
		}
	}

	private static String getId(Value arg) {
		if (arg instanceof NullConstant)
			return arg.toString();
		Var_Node n = pta.getPag().findLocalVarNode(arg);
		if (pta instanceof ContextSensPTA) {
			HashMap<Context, ContextVar_Node> m = ((ContextSensPTA) pta).getContextVarNodeMap().get(n);
			if (m.size() != 1)
				throw new RuntimeException(
						"One and Only one version of each arg in stub function is permitted!!Please check your code!");
			n = m.values().iterator().next();
		}
		return arg + "=" + n.getNumber();
	}
}
