Commit 65de0238 authored by Andrew's avatar Andrew
Browse files

Added code for handling errors where a Substitution is not properly sorted.

parent 01867425
...@@ -336,6 +336,7 @@ fmod ATTACK-SYNTAX is ...@@ -336,6 +336,7 @@ fmod ATTACK-SYNTAX is
op _|->_ : Msg MsgNumSet -> MsgPair [prec 30] . op _|->_ : Msg MsgNumSet -> MsgPair [prec 30] .
op $none : -> MsgPairs . op $none : -> MsgPairs .
op __ : MsgPairs MsgPairs -> MsgPairs [ctor assoc comm id: $none] . op __ : MsgPairs MsgPairs -> MsgPairs [ctor assoc comm id: $none] .
op _$$$;;;$$$_ : [MsgPairs] [MsgPairs] -> [MsgPairs] [ctor assoc comm id: $none] .
---Stores the information on an invalid substitution. The Python code ---Stores the information on an invalid substitution. The Python code
---invoking this Maude code then scans the output for the presence of ---invoking this Maude code then scans the output for the presence of
---this term. If the Python code finds this term, then it extracts the ---this term. If the Python code finds this term, then it extracts the
......
...@@ -809,7 +809,7 @@ rl [translateAttackWithoutNever] : ...@@ -809,7 +809,7 @@ rl [translateAttackWithoutNever] :
eq $checkSorts($none) = id . eq $checkSorts($none) = id .
---Checks if the sort of the first argument is a supersort of the sort of ---Checks if the sort of the first argument is a supersort of the sort of
---the second arugment. ---the second argument.
op $isValidPair : Msg Msg Nat -> Mapping . op $isValidPair : Msg Msg Nat -> Mapping .
ceq $isValidPair(D:Msg, R:Msg, N) = ceq $isValidPair(D:Msg, R:Msg, N) =
if sortLeq(META-MOD:Module, getType(metaReduce(META-MOD:Module, upTerm(R:Msg))), getType(metaReduce(META-MOD:Module, upTerm(D:Msg)))) if sortLeq(META-MOD:Module, getType(metaReduce(META-MOD:Module, upTerm(R:Msg))), getType(metaReduce(META-MOD:Module, upTerm(D:Msg))))
......
...@@ -274,7 +274,7 @@ def maudify(): ...@@ -274,7 +274,7 @@ def maudify():
theoryFileName = build_theory(parseTree, os.path.dirname(pslFilePath), fileName) 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. #TODO: Need to invoke different functions depending on whether we're doing protocol composition, or normal PSL translation.
intermediate = gen_intermediate(parseTree, theoryFileName) intermediate = gen_intermediate(parseTree, theoryFileName)
gen_NPA_code(intermediate, theoryFileName) gen_NPA_code(intermediate, theoryFileName, parseTree)
DEF_KEY_ROLE = 0 DEF_KEY_ROLE = 0
DEF_KEY_TERM = 1 DEF_KEY_TERM = 1
...@@ -325,7 +325,7 @@ def gen_intermediate(parseTree, theoryFileName): ...@@ -325,7 +325,7 @@ def gen_intermediate(parseTree, theoryFileName):
code.append('.') code.append('.')
return code return code
def gen_NPA_code(maudeCode, theoryFileName): def gen_NPA_code(maudeCode, theoryFileName, parseTree):
maudeCommand = [MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX, theoryFileName, maudeCommand = [MAUDE_COMMAND, NO_PRELUDE, '-no-banner', '-no-advise', '-no-wrap', PRELUDE, NPA_SYNTAX, theoryFileName,
TRANSLATION_FILE] TRANSLATION_FILE]
maudeExecution = subprocess.Popen(maudeCommand, stdout=subprocess.PIPE, maudeExecution = subprocess.Popen(maudeCommand, stdout=subprocess.PIPE,
...@@ -370,7 +370,7 @@ def gen_NPA_code(maudeCode, theoryFileName): ...@@ -370,7 +370,7 @@ def gen_NPA_code(maudeCode, theoryFileName):
except ValueError: except ValueError:
errorResult = "result [TranslationData]:" errorResult = "result [TranslationData]:"
errorIndex = stdout.index(errorResult) + len(errorResult) errorIndex = stdout.index(errorResult) + len(errorResult)
process_error(stdout[errorIndex:]) process_error(stdout[errorIndex:], parseTree)
else: else:
endOfModule = stdout.rfind("Maude>") endOfModule = stdout.rfind("Maude>")
module = '\n' + stdout[index:endOfModule].strip() module = '\n' + stdout[index:endOfModule].strip()
...@@ -378,7 +378,7 @@ def gen_NPA_code(maudeCode, theoryFileName): ...@@ -378,7 +378,7 @@ def gen_NPA_code(maudeCode, theoryFileName):
maudeFile.write(module) maudeFile.write(module)
maudeFile.write('\nselect MAUDE-NPA .') maudeFile.write('\nselect MAUDE-NPA .')
def process_error(error): def process_error(error, parseTree):
""" """
Given a partially evaluated PSL specification, extracts the offending error term, and extracts from the error term the information 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. need for a usable error message. Then raises a TranslationError containing said usable error message.
...@@ -427,7 +427,18 @@ def process_error(error): ...@@ -427,7 +427,18 @@ def process_error(error):
in zip(problemTerms, lineNumbers)])])) in zip(problemTerms, lineNumbers)])]))
raise pslErrors.TranslationError('\n'.join(errorMsg)) raise pslErrors.TranslationError('\n'.join(errorMsg))
elif errorType.strip() == "$$$invalidSorting": elif errorType.strip() == "$$$invalidSorting":
pass 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()
raise pslErrors.TranslationError(' '.join([pslErrors.error,
pslErrors.color_line_number(lineNum), "Variable",
pslErrors.color_token(var), "has sort",
pslErrors.color_token(variableSort), "but term",
pslErrors.color_token(term), "does not."]))
...@@ -451,7 +462,7 @@ def compute_end_of_term(errorType, errorTerm): ...@@ -451,7 +462,7 @@ def compute_end_of_term(errorType, errorTerm):
raise ValueError(' '.join(["End of error term of type: ", errorType, "not found when trying to extract the term from:", errorTerm])) raise ValueError(' '.join(["End of error term of type: ", errorType, "not found when trying to extract the term from:", errorTerm]))
MAX_ITERATIONS = 100 MAX_ITERATIONS = 100
def compute_sorts(defMap, syntaxFileName, pslTree): def compute_sorts(defMap, syntaxFileName, parseTree):
""" """
Computes the sorts of the user-defined shorthand. Computes the sorts of the user-defined shorthand.
...@@ -464,7 +475,7 @@ def compute_sorts(defMap, syntaxFileName, pslTree): ...@@ -464,7 +475,7 @@ def compute_sorts(defMap, syntaxFileName, pslTree):
Returns a dictionary mapping shorthand to their respective sorts. Returns a dictionary mapping shorthand to their respective sorts.
""" """
is_function(defMap) is_function(defMap)
role_variables_correct(defMap, pslTree) role_variables_correct(defMap, parseTree)
SHORTHAND = 0 SHORTHAND = 0
LINE_NUMBER = 1 LINE_NUMBER = 1
ROLE = 0 ROLE = 0
...@@ -563,14 +574,14 @@ def is_function(defMap): ...@@ -563,14 +574,14 @@ def is_function(defMap):
else: else:
definedShorthand[shorthand] = (term, lineNumber) definedShorthand[shorthand] = (term, lineNumber)
def role_variables_correct(defMap, pslTree): def role_variables_correct(defMap, parseTree):
""" """
Given a mapping from pairs (role, term) |-> (shorthand, lineNum) Given a mapping from pairs (role, term) |-> (shorthand, lineNum)
checks to make sure that the variables in term are allowed checks to make sure that the variables in term are allowed
to show up in terms associated with role. to show up in terms associated with role.
""" """
#Working on modifying the disjoint_vars code from pslTree.py to work here. #Working on modifying the disjoint_vars code from pslTree.py to work here.
protocol = pslTree.get_protocol() protocol = parseTree.get_protocol()
roleMap = protocol.variables_per_role() roleMap = protocol.variables_per_role()
declaredVars = protocol.declared_variables() declaredVars = protocol.declared_variables()
roleTermPairs = defMap.keys() roleTermPairs = defMap.keys()
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment