package fr.lifl.stc.stan.analyser;

import java.util.ArrayList;
import java.util.Iterator;
import java.util.Stack;
import java.util.Hashtable;
import java.util.Vector;
import java.util.HashMap;
import java.util.TreeMap;

import org.apache.bcel.SignatureConstants;
import org.apache.bcel.classfile.Attribute;
import org.apache.bcel.classfile.CodeException;
import org.apache.bcel.classfile.ProofAttribute;
import org.apache.bcel.classfile.JavaClass;
import org.apache.bcel.classfile.Method;
import org.apache.bcel.generic.ConstantPoolGen;
import org.apache.bcel.generic.InstructionHandle;
import org.apache.bcel.generic.InstructionList;
import org.apache.bcel.generic.InvokeInstruction;
import org.apache.bcel.generic.FieldInstruction;


import fr.lifl.stc.stan.annotation.*;
import fr.lifl.stc.stan.execution.Frame;
import fr.lifl.stc.stan.execution.InstructionType;
import fr.lifl.stc.stan.execution.Interpreter;
import fr.lifl.stc.stan.execution.MethodInfo;
import fr.lifl.stc.stan.implicitFlow.ImplicitDependences;
import fr.lifl.stc.stan.implicitFlow.data.BooleanExpression;
import fr.lifl.stc.stan.implicitFlow.data.BooleanVariable;
import fr.lifl.stc.stan.implicitFlow.execution.InterpreterIF;
import fr.lifl.stc.stan.implicitFlow.execution.MethodInfoIF;
import fr.lifl.stc.stan.policy.Policy;
import fr.lifl.stc.stan.samples.escape.EscapeAnnotation;
import fr.lifl.stc.stan.samples.flow.FlowAnnotation;
import fr.lifl.stc.stan.signature.*;
import fr.lifl.stc.stan.util.Printer;
import fr.lifl.stc.stan.dsl.FlowChecker;
import fr.lifl.stc.stan.dsl.FlowCheckerException;
import fr.lifl.stc.stan.dsl.Flow;
import fr.lifl.stc.stan.samples.flow.FlowPartialSignature;
import fr.lifl.stc.stan.samples.flow.FlowPartialSignatureData;
import fr.lifl.stc.stan.link.TableLink;
import fr.lifl.stc.stan.link.Link;
import fr.lifl.stc.stan.link.defaultLink.DefaultLink;
import org.apache.bcel.generic.ReturnInstruction;

/**
 * @author <a href="mailto:dorina.ghindici@lifl.fr">Dorina</a>
 *
 * This class provides an algorithm to perform a static analysis a method of a '.class' file.
 *
 */
public class MethodAnalyzer {

	/**
	 *  the Java class to wich the analysed belongs
	 */
	private JavaClass _class;


	private ClassAnalyser classAnalyser;

	/**
	 * contant pool of the class
	 */
	private ConstantPoolGen cpg;

	/**
	 * The method to wich the analyse applies
	 */
	private Method _method;

	/**
	 * Array of Annotations vector (one vector per instruction)
	 */
	private Annotation annotations[];

	/**
	 * A global dictionary that contains all method signature.
	 */
	private SignatureDictionary dictionary;

	private Policy policy;

    private FlowChecker flowchecker; /** Checker for dsl policies */

	private MethodInfo methodInfo;

	private Interpreter interpreter;

	private InterpreterIF interpreterIF;

	private MethodInfoIF methodInfoIF;

	private ImplicitDependences implicitDependences;

	/**
	 * label bytecode (int) => Frame
	 */
	private TreeMap<Integer,Vector<Frame>> labels = new TreeMap<Integer,Vector<Frame>>();

	/**
	 * stats for label bytecodes
	 * label(int) => number of passes (int)
	 */
	Hashtable<Integer,Integer> statsLabels = new Hashtable<Integer,Integer>();

	//public static int stat = 0;

	private int proof_index;


	////////////////////////////////////////////////////////////////
	//// Constructor
	////////////////////////////////////////////////////////////////

	/**
	 *
	 */

