OoasTools

/**

  *

  *                      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;

/// <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 QualConstraint:

				w.m_hasUnsafeElement = true;

				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);

	}

}