psl.py 31.7 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 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 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144
#!/usr/bin/python
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.
#However, if I import this, it always prints a warning about using the slow fuzzy match. While that doesn't affect 
#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.
    
    To use: type the command ./psl.py FILENAME.psl
    Options:
        -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 
        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
        strand execution statements. So, if there's a single term left, it 
        won't be an In.
        
    2. Make sure the subsort keywords and the < are correct
    3. Check the high-level syntax. 
        a. Make sure that there are no illegal operators: 
                i. _,_
                ii. _|->_
                iii. _._
                iv. In, Out, Def.
                v. anything containing a $.
                vi. _=>_
                vii. _executes protocol
                viii. Intruder learns_
                ix. without:
                x. _|-_
                xi. Any operator containing unbalanced parenthesis or curly 
                braces Basically, we assume that the user-defined syntax is 
                disjoint from 
                anything that starts a new statement, because it simplifies
                checking for missing periods, and from anything that appears
                next to user-defined terms
                in order to avoid ambiguities with the high-level syntax. 
                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'

MAUDE_COMMAND = './maude27' 
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
STATE_SPACE_REDUCTION_VARIANTS = ['state-space-reduction:', 'State-space-reduction:'] 
END_LINE = ['.', 'without:', 'Without:', 'avoid:', 'Avoid:'] + STATE_SPACE_REDUCTION_VARIANTS

def nonzero_nats():
    """
    A generator that yields as many natural numbers as you need (up to 
    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)].
    If n == 1, then it returns the list [(m_1, m_1)]. If n == 0, then it 
    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}
    numberedLines = [(tokenize(line), num) for line, num in 
            number_lines(pslFile)]
    statement = pslTree.Statement()
    #List of pairs of comment token with line number. 
    startComment = []
    errorMsgs = []
    for i in range(len(numberedLines)):
        line, num = numberedLines[i]
145 146
        for j in range(len(line)):
            token = line[j].strip()
147
            try:
148
                nextToken = line[j+1]
149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
            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:
164
                    nextNextToken = line[j+2]
165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210
                except IndexError:
                    try:
                        nextNextToken = numberedLines[i+1][0][0]
                    except IndexError:
                        nextNextToken = ''
            if token == r'/*':
                startComment.append((token, num))
            elif token == r'*/':
                try:
                    if startComment[-1][0] == r'/*': 
                        startComment = startComment[:-1]
                        continue
                    else: 
                        raise IndexError()
                except IndexError:
                    raise errorMsgs.append(' '.join([pslErrors.error, 
                        pslErrors.color_line_number(num), 
                        "Unexpected end comment token:", 
                        pslErrors.color_token(token)]))
            if startComment or re.match(singleLineComment, token): 
                continue
            elif not sectionStmts['Start'] and re.match(startSpec, token):
                stmt = pslTree.Statement([token], [num])
                sectionStmts["Start"].append(stmt)
                continue
            elif is_start_of_section(token, nextToken): 
                section = token
            elif token in END_LINE and not protocol_step(nextToken, nextNextToken):
                statement.append(token, num)
                sectionStmts[section].append(statement)
                statement = pslTree.Statement()
            else: 
                statement.append(token, num)
    for token, num in startComment:
       errorMsgs.append(' '.join([pslErrors.error, pslErrors.color_line_number(num), 
           "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]:
            stmt.tokens = [token for token in stmt.tokens if token != '*/'] 
    return sectionStmts


def protocol_step(nextToken, nextNextToken):
211 212 213 214
    """
    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.
    """
215 216 217 218 219 220 221
    try:
        return nextNextToken == '->' and nextToken not in pslTree.TOP_LEVEL_TOKENS
    except IndexError:
        return False


def type_check_sectionStmts(sectionStmts):
222 223 224
    """
    Checks to make sure that the statements in each section are in fact statement objects. For debugging purposes only.
    """
225 226 227 228 229 230
    for section in sectionStmts:
        for statement in sectionStmts:
            assert(isinstance(statement, pslTree.Statement)), "statement is not a pslTree.Statement: %s" % statement


def tokenize(line):
231 232 233
    """
    Splits the passed PSL line into a list of tokens, and returns those tokens.
    """
234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298
    return [token for token in re.split(pslTree.Token.tokenizer, line.strip()) if token]


def is_start_of_section(token, nextToken):
    return token in pslTree.SECTION_HEADINGS and (token != 'Intruder' or 
            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.
        2. Annotate the file with line numbers, and wrap the specification in 
        parenthesis
        3. Feed the annotated file into Maude, along with the Maude
        conversation file.  
    """
    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))
    theoryFileName = build_theory(parseTree, os.path.dirname(pslFilePath), fileName) 
    #TODO: Need to invoke different functions depending on whether we're doing protocol composition, or normal PSL translation.
    intermediate = gen_intermediate(parseTree, theoryFileName) 
    gen_NPA_code(intermediate, theoryFileName)

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.
    """
    code = ['load psl.maude', ' '.join(['load', theoryFileName]), 'mod INTERMEDIATE is', 'protecting TRANSLATION-TO-MAUDE-NPA .', 
            '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())]
            raise pslErrors.TranslationError(' '.join([pslErrors.error, pslErrors.color_line_number(defPair.lineNum) + ",", 
                otherDef[DEF_LINE_NUM], "Term", pslErrors.color_token(defPair.term()), 
299
                "has multiple shorthands: ", pslErrors.color_token(defPair.shorthand()) + ",", 
300 301 302
                pslErrors.color_token(otherDef[DEF_SHORTHAND])]))
        else:
            defMap[(defPair.role(), defPair.term())] = (defPair.shorthand(), defPair.lineNum)
303
    shorthandSortMap = compute_sorts(defMap, theoryFileName, parseTree)
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323
    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:
        defs = ', '.join([' '.join([''.join(['(', shorthandLineNum[DEF_SHORTHAND], ', ', str(shorthandLineNum[DEF_LINE_NUM]), ')']), ':=', 
            roleTermPair[DEF_KEY_TERM]]) for roleTermPair, shorthandLineNum in defMap.items()])
    else:
        defs = '$noDefs'
324
    code.append(' '.join(['[', '$makeIdem($checkWellFormed(', defs, '))', ']']))
325 326 327 328 329 330 331 332 333 334 335
    code.append('.')
    return code

def gen_NPA_code(maudeCode, theoryFileName):
    maudeCommand = [MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX, theoryFileName, 
            TRANSLATION_FILE]
    maudeExecution = subprocess.Popen(maudeCommand, stdout=subprocess.PIPE, 
        stdin=subprocess.PIPE, stderr=subprocess.PIPE)
    stdout, stderr = maudeExecution.communicate('\n'.join(maudeCode))
    if stderr:
        errors = []
336
        #Expected error pattern:
337 338 339
        #Warning: <standard input>, line N : <error message> 
        for line in [line.strip() for line in stderr.split('\n') if line.strip()]:
            _,lineNum, error = line.split(':')
340
            #expected pattern currently in lineNum:
341 342 343 344
            #<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]
345
            #pattern of psl statements inside Maude code
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377
            #blah blah . [ num ] 
            try:
                pslLineNum = int(pslLine.split()[-2])
            except (IndexError, ValueError): 
                pass
            else:
                bracketIndex = pslLine.rfind('[')
                errors.append(' '.join([pslErrors.error, pslErrors.color_line_number(pslLineNum), error, "\n\tCode: ", 
                    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)
            process_error(stdout[errorIndex:])
        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 .')

def process_error(error):
378 379 380 381
    """
    Given a partially evaluated PSL specification, extracts the offending error term, and extracts from the error term the information 
    need for a usable error message. Then raises a TranslationError containing said usable error message.
    """
382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
    errorTermStart = error.index("$$$")
    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(")", '')
            errorDefs.append(' '.join([pslErrors.error, pslErrors.color_line_number(lineNumber.strip()), 
                                         #Stripping off the () around the definition
                "Malformed Definition:", pslErrors.color_token(pair[1:-1])]))
        raise pslErrors.TranslationError('\n'.join(errorDefs))




def compute_end_of_term(errorType, errorTerm):
    """
    Given the start of term that contains the errorTerm as a subterm (and which starts with the first argument of the error term), 
    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]))
           
