pslTree.py 86.6 KB
Newer Older
1
"""
2 3 4
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Joy Mitra's avatar
Joy Mitra committed
5
Redistribution and use in source and binary forms, with or without modification,
6
are permitted provided that the following conditions are met:
Joy Mitra's avatar
Joy Mitra committed
7
* Redistributions of source code must retain the above copyright notice,
8
this list of conditions and the following disclaimer.
Joy Mitra's avatar
Joy Mitra committed
9 10
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
11
and/or other materials provided with the distribution.
Joy Mitra's avatar
Joy Mitra committed
12 13
* Neither the name of the University of Illinois nor the names of its contributors
may be used to endorse or promote products derived from this software without
14
specific prior written permission.
Joy Mitra's avatar
Joy Mitra committed
15 16 17 18 19
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO,
THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
20
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
Joy Mitra's avatar
Joy Mitra committed
21 22
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
23 24 25
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
-----------------------------------------------------------------------------------------------------------
Joy Mitra's avatar
Joy Mitra committed
26 27 28
Copyright (c) 2015. To the extent that a federal employee is an author of
a portion of the software or a derivative work thereof, no copyright is
claimed by the United States Government, as represented by the Secretary
29
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Joy Mitra's avatar
Joy Mitra committed
30 31 32 33
Permission to use, copy, and modify this software and its documentation is
hereby granted, provided that both the copyright notice and this permission
notice appear in all copies of the software, derivative works or modified
versions, and any portions thereof, and that both notices appear in
34
supporting documentation.
Joy Mitra's avatar
Joy Mitra committed
35 36
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
37
FROM THE USE OF THIS SOFTWARE.
Joy Mitra's avatar
Joy Mitra committed
38 39
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
40 41 42 43 44 45 46
maudenpa@chacs.nrl.navy.mil]
-or-
Naval Research Laboratory, Code 5543
4555 Overlook Avenue, SW
Washington, DC 20375
"""
"""
Joy Mitra's avatar
Joy Mitra committed
47
Important: To simplify implementation, the parser assumes that the set of user-defined tokens are disjoint from the set of top level
48
tokens.
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
"""
import re
import pslErrors
import itertools
import operator
import warnings
#from fuzzywuzzy import fuzz


TOP_LEVEL_TOKENS = ['sort', 'type', 'sorts', 'types', '.', 'subsort', 'subsorts', 'subtype', 'subtypes', 'op', 'ops', '->', ':', '[', ']', 'eq', '=', 'ceq', 'if', ':=', '==', 'In', '(', ')', 'Def', '(', ')',
        'Out', '=>', '<=>', ',', 'Intruder', 'learns', 'With', 'with', 'constraints:', 'without:', 'Subst', '|->', '!=', '|-', '$;']

'''
Blarge, don't really know what's going on with the bestTokenRatioPair crap, and I don't really feel like figuring it out right now.
def best_match(token, stmtTypes):
    """
    Takes a token, and a list of statement types (i.e. equational theory statements, intruder statements). Builds a list of tokens
    consisting of those tokens that begin each statement in stmtTypes, and returns the token that most closely matches the "token"
    argument.
    """
    bestTokenRatioPair = ('', 0)
    for stmtType in stmtTypes:
        startToken = stmtTypes[stmtType][0][0]
        ratio = fuzz.ratio(token, startToken)
        bestTokenRatioPair = (startToken, ratio) if ratio > bestTokenRatioPair[1] else bestTokenRatioPair
    tokens, args = (bestTokenRatioPair[0].tokens, iter(bestTokenRatioPair[0].argNodes))
    return ' '.join(next(args).class_name() if token == '_' else token for token in tokens)
'''


class Statement(object):
Joy Mitra's avatar
Joy Mitra committed
80 81
    """
    Contains a pair of lists. The first is a list of tokens, and the second is a list of line numbers, such that tokens[n] appears on
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105
    line lineNums[n]

    We could use a map, mapping tokens to line numbers, except that the same token may appear more than once in a single statement.
    """

    def __init__(self, tokens=None, lineNums=None):
        self.tokens = tokens if tokens else []
        self.lineNums = lineNums if lineNums else []
        #Yes, this check fails on strings, however I'm not treating strings as iterables, so this check should fail on
        #strings.
        assert(hasattr(self.tokens, '__iter__'))
        assert(hasattr(self.lineNums, '__iter__'))
        assert not (bool(self.tokens) ^ bool(self.lineNums)), "If 'tokens' is None (or empty), then 'lineNums' must also be None (or empty). If tokens is not None, then lineNums must also not be None."

    def __repr__(self):
        return str(zip(self.tokens, self.lineNums))
        """
        lines = []
        lineNums = []
        currentLine = []
        currentLineNum = self.lineNums[0]
        for token, lineNum in self:
            if lineNum == currentLineNum:
                currentLine.append(token)
Joy Mitra's avatar
Joy Mitra committed
106
            else:
107 108 109
                lines.append(currentLine)
                lineNums.append(currentLineNum)
                currentLine = [token]
Joy Mitra's avatar
Joy Mitra committed
110
                currentLineNum = lineNum
111 112 113 114 115 116 117 118 119 120 121 122 123 124 125
        lines.append(currentLine)
        lineNums.append(currentLineNum)
        lines = (' '.join(line) for line in lines)
        return '\n' + '\n'.join(map(' '.join, zip(["Line:"] * len(lineNums), map(str, lineNums), lines)))
        """

    def append(self, value, lineNum):
        self.tokens.append(value)
        self.lineNums.append(lineNum)


class Node(object):
    """
    Represents a Node in the AST. Consists of:
    1. The operator of the associated statement.
Joy Mitra's avatar
Joy Mitra committed
126
    2. Children nodes consisting of arguments to the
127
        high-level argument.
Joy Mitra's avatar
Joy Mitra committed
128
    3. The line at which this node occurs in the
129 130 131
        original file.

    For example, a statement of the form
Joy Mitra's avatar
Joy Mitra committed
132
    1 . A -> B : pk(A, B) |- M .  on line 5 would have a
133
    Node that looks like:
Joy Mitra's avatar
Joy Mitra committed
134 135 136 137 138 139

    Node(_._->_:_|-_.,
        Node(1, [], 5),
        Node(A, [], 5),
        Node(B, [], 5),
        Node(pk(A, B), [], 5),
140 141 142 143 144 145 146 147 148 149
        Node(M, [], 5), 5)

    Note that we don't attempt to parse user-defined
    operators. We leave that to Maude.

    Also has a function associated with it that performs error checking
    for this particular node.
    """
    def __init__(self, parent=None, op=None, children=None, lineNum=None):
        """
Joy Mitra's avatar
Joy Mitra committed
150
        op is a tuple of tokens representing the syntax of the statement describing this Node. children is an iterable of Nodes (or strings if we're at a leaf node, i.e. a Token) below this Node in the Tree, and line is the line number at which the Node's
151 152 153 154 155 156
        statement begins.
        """
        self.op = op
        self.parent = parent
        if children is None:
            children = []
Joy Mitra's avatar
Joy Mitra committed
157
        self.children = children
