/*
 * Copyright 2007 Wishnu Prasetya.
 *
 * This file is part of T2.
 * T2 is free software; you can redistribute it and/or modify it under
 * the terms of the GNU General Public License (GPL) as published by the
 * Free Software Foundation; either version 3 of the License, or any
 * later version.
 *
 * T2 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 General Public License
 * for more details.
 *
 * A copy of the GNU General Public License can be found in T2 distribution.
 * If it is missing, see http://www.gnu.org/licenses.
 */

package Sequenic.T2.Seq;

import Sequenic.T2.Obj.*;
import Sequenic.T2.Msg.*;
import java.io.*;
import java.util.*;
import java.lang.reflect.*;

/**
 * An object of this class is a description used to hold information about a
 * test step (what the step is, what the actual concrete parameters passed to
 * it) and the result of executing the step. By 'result' we mean the object
 * returned by the step, along with information about exception or violation
 * thrown by the step.
 * 
 * <p>
 * A "test-step" is basically an instance of "METARUN", though most of the time
 * it is an instance of TraceStep. The exception is the step that first creates
 * a target-object, which is a MkValStep.
 */
public class ExecResult {

	/**
	 * The (meta) step that produces this result.
	 */
	public METARUN step = null;

	public Class CUT = null;

	/**
	 * The target object associated to the step producing this result.
	 */
	public Object targetObj = null;

	/**
	 * Actual and concrete parameters passed to the step producing this result.
	 */
	public Object[] args = null;

	/**
	 * Actual receiver object of the step producing this result. Null if such
	 * the step has no receiver object.
	 */
	public Object receiverObj = null;

	public Object returnedObj = null;

	/**
	 * Exception thrown but expected.
	 */
	public Exception returnedException = null;

	/**
	 * Violation to an assertion marked as a pre-condition (with the marker
	 * "PRE").
	 */
	public AssertionError precViolation = null;

	/**
	 * This is to indicate that the expressions that build up the arguments to a
	 * field update, or constructor or method call throws an exception.
	 */
	public Throwable argumentFailure = null;

	/**
	 * The step producing this results may fail because it calls a constructor
	 * of CUT, and this constructor fails. The failing call is then recorded in
	 * this field.
	 */
	public CREATE_OBJECT CUT_constructor_failure = null;

	/**
	 * Violation to an assertion not marked as a pre-condition.
	 */
	public AssertionError postcViolation = null;

	/**
	 * Internal error or unexpected runtime exception thrown.
	 */
	public Throwable internalError = null;

	/**
	 * Violation to an assertion marked to be part of an application model.
	 */
	public AssertionError appmodViolation = null;

	/**
	 * A class invariant throws an exception. This is considered as a violation.
	 *
	 */
	public Throwable classinvExecptionalViolation = null;

	/**
	 * True when a class invariant is violated.
	 */
	public boolean classinvViolation = false;

	/**
	 * True when the stop is suspected as diverging (non-terminating).
	 */
	public boolean possiblyDiverging = false;
	
	
	public ExecResult() {
		super();
	}

	public ExecResult(Class C, METARUN st, Object target) {
		CUT = C;
		step = st;
		targetObj = target;
	}

	/**
	 * Return true if the result indicates a violation to either pre-cond or
	 * app. model.
	 */
	public boolean isAsmViolating() {
		return isAsmOrReqViolating() && !isReqViolating();
	}

	/**
	 * Return true if the result indicates a violation to either post-cond or
	 * classinv.
	 */
	public boolean isReqViolating() {
		return classinvViolation || (postcViolation != null)
				|| (internalError != null)
				|| (classinvExecptionalViolation != null) || possiblyDiverging;
	}

	/**
	 * True if either isAsmViolating or isReqViolating.
	 */
	public boolean isAsmOrReqViolating() {
		return (precViolation != null) || (appmodViolation != null)
				|| (argumentFailure != null) || isReqViolating();
	}

	/**
	 * When given a Throwable thrown when executing a test step, this method
	 * categorizes the kind of violation it is.
	 */
	public void checkException(InvocationTargetException e) {
		
		Throwable exc = e.getCause();

		if (argumentFailure != null) return ;
		
		if (e instanceof CUT_Constructor_failure) {
			CUT_constructor_failure = ((CUT_Constructor_failure) e).step;
		}
		// System.out.println(">>> " + exc.getMessage()) ;
		// Then classify the violation:
		if (! isERR(exc) ) {
			returnedException = (Exception) exc;
			return ;
		}
		// Else isERR true:
		if (exc instanceof ThreadDeath) {
			possiblyDiverging = true ;
			return ;
		}
		if (!(exc instanceof AssertionError)) {
			internalError = exc ;
			return ;
		}
		// Ok, else it is an AssertionError:
		AssertionError assErr = (AssertionError) exc ;
		if (! isASM(exc)) {
				postcViolation = assErr ;
				return ;
		}
		// Else then isASM must be true:
		if (step instanceof CALL_METHOD) {
			CALL_METHOD m = (CALL_METHOD) step ;
			if (causedBy(exc,m.method) || causedBySuperClass(exc,m.method)) {
				precViolation = assErr ;
				return ;
			}
			postcViolation = assErr ;
			return ;
		}
		if (step instanceof CREATE_OBJECT) {
			CREATE_OBJECT c = (CREATE_OBJECT) step ;
			if (causedBy(exc,c.con) || causedBySuperClass(exc,c.con)) {
				precViolation = assErr ;
				return ;
			}
			// System.out.println(">>> x") ;
			postcViolation = assErr ;
			return ;
		}
		
		/*
		if (exc instanceof AssertionError) {

			if (!(step instanceof CALL_METHOD)) {
				// If the step is not a method call, then it always counts as
				// pre-condition violation:
				precViolation = (AssertionError) exc;

			} else {
				
				CALL_METHOD m = (CALL_METHOD) step;
				
				AssertionError assErr = (AssertionError) exc;
				// to hold the method that causes the assertion error:
				StackTraceElement vilain = null;
				StackTraceElement[] stacktrace = assErr.getStackTrace();
				if (stacktrace != null && stacktrace.length > 0)
					vilain = stacktrace[0];

				if (! vilainMatch(vilain,m)) internalError = exc ;
				
				else if (assErr.getMessage() != null
						&& assErr.getMessage().startsWith("PRE")) {
					precViolation = assErr;
				} else {
					postcViolation = assErr;
				}
			}
		} else if (exc instanceof Error || exc instanceof RuntimeException) {
			internalError = exc;
			if (exc instanceof ThreadDeath)
				possiblyDiverging = true;
		} else {
			// else it is considered an expected exception:
			returnedException = (Exception) exc;
		}
		*/
	}