	/**
	 * Creates a new <code>MethodAnalyser</code> instance.
	 *
	 * @param dict
	 *          A global dictionary that contains all methods signatures.
	 * @param pol
	 * 			The security policy
	 * @param cpg
	 * 			The constant pool generator
	 * @param c
	 *          The class to witch m belongs
	 * @param m
	 *          The method to analyse
	 * @param proof_index
	 * 			The index for the  <code>proof</code> attribute, when adding annotations to <code>.class</code> file
	 *
	 */
	public MethodAnalyzer(SignatureDictionary dict, Policy pol, FlowChecker fc,
                          ConstantPoolGen cpg, JavaClass c, Method m, ClassAnalyser ca, int proof_index) {
		this.policy = pol;
        this.flowchecker = fc;
		this.setDictionary(dict);
		this._class = c;
		this._method = m;
		this.setCpg(cpg);
		this.classAnalyser = ca;
		this.methodInfo = new MethodInfo(this);
		this.interpreter = new Interpreter(this);
		this.proof_index = proof_index;

        // plop
		//methodInfoIF = new MethodInfoIF(this);
		//this.implicitDependences = new ImplicitDependences(_method,methodInfoIF.getConditions());
		//interpreterIF = new InterpreterIF(this);

		this.initAnnotations();
		this.initLabels();

		Stats.sizeOfProof += statsLabels.size()
				* (interpreter.getMethodInfo().getReferences().length + interpreter
						.getMethodInfo().getValues().length);
	}

	/**
	 * Initialization of the annotations vector array
	 *
	 */
	private void initAnnotations() {
		//FIXME depends on options
		annotations = new Annotation[2];
		annotations[0] = new FlowAnnotation(interpreter.getRefValues(),
				interpreter.getMethodInfo());
		annotations[1] = new EscapeAnnotation(interpreter.getRefs(),
				interpreter.getMethodInfo());
	}


	/**
	 * Initiates <code>labels</code> with labels bytecode
	 *
	 */
	private void initLabels() {
		InstructionList i_list;
		i_list = new InstructionList(_method.getCode().getCode());
		Iterator<InstructionHandle> it = i_list.iterator();
		while (it.hasNext()) {
			InstructionHandle ih = it.next();

			if (ih.hasTargeters()) {
				labels.put(new Integer(ih.getPosition()), new Vector<Frame>(0));
			} else if (InstructionType.getType(ih.getInstruction()) == InstructionType.JSR_INSTRUCTION) {
				labels.put(new Integer(ih.getPosition()), new Vector<Frame>(0));
			}
		}
		//Add exception handlers to labels table
		CodeException[] handlers = _method.getCode().getExceptionTable();
		for (int i = 0; i < handlers.length; i++) {
			labels.put(new Integer(handlers[i].getHandlerPC()), new Vector<Frame>(0));
		}

		Iterator<Integer> it2 = labels.keySet().iterator();
		while (it2.hasNext()){
			Integer lab= it2.next();
			statsLabels.put(lab, new Integer(0));
		}
	}

	/**
	 * increments number of passes for label <code>pos</code>
	 * @param pos
	 */
	private void incStat(int pos) {
		Integer posi = new Integer(pos);
		int i = statsLabels.get(posi).intValue();
		i++;
		statsLabels.put(posi, new Integer(i));
	}

	/**
	 * Merges the frame for bytecote <code>pos</code> with the frame <code>f</code>
	 * @param pos
	 * @param f
	 * @return
	 */
	private boolean mergeFrameAtLabel(int pos, Frame f) {


		if (!labels.containsKey(new Integer(pos)))
			return true;

		Integer posi = new Integer(pos);

		Vector<Frame> v = labels.get(posi);
		boolean updated = false;
		if (v.size() == 0) {
            System.out.println("new frame");
			v.add((Frame) f.clone());
			updated = true;
		} else {
            System.out.println("merge frame");
            
			Frame f0 = v.elementAt(0);
			updated = f0.merge(f);
		}
		return updated;
	}

	/**
	 *
	 * @param pos
	 * 			The bytecode position to be verified
	 * @return
	 * 		<code>true</code> if the bytecode at position <code>pos</code> is a target bytecode,
	 * 		<code>false</code> otherwise
	 */
	private boolean isLabelOrHandler(int pos) {
		return labels.containsKey(new Integer(pos));
	}