158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185
        self.lineNum = lineNum

    def error_check(self):
        raise NotImplementedError(self.class_name())

    def get_ops(self):
        return self.parent.get_ops()

    def get_root(self):
        root = self
        while root.parent:
            root = root.parent
        return root

    def translate(self):
        """
        Returns an iterable of lines of Maude code that translates the information contained in this Node into Maude-NPA code.
        """
        code = []
        assert self.children, "Node %s doesn't have any children. Perhaps you forgot to implement a custom translate() method for this node?" % str(self)
        for child in self.children:
            code.extend(child.translate())
        return code

    @staticmethod
    def parse(stmt, parent):
        """
        Given an object with the statement interface (an iterable of strings representing tokens, and an iterable of numbers representing line numbers on which those tokens appear), attempts to parse the statement
Joy Mitra's avatar
Joy Mitra committed
186
        into a parse tree. If successful, returns a parse tree with
187 188 189 190 191 192 193 194 195
        this node at the root. Otherwise, raises a SyntaxError.

        This is the function that should be overriden by children classes. The _parse static method is an internal method meant to be invoked by the children Nodes, because most of them perform the same basic
        algorithm. _parse implements that algorithm.
        """
        pass

    def _parse(self, stmt, syntax):
        """
Joy Mitra's avatar
Joy Mitra committed
196
        Given an object with the statement interface (an iterable of strings representing tokens, and an iterable of numbers representing
197
        line numbers on which those tokens appear), attempts to parse the statement
Joy Mitra's avatar
Joy Mitra committed
198
        into a parse tree. If successful, returns a parse tree with
199 200 201 202
        this node at the root. Otherwise, raises a SyntaxError.

        This method is meant to be invoked by the child classes of Node

Joy Mitra's avatar
Joy Mitra committed
203 204
        Observe that at this level, we don't know what type of node to return. So this parse function simply returns a triple of the
        operator tuple associated with the calling node, the arguments of the calling node, and the starting Line number.
205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
        The calling node then uses that information to construct a node of the appropriate type.
        """
        tokens = stmt.tokens
        opIter, argNodes = (iter(syntax.tokens), iter(syntax.argNodes))
        args = []
        unparsedTokens = iter(tokens)
        lineNumIter = iter(stmt.lineNums)
        startingLineNum = None
        terminatingToken = None
        userLevelTokenList = []
        userLevelLineNums = []
        for token in opIter:
            if token == '_':
                userLevelTokenList = []
                userLevelLineNums = []
                #Some syntaxes (i.e. DefPair) have an _ as the last token in the syntax.
                try:
                    terminatingToken = next(opIter)
                except StopIteration:
                    terminatingToken = None
                stmtToken = next(unparsedTokens)
                while stmtToken != terminatingToken:
                    userLevelTokenList.append(stmtToken)
                    currentLine = next(lineNumIter)
                    if startingLineNum is None:
                        startingLineNum = currentLine
                    userLevelLineNums.append(currentLine)
                    try:
                        stmtToken = next(unparsedTokens)
                    except StopIteration:
                        if terminatingToken:
                            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(currentLine), "Missing",
Joy Mitra's avatar
Joy Mitra committed
237
                                pslErrors.color_token(terminatingToken), "in line: ", ' '.join(color_stmt_tokens(stmt.tokens)),
238 239 240 241 242 243 244 245 246 247 248 249 250
                                "Expected a statement of the form: ", ' '.join(color_stmt_tokens(syntax.tokens))]))
                        else:
                            break
                args.append(next(argNodes).parse(Statement(userLevelTokenList, userLevelLineNums), self))
            else:
                try:
                    unparsedToken = next(unparsedTokens)
                except StopIteration:
                    #This check may (or may not, I'm not sure) vary depending on the statement.
                    if token == '.':
                        break
                    else:
                        raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(currentLine), "Missing a token matching: ",
Joy Mitra's avatar
Joy Mitra committed
251
                            pslErrors.color_token(token), "When parsing line: ", pslErrors.color_token(' '.join(stmt.tokens)),
252 253 254 255 256 257
                            "Expected a", "statement of the form: ", pslErrors.color_token(' '.join(syntax.tokens))]))
                else:
                    currentLine = next(lineNumIter)
                    if startingLineNum is None:
                        startingLineNum = currentLine
                    if token != unparsedToken:
Joy Mitra's avatar
Joy Mitra committed
258 259
                        raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(currentLine), "Unexpected token:",
                            pslErrors.color_token(unparsedToken), "when parsing statement:", pslErrors.color_token(' '.join(stmt.tokens)),
260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279
                            "Expected statement of the form: ", pslErrors.color_token(' '.join(syntax.tokens))]))
        return (syntax.tokens, args, startingLineNum)

    def __repr__(self):
        return '\n'.join(['$$$$$$$$', 'Op::', repr(self.op), 'Line Number::', repr(self.lineNum), 'Children::', '----------------\n'.join(map(repr, self.children)), '########'])

    @staticmethod
    def class_name():
        return "Node"



class Root(Node):

    def __init__(self, op=None, children=None, lineNum=None):
        super(Root, self).__init__(None, op, children, lineNum)

    @staticmethod
    def class_name():
        return "Root"
Joy Mitra's avatar
Joy Mitra committed
280

281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321
    def get_theory(self):
        try:
            return next(child for child in self.children if child.class_name() == Theory.className)
        except StopIteration:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Theory")]))

    def get_protocol(self):
        try:
            return next(child for child in self.children if child.class_name() == Protocol.className)
        except StopIteration:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Protocol")]))

    def get_intruder(self):
        try:
            return next(child for child in self.children if child.class_name() == Intruder.className)
        except StopIteration:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Intruder")]))

    def get_attacks(self):
        try:
            return next(child for child in self.children if child.class_name() == Attacks.className)
        except StopIteration:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Attacks")]))

    def sort_names(self):
        return self.get_theory().sort_names()

    def get_ops(self):
        ops = []
        for child in self.children:
            try:
                ops.append(child.get_user_defined_operator())
            except AttributeError:
                pass
        return ops


class Section(Node):

    def declared_variables(self, upToNode=None):
        """
Joy Mitra's avatar
Joy Mitra committed
322
        upToNode is a VarDeclNode. If upToNode is not None, then Theory will return all the variables declared before upToNode. This is
323 324 325 326 327 328 329 330 331
        particularly useful when checking for duplicate variable declarations.

        Note: This returns only the variable NAMES. It does not return the sorts of the variables.
        """
        declaredVars = []
        for child in self.children:
            if child is upToNode:
                break
            try:
Joy Mitra's avatar
Joy Mitra committed
332
                declaredVars.extend(child.get_vars())
333 334 335 336 337 338
            except AttributeError:
                pass
        return declaredVars

    def var_name_sort_mapping(self):
        """
339
        Returns a map from variable name to the variable's sort for all variables declared in this section.
340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367
        """
        declaredVars = {}
        for child in self.children:
            try:
                childMapping = child.name_sort_mapping()
            except AttributeError:
                pass
            else:
                for varName in childMapping:
                    declaredVars[varName] = childMapping[varName]
        return declaredVars


class PSLSection(Section):

    def sort_names(self):
        return self.parent.sort_names()

    def translate(self):
        self.error_check()
        return [self.class_name(), '{'] + super(PSLSection, self).translate() + ['}']


class Theory(Section):
    """
    Root of the theory syntax tree.
    Note that the theory section behaves differently from the other sections in a variety of ways, so it is not made a subtype of PSLSection, but rather only of Section
    """
Joy Mitra's avatar
Joy Mitra committed
368

369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405
    className = "Theory"

    def __init__(self, parent, line=0):
        super(Theory, self).__init__(parent, None, [], line)

    def class_name(self):
        return Theory.className

    def sort_nodes(self):
        """
        Returns the list of nodes that declare sort names.
        """
        return [arg for arg in self.children if arg.op in typeSyntax]

    def sort_names(self):
        """
        Returns a list of sort names declared in this module.
        """
        sortNames = []
        for arg in self.children:
            try:
                sortNames.extend(arg.sort_names())
            except AttributeError:
                pass
        return sortNames

    def ops(self):
        ops = []
        for child in self.children:
            try:
                ops.append(child.get_user_defined_operator())
            except AttributeError:
                pass
        return ops

    @staticmethod
    def parse(stmts, parent):
