/** * * OOAS Compiler (Deprecated) * * Copyright 2015, Institute for Software Technology, Graz University of * Technology. Portions are copyright 2015 by the AIT Austrian Institute * of Technology. All rights reserved. * * SEE THE "LICENSE" FILE FOR THE TERMS UNDER WHICH THIS FILE IS PROVIDED. * * Please notice that this version of the OOAS compiler is considered de- * precated. Only the Java version is maintained. * * Contributors: * Willibald Krenn (TU Graz/AIT) * Stefan Tiran (TU Graz/AIT) */ using System; using System.Collections.Generic; using System.Text; namespace TUG.Mogentes { /// /// 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) /// public sealed class OoaActionClassifierVisitor : OoaCompleteAstTraversalVisitor { private void CalcBodySafe(FunctionIdentifier methodIdentifier, FunctionType mType, ref bool m_hasUnsafeElement, ref Block ablock) { string methodAction; if (mType.functionType == FunctionTypeEnum.Method) methodAction = "Method"; else methodAction = "Action"; while ((ablock != null) && (ablock.kind != StatementKind.SeqBlock) && (ablock.statements.Count > 0)) { if (ablock.statements.Count > 1) { m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: More than one element in Nondet/Prio Block.", methodAction, methodIdentifier.tokenText))); mType.SetMiracleSafe(false); } ablock = (Block)ablock.statements.First.Value; } foreach (var s in ablock.statements) { switch (s.kind) { case StatementKind.Abort: // abort maps any postcondition to false, iow. wp(abort,X) = false m_hasUnsafeElement = true; // excluded miracle holds, but I'm not sure about continuity.. *g* m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: Abort detected.", methodAction, methodIdentifier.tokenText))); break; case StatementKind.Assignment: Assignment ass = (Assignment)s; m_hasUnsafeElement |= ass.nondetExpression != null; if (m_hasUnsafeElement) m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: possibly nondeterministic assignment.", methodAction, methodIdentifier.tokenText))); // check value expressions foreach (var x in ass.values) { if (x.GetUninitializedFreeVariables().Count > 0) { m_hasUnsafeElement = true; m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: uninitialized free variables in expression.", methodAction, methodIdentifier.tokenText))); continue; } foreach (var ct in x.callTargets) { if ( ((FunctionType)ct.type).isMiracleSafe == null) ct.Accept(this); m_hasUnsafeElement |= ((FunctionType)ct.type).isMiracleSafe ?? true; if (m_hasUnsafeElement) m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: call of extended method in value expression.", methodAction, methodIdentifier.tokenText))); } } break; case StatementKind.GuardedCommand: 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, ablock.line, ablock.pos, String.Format("{0} {1} extended: guarded command detected.", methodAction, methodIdentifier.tokenText))); break; case StatementKind.Kill: m_hasUnsafeElement = true; m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: Kill detected.", methodAction, methodIdentifier.tokenText))); break; case StatementKind.MethodCall: Call acall = (Call)s; foreach (FunctionIdentifier anid in acall.callExpression.callTargets) { FunctionType atype = (FunctionType)anid.type; if (atype.isMiracleSafe == null) atype.identifier.Accept(this); m_hasUnsafeElement |= atype.isMiracleSafe ?? true; if (m_hasUnsafeElement) m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: calls extended method '{2}'.", methodAction, methodIdentifier.tokenText,anid.tokenText))); } break; case StatementKind.NondetBlock: m_hasUnsafeElement = true; m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: more than one nondet-block.", methodAction, methodIdentifier.tokenText))); break; case StatementKind.PrioBlock: m_hasUnsafeElement = true; m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("{0} {1} extended: more than one prio block.", methodAction, methodIdentifier.tokenText))); break; case StatementKind.Skip: break; case StatementKind.QualConstraint: m_hasUnsafeElement = true; break; case StatementKind.SeqBlock: // seq block in seq block should not occur.. default: throw new NotImplementedException(); } if (m_hasUnsafeElement) break; } } public override void visit(MethodIdentifier methodIdentifier) { 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) bool m_hasUnsafeElement = false; Block ablock = methodIdentifier.body; CalcBodySafe(methodIdentifier, mType, ref m_hasUnsafeElement, ref ablock); /* if (!m_hasUnsafeElement) m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("Found basic method: '{0}'", methodIdentifier.tokenText))); */ mType.SetMiracleSafe(!m_hasUnsafeElement); } public override void visit(NamedActionIdentifier namedActionIdentifier) { FunctionType mType = (FunctionType)namedActionIdentifier.type; if (mType.isMiracleSafe != null) return; // AST of namedaction starts with a seq block with only one guarded command.. Block seqb = namedActionIdentifier.body; System.Diagnostics.Debug.Assert(seqb.statements.Count == 1); System.Diagnostics.Debug.Assert(seqb.statements.First.Value.kind == StatementKind.GuardedCommand); GuardedCommand gc = (GuardedCommand)seqb.statements.First.Value; Block ablock = gc.body; bool hasUnsafeElement = false; CalcBodySafe(namedActionIdentifier, mType, ref hasUnsafeElement, ref ablock); /* if (!hasUnsafeElement) m_ParserState.AddMessage( new ParserMessage(m_ParserState.filename, ablock.line, ablock.pos, String.Format("Found basic action: '{0}'", namedActionIdentifier.tokenText))); */ mType.SetMiracleSafe(!hasUnsafeElement); } public override void visit(OoActionSystemType ooActionSystemType) { base.visit(ooActionSystemType); bool allsafe = true; foreach (var x in ooActionSystemType.symbols.symbolList) { if (x.kind == IdentifierKind.MethodIdentifier || x.kind == IdentifierKind.NamedActionIdentifier) { allsafe &= ((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: '{0}'", ooActionSystemType.identifier.tokenText))); } public OoaActionClassifierVisitor(ParserState aState) : base(aState) { } } }