package Sequenic.T2.Engines;

import Sequenic.T2.*;
import Sequenic.P2.*;
import Sequenic.T2.Msg.*;
import Sequenic.T2.DataGen.* ;
import jargs.gnu.*;
import java.util.* ;
import java.io.* ;
import java.lang.reflect.* ;

/**
 * A wrapper to plug-in {@link BaseEngine} to the {@ Sequenic.T2.Main Main-tool}.
 * 
 * @author underdarkprime
 */
public class BaseEngineToolPlug extends ToolPlug {

    // Variables holding various options:
    private CmdLineParser.Option execLengthO = parser.addIntegerOption('l', "lenexec");//ok
    private CmdLineParser.Option objDepthO = parser.addIntegerOption('d', "depthobj");//ok
    private CmdLineParser.Option maxNumOfStepsO = parser.addIntegerOption('n', "nmax"); //ok
    private CmdLineParser.Option searchModeO = parser.addIntegerOption("searchmode"); 
    private CmdLineParser.Option maxNumOfViolO = parser.addIntegerOption('v', "violmax"); //ok
    private CmdLineParser.Option typeOfColElementO = parser.addStringOption("elemty"); //ok
    private CmdLineParser.Option customtracedirO = parser.addBooleanOption("customtracedir");//ok
    private CmdLineParser.Option pubOnlyO = parser.addBooleanOption("pubonly");//ok
    private CmdLineParser.Option ownClassOnlyO = parser.addBooleanOption("ownclassonly");//ok
    private CmdLineParser.Option nullProbO = parser.addDoubleOption("nullprob");//ok
    private CmdLineParser.Option pickPoolProbO = parser.addDoubleOption("pickpoolprob");//ok
    private CmdLineParser.Option passTObjAsParamProbO = parser.addDoubleOption("tobjasparam");//ok
    private CmdLineParser.Option fieldUpdateProbO = parser.addDoubleOption("fupdateprob");//ok
    private CmdLineParser.Option maxArrayLengthO = parser.addIntegerOption("maxarraylen");//ok
    private CmdLineParser.Option showDepthO = parser.addIntegerOption("showdepth");//ok
    private CmdLineParser.Option hideIntermediateStepsO = parser.addBooleanOption("hideintermstep");//ok
    private CmdLineParser.Option timeoutO = parser.addIntegerOption("timeout");//ok
    private CmdLineParser.Option inclPrivateO = parser.addBooleanOption("inclprivate");//ok
    private CmdLineParser.Option exclDefaultO = parser.addBooleanOption("excldefault");//ok
    private CmdLineParser.Option exclProtectedO = parser.addBooleanOption("exclprotected");//ok
    private CmdLineParser.Option exclStaticO = parser.addBooleanOption("exclstatic");//ok
    private CmdLineParser.Option exclFieldO = parser.addBooleanOption("exclfield");//ok
    private CmdLineParser.Option onlyThisMethodO = parser.addStringOption("meth");//ok
    private CmdLineParser.Option excludeThisMethodO = parser.addStringOption("xmeth");//ok
    private CmdLineParser.Option collectGoodTracesO = parser.addIntegerOption("savegoodtr"); //ok
    private CmdLineParser.Option saveFileO = parser.addStringOption("savefile");//ok
    private CmdLineParser.Option poolO = parser.addStringOption("pool");//ok
    private CmdLineParser.Option baseDomainO = parser.addStringOption("bdomain");//ok
    private CmdLineParser.Option imapO = parser.addStringOption("imap");//ok
    private CmdLineParser.Option debugO = parser.addBooleanOption("debug");//ok
    private CmdLineParser.Option inclSuperInvsO = parser.addBooleanOption("inclsuperinv");//ok
    private CmdLineParser.Option outStreamO = parser.addStringOption("outfile");//ok
    private CmdLineParser.Option silentO = parser.addBooleanOption("silent");//ok
    // Variable to hold a base engine:
    protected BaseEngine engine ;
    private PrintStream reportStream ;

    public BaseEngineToolPlug() {

        addOption(execLengthO, "Maximum execution depth.");
        addOption(objDepthO, "Maximum object depth (at the creation).");
        addOption(maxNumOfStepsO, "Maximum number of execution steps afterwhich RT2 stops.");
        addOption(maxNumOfViolO, "Maximum number of violations afterwhich RT2 stops.");
        addOption(searchModeO,"Search mode. Specify a non-negative int as upperbound of search attemps.") ;
        addOption(typeOfColElementO, "The (qualified) name of the type of elements of Collections");
        addOption(customtracedirO, "Let CUT's custom trace director drives the generation of the traces.");
        addOption(pubOnlyO, "Limit the test scope to public members.");
        addOption(ownClassOnlyO, "Limit the test scope to CUT's own declared members.");
        addOption(nullProbO, "The probability to generate null. Use negative value to surpress.");
        addOption(pickPoolProbO, "The probability to pick object from pool. Use negative value surpress.");
        addOption(passTObjAsParamProbO, "The probability to pass target object as a method's parameter instead of receiver. Use negative value to surpress.");
        addOption(fieldUpdateProbO, "The probability to choose field update for a trace step. Use negative value to surpress.");
        addOption(maxArrayLengthO, "Maximum length of created arrays.");
        addOption(showDepthO, "Maximum depth of objects showed in reports.");
        addOption(hideIntermediateStepsO,"To hide intermediate steps.") ;
        addOption(timeoutO, "Timeout period.");
        addOption(inclPrivateO, "Include private members in the test scope.");
        addOption(exclDefaultO, "Exclude members with default access from the test scope.");
        addOption(exclProtectedO, "Exclude protected members from the test scope.");
        addOption(exclStaticO, "Exclude static members from the test scope.");
        addOption(exclFieldO, "Exclude fields from the test scope.");
        addOption(onlyThisMethodO, "Only include these methods in the test scope. Will also surpress field update.", true);
        addOption(excludeThisMethodO, "Exclude these methods from the test scope.", true);
        addOption(collectGoodTracesO, "If int is positive will also save up to this much non-violating traces.");
        addOption(saveFileO, "Will save the traces in the specified name. Normally it is CUT.tr.");
        addOption(poolO, "Use this custom pool; \"name\" is a fully qualified Java name.");
        addOption(baseDomainO, "Use this custom base domain; \"name\" is a fully qualified Java name.");
        addOption(imapO, "Use this custom interface map; \"name\" is a fully qualified Java name.");
        addOption(debugO, "Turn on T2 debug-mode (only useful for T2 developer).");
        addOption(inclSuperInvsO, "Also check against the class invariants of CUT's superclasses.");
        addOption(outStreamO, "Will print the report to the specified file rather than to the console.");
        addOption(silentO, "Will not print execution trails. Overall statistics are still shown.");

        
    }

    @Override
    public void configure(String[] options) 
                throws 
                CmdLineParser.IllegalOptionValueException, 
                CmdLineParser.UnknownOptionException {
        
        assert options.length > 0 ;
        
        // Getting CUT:
        Class CUT = null ;
        try {
            CUT = Class.forName(options[0]);
        } catch (Exception e) {
            throw new T2Error("T2 fails to get class " + options[0] + ".", e);
        }
        
        // Collecting annotated options:
        T2annotation.option annotatatedO 
                = 
                (T2annotation.option) CUT.getAnnotation(T2annotation.option.class) ;
        
        String[] allOptions = options ;
	if (annotatatedO != null) {
            String[] annotatedOptions = annotatatedO.value().split("\\s") ;
            allOptions = new String[options.length + annotatedOptions.length] ;
            for (int i=0; i<options.length ; i++) allOptions[i] = options[i] ;
            for (int i=0; i<annotatedOptions.length ; i++) allOptions[options.length + i] = annotatedOptions[i] ;
        }
        
        // Now parsing all options:
        parser.parse(allOptions); 
        
        // Create an engine with a default configuration:
        engine = new BaseEngine(CUT) ;
          
        // Now do the configuration work:
        int n = 0 ;
	double p = 0 ;
	String s = null ;
	
        engine.maxNumOfSteps = (Integer) parser.getOptionValue(maxNumOfStepsO,engine.maxNumOfSteps) ;  
        engine.maxExecLength = (Integer) parser.getOptionValue(execLengthO,engine.maxExecLength) ;
	engine.maxNumViolations = (Integer) parser.getOptionValue(maxNumOfViolO,engine.maxNumViolations) ;
        engine.maxMkValSeqDepth = (Integer) parser.getOptionValue(objDepthO,engine.maxMkValSeqDepth) ;
        engine.searchMode = (Integer) parser.getOptionValue(searchModeO,engine.searchMode) ;
        n = (Integer) parser.getOptionValue(maxArrayLengthO,engine.maxArrayLengthProb.getHigh()) ;
        if (n<0) n=0 ;
        if (n!=engine.maxArrayLengthProb.getHigh()) engine.maxArrayLengthProb = new RandomIntUniform(0,n) ;
        engine.maxShowDepth = (Integer) parser.getOptionValue(showDepthO,engine.maxShowDepth) ;
        engine.showIntermediateSteps = parser.getOptionValue(hideIntermediateStepsO) == null ;
        engine.timeOutPeriod = (Integer) parser.getOptionValue(timeoutO,engine.timeOutPeriod) ;
        engine.saveThisMany = (Integer) parser.getOptionValue(collectGoodTracesO,engine.saveThisMany) ;
        
	p = (Double) parser.getOptionValue(nullProbO, engine.generateNullProb.high) ;
        if (p!=engine.generateNullProb.high) engine.generateNullProb = new RandomBoolUniform(p) ;
        p = (Double) parser.getOptionValue(pickPoolProbO, engine.pickTargetObjFromPoolProb.high) ;
        if (p!=engine.pickTargetObjFromPoolProb.high) engine.pickTargetObjFromPoolProb = new RandomBoolUniform(p) ;
	p = (Double) parser.getOptionValue(fieldUpdateProbO,engine.chooseFieldUpdateProb.high) ;
        if (p!=engine.chooseFieldUpdateProb.high) engine.chooseFieldUpdateProb = new RandomBoolUniform(p) ;
        p = (Double) parser.getOptionValue(passTObjAsParamProbO, engine.passTObjAsParamProb.high) ;
        if (p!=engine.passTObjAsParamProb.high) engine.passTObjAsParamProb = new RandomBoolUniform(p) ;
        
	engine.nameOfSaveFile = (String) parser.getOptionValue(saveFileO)  ;
	if (engine.nameOfSaveFile != null) {
		engine.nameOfSaveFile = engine.nameOfSaveFile.trim() ;
		if (!engine.nameOfSaveFile.endsWith(".tr")) engine.nameOfSaveFile += ".tr" ;
	}
        
        s = (String) (parser.getOptionValue(outStreamO)) ;
        if (s != null) {
            try { reportStream = new PrintStream(s) ; }
            catch (Exception e) {
                throw new T2Error("Fail to open " + s + ".", e) ;
            }
            engine.out = reportStream ;
            engine.reporters.setOutStream(reportStream) ;
        }
        
        engine.showViolatingTraces = parser.getOptionValue(silentO) == null ;
        /*
        if (outfileName != null) {
		
	}
         */
        
        s = (String) (parser.getOptionValue(poolO))  ;	
	if (s != null) {
            Pool P = (Pool) Util.mkAnInstance(s) ;
            if (P != null) engine.pool = P ;
            else throw new T2Error("Fail to instantiate the pool " + s + ".") ;
	}
			
	s = (String) (parser.getOptionValue(imapO))  ;	
	if (s != null) {
		InterfaceMap IM = (InterfaceMap) Util.mkAnInstance(s) ;
		if (IM != null) engine.interfaceMap = IM ;
		else throw new T2Error("Fail to instantiate the interface map " + s + ".") ;
	}
		
	s = (String) (parser.getOptionValue(baseDomainO))  ;	
	if (s != null) {
		BaseDomain D = (BaseDomain) Util.mkAnInstance(s) ;
		if (D != null) engine.baseDomain = D ;
		else throw new T2Error("Fail to instantiate the base domain " + s + ".") ;
	}
        
        engine.useCustomTraceDirector = parser.getOptionValue(customtracedirO) != null ;
        engine.accessOption.excludePrivate = parser.getOptionValue(inclPrivateO) == null ;
        engine.accessOption.excludeDefault = parser.getOptionValue(exclDefaultO) != null ;
        engine.accessOption.excludeProtected = parser.getOptionValue(exclProtectedO) != null ;
        engine.accessOption.excludeStatic = parser.getOptionValue(exclStaticO) != null ;
        engine.accessOption.excludeField = parser.getOptionValue(exclFieldO) != null ;
        engine.accessOption.excludeAncestorFieldsAndMethods = parser.getOptionValue(ownClassOnlyO) != null ; 
	if (parser.getOptionValue(pubOnlyO) != null) { 
			engine.accessOption.excludePrivate = true ;
			engine.accessOption.excludeDefault = true ;
			engine.accessOption.excludeProtected = true ;
	}
       
        // reload methods etc to match the new access option:	
        engine.consIPs = Util.filterCons(engine.accessOption, Util.getAllCons(CUT));
        engine.fieldsIPs = Util.filterFields(engine.accessOption, Util.getAllFields(CUT));
        engine.methodsIPs = Util.filterMethods(engine.accessOption, Util.getAllMeths(CUT));	
        
        Vector checkOnlyTheseMethods = parser.getOptionValues(onlyThisMethodO) ;
		
	if (checkOnlyTheseMethods != null && !checkOnlyTheseMethods.isEmpty()) {
            List<String> names = new LinkedList<String>() ;
            for (Object name : checkOnlyTheseMethods) names.add((String) name) ;					
            engine.fieldsIPs = new LinkedList<Field>() ;
            engine.methodsIPs  = Util.getMethodsByNames(names, engine.methodsIPs) ;
	}
        
      	Vector excludeTheseMethods = parser.getOptionValues(excludeThisMethodO) ;
		
	if (excludeTheseMethods != null && !excludeTheseMethods.isEmpty()) {
		List<String> names = new LinkedList<String>() ;
		for (Object name : excludeTheseMethods) names.add((String) name) ;					
		engine.methodsIPs  = Util.excludeMethodsByNames(names, engine.methodsIPs) ;
	}
	
        engine.classINV = Util.getClassINV(CUT) ;
        if (parser.getOptionValue(inclSuperInvsO) != null) {
            engine.accessOption.excludeAncestorClassInv =  false ;
            engine.allClassINVs = Util.getSuperClassINVs(CUT) ;
        }
        else {
            engine.accessOption.excludeAncestorClassInv =  true ;
            engine.allClassINVs = new LinkedList<Method>();
            if (engine.classINV != null) {
                engine.allClassINVs.add(engine.classINV);
            }
        }
        
        s = (String) parser.getOptionValue(typeOfColElementO) ;
        //println(">>>" + s) ;
        if (s!=null) {
            try { 
		engine.TYVAR0 = Class.forName(s) ; 
        //println(">>>" + engine.TYVAR0.getName()) ;
            }
            catch (Exception e) { }		
        }			
	if (parser.getOptionValue(debugO) != null) BaseEngine.debug = true ;
                
	// Calculating values for derived variables:
        engine.realign() ;	
        // Printing back how the engine has been configure:
        getInternalConfiguration() ;
                    
    }