Joy Mitra's avatar
Joy Mitra committed
406
        #stmts is a list of Statement objects, each of which consists of a list of tokens and an associated list of line numbers for
407 408 409 410
        #each token.
        root = Theory(parent)
        keywordList = [['type', 'sort', 'types', 'sorts'], ['subtype', 'subtypes', 'subsort', 'subsorts'], ['op', 'ops'],
                ['var', 'vars'], ['eq', 'ceq']]
Joy Mitra's avatar
Joy Mitra committed
411
        syntaxDeclPairs = [(typeSyntax, TypeDecl), (subTypeSyntax, SubTypeDecl), (opSyntax, OpDecl), (varSyntax, VarDecl),
412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427
                (eqSyntax, EqStmt)]
        stmtTypes = {}
        #These are already in PROTOCOL-DEFINITION-RULES, so we don't need to add them explicitly. We do however, need to remove them
        #if people already declared them.
        #builtInSorts = ['sorts'] + TypeDecl.builtInTypes + ['.']
        #stmts = [Statement(builtInSorts, [-1] * len(builtInSorts))] + stmts
        for keywords, sdPair in zip(keywordList, syntaxDeclPairs):
            for word in keywords:
                stmtTypes[word] = sdPair
        for stmt in stmts:
            for stmtType in stmtTypes:
                syntaxList, nodeType = stmtTypes[stmtType]
                if any(stmt.tokens[0] == stmtSyntax.tokens[0] for stmtSyntax in syntaxList):
                    root.children.append(nodeType.parse(stmt, root))
                    break
            else:
Joy Mitra's avatar
Joy Mitra committed
428 429
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(stmt.lineNums[0]), "Token",
                    pslErrors.color_token(stmt.tokens[0]), "does not begin an equational theory statement."])) #Did you mean:",
430 431 432 433
                    #pslErrors.color_token(best_match(stmt.tokens[0], stmtTypes)) + '?']))
        #Make all sorts subsorts of Msg.
        subsortDecl = ['subsorts'] + [sortName for sortName in root.sort_names() if sortName != 'Msg'] + ['<', 'Msg', '.']
        root.children.append(SubTypeDecl.parse(Statement(subsortDecl, [-1] * len(subsortDecl)), root))
Joy Mitra's avatar
Joy Mitra committed
434
        assert all(root.children)
435 436
        return root

Joy Mitra's avatar
Joy Mitra committed
437
    def error_check(self):
438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461
        """
        If performance becomes an issue (unlikely considering the very small
        size of specifications compared to programs. I doubt a specification
        is going to be millions of lines of code!) then we can check for
        duplicates as we parse the sort names
        """
        errors = []
        warnings = []
        for arg in self.children:
            try:
                arg.error_check()
            except pslErrors.PSLError, e:
                errors.append(e)
            except pslErrors.PSLWarning, e:
                warnings.append(e)
        try:
            self.check_repeated_sorts()
        except pslErrors.SyntaxWarning, e:
            warnings.append(e)
        try:
            self.check_axioms()
        except pslErrors.InvalidOpError, e:
            errors.append(e)
        if errors or warnings:
Joy Mitra's avatar
Joy Mitra committed
462
            raise pslErrors.ErrorsAndWarnings(errors + warnings, errors,
463 464 465 466
                    warnings)

    def check_repeated_sorts(self):
        """
Joy Mitra's avatar
Joy Mitra committed
467
        Checks if the theory section has any multiply declared sorts. If
468 469 470 471 472 473 474
        there are any, then the program raises a SyntaxWarning.
        """
        seenSorts = set()
        errorMsgs = []
        for node in self.sort_nodes():
            for sort in node.sort_names():
                if sort in seenSorts:
Joy Mitra's avatar
Joy Mitra committed
475 476
                    errorMsgs.append(' '.join([pslErrors.warning,
                        pslErrors.color_line_number(node.line), "Sort",
477 478 479 480 481 482 483 484 485 486
                        pslErrors.color_token(sort), "already declared, and will be",
                        "ignored."]))
                    node.remove_sort(sort)
                else:
                    seenSorts.add(sort)
        if errorMsgs:
            raise pslErrors.SyntaxWarning('\n'.join(errorMsgs))

    def check_axioms(self):
        """
Joy Mitra's avatar
Joy Mitra committed
487
        Checks to make sure the theory has only allowed combinations of axioms:
488
        assoc-comm, comm, assoc-comm-id.
Joy Mitra's avatar
Joy Mitra committed
489 490
        assoc, assoc-id, any combination containing only left-id, any
        combination containing right-id, or any combination containing idem are
491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522
        not allowed.
        """
        #TODO: Implement
        ops = self.get_op_nodes()

    def get_op_nodes(self):
        return [arg for arg in self.children if arg.op in opSyntax]


class StmtNode(Node):
    """
    A StmtNode (statement node) is a node that a single Maude-NPA statement (i.e. a sort declaration, an operator, an equation).
    It is assumed that Statement nodes contain a tuple "op" that defines their syntax. For example ('op', '_', ':', '_', '->', '_', '.') represents an op statement without brackets, where
    underscores represent the position at which the user provides input. Furthermore the ith _ should correspond to the ith child of this node.
    """

    @staticmethod
    def class_name():
        return "StmtNode"

    def translate(self):
        self.error_check()
        code = list(self.op)
        underscoreIndices = [i for i, x in enumerate(self.op) if x == '_']
        for i in range(len(self.children)):
            code[underscoreIndices[i]] = ' '.join(''.join(child) for child in self.children[i].translate())
        return [' '.join(code)]


class PSLStmtNode(StmtNode):

    className = "PSL Statement Node"
Joy Mitra's avatar
Joy Mitra committed
523

524 525
    def class_name(self):
        return PSLStmtNode.className
Joy Mitra's avatar
Joy Mitra committed
526

527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557

    def translate(self):
        """
        If we're translating statements that are not in the theory section, then we need to append the line number onto the end.
        """
        code = super(PSLStmtNode, self).translate()
        #Since these are all single statements, they should only create a single line of Maude code.
        assert len(code) == 1
        return self.append_line_number(code)

    def append_line_number(self, code):
        code = code[0]
        return [' '.join([code, '[', str(self.lineNum), ']'])]


class TypeDecl(StmtNode):
    """
    Used to encode type declarations (i.e. statements prefixed by one of:
    sort(s), type(s)
    A TypeDecl's children is a single PSLListNode of Tokens containing the sort names.
    """

    builtInTypes = ['Msg', 'Public', 'Fresh']

    @staticmethod
    def class_name():
        return "Type Declaration"

    @staticmethod
    def parse(stmt, parent):
        syntax = next(syntax for syntax in typeSyntax if stmt.tokens[0] == syntax.tokens[0])
Joy Mitra's avatar
Joy Mitra committed
558
        node = TypeDecl(parent, None, None, None)
559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594
        op, children, lineNum = node._parse(stmt, syntax)
        node.op = op
        node.children = children
        node.lineNum = lineNum
        assert all(node.children)
        return node

    def sort_names(self):
        """
        Returns a list of sort names declared in this node.
        """
        sortList = []
        for child in self.children:
            sortList.extend(child.get_elements())
        return [elem.get_token() for elem in sortList]

    def remove_sort(self, sort):
        for child in self.children:
            try:
                self.children.remove(sort)
            except ValueError:
                pass
            else:
                break

    def add_sort(self, sort):
        self.children[0].children.append(sort)

    def translate(self):
        self.op[0] = 'sorts'
        return super(TypeDecl, self).translate()

    def error_check(self):
        errorMsgs = []
        for sortName in self.sort_names():
            invalidTokenMsg = self.invalid_tokens(sortName)