	/**
	 * Returns the frame corresponding to bytecode at position <code>pos</code
	 * @param pos
	 *
	 * @return
	 * 			the frame corresponding to bytecode at position <code>pos</code>. If <code>pos</code>
	 * 			is not a label bytecode, it returns <code>null</code>
	 */
	private Frame getFrameForPos(int pos) {
		Vector<Frame> v = labels.get(new Integer(pos));
		if (v != null && v.size() > 0)
			return v.elementAt(0);
		return null;
	}

	////////////////////////////////////////////////////////////////
	//// Analyse
	////////////////////////////////////////////////////////////////


	/**
	 *
	 * Follows the control flow of the method
	 * Algorithm:
	 * Initialization of the control stack
	 *   do
	 *     get the instruction to execute on top of stack
	 *     get the instruction previously executed on top of stack
	 *     update the annotation vector of the current instruction
	 *     execute the instruction
	 *     get the next possible instruction after the current one
	 *
	 *     if some changes has been brougth to annotations, stack, static world
	 *       or local variables (variable and parameter)
	 *         for each of these instruction do
	 *           push on top of stack the current instruction
	 *           push on top of stack the next instruction
	 *         done
	 *     end if
	 *   while the stack is not empty
	 */
	public void analyse() {

		if (_method.isNative()) {
			System.err.println("[Warning] " + _method + " is native");
			return;
		}

		Stats.aproxMemory(labels.size(), this.methodInfo.getJvmValues().length);

		Stack<InstructionHandle> control = new Stack<InstructionHandle>();
		control.push(interpreter.getStart());
		Frame currentFrame = null;
		if (isLabelOrHandler(interpreter.getStart().getPosition())) {
			this.mergeFrameAtLabel(interpreter.getStart().getPosition(),
					this.interpreter.getDefaultFrame());
		} else {
			currentFrame = this.interpreter.getDefaultFrame();
		}

        TableLink checkedlinks = new TableLink(30, 30); //FIXME
        

        Frame prev_frame= (Frame)currentFrame.clone();
        
		InstructionHandle currentHandle = null;

		while (!control.isEmpty()) {
			currentHandle = control.pop();

			/**
			 * get current frame
			 */
			if (isLabelOrHandler(currentHandle.getPosition())) {
                System.out.println("label or handler spotted");

                prev_frame = (Frame)currentFrame.clone();
				currentFrame = null;
				currentFrame = (Frame) (this.getFrameForPos(currentHandle.getPosition()).clone());
				incStat(currentHandle.getPosition());
			}
            

            /**
             * Mod starts here
             */

            //            System.out.println(">> " + currentHandle + " <<");
//            System.out.println(currentFrame);
            
            TableLink newtbl = ((FlowAnnotation)annotations[0]).link(currentFrame);

            for(int i=0; i<newtbl.getSizeL(); i++)
                for(int j=0; j<newtbl.getSizeC(); j++)
                {
                    DefaultLink l = (DefaultLink)newtbl.get(i, j);

                    
                    //System.out.println(checkedlinks.get(i+1, j+1));
                    
                    Link currentlink = checkedlinks.get(i+1, j+1);
                    if ( currentlink != null
                         && Link.equals(currentlink, l) )
                        continue;
                    //System.out.println("cur link = " + currentlink);
                    
                    
                    if ( l != null )
                    {
                        
                        //System.out.println("j:" + j + ",i:" + i + ", l=" + l.getLink());
                    
                        Flow f = new Flow(_class, _method, j+1, i+1, l.getLink());
                        checkedlinks.set(i+1, j+1, (Link)l.clone());
                        try {
                            flowchecker.check(f);
                        } catch(FlowCheckerException e) {
                            int srcLine2 = _method.getLineNumberTable().getSourceLine(currentHandle.getPrev().getPosition());
                            System.out.println("[E]{" + _class.getClassName() + "}{" + _method.getName() + ":" + srcLine2 +"} " + e.getMessage());
                            //System.out.println(prev_frame);
                        }
                    }
                }
            
            /**
             * Mod ends here
             */

            
            
			boolean updated = false;
			for (int i = 0; i < annotations.length; i++) {       
				updated = annotations[i].update(currentFrame, currentHandle)
						|| updated;
			}



            //((FlowAnnotation)annotations[0]).printLinkValues();
            

//             if ( false )
//             {
//                 System.out.println("Checking registered flows");
                
//                 FlowPartialSignature ps = (FlowPartialSignature)annotations[0].getPartialSignature();
//                 FlowPartialSignatureData d = (FlowPartialSignatureData)ps.getComponent();
//                 TableLink links = d.getData();
//                 for(int i=0; i<links.getSizeL(); i++)
//                     for(int j=0; j<links.getSizeC(); j++)
//                     {
//                         DefaultLink l = (DefaultLink)links.get(i, j);
//                         if ( l != null )
//                         {
//                             Flow f = new Flow(_class, _method, j, i, l.getLink());
//                             try {
//                                 flowchecker.check(f);
//                             } catch(FlowCheckerException e) {
//                                 System.out.println("[E]{" + _class.getClassName() + "}{" + _method.getName() + ":" + srcLine +"} " + e.getMessage());
//                             }
//                         }
//                     }
//             }
            
            
			interpreter.abstractExecutionStep(currentHandle, currentFrame);


            
//			if(this._method.getName().equals("processGetLastTreatment")){
//				Printer.debugPrintln(""+currentHandle);
//				Printer.debugPrintln(""+currentFrame);
//				currentFrame.printLinkValues();
//			}


			/**
			 * process exceptions
			 */
			Iterator<InstructionHandle> it;
			ArrayList<InstructionHandle> list = interpreter.getNextExceptionHandlers(currentHandle);
			if (list.size() > 0) {
				Frame ex = (Frame) currentFrame.clone();
				ex.getStack().clear();
				ex.getStack().push(ex.getException());
				//ex.makePointTo(ex.getStaticWorld(),ex.getException());
				it = list.iterator();
				while (it.hasNext()) {
					InstructionHandle next = it.next();
					boolean modif = this.mergeFrameAtLabel(next.getPosition(),
							ex);
					if ((updated || modif) && !control.contains(next)) {
						control.push(next);
					}
				}
			}
            
			/**
			 * process next instructions
			 */
			it = interpreter.getNextInstructions(currentHandle, currentFrame).iterator();
			while (it.hasNext()) {
                
				InstructionHandle next = it.next();

				boolean modif = this.mergeFrameAtLabel(next.getPosition(),
						currentFrame);

				if ((updated || modif) && !control.contains(next)) {
					control.push(next);
				}
			}
            
		}

		if (Config.statisticsEnabled()) {
			Stats.stats(this);
			String st = Stats.statsToString(this);
			if (!st.equals("")){
				//Stats.println(st);
			}
		}

		Signature sign = new Signature();
		boolean updated = false;
		for (int i = 0; i < annotations.length; i++) {
			if (annotations[i].getPartialSignature() != null) {
				sign.add(annotations[i].getPartialSignature());
                //System.out.println(">>" + annotations[i] + "<<");
                updated = true;
			}
		}
		if (updated) {
            //System.out.println("coin : " + sign);
            
			String key = SignatureDictionary.key(_class, _method);
			dictionary.putSignature(key, sign, interpreter.isFinalSignature());
		}


	}

