psl.py 37 KB
Newer Older
Joy Mitra's avatar
Joy Mitra committed
1
#!/usr/bin/python
2 3 4 5
"""
Maude-PSL, Version: [1.0] [May 15th 2015]
Copyright (c) 2015, University of Illinois
All rights reserved.
Joy Mitra's avatar
Joy Mitra committed
6
Redistribution and use in source and binary forms, with or without modification,
7
are permitted provided that the following conditions are met:
Joy Mitra's avatar
Joy Mitra committed
8
* Redistributions of source code must retain the above copyright notice,
9
this list of conditions and the following disclaimer.
Joy Mitra's avatar
Joy Mitra committed
10 11
* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
12
and/or other materials provided with the distribution.
Joy Mitra's avatar
Joy Mitra committed
13 14
* 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
15
specific prior written permission.
Joy Mitra's avatar
Joy Mitra committed
16 17 18 19 20
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
21
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
Joy Mitra's avatar
Joy Mitra committed
22 23
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
24 25 26
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
27 28 29
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
30
of the Navy ("GOVERNMENT") under Title 17, U.S. Code. All Other Rights Reserved.
Joy Mitra's avatar
Joy Mitra committed
31 32 33 34
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
35
supporting documentation.
Joy Mitra's avatar
Joy Mitra committed
36 37
GOVERNMENT ALLOWS FREE USE OF THIS SOFTWARE IN ITS "AS IS" CONDITION AND
DISCLAIM ANY LIABILITY OF ANY KIND FOR ANY DAMAGES WHATSOEVER RESULTING
38
FROM THE USE OF THIS SOFTWARE.
Joy Mitra's avatar
Joy Mitra committed
39 40
GOVERNMENT requests users of this software to return modifications,
improvements or extensions that they make to:
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

48 49 50 51 52 53 54 55 56
from __future__ import print_function
import itertools
import pslErrors
import pslTree
import re
import subprocess
import sys
import os
#I was  going to use this to improve some of the error messages, but I haven't had time to write awesome messages.
Joy Mitra's avatar
Joy Mitra committed
57
#However, if I import this, it always prints a warning about using the slow fuzzy match. While that doesn't affect
58 59 60 61 62 63 64
#the running of the program, it is mildly annoying.
#from fuzzywuzzy import fuzz

"""
    Note: If at any time an error has a line number of -1, this means that
    there was a problem with some automatically generated code, in which case
    there's an error that I missed while performing initial error checking.
Joy Mitra's avatar
Joy Mitra committed
65

66 67
    To use: type the command ./psl.py FILENAME.psl
    Options:
Joy Mitra's avatar
Joy Mitra committed
68 69 70 71 72
        -m PATH/TO/MAUDE/EXECUTABLE use to specify the path to the maude
        executable you'd like to use. If option not provided, defaults to just
        using the 'maude' command. We'll probably have additional options for
        such things as loading the specification directly into the maude-npa,
        choosing a different version of maude, choosing other maude files to
73 74 75 76 77
        load into maude, etc, but that's a task for the future.

    Some of the errors that the Python code needs to check for include:
    0. Make sure parenthesis are balanced. done
    1. make sure that every In has accompanying Out and
Joy Mitra's avatar
Joy Mitra committed
78
        strand execution statements. So, if there's a single term left, it
79
        won't be an In.
Joy Mitra's avatar
Joy Mitra committed
80

81
    2. Make sure the subsort keywords and the < are correct
Joy Mitra's avatar
Joy Mitra committed
82 83
    3. Check the high-level syntax.
        a. Make sure that there are no illegal operators:
84 85 86 87 88 89 90 91 92 93
                i. _,_
                ii. _|->_
                iii. _._
                iv. In, Out, Def.
                v. anything containing a $.
                vi. _=>_
                vii. _executes protocol
                viii. Intruder learns_
                ix. without:
                x. _|-_
Joy Mitra's avatar
Joy Mitra committed
94 95 96
                xi. Any operator containing unbalanced parenthesis or curly
                braces Basically, we assume that the user-defined syntax is
                disjoint from
97 98 99
                anything that starts a new statement, because it simplifies
                checking for missing periods, and from anything that appears
                next to user-defined terms
Joy Mitra's avatar
Joy Mitra committed
100
                in order to avoid ambiguities with the high-level syntax.
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
                Note: This may be more restrictive than necessary, but we can
                relax these requirements later.

    QUESTION: Do we want to declare the macros globally, since ostensibly
    they could show up anywhere?