	/**
	 * Check/execute the given class-invariants; record violation in this
	 * ExecResult object.
	 */
	public void execClassInv(List<Method> classInvariants, Object targetObj) {

		classinvViolation = false;

		if (classInvariants == null || classInvariants.isEmpty()) {
			return;
		}
		Class D = null;

		for (Method classinv : classInvariants) {

			classinv.setAccessible(true);

			try {
				D = classinv.getDeclaringClass();
				classinvViolation = !(Boolean) (classinv.invoke(D
						.cast(targetObj), (Object[]) null));
				// System.out.println("##" + D.getName() + " : " +
				// result.classinvViolation) ;
			}

			catch (InvocationTargetException e) {

				Throwable c = e.getCause();

				// Possible non-termination in classinv:
				if (c instanceof ThreadDeath) {
					possiblyDiverging = true;
					break;
				}

				if (isASM(c)) {
						appmodViolation = (AssertionError) c ;
						break ;
					} 
				// Else it is considered as a violation:
				// classinvViolation = true ;
				classinvExecptionalViolation =  c;
				break ;
				
			} catch (Exception e) {
				throw new T2Error("Fail to invoke the classinvariant.");
			}
			if (classinvViolation) {
				break;
			}
		}
	}
	
	static public boolean isERR(Throwable e){ 
		return (e instanceof Error) || (e instanceof RuntimeException) ; 
		}
	
	static public boolean isPRE(Throwable e){
		if (!(e instanceof AssertionError)) return false ;
		if (e.getMessage() != null
				&& e.getMessage().startsWith("PRE")) return true ;
		return false ;
	}
	
	static public boolean isAPPM(Throwable e){
		if (!(e instanceof AssertionError)) return false ;
		if (e.getMessage() != null
				&& e.getMessage().startsWith("APPMODEL")) return true ;
		return false ;
	}
	
	static public boolean isASM(Throwable e){
		return isPRE(e) || isAPPM(e) ;
	}
	
	static public StackTraceElement source(Throwable e){
		StackTraceElement vilain = null;
		StackTraceElement[] stacktrace = e.getStackTrace();
		if (stacktrace != null && stacktrace.length > 0)
			vilain = stacktrace[0];
		return vilain ;
	}
	
	/**
	 * True if the root cause of e is the method m.
	 */
	static public boolean causedBy(Throwable e,Method m ) {
		
		StackTraceElement vilain = source(e) ;
		if (vilain==null) return false ;
		
		String method_declaring_class = m.getDeclaringClass().getName();
		
		if (! vilain.getClassName().equals(method_declaring_class))
			return false ;
		
		String method_name = m.getName();
		boolean is_spec = method_name.endsWith(Sequenic.T2.Engines.BaseEngine.SPEC_STR) ;
		
		if (! is_spec) return vilain.getMethodName().equals(method_name) ;
		
		String method_name_org = method_name.substring(0, method_name.length() - Sequenic.T2.Engines.BaseEngine.SPEC_STR.length()) ;

		return 	vilain.getMethodName().equals(method_name)
				||
				vilain.getMethodName().equals(method_name_org) ;
		
	}
	
	/**
	 * Check if the exception e is thrown by a superclass of the class
	 * that declares m.
	 */
	static public boolean causedBySuperClass(Throwable e,Method m ) {
		StackTraceElement vilain = source(e) ;
		if (vilain==null) return false ;
		
		Class method_declaring_class = m.getDeclaringClass() ;
		Class vilain_class = null ;
		try {
			vilain_class = Class.forName(vilain.getClassName()) ;
		}
		catch (Exception f) { 
			throw new T2Error(T2Error.BUG,f) ;
		}
		return vilain_class.isAssignableFrom(method_declaring_class) ;
	}
	
	/**
	 * True if the root cause of e is the constructor c.
	 */
	static public boolean causedBy(Throwable e,Constructor c ) {
		
		StackTraceElement vilain = source(e) ;
		if (vilain==null) return false ;
		
		String declaring_class = c.getDeclaringClass().getName();
		
		if (! vilain.getClassName().equals(declaring_class))
			return false ;
		
		String cons_name = c.getName();
		
		return 	vilain.getMethodName().equals("<init>") ;
	}
	
	/**
	 * Check if the exception e is thrown by a superclass of c.
	 */
	static public boolean causedBySuperClass(Throwable e,Constructor c ) {
		StackTraceElement vilain = source(e) ;
		if (vilain==null) return false ;
		
		Class method_declaring_class = c.getDeclaringClass() ;
		Class vilain_class = null ;
		try {
			vilain_class = Class.forName(vilain.getClassName()) ;
		}
		catch (Exception f) { 
			throw new T2Error(T2Error.BUG,f) ;
		}
		return vilain_class.isAssignableFrom(method_declaring_class) ;
	}
}