	/**
	 * Computes the proof annotation to be embedded with the code , in order to ease the online verification.
	 * The proof associates to each label bytecode its corresponding frame.
	 *
	 * format
	 * 		codification length_of_jvmType_tablearray_of_proofs_length 	array_of_proofs
	 *
	 * array_of_proof contains elements of form:
	 * 		label size_of_proof(in bytes)	proof
	 *
	 * 	where proof is the codification of a frame
	 *
	 * The labels are order, to facilitate the oncard algorithm
	 * @return
	 * 		The proof annotation to be embedded with the code , in order to ease the online verification
	 */
	public byte[] getProof() {
		byte[] output = null;

		//no proof if there are no labels
/*		if (labels.size() == 0)
			return null;
*/
		int length = 0;
		Frame fr;
		Vector<Frame> v;
		Integer key;

		byte codification = this.getProofCodification();
		//add length at the begining?

		//compute length
		length += 1;
		length += SignatureConstants.LABEL_BYTECODE_SIZE;
		length += SignatureConstants.LABEL_BYTECODE_SIZE;
		Iterator<Integer> keys = labels.keySet().iterator();
		Frame tmp = null;
		for (; keys.hasNext();) {
			key = keys.next();
			v = labels.get(key);
			length += SignatureConstants.LABEL_BYTECODE_SIZE;
			if (v.size() > 0) {
				fr = v.elementAt(0);
				byte[] arr = fr.toBytes(codification, tmp);
				length += arr.length;
				tmp = fr;
			}
			else {
				length += SignatureConstants.TOTAL_LENGTH_SIZE;
				tmp = null;
			}
		}

		//construct output
		output = new byte[length];
		int index = 0;
		output[index++] = codification;
		byte[] arrSize = SignatureConstants.toByteArray( this.interpreter.refValuesLength ,
				SignatureConstants.LABEL_BYTECODE_SIZE);
		System.arraycopy(arrSize, 0, output, index, arrSize.length);
		index += arrSize.length;
		arrSize = SignatureConstants.toByteArray(labels.size(),
				SignatureConstants.LABEL_BYTECODE_SIZE);
		System.arraycopy(arrSize, 0, output, index, arrSize.length);
		index += arrSize.length;
		keys = labels.keySet().iterator();

		tmp = null;
		for (; keys.hasNext();) {
			key = keys.next();
			v = labels.get(key);

				//set label
				arrSize = SignatureConstants.toByteArray(key.intValue(),
						SignatureConstants.LABEL_BYTECODE_SIZE);
				System.arraycopy(arrSize, 0, output, index, arrSize.length);
				index += arrSize.length;

				byte[] arr = null;
				if (v.size() > 0) {
					fr = v.elementAt(0);
					//compute frame
					arr = fr.toBytes(codification, tmp);
					tmp = fr;
				}
				else {
					arr = new byte[SignatureConstants.TOTAL_LENGTH_SIZE];
					tmp = null;
				}
				System.arraycopy(arr, 0, output, index, arr.length);
				index += arr.length;

			}
		return output;
	}