"""

#TODO: Replace the role names with NAME_OF_MODULE-ROLENAME, and add
#NAME_OF_MODULE-ROLENAME as constants of sort Role to the theory.
#Also, for composition, automatically replace the role names with the same
#generated constant.

#Terms are "blackboxes" of user-defined syntax. For simplicity, we assume
#that all tokens in the user defined syntax are disjoint from all tokens
#in the higher-level syntax.
#We may be able to relax this restriction, depending on how much I actually
#need to know at the parser level.


MAUDE_DEFAULT = 'maude'

MAUDE_FAN = '/Users/fan/Documents/maude/maude.darwin64'

Joy Mitra's avatar
Joy Mitra committed
124
MAUDE_COMMAND = './maude27'
125 126 127 128 129 130 131 132 133 134
NO_PRELUDE = '-no-prelude'
PRELUDE = 'prelude.maude'
FULL_MAUDE = 'full-maude.maude'
#MAUDE_COMMAND = 'maude'

NPA_SYNTAX = 'NPA-Syntax.maude'
TRANSLATION_FILE = 'psl.maude'

CODE = 0
LINE_NUM = 1
Joy Mitra's avatar
Joy Mitra committed
135
STATE_SPACE_REDUCTION_VARIANTS = ['state-space-reduction:', 'State-space-reduction:']
136 137 138 139
END_LINE = ['.', 'without:', 'Without:', 'avoid:', 'Avoid:'] + STATE_SPACE_REDUCTION_VARIANTS

def nonzero_nats():
    """
Joy Mitra's avatar
Joy Mitra committed
140
    A generator that yields as many natural numbers as you need (up to
141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161
    physical limitations).
    """
    count = 1
    while True:
        yield count
        count += 1


def number_lines(lines):
    """
    Given an iterable of PSL lines, returns an iterable of pairs pairing
    each line with its line number.
    """
    return zip(lines, nonzero_nats())



def pairwise(iterable):
    """
    Given an iterable: [m_1, m_2, ..., m_n] returns a list of pairs:
    [(m_1, m_2), (m_2, m_3), ...(m_{n-1}, m_n), (m_n, m_n)].
Joy Mitra's avatar
Joy Mitra committed
162
    If n == 1, then it returns the list [(m_1, m_1)]. If n == 0, then it
163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182
    returns an empty list.
    """
    listIt = list(iterable)
    try:
        result = zip(listIt, listIt[1:]) + [(listIt[-1], listIt[-1])]
    except IndexError:
        result = []
    return result



singleLineComment = re.compile(r'//.*$')
startSpec = re.compile(r'spec \S+ is')

def lex_code(pslFile):
    """
    Given an iterable of lines of PSL code, returns a dictionary mapping
    section names to lists of statements.
    """
    sectionStmts = {heading:[] for heading in pslTree.SECTION_HEADINGS}
Joy Mitra's avatar
Joy Mitra committed
183
    numberedLines = [(tokenize(line), num) for line, num in
184 185
            number_lines(pslFile)]
    statement = pslTree.Statement()
Joy Mitra's avatar
Joy Mitra committed
186
    #List of pairs of comment token with line number.
187 188 189 190
    startComment = []
    errorMsgs = []
    for i in range(len(numberedLines)):
        line, num = numberedLines[i]
191 192
        for j in range(len(line)):
            token = line[j].strip()
193
            try:
194
                nextToken = line[j+1]
195 196 197 198 199 200 201 202 203 204 205 206 207 208 209
            except IndexError:
                try:
                    nextToken = numberedLines[i+1][0][0]
                except IndexError:
                    nextToken = nextNextToken = ''
                else:
                    try:
                        nextNextToken = numberedLines[i+1][0][1]
                    except IndexError:
                        try:
                            nextNextToken = numberedLines[i+2][0][0]
                        except IndexError:
                            nextNextToken = ''
            else:
                try:
210
                    nextNextToken = line[j+2]
211 212 213 214 215 216 217 218 219
                except IndexError:
                    try:
                        nextNextToken = numberedLines[i+1][0][0]
                    except IndexError:
                        nextNextToken = ''
            if token == r'/*':
                startComment.append((token, num))
            elif token == r'*/':
                try:
Joy Mitra's avatar
Joy Mitra committed
220
                    if startComment[-1][0] == r'/*':
221 222
                        startComment = startComment[:-1]
                        continue
Joy Mitra's avatar
Joy Mitra committed
223
                    else:
224 225
                        raise IndexError()
                except IndexError:
Joy Mitra's avatar
Joy Mitra committed
226 227 228
                    raise errorMsgs.append(' '.join([pslErrors.error,
                        pslErrors.color_line_number(num),
                        "Unexpected end comment token:",
229
                        pslErrors.color_token(token)]))
Joy Mitra's avatar
Joy Mitra committed
230
            if startComment or re.match(singleLineComment, token):
231 232 233 234 235
                continue
            elif not sectionStmts['Start'] and re.match(startSpec, token):
                stmt = pslTree.Statement([token], [num])
                sectionStmts["Start"].append(stmt)
                continue
Joy Mitra's avatar
Joy Mitra committed
236
            elif is_start_of_section(token, nextToken):
237 238 239 240 241
                section = token
            elif token in END_LINE and not protocol_step(nextToken, nextNextToken):
                statement.append(token, num)
                sectionStmts[section].append(statement)
                statement = pslTree.Statement()
Joy Mitra's avatar
Joy Mitra committed
242
            else:
243 244
                statement.append(token, num)
    for token, num in startComment:
Joy Mitra's avatar
Joy Mitra committed
245
       errorMsgs.append(' '.join([pslErrors.error, pslErrors.color_line_number(num),
246 247 248 249 250 251
           "Dangling comment token:", pslErrors.color_token(token)]))
    if errorMsgs:
        raise pslErrors.LexingError('\n'.join(errorMsgs))
    #Removes some unnecessary end of comment statements that are still floating around.
    for key in sectionStmts:
        for stmt in sectionStmts[key]:
Joy Mitra's avatar
Joy Mitra committed
252
            stmt.tokens = [token for token in stmt.tokens if token != '*/']
253 254 255 256
    return sectionStmts


def protocol_step(nextToken, nextNextToken):
257 258 259 260
    """
    Returns true if nextToken and nextNextToken correspond to what's expected as the second and third tokens in a protocol
    step. This is important to distinguish between statement terminating periods, and the periods in each protocol step statement.
    """
261 262 263 264 265 266 267
    try:
        return nextNextToken == '->' and nextToken not in pslTree.TOP_LEVEL_TOKENS
    except IndexError:
        return False


def type_check_sectionStmts(sectionStmts):
268 269 270
    """
    Checks to make sure that the statements in each section are in fact statement objects. For debugging purposes only.
    """
271 272 273 274 275 276
    for section in sectionStmts:
        for statement in sectionStmts:
            assert(isinstance(statement, pslTree.Statement)), "statement is not a pslTree.Statement: %s" % statement


def tokenize(line):
277 278 279
    """
    Splits the passed PSL line into a list of tokens, and returns those tokens.
    """
280 281 282 283
    return [token for token in re.split(pslTree.Token.tokenizer, line.strip()) if token]


def is_start_of_section(token, nextToken):
Joy Mitra's avatar
Joy Mitra committed
284
    return token in pslTree.SECTION_HEADINGS and (token != 'Intruder' or
285 286 287 288 289 290 291 292 293 294 295
            nextToken != 'learns')


def maudify():
    """
    Given a pslFilePath, and a set of conversion options(TBD), converts the PSL
    file specification into a Maude-NPA specification.  options:
         -m Allows you to specify a path to the maude executable you'd like
                         to execute
        The steps to doing this are:
        1. Error check the high level syntax.
Joy Mitra's avatar
Joy Mitra committed
296
        2. Annotate the file with line numbers, and wrap the specification in
297 298
        parenthesis
        3. Feed the annotated file into Maude, along with the Maude
Joy Mitra's avatar
Joy Mitra committed
299
        conversation file.
300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319
    """
    try:
        pslFilePath = sys.argv[1]
    except IndexError:
        print("Usage: ./psl.py FILENAME.psl")
        return
    try:
        options = sys.argv[2:]
    except IndexError:
        pass
    else:
        for option, argument in zip(options, options[1:]):
            if option == "-m":
                global MAUDE_COMMAND, PRELUDE
                MAUDE_COMMAND = argument
                NO_PRELUDE = ''
                PRELUDE = ''
    fileName = os.path.basename(pslFilePath).split('.')[0]
    with open(pslFilePath, 'r') as f:
        parseTree = parse_code(lex_code(f))
Joy Mitra's avatar
Joy Mitra committed
320
    theoryFileName = build_theory(parseTree, os.path.dirname(pslFilePath), fileName)
321
    #TODO: Need to invoke different functions depending on whether we're doing protocol composition, or normal PSL translation.
Joy Mitra's avatar
Joy Mitra committed
322
    intermediate = gen_intermediate(parseTree, theoryFileName)
323
    gen_NPA_code(intermediate, theoryFileName, parseTree)
324 325 326 327 328 329 330 331 332 333

DEF_KEY_ROLE = 0
DEF_KEY_TERM = 1
DEF_SHORTHAND = 0
DEF_LINE_NUM = 1
def gen_intermediate(parseTree, theoryFileName):
    """
    Generates the maude code needed to translate a PSL specification into a trio of Maude-NPA module.
    Returns the code as a list of lines.
    """
Joy Mitra's avatar
Joy Mitra committed
334
    code = ['load psl.maude', ' '.join(['load', theoryFileName]), 'mod INTERMEDIATE is', 'protecting TRANSLATION-TO-MAUDE-NPA .',
335 336 337 338 339 340 341 342
            'protecting PROTOCOL-EXAMPLE-SYMBOLS .']
    defPairs = []
    for defNode in parseTree.get_protocol().get_defs():
        defPairs.extend(defNode.def_pairs())
    defMap = {}
    for defPair in defPairs:
        if (defPair.role(), defPair.term()) in defMap:
            otherDef = defMap[(defPair.role(), defPair.term())]
Joy Mitra's avatar
Joy Mitra committed
343 344 345
            raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(defPair.lineNum) + ",",
                otherDef[DEF_LINE_NUM], "Term", pslErrors.color_token(defPair.term()),
                "has multiple shorthands: ", pslErrors.color_token(defPair.shorthand()) + ",",
346 347 348
                pslErrors.color_token(otherDef[DEF_SHORTHAND])]))
        else:
            defMap[(defPair.role(), defPair.term())] = (defPair.shorthand(), defPair.lineNum)
349
    shorthandSortMap = compute_sorts(defMap, theoryFileName, parseTree)
350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365
    code.extend([' '.join(['op', shorthand, ':', '->', sort, '.']) for shorthand, sort in shorthandSortMap.items()])
    code.append('endm')
    code.append('rew')
    code.extend(['Specification', '{'])
    protocol = parseTree.get_protocol()
    code.extend(stmt for stmt in protocol.translate() if stmt)
    intruder = parseTree.get_intruder()
    code.extend([stmt for stmt in intruder.translate() if stmt])
    attacks = parseTree.get_attacks()
    code.extend([stmt for stmt in attacks.translate() if stmt])
    code.append('}')
    #Empty StrandData for protocols
    code.append('[mt]')
    #Empty strand set for intruders
    code.append('[empty]')
    if defMap:
Joy Mitra's avatar
Joy Mitra committed
366
        defs = ', '.join([' '.join([''.join(['(', shorthandLineNum[DEF_SHORTHAND], ', ', str(shorthandLineNum[DEF_LINE_NUM]), ')']), ':=',
367 368 369
            roleTermPair[DEF_KEY_TERM]]) for roleTermPair, shorthandLineNum in defMap.items()])
    else:
        defs = '$noDefs'
370
    code.append(' '.join(['[', '$makeIdem($checkWellFormed(', defs, '))', ']']))
371 372 373
    code.append('.')
    return code

374
def gen_NPA_code(maudeCode, theoryFileName, parseTree):
Joy Mitra's avatar
Joy Mitra committed
375
    maudeCommand = [MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX, theoryFileName,
376
            TRANSLATION_FILE]
377
    print(maudeCommand)
Joy Mitra's avatar
Joy Mitra committed
378
    maudeExecution = subprocess.Popen(maudeCommand, stdout=subprocess.PIPE,
379 380 381 382
        stdin=subprocess.PIPE, stderr=subprocess.PIPE)
    stdout, stderr = maudeExecution.communicate('\n'.join(maudeCode))
    if stderr:
        errors = []
383
        #Expected error pattern:
Joy Mitra's avatar
Joy Mitra committed
384
        #Warning: <standard input>, line N : <error message>
385
        for line in [line.strip() for line in stderr.split('\n') if line.strip()]:
386 387
            try:
                _,lineNum, error = line.split(':')
Joy Mitra's avatar
Joy Mitra committed
388
                print(line)
389 390 391
            except ValueError:
                print(stderr)
                assert False
392
            #expected pattern currently in lineNum:
393 394 395 396
            #<standard input>, line N
            lineNum = int(lineNum.split()[-1])
            #Maude's lines on the terminal start counting from 1, but Python lists start counting at 0.
            pslLine = maudeCode[lineNum-1]
397
            #pattern of psl statements inside Maude code
Joy Mitra's avatar
Joy Mitra committed
398
            #blah blah . [ num ]
399 400
            try:
                pslLineNum = int(pslLine.split()[-2])
Joy Mitra's avatar
Joy Mitra committed
401
            except (IndexError, ValueError):
402 403 404
                pass
            else:
                bracketIndex = pslLine.rfind('[')
Joy Mitra's avatar
Joy Mitra committed
405
                errors.append(' '.join([pslErrors.error, pslErrors.color_line_number(pslLineNum), error, "\n\tCode: ",
406 407 408 409 410 411 412 413 414 415 416 417 418 419 420
                    pslLine[:bracketIndex]]))
        raise pslErrors.SyntaxError('\n'.join(errors))
    else:
        #rewrite in <module-name> : Maude term
        #rewrites: blah blah
        #result ModuleNPA: maude module (if things go right)
        #result [ModuleNPA] : vomit (if things go wrong)
        #command, _, result = [line.replace("Maude>", "") for line in stdout.split('\n')]
        #_, sortName = result[:result.index(':')
        desiredResult = "result ModuleNPA:"
        try:
            index = stdout.index(desiredResult) + len(desiredResult)
        except ValueError:
            errorResult = "result [TranslationData]:"
            errorIndex = stdout.index(errorResult) + len(errorResult)
421
            process_error(stdout[errorIndex:], parseTree)
422 423 424 425 426 427 428
        else:
            endOfModule = stdout.rfind("Maude>")
            module = '\n' + stdout[index:endOfModule].strip()
            with open(theoryFileName, 'a') as maudeFile:
                maudeFile.write(module)
                maudeFile.write('\nselect MAUDE-NPA .')

429
def process_error(error, parseTree):
430
    """
Joy Mitra's avatar
Joy Mitra committed
431
    Given a partially evaluated PSL specification, extracts the offending error term, and extracts from the error term the information
432 433
    need for a usable error message. Then raises a TranslationError containing said usable error message.
    """
434 435 436
    try:
        errorTermStart = error.index("$$$")
    except ValueError as e:
Joy Mitra's avatar
Joy Mitra committed
437
        raise ValueError(error)
438 439 440 441 442 443 444 445 446 447 448 449 450 451
    errorType, errorTerm = error[errorTermStart:].split('(', 1)
    numParens = 1
    endOfTerm = compute_end_of_term(errorType, errorTerm)
    errorTerm = errorTerm[:endOfTerm]
    if errorType == "$$$infiniteIdem":
        invalidMapping, lineNumbers = errorTerm.rsplit(',', 1)
        lineNumbers = [number.strip() for number in lineNumbers.split(':')]
        raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(','.join(lineNumbers)),
            "The substitution: ", invalidMapping, "cannot be made idempotent."]))
    elif errorType.strip() == "$$$malformedDefs":
        errorDefs = []
        for error in errorTerm.split("$$;;;;$$"):
            pair, lineNumber = error.split("$$,$$")
            lineNumber = lineNumber.replace(")", '')
Joy Mitra's avatar
Joy Mitra committed
452
            errorDefs.append(' '.join([pslErrors.error, pslErrors.color_line_number(lineNumber.strip()),
453 454 455
                                         #Stripping off the () around the definition
                "Malformed Definition:", pslErrors.color_token(pair[1:-1])]))
        raise pslErrors.TranslationError('\n'.join(errorDefs))
456 457 458
    elif errorType.strip() == "$$$malformedTerm":
        errorTerm, lineNumber =  errorTerm.rsplit(',', 1)
        raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNumber.strip()), "Malformed term:", errorTerm]))
459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478
    elif errorType.strip() == "$$$notAFunction":
        errorMappings = errorTerm.split("$$$;;;$$$")
        errorMsg = []
        for error in errorMappings:
            var, results = [string.strip() for string in error.split('|->')]
            problemTerms = []
            lineNumbers = []
            for result in [r.strip() for r in results.split('}$') if r.strip()]:
                result = result.replace('${', '')
                startLineNum = result.rindex(';')+1
                lineNumber = result[startLineNum:].strip()
                result = result[:startLineNum-1].strip()
                problemTerms.append(result)
                lineNumbers.append(lineNumber)
            errorMsg.append(''.join([pslErrors.errorNoLine, " Substitution does not",
                " define a function. Variable: ", pslErrors.color_token(var),
                " maps to the terms:\n\t", '\n\t'.join([' Line: '.join([
                    pslErrors.color_token(term),
                    pslErrors.color_line_number(lineNum)]) for term, lineNum
                    in zip(problemTerms, lineNumbers)])]))
Joy Mitra's avatar
Joy Mitra committed
479
        raise pslErrors.TranslationError('\n'.join(errorMsg))
480
    elif errorType.strip() == "$$$invalidSorting":
481 482 483 484 485 486
        var, termLineNum = [s.strip() for s in errorTerm.split('|->')]
        var, variableSort = var.split(':')
        termLineNum = termLineNum.replace('${', '').replace('}$', '')
        lineNumberIndex = termLineNum.rindex(';')+1
        lineNum = termLineNum[lineNumberIndex:].strip()
        term = termLineNum[:lineNumberIndex-1].strip()
Joy Mitra's avatar
Joy Mitra committed
487 488 489
        raise pslErrors.TranslationError(' '.join([pslErrors.error,
            pslErrors.color_line_number(lineNum), "Variable",
            pslErrors.color_token(var), "has sort",
490 491 492
            pslErrors.color_token(variableSort), "but term",
            pslErrors.color_token(term), "does not."]))

493 494 495 496 497 498




def compute_end_of_term(errorType, errorTerm):
    """