Joy Mitra's avatar
Joy Mitra committed
595
            if invalidTokenMsg:
596 597
                errorMsgs.append(invalidTokenMsg)
            if sortName in TypeDecl.builtInTypes:
Joy Mitra's avatar
Joy Mitra committed
598
                errorMsgs.append(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum),
599 600 601 602 603 604 605 606 607 608
                    "Type", pslErrors.color_token(sortName),
                    "already has a special meaning in Maude-NPA, and should not be explicitly declared in a PSL specification."]))
        if errorMsgs:
            raise pslErrors.SyntaxError('\n'.join(errorMsgs))

    def invalid_tokens(self, sortName):
        invalidTokens = ['`', '}', '{', '(', ')', '[', ']', ',']
        invalidTokens = ', '.join([token for token in invalidTokens if token in sortName])
        if invalidTokens:
            return ' '.join(["Invalid tokens:", pslErrors.color_token(invalidTokens),
Joy Mitra's avatar
Joy Mitra committed
609
                    "are not allowed in sort names.",
610 611 612 613 614 615 616
                    "Invalid sort name: ", pslErrors.color_token(sortName)])
        else:
            return ''


class Term(Node):
    """
Joy Mitra's avatar
Joy Mitra committed
617
    Used for discrete units of syntax (i.e. individual terms that serve
618 619 620 621 622 623 624 625 626 627
    as arguments to one of the statements listed at bottom of this
    file). These include
    variables, numbers and terms using user-defined syntax that Python can't
    handle as well as Maude.
    """

    @staticmethod
    def class_name():
        return "Term"

Joy Mitra's avatar
Joy Mitra committed
628
    def __init__(self, parent=None, children=None, lineNum=None):
629 630
        """
        Children is an iterable of Tokens. lineNum is the line number on which this term begins.
Joy Mitra's avatar
Joy Mitra committed
631
        op is not specified by the creator. It is always '_' because terms should only appear in
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
        places where '_' appears in the high level syntax.
        """
        super(Term, self).__init__(parent, '_', children, lineNum)

    def __repr__(self):
        return '\n'.join(map(repr, self.children))

    def __str__(self):
        return ' '.join(map(str, self.children))

    def tokens(self):
        return self.children

    @staticmethod
    def parse(stmt, parent):
        node = Term(parent, [], stmt.lineNums[0])
        node.children = [Token(node, [token], lineNum) for token, lineNum in zip(stmt.tokens, stmt.lineNums)]
        return node

    def translate(self):
        code = []
        opDecls = self.parent.get_ops()
        for child in self.children:
            code.extend(child.translate())
        return [' '.join(code)]

    def get_tokens(self):
        """
        Returns the tokens (as token objects) that make up this term.
        """
        return self.children


class Token(Node):
    """
        A single token. This is a leaf node of the parse tree.
    """
Joy Mitra's avatar
Joy Mitra committed
669
                              #start multi-line comment /* ... */|end multi-line comment
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693
                              #| single line comment|start of specification| parens/brackets/curly braces | whitespace
    #tokenizer = re.compile(r'(/\*)|(\*/)|(//.*$)|(spec \S+ is)|([[\](){}])|(,)|(_)|(\s)')
    tokenizer = re.compile(r'(/\*)|(\*/)|(//.*$)|(spec \S+ is)|([[\](){}])|(,)|\s')

    @staticmethod
    def class_name():
        return "Token"

    def __init__(self, parent, tokenList, lineNum):
        assert(isinstance(tokenList, list))
        super(Token, self).__init__(parent, None, tokenList, lineNum)

    @staticmethod
    def parse(stmt, parent, lineNum=None):
        assert len(stmt.tokens) == 1, "Statement has been passed to the Token node with more than one tokens: %s" % ', '.join(stmt.tokens)
        assert len(stmt.lineNums) == 1, "Statement has been passed to the Token node with more than one line number: %s" % ', '.join(map(str, stmt.lineNums))
        return Token(parent, stmt.tokens, stmt.lineNums)

    def get_token(self):
        return self.children[0]

    def translate(self):
        """
        We don't need to do anything fancy to tokens to turn them into Maude-NPA code, since they're just discrete bits of string that are provided by the user.
Joy Mitra's avatar
Joy Mitra committed
694
        """
695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724
        token = self.get_token()
        parent = self.parent
        while True:
            try:
                declaredVars = parent.declared_variables()
            except AttributeError:
                parent = parent.parent
            else:
                break
        if token in declaredVars:
            parent = self.parent
            while True:
                try:
                    varsWithSorts = parent.var_name_sort_mapping()
                except AttributeError:
                    parent = parent.parent
                else:
                    break
            token = ':'.join([token, varsWithSorts[token]])
        return [token]

    def __repr__(self):
        return ''.join([str(self.lineNum), ': ', ''.join(self.children)])

    def __str__(self):
        return ''.join(self.children)


class SubTypeDecl(StmtNode):
    """
Joy Mitra's avatar
Joy Mitra committed
725 726
    The child of a SubTypeDecl node is a PSLListNode of lists of tokens: [[Token_1, Token_2, ..., Token_n], ..., [Token_m1, Token_m2, ... Token_mp] s.t.
     s.t. Token_1 Token_2 ... Token_n < ... < Token_m1 Token_m2 ... Token_mp
727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780
    """

    @staticmethod
    def class_name():
        return "Subtype Declaration"

    @staticmethod
    def parse(stmt, parent):
        syntax = next(syntax for syntax in subTypeSyntax if syntax.tokens[0] == stmt.tokens[0])
        node = SubTypeDecl(parent, None, None, None)
        node.op, node.children, node.lineNum = node._parse(stmt, syntax)
        assert all(node.children)
        return node

    def translate(self):
        self.op[0] = 'subsorts'
        code = super(SubTypeDecl, self).translate()[0]
        return [code]

    def error_check(self):
        """
        All we need to check for subtype declarations is that the sorts used in the sub type declaration have been declared.
        """
        declaredSorts = self.parent.sort_names()
        sortNames = []
        for child in self.children:
            assert not isinstance(child.get_elements(), Node), "Should be a list: %s" % str(child.get_elements)
            for element in child.get_elements():
                sortNames.extend(element.get_elements())
        sortNames = [sort.get_token() for sort in sortNames]
        undeclaredSorts = [sort for sort in sortNames if not sort in declaredSorts]
        errorMsgs = ''
        for sort in filter(lambda x : x not in TypeDecl.builtInTypes, undeclaredSorts):
            '\n'.join([errorMsgs, ' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Type name: ", pslErrors.color_token(sort) + " has not been declared."])])
        if errorMsgs:
            raise pslErrors.SyntaxError(errorMsgs)

class OpDecl(StmtNode):

    @staticmethod
    def class_name():
        return "Op Declaration"

    @staticmethod
    def parse(stmt, parent):
        #First, we distinguish between op and ops, then we'll distinguish between [_] and no [_].
        syntaxList = [syntax for syntax in opSyntax if stmt.tokens[0] == syntax.tokens[0]]
        reversedTokens = stmt.tokens[::-1]
        indexBeforeColon = reversedTokens.index(':')-1
        if stmt.tokens[-2] == ']':
            syntaxList = (syntax for syntax in syntaxList if syntax.tokens[-2] == ']')
        else:
            syntaxList = (syntax for syntax in syntaxList if syntax.tokens[-2] != ']')
        #We're checking the token after the colon in the original, non-reversed list.
Joy Mitra's avatar
Joy Mitra committed
781
        if reversedTokens[indexBeforeColon] == '->':
782 783 784 785 786 787 788 789 790 791 792 793 794
            syntax = next(syntax for syntax in syntaxList if syntax.tokens[-syntax.tokens[::-1].index(':')] == '->')
        else:
            syntax = next(syntax for syntax in syntaxList if syntax.tokens[-syntax.tokens[::-1].index(':')] != '->')
        node = OpDecl(parent, None, None, None)
        node.op, node.children, node.lineNum = node._parse(stmt, syntax)
        assert all(node.children)
        return node

    def translate(self):
        #Need to check if one of the attributes is frozen.
        if '[' in self.op:
            attributes = self.get_attributes()
            if not 'frozen' in attributes and not self.is_constant():
Joy Mitra's avatar
Joy Mitra committed
795
                opAttributeList = self.children[-1]
796 797 798
                opAttributeList.append(Token(self, ['frozen'], self.lineNum))
            elif not self.is_constant():
                frozenIndex = attributes.index('frozen')
Joy Mitra's avatar
Joy Mitra committed
799
                #This handles converting frozen(1, 2, 3) (or whatever operator positions) into frozen, since Maude-NPA requires every
800 801 802 803 804 805 806 807 808
                #argument to be frozen.
                try:
                    startParenIndex = frozenIndex+1
                except IndexError:
                    pass
                else:
                    try:
                        endParenIndex = attributes[frozenIndex:].index(')')
                    except ValueError:
Joy Mitra's avatar
Joy Mitra committed
809
                        raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum),
810 811
                            "Unbalanced parenthesis when declaring frozen properties."]))
                    self.children[-1].remove_range(startParenIndex, endParenIndex)
Joy Mitra's avatar
Joy Mitra committed
812
                    warnings.warn(' '.join([pslErrors.warning, pslErrors.color_line_number(self.lineNum),
813 814 815 816 817
                        "Maude-NPA requires all arguments on all operators to be frozen. Your partially frozen operator",
                        "has been converted into a completely frozen operator."]))
        else:
            if not self.is_constant():
                self.children.append(PSLListNode(self, '', [Token(self, ['frozen'], self.lineNum)], self.lineNum))
Joy Mitra's avatar
Joy Mitra committed
818 819
                #Need to change the op to be the version with operator attributes. Note that since we don't add frozen to the constant
                #operators, we don't care about
820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847
                #changing those (because we don't need to).
                if 'ops' in self.op:
                    self.op = opSyntax[-1].tokens
                else:
                    self.op = opSyntax[1].tokens
        return super(OpDecl, self).translate()

    def is_constant(self):
        userOp = self.op[self.op.index(':'):self.op.index('->')]
        for token in userOp:
            if '_' in token:
                return False
        else:
            return True

    def error_check(self):
        attributes = self.get_attributes()
        if 'assoc' in attributes and not 'comm' in attributes:
            raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Operator attribute", pslErrors.color_token('assoc'), "not allowed without the",
                pslErrors.color_token('comm'), "attribute"]))
        if 'id:' in attributes and not ('assoc' in attributes and 'comm' in attributes):
            raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Operator attribute", pslErrors.color_token('id:'), "not allowed without the",
                pslErrors.color_token('comm'), "and", pslErrors.color_token('assoc'), "attributes."]))
        if 'idem' in attributes:
            raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Operator attribute", pslErrors.color_token('idem'), "is not allowed."]))
        userDefinedOperator = self.get_user_defined_operator()
        for token in userDefinedOperator:
            if token in TOP_LEVEL_TOKENS and (token != '(' and token != ')' or token == 'op'):
Joy Mitra's avatar
Joy Mitra committed
848
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Token:", pslErrors.color_token(token),
849 850 851 852
                    "is a token in the Maude-PSL top level syntax",
                    "and therefore is not allowed in a user-defined operator. Consider doubling the token (i.e.", pslErrors.color_token(token + token), "or tweaking the token in some other manner",
                    "to make it distinct."]))
            elif (token == '(' or token == ')') and token == 'ops':
Joy Mitra's avatar
Joy Mitra committed
853
                warnings.warn(' '.join([pslErrors.warning, pslErrors.color_line_number(self.lineNum), "Token ",
854
                    pslErrors.color_token(token),
Joy Mitra's avatar
Joy Mitra committed
855 856
                    "is not allowed to be part of a user-defined operator. Therefore,", pslErrors.color_token(token),
                    "is assumed to be enclosing one of several operators declared on the same line."]))
857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898

    def get_attributes(self):
        if '[' in self.op:
            opAttributes = self.children[-1]
            return [attribute.get_token() for attribute in opAttributes.children]
        else:
            return []

    def get_user_defined_operator(self):
        return [elem.get_token() for elem in self.children[0].get_elements()]


class VarDecl(StmtNode):

    className = "Variable Declaration"

    @staticmethod
    def class_name():
        return "Variable Declaration"

    @staticmethod
    def parse(stmt, parent):
        syntax = next(syntax for syntax in varSyntax if stmt.tokens[0] == syntax.tokens[0])
        node = VarDecl(parent, None, None, None)
        node.op, node.children, node.lineNum = node._parse(stmt, syntax)
        assert all(node.children)
        return node

    def get_sort_name(self):
        return self.children[1].get_token()

    def get_vars(self):
        """
        Returns the tokens that represent variable names declared as a part of this decl.
        """
        return [elem.get_token() for elem in self.children[0].get_elements()]

    def error_check(self):
        varNames = self.get_vars()
        allVarsUpToMe = self.parent.declared_variables(self)
        redeclaredVars = [varName for varName in varNames if varName in allVarsUpToMe]
        if redeclaredVars:
Joy Mitra's avatar
Joy Mitra committed
899
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Variables: ",
900 901
                pslErrors.color_token(' '.join(redeclaredVars)), "have already been declared."]))
        if not self.get_sort_name() in self.parent.sort_names() + TypeDecl.builtInTypes:
Joy Mitra's avatar
Joy Mitra committed
902
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Sort: ",
903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918
                pslErrors.color_token(self.get_sort_name()), "has not been declared."]))

    def name_sort_mapping(self):
        """
        Returns a mapping from var name to sort name for each var name in this var declaration.
        """
        sortName = self.get_sort_name()
        return {varName:sortName for varName in self.get_vars()}

    def translate(self):
        """
        We convert all the variables into inline declarations as part of the translation of the Tokens, so we don't carry over the explicit variable declarations into the Maude code.
        """
        self.error_check()
        return ['']

Joy Mitra's avatar
Joy Mitra committed
919

920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947
class EqStmt(StmtNode):

    @staticmethod
    def class_name():
        return "Equation"

    @staticmethod
    def parse(stmt, parent):
        if stmt.tokens[-2] == ']':
            syntax = next(syntax for syntax in eqSyntax if syntax.tokens[-2] == ']')
        else:
            syntax = next(syntax for syntax in eqSyntax if syntax.tokens[-2] != ']')
        node = EqStmt(parent, None, None, None)
        node.op, node.children, node.lineNum = node._parse(stmt, syntax)
        assert all(node.children), "%s" % str(node)
        return node

    def get_attributes(self):
        if '[' in self.op:
            attributes = [elem.get_token() for elem in self.children[-1].get_elements()]
            return attributes
        else:
            return []

    def translate(self):
        self.error_check()
        if '[' in self.op:
            attributes = self.get_attributes()
Joy Mitra's avatar
Joy Mitra committed
948
            print(attributes)