MAX_ITERATIONS = 100
424
def compute_sorts(defMap, syntaxFileName, pslTree):
425 426 427 428 429 430 431 432 433 434 435 436
    """
    Computes the sorts of the user-defined shorthand. 
    
    defMap is expected to be a dictionary with the following format:
    (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 
    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)
437
    role_variables_correct(defMap, pslTree)
438 439 440 441 442 443 444 445 446
    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()}
447
    dependentShorthand = {(role, term):shorthandLineNum for ((role, term), shorthandLineNum) in defMap.iteritems() if
448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 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 523 524 525 526 527 528 529 530 531 532 533 534 535
        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
        dependentShorthand = {(role, term):shorthandLinenum for (role, term), shorthandLinenum in 
                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():
            assert key not in knownShorthand or knownShorthand[key] == value, "Internal Error: Disagreement on shorthand: %s\n%s\n%s\n" % (str(key), 
                    str(value), str(knownShorthand))
            knownShorthand[key] = value
    if dependentShorthand:
        raise pslErrors.TranslationError([pslErrors.error, pslErrors.color_line_number(', '.join([lineNum for (shorthand, lineNum) in 
            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):
    """
    Given a mapping from (role, term) to (shorthand, lineNumber), and a mapping of all shorthand appearing in each "term" to their 
    respective
    sorts, returns a mapping of all shorthand in independentShorthand to their respective sorts.
    """
    maudeCmds = (["fmod SHORTHAND is", "protecting PROTOCOL-EXAMPLE-SYMBOLS ."] +
                [' '.join(['op', shorthand, ':', '->', sort, '.']) for (shorthand, sort) in knownShorthand.iteritems()] + 
                ["endfm"])
    maudeCmds += [' '.join(['parse', termRolePair[DEF_KEY_TERM], '.']) for termRolePair in independentShorthand.keys()] + ['q']
    maudeExecution = subprocess.Popen([MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX, 
        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):
                errors.append(' '.join([pslErrors.error, 
                    pslErrors.color_line_number(independentShorthand[(role, problemTerm)][DEF_LINE_NUM]), 
                    "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
    return {independentShorthand[termRolePair][DEF_SHORTHAND]:line.split(':')[0] for termRolePair, line in 
            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'

    In other words, the mapping from shorthand to 
    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)

536
def role_variables_correct(defMap, pslTree):
537 538
    """
    Given a mapping from pairs (role, term) |-> (shorthand, lineNum)
539 540
    checks to make sure that the variables in term are allowed
    to show up in terms associated with role. 
541
    """
542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569
    #Working on modifying the disjoint_vars code from pslTree.py to work here.
    protocol = pslTree.get_protocol()
    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:
                    errorMsg = ' '.join([pslErrors.error, pslErrors.color_line_number(defMap[(role, term)][LINE_NUM]), "Variable", pslErrors.color_token(varName.strip()), 
                        "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))


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 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 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 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

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):
    """
    Given two iterables of lines (strings) of maude code, one representing PROTOCOL-EXAMPLE-ALGEBRAIC and the 
    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()]
    equations = [line for line in equations if not 'eq' in line.split()]
    equations = equations[:-1] + compute_equations(eqLines, syntax) + [equations[-1]]
    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)
    maudeCode.extend(["fmod THROW-AWAY is", "protecting PROTOCOL-EXAMPLE-SYMBOLS .", "protecting META-LEVEL .", 
        "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()
        righthandSide, attributes = [term.strip() for term in righthandSide.split('[')]
        attributes = attributes[:attributes.index(']')]
        eqDict[lefthandSide] = (righthandSide, attributes)
    return eqDict


def split_eq_theory(eqTheory):
    """
    Partitions the equational theory into the syntax and equations
    """
    spaceSplitTheory = [line.split() for line in eqTheory]
    equations = [' '.join(stmt) for stmt in spaceSplitTheory if stmt[0] == 'eq' or 
            stmt[0] == 'ceq'] 
    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))