Joy Mitra's avatar
Joy Mitra committed
499
    Given the start of term that contains the errorTerm as a subterm (and which starts with the first argument of the error term),
500 501 502 503 504 505 506 507 508 509 510 511 512 513
    finds the index of the end of the error term (i.e. the closing parenthesis) and returns that index.
    If a closing parenthesis is not found, a ValueError is raised.
    """
    endOfTerm = 0
    numParens = 1
    for character in errorTerm:
        if character == '(':
            numParens += 1
        elif character == ')':
            numParens -= 1
            if not numParens:
                return endOfTerm
        endOfTerm += 1
    raise ValueError(' '.join(["End of error term of type: ", errorType, "not found when trying to extract the term from:", errorTerm]))
Joy Mitra's avatar
Joy Mitra committed
514

515
MAX_ITERATIONS = 100
516
def compute_sorts(defMap, syntaxFileName, parseTree):
517
    """
Joy Mitra's avatar
Joy Mitra committed
518 519
    Computes the sorts of the user-defined shorthand.

520
    defMap is expected to be a dictionary with the following format:
Joy Mitra's avatar
Joy Mitra committed
521 522
    (role, term) : (shorthand, lineNumber)
    where term is the term whose sort is to be computed, shorthand is the user-defined shorthand, and line number is the line number in
