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;

import org.momut.ooas.ast.AstNodeTypeEnum;

import org.momut.ooas.ast.IAst;

import org.momut.ooas.ast.expressions.AccessExpression;

import org.momut.ooas.ast.expressions.Expression;

import org.momut.ooas.ast.expressions.ExpressionKind;

import org.momut.ooas.ast.expressions.IdentifierExpression;

import org.momut.ooas.ast.expressions.TupleMapAccessExpression;

import org.momut.ooas.ast.expressions.UnaryOperator;

import org.momut.ooas.ast.identifiers.AttributeIdentifier;

import org.momut.ooas.ast.identifiers.ExpressionVariableIdentifier;

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.statements.Assignment;

import org.momut.ooas.ast.statements.Call;

import org.momut.ooas.ast.statements.GuardedCommand;

import org.momut.ooas.ast.statements.KillStatement;

import org.momut.ooas.ast.statements.QualitativeConstraintStatement;

import org.momut.ooas.ast.statements.Statement;

import org.momut.ooas.ast.types.FunctionType;

import org.momut.ooas.ast.types.TypeKind;

import org.momut.ooas.ast.types.UlyssesType;

import org.momut.ooas.parser.ParserError;

import org.momut.ooas.parser.ParserState;

import org.momut.ooas.parser.ParserWarning;

import org.momut.ooas.parser.SymbolTable;

import org.momut.ooas.utils.exceptions.ArgumentException;

import org.momut.ooas.utils.exceptions.NotImplementedException;

import org.momut.ooas.utils.exceptions.OoasCompilerRuntimeException;

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

        }

}