/*
 * 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 should not throw an exception. When it does then it
     * is because its encoding is not complete yet. We record exception
     * thrown by a class invariant here.
     */
    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) {
            // Check first for possible CUT constructor failure:
            if (e instanceof CUT_Constructor_failure) {
                CUT_constructor_failure = ((CUT_Constructor_failure) e).step ;
            }
            else return ;
        }
        // Then classify the violation:
        if (exc instanceof AssertionError) {
                AssertionError assErr = (AssertionError) exc;
                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 ;
                }  
                
                // Next, to handle application model, encoded as pre-cond of
                // class invariant, and possible assertion violation:
                if (c instanceof AssertionError) {
                    if (c.getMessage() != null && c.getMessage().startsWith("APPMODEL")) {
                        appmodViolation = (AssertionError) c;
                    } else {
                        //classinvViolation = true ;
                        classinvExecptionalViolation = (AssertionError) c;
                    }
                } else {
                    //classinvViolation = true ;
                    classinvExecptionalViolation = c;
                }
                break;
            } catch (Exception e) {
                throw new T2Error("Fail to invoke the classinvariant.");
            }
            if (classinvViolation) {
                break;
            }
        }
    }

}