523 524 525 526 527 528
    PSL at which the term appears.
    pslSyntaxFileName is the name of the maude file that contains the user-defined syntax (this is the partially filled file containing the translated NPA code).

    Returns a dictionary mapping shorthand to their respective sorts.
    """
    is_function(defMap)
529
    role_variables_correct(defMap, parseTree)
530 531 532 533 534 535 536 537 538
    SHORTHAND = 0
    LINE_NUMBER = 1
    ROLE = 0
    TERM = 1
    termRolePairs = sorted(defMap.keys(), key=lambda pair: defMap[pair][DEF_LINE_NUM])
    #Note: We need to split the shorthand mappings into shorthand we can figure out (i.e. shorthand that doesn't depend on other
    #shorthand, and shorthand that does. Then we iteratively grow the shorthand that doesn't depend on others as we compute the
    #sorts of the indepedent shorthand, until we've computed the sorts of all the shorthand.
    shorthand = {shorthand for shorthand, lineNumber in defMap.values()}
539
    dependentShorthand = {(role, term):shorthandLineNum for ((role, term), shorthandLineNum) in defMap.iteritems() if
540 541 542 543 544 545 546 547 548
        set(term.split()).intersection(shorthand)}
    independentShorthand = {roleTerm:defMap[roleTerm] for roleTerm in defMap if not roleTerm in dependentShorthand}
    knownShorthand = dict()
    knownShorthand = sorts_independent_shorthand(independentShorthand, knownShorthand, syntaxFileName)
    previousShorthand = {}
    while dependentShorthand and dependentShorthand != previousShorthand:
        independentShorthand = {(role, term):shorthandLineNum for (role, term), shorthandLineNum in dependentShorthand.iteritems()
            if set(term.split()).intersection(shorthand) <= set(knownShorthand.keys())}
        previousShorthand = dependentShorthand
Joy Mitra's avatar
Joy Mitra committed
549
        dependentShorthand = {(role, term):shorthandLinenum for (role, term), shorthandLinenum in
550 551 552 553 554 555 556
                dependentShorthand.iteritems() if not set(term.split()).intersection(shorthand) <= set(knownShorthand.keys())}
        for shorthand, sort in sorts_independent_shorthand(independentShorthand, knownShorthand, syntaxFileName).iteritems():
            assert not shorthand in knownShorthand, "Internal Error: It seems that our defMap is not a function like it's supposed to be: %s\n%s\n" % (
                    str(knownShorthand), str(shorthand))
            knownShorthand[shorthand] = sort
        newlyIndependentShorthand = sorts_independent_shorthand(independentShorthand, knownShorthand, syntaxFileName)
        for key, value in newlyIndependentShorthand.iteritems():
Joy Mitra's avatar
Joy Mitra committed
557
            assert key not in knownShorthand or knownShorthand[key] == value, "Internal Error: Disagreement on shorthand: %s\n%s\n%s\n" % (str(key),
558 559 560
                    str(value), str(knownShorthand))
            knownShorthand[key] = value
    if dependentShorthand:
Joy Mitra's avatar
Joy Mitra committed
561
        raise pslErrors.TranslationError([pslErrors.error, pslErrors.color_line_number(', '.join([lineNum for (shorthand, lineNum) in
562 563 564 565 566 567 568
            dependentShorthand])), "Shorthand dependencies cannot be resolved: ", ' '.join([' '.join([shorthand, ":=", term]) for
                ((role, term), (shorthand, lineNum)) in dependentShorthand.iteritems])])
    else:
        return knownShorthand

def sorts_independent_shorthand(independentShorthand, knownShorthand, syntaxFileName):
    """
Joy Mitra's avatar
Joy Mitra committed
569
    Given a mapping from (role, term) to (shorthand, lineNumber), and a mapping of all shorthand appearing in each "term" to their
570 571 572 573
    respective
    sorts, returns a mapping of all shorthand in independentShorthand to their respective sorts.
    """
    maudeCmds = (["fmod SHORTHAND is", "protecting PROTOCOL-EXAMPLE-SYMBOLS ."] +
Joy Mitra's avatar
Joy Mitra committed
574
                [' '.join(['op', shorthand, ':', '->', sort, '.']) for (shorthand, sort) in knownShorthand.iteritems()] +
575 576
                ["endfm"])
    maudeCmds += [' '.join(['parse', termRolePair[DEF_KEY_TERM], '.']) for termRolePair in independentShorthand.keys()] + ['q']
Joy Mitra's avatar
Joy Mitra committed
577
    maudeExecution = subprocess.Popen([MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX,
578 579 580 581 582 583 584 585 586 587 588 589 590 591
        syntaxFileName], stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
    stdout, stderr = maudeExecution.communicate('\n'.join(maudeCmds))
    #Print any maude errors
    if stderr:
        stderr = stderr.strip().split('\n')
        errors = []
        for line in stderr:
            #Warning format:
            #Warning: <standard input>, line i: error message
            line = line.split(':')
            termIndex = int(line[1].split()[-1])
            startParsingIndex = maudeCmds.index('endfm')+2
            role, problemTerm = independentShorthand.keys()[termIndex - startParsingIndex]
            if "no parse for term" not in ''.join(line):
Joy Mitra's avatar
Joy Mitra committed
592 593
                errors.append(' '.join([pslErrors.error,
                    pslErrors.color_line_number(independentShorthand[(role, problemTerm)][DEF_LINE_NUM]),
594 595 596 597 598 599
                    "Term: ", pslErrors.color_token(problemTerm), ':'.join(line[2:])]))
        raise pslErrors.SyntaxError('\n'.join(errors))
    stdout = stdout.split('\n')
    stdout = [line.replace('Maude>', '').strip() for line in stdout]
    #Maude output after removing Maude>:
    #Sort: term
Joy Mitra's avatar
Joy Mitra committed
600
    return {independentShorthand[termRolePair][DEF_SHORTHAND]:line.split(':')[0] for termRolePair, line in
601 602 603 604 605 606 607 608 609 610 611
            zip(independentShorthand, stdout)}

def is_function(defMap):
    """
    Given a mapping from pairs (role, term) |-> (shorthand, lineNum)
    checks to make sure that for any two
    (role, term) |-> (shorthand, lineNum)
    (role', term') |-> (shorthand', lineNum')

    term = term' iff shorthand = shorthand'

