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.ArrayList;

import java.util.ListIterator;

/// <summary>

/// Requires: ResolveExpressionVisitor and MethodPureClassifierVisitor

///

/// Does the typechecking of statements and initializers.

/// Needs resolved expressions, hence a run of ResolveVisitor first.

/// </summary>

public final class OoaTypeCheckVisitor extends OoaCompleteAstTraversalVisitor

{

	/// <summary>

	/// internal; used to count occurrences of attribute access in an expression

	/// </summary>

	private static final class OoaInitializerCheck extends OoaExpressionVisitor

	{

		ArrayList<Identifier> attributeAccess = new ArrayList<Identifier>();

		@Override

		public void visit(IdentifierExpression identifierExpression)

		{

			final Identifier id = identifierExpression.identifier();

			if (id.kind() == IdentifierKind.AttributeIdentifier)

				attributeAccess.add(id);

			super.visit(identifierExpression);

		}

	}

	private void Error(Statement statement, String p)

	{

		final ParserError error = new ParserError(m_ParserState.filename,

				statement.line(), statement.pos(), p);

		m_ParserState.AddErrorMessage(error);

	}

	private void Error(Identifier id, String p)

	{

		final ParserError error = new ParserError(m_ParserState.filename,

				id.line(), id.column(), p);

		m_ParserState.AddErrorMessage(error);

	}

	private void Warning(Statement aStatement, String p)

	{

		final ParserWarning warn = new ParserWarning(m_ParserState.filename,

				aStatement.line(), aStatement.pos(), p);

		m_ParserState.AddWarningMessage(warn);

	}

	private void Warning(Identifier aStatement, String p)

	{

		final ParserWarning warn = new ParserWarning(m_ParserState.filename,

				aStatement.line(), aStatement.column(), p);

		m_ParserState.AddWarningMessage(warn);

	}

	private void RemoveWarning(Identifier expression, String p)

	{

		final ArrayList<ParserWarning> toRemove = new ArrayList<ParserWarning>();

		for (final ParserWarning x: m_ParserState.listOfParserWarnings)

		{

			if (p.equals(x.message()) && x.line() == expression.line() && x.column() == expression.column())

				toRemove.add(x);

		}

		for (final ParserWarning x: toRemove)

			m_ParserState.listOfParserWarnings.remove(x);

	}

	private void TypeCheckGuardedCommand(GuardedCommand gc)

	{

		if (gc.guard().type() == null ||

				gc.guard().type().kind() != TypeKind.BoolType)

			Error(gc, "Guard needs to be boolean expression");

		final ArrayList<ExpressionVariableIdentifier> uninitfree = gc.guard().GetUninitializedFreeVariables();

		if (uninitfree.size() > 0)

			Error(gc, String.format("Undefined variable: '%s'", uninitfree.get(0).tokenText()));

		CheckMethodCallsArePure(gc.guard());

		gc.body().Accept(this);

	}

	private void CheckMethodCallsArePure(Expression expression)

	{

		for (final FunctionIdentifier method: expression.callTargets())

		{

			if (!((FunctionType)method.type()).isPureFunction())

				Error(method, String.format("Method '%s' needs to be pure: No change of state allowed.", method.tokenText()));

		}

	}

	private void TypeCheckAssignment(Assignment assignment)