949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967
            if not 'variant' in attributes and not 'homomorphism' in attributes:
                self.children[-1].append(Token(self, ['variant'], self.lineNum))
            elif 'homomorphism' in attributes:
                self.children[-1].remove('homomorphism')
                newTokens = ['label', 'homomorphism', 'metadata', '"builtin-unify"']
                self.children[-1].extend([Token(self, [token], self.lineNum) for token in newTokens])
            if not 'nonexec' in attributes:
                pass
                #self.children[-1].append(Token(self, ['nonexec'], self.lineNum))
        else:
            self.op = eqSyntax[1].tokens
            self.children.append(PSLListNode(self, '', [Token(self, ['variant'], self.lineNum)],  self.lineNum))
                #Token(self, ['nonexec'], self.lineNum)]
        return super(EqStmt, self).translate()

    def error_check(self):
        attributes = self.get_attributes()
        if '[' in self.op:
            if 'variant' in attributes and 'homomorphism' in attributes:
Joy Mitra's avatar
Joy Mitra committed
968 969
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum),
                    "Equation cannot have both the attribute:", pslErrors.color_token('variant'), 'and the attribute:',
970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025
                    pslErrors.color_token('homomorphism') + '.']))



class Int(Node):
    """
    Encapsulates integers
    """

    @staticmethod
    def class_name():
        return "Integer"

    @staticmethod
    def parse(stmt, parent):
        if len(stmt.tokens) != 1:
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(stmt.lineNums[0]), "Expected a single integer when parsing ", pslErrors.color_token(' '.join(stmt.tokens)) + ".", "Make sure there are no spaces between your digits, and there is a",
            "period after the integer."]))
        try:
            int(stmt.tokens[0])
        except ValueError:
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(stmt.lineNums[0]), "Expected: ", pslErrors.color_token(' '.join(stmt.tokens)), "to be an integer."]))
        else:
            return Int(parent=parent, children=stmt.tokens, lineNum=stmt.lineNums[0])

    def translate(self):
        return [self.children[0]]

    def value(self):
        return int(self.children[0])


class Protocol(PSLSection):

    className = "Protocol"

    @staticmethod
    def class_name():
        return Protocol.className

    def role_names(self):
        roleNames = []
        for child in self.children:
            try:
                roleNames.extend(child.role_names())
            except AttributeError:
                pass
        return roleNames

    def role_decls(self):
        roleDecls = []
        for child in self.children:
            if child.className == RoleDecl.className:
                roleDecls.append(child)
        return roleDecls

Joy Mitra's avatar
Joy Mitra committed
1026

1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047
    def __init__(self, parent, line=0):
        super(Protocol, self).__init__(parent, None, [], line)

    def statement_vars(self, stepNumber):
        """
        Returns a mapping from role names (as strings) to the variables that appear in that role's protocol steps and input (as strings).
        """
        allStepVars = {}
        for child in self.children:
            try:
                childStepNumber = child.get_step_number()
            except AttributeError:
                pass
            else:
                if childStepNumber <= stepNumber:
                    stepVars = child.statement_vars()
                    for role in stepVars:
                        if role in allStepVars:
                            allStepVars[role].extend(stepVars[role])
                        else:
                            allStepVars[role] = stepVars[role]
Joy Mitra's avatar
Joy Mitra committed
1048
        return allStepVars
1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099

    def variables_per_role(self):
        """
        Returns a map, mapping role names to a list of variables that may show up in that role's terms.
        """
        return {inDecl.role_name():inDecl.variables() for inDecl in self.in_decls()}

    def in_decls(self, upToMe=None):
        inDecls = []
        for child in self.children:
            if child is upToMe:
                break
            elif child.class_name() == InDecl.className:
                inDecls.append(child)
        return inDecls

    def in_decl_with_role_name(self, roleName):
        return next(inDecl for inDecl in self.in_decls() if inDecl.role_name() == roleName)

    def out_decls(self):
        return [child for child in self.children if child.class_name() == OutDecl.className]

    def in_decl_role_names(self, upToMe=None):
        return [inDecl.role_name() for inDecl in self.in_decls(upToMe)]

    def out_decl_role_names(self):
        return [outDecl.role_name() for outDecl in self.out_decls()]

    def get_defs(self):
        return [child for child in self.children if child.class_name() == DefDecl.className]

    @staticmethod
    def parse(stmts, parent):
        root = Protocol(parent)
        #Possible beginnings of each statement:
        #1. roles
        #2. Def
        #3. In
        #4. Out
        #5. An integer
        #6. var(s)
        stmtTypes = [roleSyntax, defSyntax, outSyntax, inSyntax, varSyntax[0], varSyntax[1]]
        for stmt in stmts:
            for stmtType in stmtTypes:
                if stmt.tokens[0] == stmtType.tokens[0]:
                    root.children.append(stmtType.stmtNode.parse(stmt, root))
                    break
            else:
                try:
                    int(stmt.tokens[0])
                except ValueError:
Joy Mitra's avatar
Joy Mitra committed
1100
                    raise SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(stmt.lineNums[0]), "Token",
1101 1102 1103 1104 1105
                        pslErrors.color_token(stmt.tokens[0]), "does not begin a Protocol statement."]))
                else:
                    root.children.append(stepSyntax.stmtNode.parse(stmt, root))
        return root

Joy Mitra's avatar
Joy Mitra committed
1106
    def error_check(self):
1107 1108 1109 1110 1111 1112 1113
        roleDecls = self.role_decls()
        inDeclRoleNames = set(self.in_decl_role_names())
        outDeclRoleNames = set(self.out_decl_role_names())
        for roleDecl in roleDecls:
            roleNames = roleDecl.role_names()
            for role in roleNames:
                if role not in inDeclRoleNames:
Joy Mitra's avatar
Joy Mitra committed
1114 1115 1116
                    raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(roleDecl.lineNum),
                        "Missing In(put) for role", pslErrors.color_token(role) + ".",
                        ' '.join(["The roles syntax does NOT contain a colon." if role == ':' else "The role names are NOT separated by commas. They are separated by spaces.",
1117 1118 1119
                            "Role Syntax:", pslErrors.color_token(' '.join(['roles', 'Role1', 'Role2', 'Role3', '.']))]) if role == ':' or role == ',' else ''
                        ]))
                if role not in outDeclRoleNames:
Joy Mitra's avatar
Joy Mitra committed
1120
                    raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(roleDecl.lineNum),
1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177
                        "Missing Out(put) for", pslErrors.color_token(role) + "."]))

class RoleDecl(PSLStmtNode):

    className = "Role Declaration"

    def class_name(self):
        return RoleDecl.className

    def role_names(self):
        return [role.role_name() for role in self.roles()]

    def roles(self):
        roles = []
        for child in self.children:
            roles.extend(child.get_elements())
        return roles

    @staticmethod
    def parse(stmt, parent):
        node = RoleDecl(parent=parent)
        node.op, node.children, node.lineNum = node._parse(stmt, roleSyntax)
        return node

    def error_check(self):
        pass

    def translate(self):
        """
        Roles do not show up in the Maude code. They're only used to catch errors at the PSL level.
        """
        return []


class Role(Node):

    def class_name(self):
        return "Role"

    @staticmethod
    def parse(stmt, parent):
        node = Role(parent=parent)
        assert len(stmt.tokens) == 1, "Role: %s" % str(stmt.tokens)
        node.children = stmt.tokens
        node.lineNum = stmt.lineNums[0]
        return node

    def role_name(self):
        return self.children[0]

    def translate(self):
        self.error_check()
        return [self.children[0] + ':Role']

    def error_check(self):
        roleNames = self.get_root().get_protocol().role_names()
        if self.role_name() not in roleNames:
Joy Mitra's avatar
Joy Mitra committed
1178 1179
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Undeclared role:",
                pslErrors.color_token(self.role_name()) + ".", "Declared role names:",
