/**
  *
  *                      OOAS Compiler
  *
  *       Copyright 2015, AIT Austrian Institute of Technology.
  * This code is based on the C# Version of the OOAS Compiler, which is
  * copyright 2015 by the Institute of Software Technology, Graz University
  * of Technology with portions copyright by the AIT Austrian Institute of
  * Technology. All rights reserved.
  *
  * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED.
  *
  * If you modify the file please update the list of contributors below to in-
  * clude your name. Please also stick to the coding convention of using TABs
  * to do the basic (block-level) indentation and spaces for anything after
  * that. (Enable the display of special chars and it should be pretty obvious
  * what this means.) Also, remove all trailing whitespace.
  *
  * Contributors:
  *               Willibald Krenn (AIT)
  *               Stephan Zimmerer (AIT)
  *               Markus Demetz (AIT)
  *               Christoph Czurda (AIT)
  *
  */


package org.momut.ooas.visitors;

import java.util.LinkedList;

import org.momut.ooas.ast.expressions.Expression;
import org.momut.ooas.ast.identifiers.FunctionIdentifier;
import org.momut.ooas.ast.identifiers.Identifier;
import org.momut.ooas.ast.identifiers.IdentifierKind;
import org.momut.ooas.ast.identifiers.MethodIdentifier;
import org.momut.ooas.ast.identifiers.NamedActionIdentifier;
import org.momut.ooas.ast.statements.Assignment;
import org.momut.ooas.ast.statements.Block;
import org.momut.ooas.ast.statements.Call;
import org.momut.ooas.ast.statements.Statement;
import org.momut.ooas.ast.statements.StatementKind;
import org.momut.ooas.ast.types.FunctionType;
import org.momut.ooas.ast.types.OoActionSystemType;
import org.momut.ooas.ast.types.FunctionType.FunctionTypeEnum;
import org.momut.ooas.parser.ParserMessage;
import org.momut.ooas.parser.ParserState;
import org.momut.ooas.utils.exceptions.NotImplementedException;

/// <summary>
/// This visitor scans all methods and named actions in order to check
/// whether they are safe, in the sense that they are only using
/// basic commands that obey the excluded miracle rule automatically.
///
/// The idea is that the weakest precondition of "safe named actions"
/// automatically is the guard of the obligatorty guarded command.
///
/// Allowed commands for "safe" code:
///    -> Assignment (deterministic!)
///    -> Sequential Composition
/// Currently not supported within the analysis:
///    -> Conditional Statement (emulated by requires A: end [] requires not A: end)
///    -> Iteration (not available)
/// </summary>
public final class OoaActionClassifierVisitor extends OoaCompleteAstTraversalVisitor
{
	private static final class RefWorkAround {
		boolean m_hasUnsafeElement;
		Statement ablock;
		public RefWorkAround(boolean ue, Statement b) {
			m_hasUnsafeElement = ue;
			ablock = b;
		}
	}

	private boolean getValue(Boolean input, boolean defaultValue) {
		return input == null ? defaultValue: input;
	}