	/**
	 * Returns to codification to be used in order to codify the proof
	 * @return
	 *
	 */
	private byte getProofCodification() {
		int length = this.interpreter.getRefValues().length
				+ this.interpreter.getAddresses().length;
		if (length <= 63)
			return SignatureConstants.CODIF_6B;
		if (length <= 255)
			return SignatureConstants.CODIF_8B;
		if (length <= 16384)
			return SignatureConstants.CODIF_14B;
		return SignatureConstants.ERROR_CODIFICATION;
	}

	/**
	 *
	 * annotates the .class with the proof (the frame of each jump target)
	 *
	 */
	public void annotateProof() {

		byte[] byteStream = this.getProof();
		if (byteStream == null) {
			return;
		}

		Attribute[] orig = this._method.getAttributes();
		if (byteStream.length > 0) {
			ProofAttribute linkAttr = new ProofAttribute(proof_index,
					byteStream.length, byteStream, _class.getConstantPool());

			int j = 0;
			while (j < orig.length) {
				if (orig[j] instanceof ProofAttribute)
					break;
				j++;
			}
			if (j < orig.length) {
				orig[j] = linkAttr;
				_method.setAttributes(orig);
			} else {
				Attribute[] new_attr = new Attribute[orig.length + 1];
				new_attr[0] = linkAttr;
				System.arraycopy(orig, 0, new_attr, 1, orig.length);
				_method.setAttributes(new_attr);
			}
		} else {
			//suppress the attribute
			int j = 0;
			while (j < orig.length) {
				if (orig[j] instanceof ProofAttribute) {
					break;
				}
				j++;
			}
			if (j < orig.length) {
				Attribute[] new_attr = new Attribute[orig.length - 1];
				if (j > 0)
					System.arraycopy(orig, 0, new_attr, 0, j);
				if (j < orig.length - 1)
					System.arraycopy(orig, j + 1, new_attr, j, orig.length - j
							- 1);
				_method.setAttributes(new_attr);
			}
		}
	}