1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205
                pslErrors.color_token(', '.join(roleNames) if roleNames else "None")]))


class TermList(Node):

    @staticmethod
    def parse(stmt, parent):
        """
        Because of the difficulty in parsing terms in a comma-separated list, we punt that parsing off to Maude.
        """
        node = TermList(parent)
        node.children = [Token(node, [token], lineNum) for token, lineNum in zip(stmt.tokens, stmt.lineNums)]
        node.lineNum = stmt.lineNums[0]
        return node

    def translate(self):
        return [child.translate() for child in self.children]


class InDecl(PSLStmtNode):

    className = "In Declaration"

    def class_name(self):
        return InDecl.className

Joy Mitra's avatar
Joy Mitra committed
1206
    @staticmethod
1207 1208 1209 1210 1211 1212 1213 1214 1215
    def parse(stmt, parent):
        node = InDecl(parent=parent)
        node.op, node.children, node.lineNum = node._parse(stmt, inSyntax)
        return node

    def error_check(self):
        if self.children[0].role_name() not in self.parent.role_names():
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Undeclared role name:", pslErrors.color_token(self.children[0].role_name())]))
        if self.children[0].role_name() in self.parent.in_decl_role_names(self):
Joy Mitra's avatar
Joy Mitra committed
1216
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Input for role", pslErrors.color_token(self.children[0].role_names()),
1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242
                "already declared", "on line: ", pslErrors.color_line_number(self.parent.in_decl_with_role(self.role_name()).lineNum)]))
        declaredVars = self.parent.declared_variables()
        errors = []
        for token in self.children[1].get_elements():
            if token.get_token() not in declaredVars:
                errors.append(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Undeclared variable:", pslErrors.color_token(token.get_token())]))
        if errors:
            raise pslErrors.SyntaxError('\n'.join(errors))

    def role_name(self):
        return self.children[0].role_name()

    def variables(self):
        """
        Returns the list of variables that may be used by the role associated with this in decl.
        """
        return [token.get_token() for token in self.children[1].get_elements()]


class OutDecl(PSLStmtNode):

    className = "Out Declaration"

    def class_name(self):
        return OutDecl.className

Joy Mitra's avatar
Joy Mitra committed
1243
    @staticmethod
1244 1245 1246 1247 1248 1249 1250 1251
    def parse(stmt, parent):
        node = OutDecl(parent=parent)
        node.op, node.children, node.lineNum = node._parse(stmt, outSyntax)
        return node

    def error_check(self):
        roleName = self.children[0].role_name()
        if roleName not in self.parent.role_names():
Joy Mitra's avatar
Joy Mitra committed
1252
            raise pslErrors.SyntaxError([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Role name: ", pslErrors.color_token(roleName),
1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273
                "not declared."])

    def role_name(self):
        return self.children[0].role_name()


class DefDecl(PSLStmtNode):
    """
    Encodes a def decl. Children:
    1. The role associated with these definitions.
    2. The list of definition pairs defined in this def statement.
    """

    className = "Def Declaration"

    def class_name(self):
        return self.className

    def role(self):
        return self.children[0].get_token()

Joy Mitra's avatar
Joy Mitra committed
1274
    @staticmethod
1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291
    def parse(stmt, parent):
        node = DefDecl(parent=parent)
        term = []
        colonEqualsFound = False
        pairComplete = False
        roleNameFound = False
        #Removing the period at the end, because we don't need (or want) it here.
        stmt.tokens, stmt.lineNums = stmt.tokens[:-1], stmt.lineNums[:-1]
        for token, lineNum in zip(stmt.tokens, stmt.lineNums):
            if token == 'Def' or token == '(' or token == ')':
                continue
            elif token == '=':
                break
            elif not roleNameFound:
                node.children.append(Token(node, [token], lineNum))
                roleNameFound = True
            elif roleNameFound:
Joy Mitra's avatar
Joy Mitra committed
1292 1293
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNum), "Unexpected token: ",
                    pslErrors.color_token(token) + ".",
1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304
                "Expected a statement of the form:", pslErrors.color_token(' '.join(defSyntax.tokens))]))
        equalityIndex = stmt.tokens.index('=')
        defs = zip(stmt.tokens[equalityIndex+1:], stmt.lineNums[equalityIndex+1:])
        for token, lineNum in reversed(defs):
            if pairComplete and token == ',':
                pairComplete = False
                continue
            elif pairComplete:
                lastDef = node.children[-1]
                lastDefTokens = [lastDef.children[0], ':=']
                lastDefTokens.extend([token.get_token() for token in lastDef.children[1]])
Joy Mitra's avatar
Joy Mitra committed
1305
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNum),
1306
                    "Missing comma before definition:", ' '.join(lastDefTokens)]))
1307
            elif token == ',' and colonEqualsFound:
Joy Mitra's avatar
Joy Mitra committed
1308
                raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNum),
1309
                    "Missing identifier for term: ", ' '.join([token.get_token() for token in term]) + "."]))
1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320
            if colonEqualsFound:
                roleName = token
                node.children.append(DefPair(node, children=[roleName, list(reversed(term))], lineNum=lineNum))
                term = []
                colonEqualsFound = False
                pairComplete = True
            elif token == ':=':
                colonEqualsFound = True
            else:
                term.append(Token(node, [token], lineNum))
        if colonEqualsFound:
Joy Mitra's avatar
Joy Mitra committed
1321
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNum),
1322
                "Missing identifier for term: ", ' '.join([token.get_token() for token in term]) + "."]))
1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340
        return node

    def translate(self):
        return []

    def def_set(self):
        """
        Returns the maude term representing the set of definition pairs associated with this def decl.
        """
        return ', '.join([child.def_elem() for child in self.children[1:]])

    def def_pairs(self):
        """
        Returns the list of PSL Tree node objects that represent definition pairs.
        Note that the first child is the role associated with these definitions.
        """
        return self.children[1:]

Joy Mitra's avatar
Joy Mitra committed
1341

1342 1343 1344 1345 1346 1347
class DefPair(Node):
    """
    A DefPair encodes a term of the form I := T, where I is an identifier (token), and T is a user-level term.
    The children are the string I, and a list of the tokens in T.
    """

Joy Mitra's avatar
Joy Mitra committed
1348
    @staticmethod
1349 1350 1351 1352 1353 1354 1355 1356
    def parse(stmt, parent):
        """
        Don't actually need to use this.
        """
        raise NotImplementedError()

    def role(self):
        return self.parent.role()
Joy Mitra's avatar
Joy Mitra committed
1357

1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389
    def translate(self):
        """
        Not used, because defs show up outside the specification term.
        """
        return []

    def def_elem(self):
        return self.children[1] + ' := ' +  ' '.join([token.get_token() for token in self.children[2]])

    def shorthand(self):
        """
        Returns the identifier used as shorthand by the def as a string.
        """
        return self.children[0]

    def term(self):
        """
        Returns the (translated) term represented by the shorthand as a string.
        """
        term = []
        for token in self.children[1]:
            term.extend(token.translate())
        return ' '.join(term)


class StepStmt(PSLStmtNode):

    className = "Step Statement"

    def class_name(self):
        return StepStmt.className

Joy Mitra's avatar
Joy Mitra committed
1390
    @staticmethod