	{

		SymbolTable freevars = new SymbolTable();

		if (assignment.nondetExpression() != null)

		{

			CheckMethodCallsArePure(assignment.nondetExpression());

			if (assignment.nondetExpression().freeVariables() != null

					&& assignment.nondetExpression().freeVariables().symbolList().size() > 0)

			{

				// expression has free variables we need to match with right-hand-side of assignment.

				freevars = assignment.nondetExpression().freeVariables();

				for (final Expression aRhsExpr: assignment.values())

				{

					if (aRhsExpr.freeVariables() != null)

						for (final Identifier freeRhsVar: aRhsExpr.freeVariables().symbolList())

						{

							if (freevars.Defined(freeRhsVar.tokenText()))

							{

								final Identifier exprvar = freevars.Get(freeRhsVar.tokenText());

								if (freeRhsVar.type().kind() == TypeKind.Any)

								{

									freeRhsVar.SetType(exprvar.type());

									assignment.AddIdentifier(exprvar, null);

									// remove free variable warnings

									RemoveWarning(exprvar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));

									RemoveWarning(freeRhsVar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));

								}

								else if (UlyssesType.TypeEqual(freeRhsVar.type(), exprvar.type()))

								{

									assignment.AddIdentifier(exprvar, null);

									// remove free variable warnings

									RemoveWarning(exprvar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));

									RemoveWarning(freeRhsVar, String.format("Free variable in expression: '%s'.", exprvar.tokenText()));

								}

								else

									Error(assignment, String.format("Type mismatch on variable %s: %s <> %s", freeRhsVar.tokenText(), freeRhsVar.type().toString(), exprvar.type().toString()));

							}

							else

								Error(assignment, String.format("Undefined variable '%s'", freeRhsVar.tokenText()));

						}

				}

			}

		}

		for (final Identifier avar: freevars.symbolList())

			if (!assignment.symbols().Defined(avar.tokenText()))

				Error(assignment, String.format("Undefined variable '%s'", avar.tokenText()));

		if (assignment.places().size() != assignment.values().size())

		{

			Error(assignment, "Number of places does not match number of values in assignment.");

			//return;

		}

		final ListIterator<Expression> aplaceIt = assignment.places().listIterator();

		final ListIterator<Expression> avalueIt = assignment.values().listIterator();

		while (aplaceIt.hasNext() && avalueIt.hasNext())

		{

			final Expression aplace = aplaceIt.next();

			Expression avalue = avalueIt.next();

			CheckPlace(aplace, assignment);

			// we allow non-pure methods only for assignments of the form 'variable := function(x,y)'

			if (avalue.kind() != ExpressionKind.Call)

				CheckMethodCallsArePure(avalue);

			final UlyssesType acover = UlyssesType.CoverType(aplace.type(), avalue.type());

			if (acover == null)

				Error(assignment, String.format("Type mismatch in assignment: %s ( %s := %s )", aplace.toString(), aplace.type().toString(), avalue.type().toString()));

			else if (!UlyssesType.TypeEqualByKind(aplace.type(), acover)) /*ignore range things.. (see warning below)*/

				Error(assignment, String.format("Type mismatch in assignment: %s ( %s := %s )", aplace.toString(), aplace.type().toString(), acover.toString()));

			else

			{

				final ArrayList<ExpressionVariableIdentifier> uninitvars = avalue.GetUninitializedFreeVariables();

				final Expression constantvalue = avalue.kind() == ExpressionKind.Value ? avalue : null;

				if (uninitvars.size() > 0)

					Error(assignment, String.format("Undefined variable '%s'", uninitvars.get(0).tokenText()));

				if (!UlyssesType.TypeEqual(avalue.type(), acover))

				{

					final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue, avalue.line(), avalue.pos());

					cast.SetType(acover);

					avalueIt.remove();

					avalueIt.add(cast);

					avalue = avalueIt.previous();

					if (avalue != cast)

						throw new OoasCompilerRuntimeException();

				}

				if (UlyssesType.FirstTypeLessRange(aplace.type(), acover))

				{

					if (constantvalue == null)

					{

						Warning(assignment, String.format("Assignment may over/underflow: %s := %s", aplace.type().toString(), acover.toString()));

						final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, avalue, avalue.line(), avalue.pos());

						cast.SetType(aplace.type());

						avalueIt.remove();

						avalueIt.add(cast);

						avalue = avalueIt.previous();

						if (avalue != cast)

							throw new OoasCompilerRuntimeException();

					}

					else

					{

						Error(assignment, String.format("Assignment out of range (%s  := %s)", aplace.toString(), constantvalue.toString()));

					}

				}

			}

		}

	}

	/// <summary>

	/// Checks whether the LHS-expression of an assignment is a valid place.

	/// IMPORTANT: If more complicated LHS expressions are allowed, then

	///            ooaPrologExpression.cs needs to be adapted too!

	/// </summary>

	private void CheckPlace(Expression expression, Assignment assignment)

	{

		// check that we have some LHS of following forms

		// self.<var/attr>

		// attr[..]

		boolean result = true;

		// one array/map access allowed

		if (expression.kind() == ExpressionKind.TupleMapAccess)

		{

			final TupleMapAccessExpression tAccessExpression = (TupleMapAccessExpression)expression;

			expression = tAccessExpression.child();

		}

		// attributes feature a self ref

		if (expression.kind() == ExpressionKind.Access)

		{

			final AccessExpression accessExpression = (AccessExpression)expression;

			if (accessExpression.left().kind() == ExpressionKind.Identifier && ((IdentifierExpression)accessExpression.left()).isSelf())

				expression = accessExpression.right();

			else

				result = false;

		}

		// now we need to have an identifier

		if (expression.kind() != ExpressionKind.Identifier)

			result = false;

		if (!result)

			Error(assignment, String.format("LHS of assignment must be variable or attribute."));

	}

	private void TypeCheckQualConstraint(QualitativeConstraintStatement qualConstr)

	{

		if (qualConstr.variable0().type().kind() != TypeKind.QrType && qualConstr.variable0().type().kind() != TypeKind.Any)

			Error(qualConstr, String.format("Qualitative type expected: '%s'", qualConstr.variable0().tokenText()));

		if (qualConstr.variable1().type().kind() != TypeKind.QrType && qualConstr.variable1().type().kind() != TypeKind.Any)

			Error(qualConstr, String.format("Qualitative type expected: '%s'", qualConstr.variable0().tokenText()));

		if (qualConstr.variable2() != null && qualConstr.variable2().type().kind() != TypeKind.QrType

				&& qualConstr.variable2().type().kind() != TypeKind.Any)

			Error(qualConstr, String.format("Qualitative type expected: '%s'", qualConstr.variable0().tokenText()));

	}

	private void TypeCheck(Statement statement)

	{

		switch (statement.kind())

		{

		case Abort:

		case Skip:

		case Break:

			break;

		case NondetBlock:

		case PrioBlock:

		case SeqBlock:

			statement.Accept(this);

			break;

		case Assignment:

			final Assignment assignment = (Assignment)statement;

			TypeCheckAssignment(assignment);

			break;

		case GuardedCommand:

			final GuardedCommand gc = (GuardedCommand)statement;

			TypeCheckGuardedCommand(gc);

			break;

		case Kill:

			final KillStatement kill = (KillStatement)statement;

			if (kill.someOne.type().kind() != TypeKind.OoActionSystemType)

				Error(kill, String.format(" %s not an object", kill.someOne.tokenText()));

			break;

		case MethodCall:

			final Call callstatement = (Call)statement;

			if (callstatement.callExpression().GetUninitializedFreeVariables().size() > 0)

				Error(callstatement, "Uninitialized free variables in call expression.");

			if (callstatement.callExpression().kind() != ExpressionKind.Call

					&& callstatement.callExpression().kind() != ExpressionKind.foldRL

					&& callstatement.callExpression().kind() != ExpressionKind.foldLR)

				Error(callstatement, "Not a valid method call");

			break;

		case QualConstraint:

			final QualitativeConstraintStatement qualConstr = (QualitativeConstraintStatement)statement;

			TypeCheckQualConstraint(qualConstr);

			break;

		default:

			throw new NotImplementedException();

		}

	}

	//private void TypeCheck()

	private void TypeCheck(AttributeIdentifier attributeIdentifier)

	{

		if (attributeIdentifier.initializer() == null)

			throw new ArgumentException();

		final UlyssesType atype = attributeIdentifier.initializer().type();

		if (atype == null)

			Error(attributeIdentifier, "Initializer lacks type.");

		else

		{

			/* we use the typecheck to validate a few more properties of the initializer that

			 * need a completely resolved expression

			 */

			final OoaInitializerCheck initCheck = new OoaInitializerCheck();

			attributeIdentifier.initializer().Accept(initCheck);

			if (initCheck.attributeAccess.size() > 0)

				// disallow use of other attributes in initializer

				Error(attributeIdentifier, "Access of other attributes not allowed in attribute initializer.");

			else if (attributeIdentifier.initializer().callTargets().size() > 0)

				// disallow method calls in initializer

				Error(attributeIdentifier, "Method calls not allowed in attribute initializer.");

			else if (attributeIdentifier.initializer().freeVariables().symbolList().size() > 0)

				// disallow use of free variables in initializer

				Error(attributeIdentifier,

						String.format("Unknown identifier in initializer: '%s'",

								attributeIdentifier.initializer().freeVariables().symbolList().get(0).tokenText()));

			else

			{

				final UlyssesType idtype = attributeIdentifier.type();

				final UlyssesType acover = UlyssesType.CoverType(idtype, atype);

				if (acover == null)

					Error(attributeIdentifier, String.format("Type mismatch in attribute initializer: %s ( %s := %s )", attributeIdentifier.toString(), idtype.toString(), atype.toString()));

				else if (!UlyssesType.TypeEqualByKind(idtype, acover)) /*ignore range things.. (see warning below)*/

					Error(attributeIdentifier, String.format("Type mismatch in attribute initializer: %s ( %s := %s )", attributeIdentifier.toString(), idtype.toString(), acover.toString()));

				else

				{

					final Expression constantvalue = attributeIdentifier.initializer().kind() == ExpressionKind.Value ? attributeIdentifier.initializer() : null;

					if (!UlyssesType.TypeEqual(atype, acover))

					{

						final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer(),

								attributeIdentifier.initializer().line(), attributeIdentifier.initializer().pos());

						cast.SetType(acover);

						attributeIdentifier.SetInitializer(cast);

					}

					if (UlyssesType.FirstTypeLessRange(idtype, acover))

					{

						if (constantvalue == null)

						{

							Warning(attributeIdentifier, String.format("Assignment may over/underflow: %s := %s", idtype.toString(), acover.toString()));

							final UnaryOperator cast = new UnaryOperator(ExpressionKind.Cast, attributeIdentifier.initializer(),

									attributeIdentifier.initializer().line(), attributeIdentifier.initializer().pos());

							cast.SetType(idtype);

							attributeIdentifier.SetInitializer(cast);

						}

						else

						{

							Error(attributeIdentifier, String.format("Initialization out of range (%s  := %s)", attributeIdentifier.toString(), constantvalue.toString()));

						}

					}

				}

				/*

                if (cover == null || !UlyssesType.TypeEqual(cover, idtype))

                    Error(attributeIdentifier,

                        String.Format("Type mismatch in attribute initializer: expected '%s', found '%s'",

                            idtype.ToString(), atype.ToString()));

                else

                    attributeIdentifier.SetInitializer(UnaryOperator.CoerceUp(attributeIdentifier.initializer, idtype));

				 * */

			}

		}

	}

	@Override

	protected void VisitAstElement(IAst element, IAst parent)

	{

		if (element.nodeType() == AstNodeTypeEnum.statement)

		{

			TypeCheck((Statement)element);

		}

		else if (element.nodeType() == AstNodeTypeEnum.identifier

				&& ((Identifier)element).kind() == IdentifierKind.AttributeIdentifier)

		{

			TypeCheck((AttributeIdentifier)element);

		}

		else super.VisitAstElement(element, parent);

	}

	public OoaTypeCheckVisitor(ParserState aState)

	{

		super (aState);

		if (aState == null)

			throw new ArgumentException();

	}

}