	public void addExternalMethod(InvokeInstruction i, int signType) {
		this.classAnalyser.addExternalMethod(i, signType);
	}

	public void addExternalField(FieldInstruction i) {
		this.classAnalyser.addExternalField(i);
	}
	////////////////////////////////////////////////////////////////
	//// toString
	////////////////////////////////////////////////////////////////

	/**
	 * @see java.lang.Object#toString()
	 */
	public String toString() {
		return "MethodAnalyser.toString() not yet implemented\n";
	}



	/////////////////////////////////////////////////////////////
	//IMPLICIT FLOW
	/////////////////////////////////////////////////////////////

	public void analyseImplicitFlow() {

		if (_method.isNative()) {
			System.err.println("Warning: " + _method + " is native");
			return;
		}

		Printer.println("Analyzing method " + _method);

		Stack<InstructionHandle> control = new Stack<InstructionHandle>();
		control.push(interpreterIF.getStart());

		this.implicitDependences.set(interpreterIF.getStart().getPosition(),
				new BooleanExpression(BooleanVariable.condition_true));

		InstructionHandle currentHandle = null;
		while (!control.isEmpty()) {
			currentHandle = control.pop();

			//Printer.println("pop from control stack : "+currentHandle);

			/*
			 ArrayList list = interpreterIF.getNextExceptionHandlers(currentHandle);
			 if (list.size() > 0) {
			 Frame ex = (Frame)currentFrame.clone();
			 ex.getStack().clear();
			 ex.getStack().push(ex.getException());

			 //ex.makePointTo(ex.getStaticWorld(),ex.getException());

			 it = list.iterator();
			 while (it.hasNext()) {
			 InstructionHandle next = (InstructionHandle) it.next();
			 boolean modif = this.mergeFrameAtLabel(next.getPosition(), ex);
			 if( (updated || modif) && !control.contains(next)){
			 //Printer.println("push exception "+next);
			 control.push(next);
			 }

			 }
			 }
			 */

			HashMap<InstructionHandle, BooleanExpression> succ = interpreterIF.getNextInstructions(currentHandle);
			Iterator<InstructionHandle> it = succ.keySet().iterator();
			while (it.hasNext()) {
				InstructionHandle next = it.next();
				BooleanExpression condition = succ
						.get(next);

				boolean modif = interpreterIF.abstractExecutionStep(
						currentHandle, next, condition);

				if (modif && !control.contains(next)) {
					control.push(next);
				}
			}
		}

		Printer.println(this.implicitDependences.toString());
	}


	public MethodInfo getMethodInfo() {
		return this.methodInfo;
	}

	public MethodInfoIF getMethodInfoIF() {
		return this.methodInfoIF;
	}

	public ImplicitDependences getImplicitDeps() {
		return this.implicitDependences;
	}

	////////////////////////////////////////
	//// IMPLICIT FLOW - END
	////////////////////////////////////////


	/**
	 * @param cpg The cpg to set.
	 */
	private void setCpg(ConstantPoolGen cpg) {
		this.cpg = cpg;
	}

	/**
	 * @return Returns the cpg.
	 */
	public ConstantPoolGen getCpg() {
		return cpg;
	}

	/**
	 * @param dictionary The dictionary to set.
	 */
	private void setDictionary(SignatureDictionary dictionary) {
		this.dictionary = dictionary;
	}

	/**
	 * @return the dictionary.
	 */
	public SignatureDictionary getDictionary() {
		return dictionary;
	}

	/**
	 * @return the policy
	 */
	public Policy getPolicy() {
		return policy;
	}

    /**
	 * @return the flow checker
	 */
	public FlowChecker getFlowChecker() {
		return flowchecker;
	}

	/**
	 *
	 * @return the bcel <code>Method</code> object
	 */
	public Method getMethod() {
		return _method;
	}

	/**
	 *
	 * @return the bcel <code>JavaClass</code> object associated to analyzed method
	 */
	public JavaClass getJavaClass() {
		return this._class;
	}

	/**
	 *
	 * @return the class name
	 */
	public String getClassName() {
		return _class.getClassName();
	}

	/**
	 *
	 * @return the annotations of the method
	 */
	public Annotation[] getAnnotations(){
		return this.annotations;
	}

}