Joy Mitra's avatar
Joy Mitra committed
612
    In other words, the mapping from shorthand to
613 614 615 616 617 618 619 620 621 622 623 624 625 626 627
    term defines a function.
    """
    definedShorthand = {}
    for role, term in defMap:
        shorthand, lineNumber = defMap[(role, term)]
        if shorthand in definedShorthand:
            tokenizedTerm1 = tokenize(term)
            term2, lineNumber2 = definedShorthand[shorthand]
            tokenizedTerm2 = tokenize(term2)
            if any([token1 != token2 for token1, token2 in zip(tokenizedTerm1, tokenizedTerm2)]):
                raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(lineNumber) + ",",  pslErrors.color_line_number(lineNumber2),
                    "Multiple definitions of", pslErrors.color_token(shorthand)  + ":", pslErrors.color_token(term) + ",", pslErrors.color_token(term2)]))
        else:
            definedShorthand[shorthand] = (term, lineNumber)

628
def role_variables_correct(defMap, parseTree):
629 630
    """
    Given a mapping from pairs (role, term) |-> (shorthand, lineNum)
631
    checks to make sure that the variables in term are allowed
Joy Mitra's avatar
Joy Mitra committed
632
    to show up in terms associated with role.
633
    """
634
    #Working on modifying the disjoint_vars code from pslTree.py to work here.
635
    protocol = parseTree.get_protocol()
636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651
    roleMap = protocol.variables_per_role()
    declaredVars = protocol.declared_variables()
    roleTermPairs = defMap.keys()
    errors = []
    checkedRoles = []
    for role, term in roleTermPairs:
        #checkedRoles.append(role)
        inVars = set(roleMap[role])
        otherStmtVars = protocol.statement_vars(float('inf'))
        otherStmtVars = {roleName:otherStmtVars[roleName] for roleName in otherStmtVars if roleName != role}
        #Because we've already passed the terms to Maude to be parsed, the variables in the term are annotated with their sort. We need to ignore that sort
        #when checking if a variable is in someone else's variables.
        for var in [token for token in tokenize(term) if token.split(':')[0] in declaredVars]:
            for roleName in otherStmtVars:
                varName = var.split(':')[0]
                if varName in otherStmtVars[roleName] and varName not in inVars:
Joy Mitra's avatar
Joy Mitra committed
652
                    errorMsg = ' '.join([pslErrors.error, pslErrors.color_line_number(defMap[(role, term)][LINE_NUM]), "Variable", pslErrors.color_token(varName.strip()),
653 654 655 656 657 658 659 660 661
                        "appears in the protocol terms of roles",
                        pslErrors.color_token(roleName), "and", pslErrors.color_token(role) + ".",
                        "Variables must be disjoint between roles, with the possible exception of In(put) variables."])
                    if errorMsg not in errors:
                        errors.append(errorMsg)
    if errors:
        raise pslErrors.TranslationError('\n'.join(errors))


662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702

def parse_code(sectionStmts):
    root = pslTree.Root()
    try:
        root.children.append(pslTree.Theory.parse(sectionStmts['Theory'], root))
    except KeyError:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Theory")]))
    try:
        root.children.append(pslTree.Protocol.parse(sectionStmts['Protocol'], root))
    except KeyError:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Protocol")]))
    try:
        root.children.append(pslTree.Intruder.parse(sectionStmts['Intruder'], root))
    except KeyError:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Intruder")]))
    try:
        root.children.append(pslTree.Attacks.parse((sectionStmts['Attacks']), root))
    except KeyError:
            raise pslErrors.SyntaxError(' '.join([pslErrors.errorNoLine, "Missing Section:", pslErrors.color_token("Attacks")]))
    return root

SPEC_NAME = 1
def build_theory(parseTree, filePath, fileName):
    eqTheory = parseTree.get_theory()
    code = [line for line in eqTheory.translate() if line]
    syntax, equations = split_eq_theory(code)
    symbolsModuleName = "fmod PROTOCOL-EXAMPLE-SYMBOLS is protecting DEFINITION-PROTOCOL-RULES ."
    syntax.insert(0, symbolsModuleName)
    syntax.append('op _$;_ : Msg Msg -> Msg [ctor gather(e E) frozen].')
    syntax.append('endfm')
    equationModuleName = "fmod PROTOCOL-EXAMPLE-ALGEBRAIC is protecting PROTOCOL-EXAMPLE-SYMBOLS ."
    equations.insert(0, equationModuleName)
    equations.append('endfm')
    coherentEquations = make_coherent(equations, syntax)
    theoryFileName = os.path.join(filePath, '.'.join([fileName, 'maude']))
    with open(theoryFileName, 'w') as maudeFile:
        maudeFile.write('\n\n'.join(['\n'.join(syntax), '\n'.join(coherentEquations)]))
    return theoryFileName

def make_coherent(equations, syntax):
    """
