package jayhorn;

import java.nio.file.Path;
import java.nio.file.Paths;

import org.kohsuke.args4j.CmdLineException;
import org.kohsuke.args4j.CmdLineParser;

import com.google.common.base.Stopwatch;

import jayhorn.checker.Checker;
import jayhorn.solver.ProverFactory;
import jayhorn.solver.princess.PrincessProverFactory;
import jayhorn.solver.z3.Z3ProverFactory;
import jayhorn.utils.Stats;
import soottocfg.cfg.Program;
import soottocfg.soot.SootToCfg;
import soottocfg.soot.SootToCfg.MemModel;

public class Main {
	
    private static String parseResult(String solver, boolean result)
    {
    	if (result){
			return "SAFE";
		}else{
			return "UNSAFE";
		}
    }
    /**
     * Safety Analysis with JayHorn
     * @param options
     * @param factory
     */
    public static void safetyAnalysis(ProverFactory factory){
    	Log.info("Building CFG  ... ");
  		SootToCfg soot2cfg = new SootToCfg();
  		soottocfg.Options.v().setBuiltInSpecs(Options.v().useSpecs);
  		soottocfg.Options.v().setResolveVirtualCalls(true);
  		soottocfg.Options.v().setMemModel(MemModel.PullPush);
  		if (Options.v().getOut()!=null) {
  			Path outDir = Paths.get(Options.v().getOut());
  			String in = Options.v().getJavaInput();
  			String outName = in.substring(in.lastIndexOf('/') + 1, in.length()).replace(".java", "").replace(".class", "");
  			soottocfg.Options.v().setOutDir(outDir);
  			soottocfg.Options.v().setOutBaseName(outName);
  		}
  		soot2cfg.run(Options.v().getJavaInput(), Options.v().getClasspath());	
  	
  		Stopwatch sootTocfgTimer = Stopwatch.createStarted();
  		Program program = soot2cfg.getProgram();
  	    Stats.stats().add("SootToCFG", String.valueOf(sootTocfgTimer.stop()));
  		
  		Log.info("Safety Verification ... ");
  		Checker hornChecker = new Checker(factory);
  		
  		boolean result = hornChecker.checkProgram(program);
  		
  		String prettyResult = parseResult(Options.v().getSolver(), result);
  		
  		Stats.stats().add("Result", prettyResult);
  		
  		if (Options.v().stats){ Stats.stats().printStats(); }
      
  		Log.info("Safety Result ... " + prettyResult);
  		
      }
    
	public static void main(String[] args) {
		System.out.println("\t\t ---   JAYHORN : Static Analayzer for Java Programs ---- ");
		
		Options options = Options.v();
		CmdLineParser parser = new CmdLineParser(options);
		try {
			// parse command-line arguments
			parser.parseArgument(args);
			options.updateSootToCfgOptions();
			ProverFactory factory = null;
			if ("z3".equals(Options.v().getSolver())) {
				factory = new Z3ProverFactory();
			} else if ("eldarica".equals(Options.v().getSolver())) {
				factory = new PrincessProverFactory();
			} else {
				throw new RuntimeException("Don't know solver " + Options.v().getSolver() + ". Using Eldarica instead.");
			}
			
			if ("safety".equals(Options.v().getChecker())) {			
				safetyAnalysis(factory);
				
			} else {
				Log.error(String.format("Checker %s is unknown", Options.v().getChecker()) );
			}
			
		} catch (CmdLineException e) {
			Log.error(e.toString());
			Log.error("java -jar jayhorn.jar [options...] -j [JAR, DIR]");
			parser.printUsage(System.err);
		} catch (Throwable t) {
			Log.error(t.toString());
			throw t;
		} finally {
			Options.resetInstance();
			soot.G.reset();
		}
	}

}

@@ -1990,16 +1990,65 @@
 %0A  %09%09%0A  
+%09%09Log.info(%22Safety Result ... %22 + prettyResult);%0A
 %09%09if (Op
@@ -2099,71 +2099,8 @@
 ; %7D%0A
-      %0A  %09%09Log.info(%22Safety Result ... %22 + prettyResult);%0A  %09%09%0A
     
@@ -3141,16 +3141,19 @@
 m.err);%0A
+%09%09%0A
 %09%09%7D catc
@@ -3166,24 +3166,24 @@
 owable t) %7B%0A
-
 %09%09%09Log.error
@@ -3198,16 +3198,116 @@
 ing());%0A
+%09%09%09Stats.stats().add(%22Result%22, %22UNKNOWN%22);%0A%09%09%09if (Options.v().stats)%7B Stats.stats().printStats(); %7D%0A
 %09%09%09throw
@@ -3309,16 +3309,17 @@
 throw t;
+%09
 %0A%09%09%7D fin
@@ -3376,14 +3376,16 @@
 ();%0A%09%09%7D%0A
+%0A
 %09%7D%0A
+%09
 %0A%7D%0A

print unknown in stats