    /**
     * This will get the engine's internal configuration; we will store various
     * configuration attributes in the variable config, to be reported back
     * to the user.
     */
    private void getInternalConfiguration() {
        boolean b ;
        config.add("CUT = " + engine.CUT.getName()) ;
        if (engine.TYVAR0 == null) 
            config.add("TYVAR0 = " + "null") ;
	else
            config.add("TYVAR0 = " + engine.TYVAR0.getName()) ;
        config.add("Pool = " + engine.pool.getClass().getName()) ;
	config.add("Base domain = " + engine.baseDomain.getClass().getName()) ;
	config.add("Interface map = " + engine.interfaceMap.getClass().getName()) ;
        if (engine.timeOutPeriod<=0)
            config.add("Time-out = none") ;
        else 
            config.add("Time-out = " + engine.timeOutPeriod) ;
        config.add("Max. number of steps = " + engine.maxNumOfSteps) ;
	config.add("Max. execution depth = " + engine.maxExecLength) ;
	config.add("Max. number of violations to look = " + engine.maxNumViolations) ;		
	config.add("Max. object depth (on creation) = " + engine.maxMkValSeqDepth) ;
	config.add("Max. show depth = " + engine.maxShowDepth) ;
	config.add("Max. array/collection size = " + (engine.maxArrayLengthProb.getHigh()-1)) ;
	config.add("Incl. Private = " + !engine.accessOption.excludePrivate) ;
	config.add("Incl. Default = " + !engine.accessOption.excludeDefault) ;
	config.add("Incl. Protected = " + !engine.accessOption.excludeProtected) ;
	config.add("Incl. Static = " + !engine.accessOption.excludeStatic) ;
	config.add("Incl. superclass members = " + !engine.accessOption.excludeAncestorFieldsAndMethods) ;
	config.add("Incl. superclass classinvs = " + !engine.accessOption.excludeAncestorClassInv) ;
        b = !engine.accessOption.excludeField && engine.chooseFieldUpdateProb.high > 0 ;
	config.add("Field update enabled = " + b) ;
        if (b) config.add("Prob. of updating field = " + engine.chooseFieldUpdateProb.high) ;
	config.add("Prob. to generate NULL = " + Math.max(0,engine.generateNullProb.high)) ;
        config.add("Prob. to pass targetobj as param = " + Math.max(0,engine.passTObjAsParamProb.high)) ;
	config.add("Prob. of trying pool before constuctor = " + Math.max(0,engine.pickTargetObjFromPoolProb.high)) ;
    }
    
    public void run() {
        printConfig() ;
        engine.timedRun();
        if (reportStream!=null) reportStream.close() ;
        // Throw a 'violation' signal...
        if (!engine.violatingTraces.isEmpty()) throw new Violation() ;
    }

    public void consoleHelp() {
        println(Message.GREET);
        println(Message.BEGIN);
        println("Base-engine GENERAL USE:\n");
        println("   java -ea -cp <classpaths> Sequenic.T2.Main [-E] <CUT> <option>*\n");
        println(StringFormater.alignLeft("CUT is a fully qualified java name of the target class. " +
                "Available options are explained below.",
                80,0));
        println("") ;
      
        consoleOptionsHelp();

        println(Message.END);

    }
}