1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411
    def parse(stmt, parent):
        node = StepStmt(parent=parent)
        node.op, node.children, node.lineNum = node._parse(stmt, stepSyntax)
        return node

    def get_step_number(self):
        return self.children[0].value()

    def error_check(self):
        errors = self.disjoint_vars()
        errors.extend(self.no_new_vars_in_sent_msgs())
        if errors:
            raise pslErrors.StepError('\n'.join(errors))

    def disjoint_vars(self):
        """
        Let A and B be the roles in this step, where
        A is the sender and B is the receiver. Let
        t_a be the term sent by A, and t_b be the
        term received by B.
        Then, this function checks to make sure
Joy Mitra's avatar
Joy Mitra committed
1412 1413
        vars(t_a) and vars(t_b) are disjoint from the
        vars of
1414
        every other role in this and all previous steps,
Joy Mitra's avatar
Joy Mitra committed
1415 1416
        with the exception of variables declared as
        input.
1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430
        """
        roleMap = self.parent.variables_per_role()
        declaredVars = self.parent.declared_variables()
        roleTermPairs = [(self.children[FIRST_ROLE_INDEX], self.children[FIRST_TERM_INDEX]), (self.children[SECOND_ROLE_INDEX], self.children[SECOND_TERM_INDEX])]
        errors = []
        checkedRoles = []
        for role, term in roleTermPairs:
            checkedRoles.append(role.role_name())
            inVars = set(roleMap[role.role_name()])
            otherStmtVars = self.parent.statement_vars(self.get_step_number())
            otherStmtVars = {roleName:otherStmtVars[roleName] for roleName in otherStmtVars if roleName not in checkedRoles}
            for var in [token.get_token() for token in term.get_tokens() if token.get_token() in declaredVars]:
                for roleName in otherStmtVars:
                    if var in otherStmtVars[roleName] and var not in inVars:
Joy Mitra's avatar
Joy Mitra committed
1431
                        errorMsg = ' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Variable", pslErrors.color_token(var.strip()),
1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456
                            "appears in the protocol terms of roles",
                            pslErrors.color_token(roleName), "and", pslErrors.color_token(role.role_name()) + ".",
                            "Variables must be disjoint between roles, with the possible exception of In(put) variables."])
                        if errorMsg not in errors:
                            errors.append(errorMsg)
        return errors

    def no_new_vars_in_sent_msgs(self):
        """
        Checks to make sure the sent message t in
        this step does not introduce any new variables.
        All variables in t were either declared in this
        role's input, or showed up in a previous
        message received by the sender.
        """
        senderRoleName = self.children[FIRST_ROLE_INDEX].role_name()
        inVars = set(self.parent.variables_per_role()[senderRoleName])
        statementVars = self.parent.statement_vars(self.get_step_number()-1)
        if statementVars:
            senderVars = statementVars[senderRoleName]
        else:
            senderVars = []
        sentTerm = ' '.join([token.get_token() for token in self.children[FIRST_TERM_INDEX].tokens()])
        sentTermVars = self.statement_vars()[senderRoleName]
        errors = []
1457
        freshVars = [var for (var, sort) in self.get_root().get_protocol().var_name_sort_mapping().iteritems() if sort == "Fresh"]
1458
        for var in sentTermVars:
1459
            if var not in inVars and var not in senderVars and var not in freshVars:
Joy Mitra's avatar
Joy Mitra committed
1460
                errors.append(' '.join([pslErrors.error, pslErrors.color_line_number(self.lineNum), "Variable", pslErrors.color_token(var), "appears in neither",
1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517
                    pslErrors.color_token(''.join(['In(', senderRoleName, ')'])), "nor in the previous received terms of", pslErrors.color_token(senderRoleName) + "."]))
        return errors

    def statement_vars(self):
        """
        Returns a mapping from role names (as strings) to the variables (as strings) that appear in that role.
        """
        firstRole = self.children[FIRST_ROLE_INDEX].role_name()
        secondRole = self.children[SECOND_ROLE_INDEX].role_name()
        declaredVars = self.get_root().get_protocol().declared_variables()
        firstRoleTokens = [token.get_token() for token in self.children[FIRST_TERM_INDEX].tokens()]
        secondRoleTokens = [token.get_token() for token in self.children[SECOND_TERM_INDEX].tokens()]
        firstRoleVars = [token for token in firstRoleTokens if token in declaredVars]
        secondRoleVars = [token for token in secondRoleTokens if token in declaredVars]
        return {firstRole:firstRoleVars, secondRole:secondRoleVars}


class Intruder(PSLSection):

    className = "Intruder"

    def class_name(self):
        return Intruder.className

    @staticmethod
    def parse(stmts, parent):
        root = Intruder(parent=parent)
        #Possible beginnings of each statement:
        #1. TermList
        #2. =>
        keywordStarts = [syntax for syntax in intrSyntax + varSyntax if syntax.tokens[0] != '_']
        underscoreStart = [intrSyntax[0], intrSyntax[2]]
        for stmt in stmts:
            for stmtType in keywordStarts:
                if stmt.tokens[0] == stmtType.tokens[0]:
                    root.children.append(stmtType.stmtNode.parse(stmt, root))
                    break
            else:
                stmtType = underscoreStart[0]
                try:
                    root.children.append(stmtType.stmtNode.parse(stmt, root))
                except pslErrors.SyntaxError:
                    stmtType = underscoreStart[1]
                    root.children.append(stmtType.stmtNode.parse(stmt, root))
        return root

    def error_check(self):
        pass


class IntrStmt(PSLStmtNode):

    className = "Intruder Statement"

    def class_name(self):
        return IntrStmt.className

Joy Mitra's avatar
Joy Mitra committed
1518
    @staticmethod
1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584
    def parse(stmt, parent):
        node = IntrStmt(parent=parent)
        if '=>' == stmt.tokens[0]:
            syntax = intrSyntax[1]
        elif '=>' in stmt.tokens:
            syntax = intrSyntax[0]
        elif '<=>' in stmt.tokens:
            syntax = intrSyntax[2]
        else:
            raise pslErrors.SyntaxError(' '.join([pslErrors.error, pslErrors.color_line_number(stmt.lineNums[0]), "Invalid intruder statement. Expected a statement of one of the following forms:",
                '\n'.join(pslErrors.color_token(' '.join(syntax.tokens)) for syntax in intrSyntax)]))
        node.op, node.children, node.lineNum = node._parse(stmt, syntax)
        return node

    def error_check(self):
        pass


class Attacks(PSLSection):

    className = "Attacks"

    def class_name(self):
        return Attacks.className

    @staticmethod
    def parse(stmts, parent):
        attPatternStmts = []
        node = Attacks(parent=parent)
        previousAttackNum = None
        for stmt in stmts:
            try:
                attackNum = int(stmt.tokens[0])
            except ValueError:
                attPatternStmts.append(stmt)
            else:
                if attPatternStmts:
                    node.children.append(AttPattern.parse(attPatternStmts, node, previousAttackNum))
                previousAttackNum = attackNum
                attPatternStmts = []
        if attPatternStmts:
            node.children.append(AttPattern.parse(attPatternStmts, node, attackNum))
        return node

    def declared_variables(self):
        """
        The declared variables of the attack section consists solely of the declared variables in the protocol section.
        """
        return self.parent.get_protocol().declared_variables()

    def var_name_sort_mapping(self):
        return self.parent.get_protocol().var_name_sort_mapping()

    def error_check(self):
        """
        Checks to make sure none of the attack patterns have the same number.
        """
        seenNumbers = {}
        for child in self.children:
            try:
                alreadyDeclaredLineNum = seenNumbers[child.attackNum]
            except KeyError:
                seenNumbers[child.attackNum] = child.lineNum
            except AttributeError:
                pass
            else:
Joy Mitra's avatar
Joy Mitra committed
1585
                raise pslErrors.TranslationError([' '.join([pslErrors.error, pslErrors.color_line_number(child.lineNum), "Attack pattern", pslErrors.color_token(str(child.lineNum)),
1586