package edu.rpi.dim;

import java.util.HashMap;
import java.util.Set;

import checkers.inference.reim.quals.Readonly;
import checkers.inference.reim.quals.Polyread;
import checkers.inference.reim.quals.MaybeMutable;
import checkers.inference.reim.quals.PolyOrMaybe;

import java.io.PrintStream;
import java.io.File;

import soot.PackManager;
import soot.PrimType;
import soot.SourceLocator;
import soot.Transform;
import edu.rpi.AnnotatedValue;
import edu.rpi.AnnotatedValueMap;
import edu.rpi.AnnotationUtils;
import edu.rpi.Constraint;
import edu.rpi.ConstraintSolver;
import edu.rpi.InferenceTransformer;
import edu.rpi.SetbasedSolver;
import edu.rpi.reim.*;

import static com.esotericsoftware.minlog.Log.*;


public class SootDefiniteImmutability {
	
	private static boolean isLibraryVar(AnnotatedValue av) {
			
		if (av.getEnclosingClass().isJavaLibraryClass()) 
			return true;
		else 
			return false;
				
	}
	
	private static boolean ignorePrefix(String s) {
		if (s.startsWith("fake-") || s.startsWith("lib-"))
			return true;
		else 
			return false;
	}
	
	private static boolean isPrimitiveType(AnnotatedValue av) {
		if (av.getType() instanceof PrimType) 
			return true;
		else
			return false;
	}
	
	private static void printTypeInfo(HashMap<String,AnnotatedValue> vm, boolean verbose) {
		if (verbose) System.out.println("INFO: ");
		int readonly = 0;
		int polyread = 0;
		int maybe = 0;
		int mutable = 0;
		int polyOrMaybe = 0;
		for (String v : vm.keySet()) {
			AnnotatedValue av = vm.get(v);
			if (isLibraryVar(av) || ignorePrefix(v) || isPrimitiveType(av)) continue;
			if (av.containsAnno(AnnotationUtils.fromClass(Readonly.class))){
				readonly++;
				if (verbose) System.out.println(v + " is readonly");
			}
			else if (av.containsAnno(AnnotationUtils.fromClass(MaybeMutable.class))) {
				maybe++;
				if (verbose) System.out.println(v + " is maybemutable");
			}
			else if (av.containsAnno(AnnotationUtils.fromClass(Polyread.class))) {
				polyread++;
				if (verbose) System.out.println(v + " is polyread");
			}
			else if (av.containsAnno(AnnotationUtils.fromClass(PolyOrMaybe.class))) {
				polyOrMaybe++;
				if (verbose) System.out.println(v + " is polyOrMaybe");
			}
			else {
				mutable++;
				if (verbose) System.out.println(v + " is mutable");
			}
		}
		System.out.println("INFO: Annotated value size: " + vm.size());
		System.out.println("INFO: "+readonly+" READONLY, "+polyread+" POLYREAD, "+mutable+" MUTABLE.");
		System.out.println("INFO: readonly/all: "+ ((float) readonly)/(readonly+mutable+maybe+polyOrMaybe+polyread));
		System.out.println("INFO: mutable/all: "+ ((float) mutable)/(readonly+mutable+maybe+polyOrMaybe+polyread));
		System.out.println("INFO: "+maybe+" MAYBEMUTABLE.");
		System.out.println("INFO: "+polyOrMaybe+" POLYORMAYBE. ");
		
		System.out.println("INFO: MUTABLE/(MUTABLE+MAYBE+POLYORMAYBE): "+((float) mutable)/(maybe+polyOrMaybe+mutable));
	}
	
	public static void main(String[] args) {
        long startTime = System.currentTimeMillis();
		
        set(LEVEL_DEBUG);


        InferenceTransformer reimTransformer = new DimTransformer(); // to change to Reim
        PackManager.v().getPack("jtp").add(new Transform("jtp.reim", reimTransformer));

		soot.Main.main(args);

        info(String.format("%6s: %14d", "size", AnnotatedValueMap.v().size()));
        info(String.format("%6s: %14f MB", "free", ((float) Runtime.getRuntime().freeMemory()) / (1024*1024)));
        info(String.format("%6s: %14f MB", "total", ((float) Runtime.getRuntime().totalMemory()) / (1024*1024)));

        String outputDir = SourceLocator.v().getOutputDir();

        System.out.println("INFO: Solving Rem constraints:  " + reimTransformer.getConstraints().size() + " in total...");
        ConstraintSolver cs = new SetbasedSolver(reimTransformer, false);
        Set<Constraint> errors = cs.solve();
        try {
            PrintStream remOut = new PrintStream(outputDir + File.separator + "rem-constraints.log");
            for (Constraint c : reimTransformer.getConstraints()) {
                remOut.println(c); 
            }
            remOut.close();
        } catch (Exception e) {
            e.printStackTrace();
        }
                                        
        printTypeInfo(AnnotatedValueMap.v(), false);

        /*
        for (Constraint c : errors) {
            System.out.println(c); // TODO: figure our errors. Conj: erros are casts.
        }
        */
        
        System.out.println("INFO: Finished solving Rem constraints. " + errors.size() + " error(s)");

        // printTypeInfo(AnnotatedValueMap.v(), true);
        
        try {
            PrintStream reimOut = new PrintStream(outputDir + File.separator + "rem-result.jaif");
            reimTransformer.printJaif(reimOut);
            reimTransformer.clear();
        } catch (Exception e) {
            e.printStackTrace();
        }

		
        long endTime   = System.currentTimeMillis();
        System.out.println("INFO: Total running time: " + ((float)(endTime - startTime) / 1000) + " sec");
        
	}
	
	
}