	@SuppressWarnings("serial")
	private void CalcBodySafe(FunctionIdentifier methodIdentifier, FunctionType mType, final RefWorkAround w)
	{
		String methodAction;
		if (mType.functionType() == FunctionTypeEnum.Method)
			methodAction = "Method";
		else
			methodAction = "Action";


		while ((w.ablock != null) && (w.ablock.kind() == StatementKind.PrioBlock || w.ablock.kind() == StatementKind.NondetBlock))
		{
			final Block block = (Block) w.ablock;
			if (block.statements().size() == 0)
				break;

			if (block.statements().size() > 1)
			{
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: More than one element in Nondet/Prio Block.",
										methodAction, methodIdentifier.tokenText())));
				mType.SetMiracleSafe(false);
			}
			w.ablock = block.statements().peekFirst();
		}

		final LinkedList<Statement> stmts = w.ablock.kind() == StatementKind.SeqBlock ? ((Block) w.ablock).statements() : new LinkedList<Statement>(){{add(w.ablock);}};
		for (final Statement s: stmts)
		{
			switch (s.kind())
			{
			case Abort:
				// abort maps any postcondition to false, iow. wp(abort,X) = false
				w.m_hasUnsafeElement = true; // excluded miracle holds, but I'm not sure about continuity.. *g*
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: Abort detected.",
										methodAction, methodIdentifier.tokenText())));
				break;
			case Assignment:
				final Assignment ass = (Assignment)s;
				w.m_hasUnsafeElement |= ass.nondetExpression() != null;
				if (w.m_hasUnsafeElement)
					m_ParserState.AddMessage(
							new ParserMessage(m_ParserState.filename, w.ablock.line(),
									w.ablock.pos(), String.format("%s %s extended: possibly nondeterministic assignment.",
											methodAction, methodIdentifier.tokenText())));
				// check value expressions
				for (final Expression x: ass.values())
				{
					if (x.GetUninitializedFreeVariables().size() > 0)
					{
						w.m_hasUnsafeElement = true;
						m_ParserState.AddMessage(
								new ParserMessage(m_ParserState.filename, w.ablock.line(),
										w.ablock.pos(), String.format("%s %s extended: uninitialized free variables in expression.",
												methodAction, methodIdentifier.tokenText())));
						continue;
					}
					for (final FunctionIdentifier ct: x.callTargets())
					{
						if ( ((FunctionType)ct.type()).isMiracleSafe() == null)
							ct.Accept(this);
						w.m_hasUnsafeElement |= getValue(((FunctionType)ct.type()).isMiracleSafe(), true);
						if (w.m_hasUnsafeElement)
							m_ParserState.AddMessage(
									new ParserMessage(m_ParserState.filename, w.ablock.line(),
											w.ablock.pos(), String.format("%s %s extended: call of extended method in value expression.",
													methodAction, methodIdentifier.tokenText())));
					}
				}
				break;
			case GuardedCommand:
				w.m_hasUnsafeElement = true; // we do not allow guarded commands in methods as they would be included in actions!
				// we do not allow a second guarded command in named actions.
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: guarded command detected.",
										methodAction, methodIdentifier.tokenText())));
				break;
			case Kill:
				w.m_hasUnsafeElement = true;
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: Kill detected.",
										methodAction, methodIdentifier.tokenText())));
				break;
			case MethodCall:
				final Call acall = (Call)s;

				for (final FunctionIdentifier anid: acall.callExpression().callTargets())
				{
					final FunctionType atype = (FunctionType)anid.type();
					if (atype.isMiracleSafe() == null)
						atype.identifier().Accept(this);
					w.m_hasUnsafeElement |= getValue(atype.isMiracleSafe(), true);
					if (w.m_hasUnsafeElement)
						m_ParserState.AddMessage(
								new ParserMessage(m_ParserState.filename, w.ablock.line(),
										w.ablock.pos(), String.format("%s %s extended: calls extended method '%s'.",
												methodAction, methodIdentifier.tokenText(),anid.tokenText())));
				}
				break;
			case NondetBlock:
				w.m_hasUnsafeElement = true;
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: more than one nondet-block.",
										methodAction, methodIdentifier.tokenText())));
				break;
			case PrioBlock:
				w.m_hasUnsafeElement = true;
				m_ParserState.AddMessage(
						new ParserMessage(m_ParserState.filename, w.ablock.line(),
								w.ablock.pos(), String.format("%s %s extended: more than one prio block.",
										methodAction, methodIdentifier.tokenText())));
				break;
			case Skip:
			case Break:
				break;
			case SeqBlock:
				// seq block in seq block should not occur..
			default:
				throw new NotImplementedException();
			}
			if (w.m_hasUnsafeElement)
				break;
		}
	}


	@Override
	public void visit(MethodIdentifier methodIdentifier)
	{
		final FunctionType mType = (FunctionType)methodIdentifier.type();
		if (mType.isMiracleSafe() != null)
			return;

		// AST of method may have one prioritized block before the nondet block
		// both blocks must not have more than one element. (we do not implement conditional)
		final RefWorkAround w = new RefWorkAround(false, methodIdentifier.body());
		CalcBodySafe(methodIdentifier, mType, w);

		/*
        if (!m_hasUnsafeElement)
            m_ParserState.AddMessage(
                new ParserMessage(m_ParserState.filename, ablock.line,
                    ablock.pos, String.Format("Found basic method: '%s'",
                    methodIdentifier.tokenText)));
		 */

		mType.SetMiracleSafe(!w.m_hasUnsafeElement);
	}


	@Override
	public void visit(NamedActionIdentifier namedActionIdentifier)
	{
		final FunctionType mType = (FunctionType)namedActionIdentifier.type();
		if (mType.isMiracleSafe() != null)
			return;

		final RefWorkAround w = new RefWorkAround(false, namedActionIdentifier.body());

		CalcBodySafe(namedActionIdentifier, mType, w);
		/*
        if (!hasUnsafeElement)
            m_ParserState.AddMessage(
                new ParserMessage(m_ParserState.filename, ablock.line,
                    ablock.pos, String.Format("Found basic action: '%s'",
                    namedActionIdentifier.tokenText)));
		 */
		mType.SetMiracleSafe(!w.m_hasUnsafeElement);
	}

	@Override
	public void visit(OoActionSystemType ooActionSystemType)
	{
		super.visit(ooActionSystemType);
		boolean allsafe = true;
		for (final Identifier x: ooActionSystemType.symbols().symbolList())
		{
			if (x.kind() == IdentifierKind.MethodIdentifier
					|| x.kind() == IdentifierKind.NamedActionIdentifier)
			{
				allsafe &= getValue(((FunctionType)x.type()).isMiracleSafe(), false);
			}
		}
		if (allsafe)
			m_ParserState.AddMessage(
					new ParserMessage(m_ParserState.filename, ooActionSystemType.identifier().line(),
							ooActionSystemType.identifier().column(), String.format("Found action system with basic actions/methods only: '%s'",
									ooActionSystemType.identifier().tokenText())));
	}


	public OoaActionClassifierVisitor(ParserState aState)
	{
		super (aState);
	}
}