Joy Mitra's avatar
Joy Mitra committed
703
    Given two iterables of lines (strings) of maude code, one representing PROTOCOL-EXAMPLE-ALGEBRAIC and the
704 705 706 707 708 709 710 711 712 713 714 715 716 717
    other PROTOCOL-EXAMPLE-SYMBOLS,
    generates a new version of PROTOCOL-EXAMPLE-SYMBOLS where the equations have been made explicitly coherent modulo the axioms.
    """
    maudeExecution = subprocess.Popen([MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX],
         stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
    maudeCode = syntax + equations
    maudeCode.append('load full-maude.maude .')
    maudeCode.append('( select AX-COHERENCE-COMPLETION .)')
    maudeCode.append(' '.join(['(', 'red axCohComplete(', 'upModule(', "'PROTOCOL-EXAMPLE-ALGEBRAIC,", 'false', ')', ')', '.)']))
    maudeCode.append('q')
    stdout, stderr = maudeExecution.communicate('\n'.join(maudeCode))
    if stderr:
        raise pslErrors.TranslationError(stderr)
    eqLines = [line for line in stdout.split('\n') if 'eq' in line.split()]
718 719
    equationModule = [line for line in equations if 'eq' not in line.split()]
    equationModule = equationModule[:-1] + compute_equations(eqLines, syntax) + [equationModule[-1]]
720 721 722 723 724 725 726 727 728 729 730 731
    return equations

def compute_equations(eqLines, syntax):
    """
    Given a list of strings, representing meta equations in Maude, and a list of lines representing the syntax file associated with
    the equations, returns a list of lines representing the Ax-complete object level
    Maude equations
    """
    maudeExecution = subprocess.Popen([MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX],
         stdout=subprocess.PIPE, stdin=subprocess.PIPE, stderr=subprocess.PIPE)
    equationTerms = extract_equation_terms_attributes(eqLines)
    maudeCode = list(syntax)
Joy Mitra's avatar
Joy Mitra committed
732
    maudeCode.extend(["fmod THROW-AWAY is", "protecting PROTOCOL-EXAMPLE-SYMBOLS .", "protecting META-LEVEL .",
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
        "op $$$m$$$ : -> [Msg] .",
        "endfm"])
    CONSTANT = "$$$m$$$"
    for left, right in equationTerms.items():
        right = right[0]
        maudeCode.append(' '.join(["red downTerm(", left, ",", CONSTANT, ")", "."]))
        maudeCode.append(' '.join(["red downTerm(", right, ",", CONSTANT, ")", "."]))
    maudeCode.append('q')
    stdout, stderr = maudeExecution.communicate('\n'.join(maudeCode))
    termList = [line[line.index(':')+1:].strip() for line in stdout.split('\n') if line.strip() and line.strip().split()[0] == 'result']
    termPairs = []
    leftTerm = True
    for term in termList:
        if leftTerm:
            termPairs.append([term])
            leftTerm = False
        else:
            leftTerm = True
            termPairs[-1].append(term)
    completeEqs = []
    for terms, attributes in zip(termPairs, equationTerms.values()):
        left, right = terms
        attributes = attributes[-1]
        completeEqs.append(' '.join(['eq', left, '=', right, '[', attributes, ']', '.']))
    return completeEqs


def extract_equation_terms_attributes(eqLines):
    """
    Given a list of strings representing maude meta-level equations eq metaTerm1= metaTerm2 [attributes], extracts and returns a dictionary
    {metaTerm1:(metaTerm2, attributes)}.
    """
    eqDict = {}
    for line in eqLines:
        lefthandSide, righthandSide = line.split('=')
        lefthandSide = lefthandSide.split()[1].strip()
769
        righthandSide, attributes = compute_righthand_attributes(righthandSide)
770 771 772 773
        attributes = attributes[:attributes.index(']')]
        eqDict[lefthandSide] = (righthandSide, attributes)
    return eqDict

774 775 776 777 778 779 780 781 782 783
def compute_righthand_attributes(righthandSide):
    """
    Given a righthand side of a meta equation, splits it into the righthand
    side of the equation, and the equation attributes, and returns them as
    an ordered pair.
    """
    righthandSide = righthandSide.strip()
    attributeStart = righthandSide.rfind('[')
    return (righthandSide[:attributeStart], righthandSide[attributeStart+1:-1])

784 785 786 787 788 789

def split_eq_theory(eqTheory):
    """
    Partitions the equational theory into the syntax and equations
    """
    spaceSplitTheory = [line.split() for line in eqTheory]
Joy Mitra's avatar
Joy Mitra committed
790 791
    equations = [' '.join(stmt) for stmt in spaceSplitTheory if stmt[0] == 'eq' or
            stmt[0] == 'ceq']
792 793 794 795 796 797 798 799
    syntax = [stmt for stmt in eqTheory if stmt.split()[0] != 'eq' and stmt.split()[0] != 'ceq']
    return (syntax, equations)

if __name__ == '__main__':
    try:
        maudify()
    except pslErrors.PSLError, e:
        print(str(e))