Pyk updates and bugfixes (#1064)

* k-distribution/pyk: pass symbol table through to recursive prettyPrintKast

* kore/outer.scala: FlatModules should store localSentences, not all sentences

* k-distribution/pyk/kast: add getAttribute function

* k-distribution/pyk/kast: handle KProduction for addAttributes

* k-distribution/pyk/kast: handle remaining cases for prettyPrintKast

* pyk/__main__.py: add initial definition minimizer

* pyk: move definition minimizer into place

* k-distribution/pyk/__main__: switch to proper subcommand parsing

* k-distribution/pyk/__main__: fix arguments for coverage command

* k-distribution/tests/pyk: update coverage log test

* k-distribution/pyk: working removal of log calls from rules

* k-distribution/pyk: minimize rules too

* k-distribution/tests/pyk: add test that definition minimization works

* k-distribution/pyk: remove main interface to definition minimizer

* k-distribution/pyk/definition: remove unneeded code

Co-authored-by: rv-jenkins <admin@runtimeverification.com>

k-distribution/src/main/scripts/lib/pyk/__init__.py

@@ -5,9 +5,10 @@
 import sys
 import tempfile
 
-from .kast      import _notif, _warning, _fatal
-from .kastManip import *
-from .coverage  import *
+from .kast       import _notif, _warning, _fatal
+from .kastManip  import *
+from .coverage   import *
+from .definition import *
 
 def _teeProcessStdout(args, tee = True, buffer_size = 80):
         process = subprocess.Popen(args, stdout = subprocess.PIPE, stderr = subprocess.PIPE, universal_newlines = True)

k-distribution/src/main/scripts/lib/pyk/__main__.py

@@ -2,60 +2,81 @@
 
 import argparse
 import tempfile
+import os.path as path
 
 from .         import *
 from .graphviz import *
 
 pykArgs = argparse.ArgumentParser()
+pykArgs.add_argument('kompiled-dir', type = str, help = 'Kompiled directory for definition.')
 
-pykArgs.add_argument('command' , choices = ['parse', 'run', 'prove', 'graph-imports', 'coverage-log'])
-
-pykArgs.add_argument('-d', '--definition')
-
-pykArgs.add_argument('-i', '--input',  type = argparse.FileType('r'), default = '-')
-pykArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-')
-
-pykArgs.add_argument('-f', '--from', default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
-pykArgs.add_argument('-t', '--to',   default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
-
-pykArgs.add_argument('kArgs', nargs='*', help = 'Arguments to pass through to K invocation.')
-
-pykArgs.add_argument('--coverage-file', type = argparse.FileType('r'))
-
-args = vars(pykArgs.parse_args())
-
-print(args)
-
-inputFile = args['input'].name
-if inputFile == '-':
-    with tempfile.NamedTemporaryFile(mode = 'w') as tempf:
-        tempf.write(args['input'].read())
-        inputFile = tempf.name
-
-returncode = 0
-definition = args['definition']
-if args['command'] == 'parse':
-    (returncode, stdout, stderr) = kast(definition, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
-    args['output'].write(stdout)
-elif args['command'] == 'run':
-    (returncode, stdout, stderr) = krun(definition, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
-    args['output'].write(stdout)
-elif args['command'] == 'prove':
-    (returncode, stdout, stderr) = kprove(definition, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
-    args['output'].write(stdout)
-elif args['command'] == 'graph-imports':
-    returncode = 0 if graphvizImports(definition + '/parsed') and graphvizImports(definition + '/compiled') else 1
-elif args['command'] == 'coverage-log':
-    json_definition = removeSourceMap(readKastTerm(definition + '/compiled.json'))
-    symbolTable = buildSymbolTable(json_definition)
-    for rid in args['coverage_file']:
-        rule = minimizeRule(stripCoverageLogger(getRuleById(json_definition, rid.strip())))
-        args['output'].write('\n\n')
-        args['output'].write('Rule: ' + rid.strip())
-        args['output'].write('\nUnparsed:\n')
-        args['output'].write(prettyPrintKast(rule, symbolTable))
-
-args['output'].flush()
-
-if returncode != 0:
-    _fatal('Non-zero exit code (' + str(returncode) + ': ' + str(kCommand), code = returncode)
+pykCommandParsers = pykArgs.add_subparsers(dest = 'command')
+
+kastArgs = pykCommandParsers.add_parser('parse', help = 'Parse an input program.')
+kastArgs.add_argument('-i', '--input',  type = argparse.FileType('r'), default = '-')
+kastArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-')
+kastArgs.add_argument('-f', '--from', default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
+kastArgs.add_argument('-t', '--to',   default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
+kastArgs.add_argument('kArgs', nargs='*', help = 'Arguments to pass through to K invocation.')
+
+krunArgs = pykCommandParsers.add_parser('run', help = 'Run an input program.')
+krunArgs.add_argument('-i', '--input',  type = argparse.FileType('r'), default = '-')
+krunArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-')
+krunArgs.add_argument('-f', '--from', default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
+krunArgs.add_argument('-t', '--to',   default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
+krunArgs.add_argument('kArgs', nargs='*', help = 'Arguments to pass through to K invocation.')
+
+kproveArgs = pykCommandParsers.add_parser('prove', help = 'Prove an input specification.')
+kproveArgs.add_argument('-i', '--input',  type = argparse.FileType('r'), default = '-')
+kproveArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-')
+kproveArgs.add_argument('-t', '--to',   default = 'pretty', choices = ['pretty', 'json', 'kast', 'binary', 'kore'])
+kproveArgs.add_argument('kArgs', nargs='*', help = 'Arguments to pass through to K invocation.')
+
+graphImportsArgs = pykCommandParsers.add_parser('graph-imports', help = 'Graph the imports of a given definition.')
+
+coverageArgs = pykCommandParsers.add_parser('coverage', help = 'Convert coverage file to human readable log.')
+coverageArgs.add_argument('coverage-file', type = argparse.FileType('r'), help = 'Coverage file to build log for.')
+coverageArgs.add_argument('-o', '--output', type = argparse.FileType('w'), default = '-')
+
+def definitionDir(kompiledDir):
+    return path.dirname(path.abspath(kompiledDir))
+
+if __name__ == '__main__':
+    returncode = 0
+    args = vars(pykArgs.parse_args())
+    kompiled_dir = args['kompiled-dir']
+
+    if args['command'] in [ 'parse' , 'run' , 'prove' ]:
+        inputFile = args['input'].name
+        if inputFile == '<stdin>':
+            with tempfile.NamedTemporaryFile(mode = 'w') as tempf:
+                tempf.write(args['input'].read())
+                inputFile = tempf.name
+        definition_dir = definitionDir(kompiled_dir)
+        if args['command'] == 'parse':
+            (returncode, stdout, stderr) = kast(definition_dir, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
+            args['output'].write(stdout)
+        elif args['command'] == 'run':
+            (returncode, stdout, stderr) = krun(definition_dir, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
+            args['output'].write(stdout)
+        elif args['command'] == 'prove':
+            (returncode, stdout, stderr) = kprove(definition_dir, inputFile, kArgs = ['--input', args['from'], '--output', args['to']] + args['kArgs'])
+            args['output'].write(stdout)
+
+    elif args['command'] == 'graph-imports':
+        returncode = 0 if graphvizImports(kompiled_dir + '/parsed') and graphvizImports(kompiled_dir + '/compiled') else 1
+
+    elif args['command'] == 'coverage':
+        json_definition = removeSourceMap(readKastTerm(kompiled_dir + '/compiled.json'))
+        symbolTable = buildSymbolTable(json_definition)
+        for rid in args['coverage-file']:
+            rule = minimizeRule(stripCoverageLogger(getRuleById(json_definition, rid.strip())))
+            args['output'].write('\n\n')
+            args['output'].write('Rule: ' + rid.strip())
+            args['output'].write('\nUnparsed:\n')
+            args['output'].write(prettyPrintKast(rule, symbolTable))
+
+    args['output'].flush()
+
+    if returncode != 0:
+        _fatal('Non-zero exit code (' + str(returncode) + '): ' + str(kCommand), code = returncode)

k-distribution/src/main/scripts/lib/pyk/definition.py

@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+
+import sys
+import subprocess
+
+from .kast      import *
+from .kastManip import *
+from .kast      import _notif, _warning, _fatal
+
+def ruleHasId(sentence, ruleIds):
+    if isKRule(sentence):
+        ruleId = getAttribute(sentence, 'UNIQUE_ID')
+        return ruleId is not None and ruleId in ruleIds
+    return True
+
+def syntaxHasKLabel(sentence, klabels):
+    if isKProduction(sentence) and 'klabel' in sentence:
+        return sentence['klabel'] in klabels
+    return True
+
+def keepSentences(kOuter, filter):
+    att = None if 'att' not in kOuter else kOuter['att']
+    if isKDefinition(kOuter):
+        newModules = [ keepSentences(mod, filter) for mod in kOuter['modules'] ]
+        requires = None if 'requires' not in kOuter else kOuter['requires']
+        return KDefinition(kOuter['mainModule'], newModules, requires = requires, att = att)
+    elif isKFlatModule(kOuter):
+        newSentences = [ sent for sent in kOuter['localSentences'] if filter(sent) ]
+        return KFlatModule(kOuter['name'], kOuter['imports'], newSentences, att = att)
+    else:
+        return kOuter
+
+def collectKLabels(kast):
+    labels = []
+    def _collectKLabels(_kast):
+        if isKApply(_kast):
+            labels.append(_kast['label'])
+    collectBottomUp(kast, _collectKLabels)
+    return labels
+
+def collectKLabelsFromRules(definition):
+    used_labels = []
+    for module in definition['modules']:
+        for sentence in module['localSentences']:
+            if isKRule(sentence):
+                used_labels += collectKLabels(sentence['body'])
+    return used_labels
+
+def minimizeDefinition(definition, rulesList):
+    new_definition = keepDefinitionModulesOnly(definition)
+    new_definition = keepSentences(new_definition, lambda sent: ruleHasId(sent, rulesList))
+    used_labels    = collectKLabelsFromRules(new_definition)
+    new_definition = keepSentences(new_definition, lambda sent: syntaxHasKLabel(sent, used_labels))
+    return new_definition

k-distribution/src/main/scripts/lib/pyk/kast.py

@@ -182,14 +182,23 @@ def isKDefinition(k):
 def isCellKLabel(label):
     return len(label) > 1 and label[0] == "<" and label[-1] == ">"
 
+def getAttribute(k, key):
+    if 'att' in k.keys() and isKAtt(k['att']):
+        katts = k['att']['att']
+        if key in katts.keys():
+            return katts[key]
+        return None
+
 def addAttributes(kast, att):
     if isKAtt(kast):
         return KAtt(combineDicts(att, kast['att']))
     if isKRule(kast):
         return KRule(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = addAttributes(kast['att'], att))
+    if isKProduction(kast):
+        return KProduction(kast['productionItems'], kast['sort'], att = addAttributes(kast['att'], att))
     else:
-        notif('Do not know how to add attributes to KAST!')
-        sys.stderr.write(kast)
+        _notif('Do not know how to add attributes to KAST!')
+        sys.stderr.write(str(kast))
         sys.stderr.flush()
         sys.exit(1)
 
@@ -290,9 +299,9 @@ def prettyPrintKast(kast, symbolTable):
         unparser = appliedLabelStr(label) if label not in symbolTable else symbolTable[label]
         return unparser(*unparsedArgs)
     if isKAs(kast):
-        pattern = prettyPrintKast(kast["pattern"], symbolTable)
-        alias   = prettyPrintKast(kast["alias"], symbolTable)
-        return "( " + pattern + " #as " + alias + ")"
+        patternStr = prettyPrintKast(kast["pattern"], symbolTable)
+        aliasStr   = prettyPrintKast(kast["alias"], symbolTable)
+        return patternStr + ' #as ' + aliasStr
     if isKRewrite(kast):
         lhsStr = prettyPrintKast(kast["lhs"], symbolTable)
         rhsStr = prettyPrintKast(kast["rhs"], symbolTable)
@@ -305,35 +314,74 @@ def prettyPrintKast(kast, symbolTable):
         else:
             unparsedKSequence = '.'
         return unparsedKSequence
+    if isKSort(kast):
+        return kast['name']
+    if isKTerminal(kast):
+        return '"' + kast['value'] + '"'
+    if isKRegexTerminal(kast):
+        return 'r"' + kast['regex'] + '"'
+    if isKNonTerminal(kast):
+        return prettyPrintKast(kast['sort'], symbolTable)
+    if isKProduction(kast):
+        if getAttribute(kast, 'klabel') is None and 'klabel' in kast:
+            kast = addAttributes(kast, {'klabel' : kast['klabel']})
+        sortStr       = prettyPrintKast(kast['sort'], symbolTable)
+        productionStr = ' '.join([ prettyPrintKast(pi, symbolTable) for pi in kast['productionItems'] ])
+        attStr        = prettyPrintKast(kast['att'], symbolTable)
+        return 'syntax ' + sortStr + ' ::= ' + productionStr + ' ' + attStr
+    if isKSyntaxSort(kast):
+        sortStr = prettyPrintKast(kast['sort'], symbolTable)
+        attStr  = prettyPrintKast(kast['att'], symbolTable)
+        return 'syntax ' + sortStr + ' ' + attStr
+    if isKSortSynonym(kast):
+        newSortStr = prettyPrintKast(kast['newSort'], symbolTable)
+        oldSortStr = prettyPrintKast(kast['oldSort'], symbolTable)
+        attStr     = prettyPrintKast(kast['att'], symbolTable)
+        return 'syntax ' + newSortStr + ' = ' + oldSortStr + ' ' + attStr
+    if isKSyntaxAssociativity(kast):
+        assocStr = kast['assoc'].lower()
+        tagsStr  = ' '.join(kast['tags'])
+        attStr   = prettyPrintKast(kast['att'], symbolTable)
+        return 'syntax associativity ' + assocStr + ' ' + tagsStr + ' ' + attStr
+    if isKSyntaxPriority(kast):
+        prioritiesStr = ' > '.join([ ' '.join(group) for group in kast['priorities'] ])
+        attStr        = prettyPrintKast(kast['att'], symbolTable)
+        return 'syntax priority ' + prioritiesStr + ' ' + attStr
+    if isKBubble(kast):
+        bubbleStr = prettyPrintKast(KModuleComment('KBubble(' + kast['sentenceType'] + ', ' + kast['contents'] + ')'), symbolTable)
+        attStr    = prettyPrintKast(kast['att'], symbolTable)
+        return bubbleStr
     if isKRule(kast):
-        body     = indent(prettyPrintKast(kast["body"], symbolTable))
+        body     = "\n     ".join(prettyPrintKast(kast["body"], symbolTable).split("\n"))
         ruleStr = "rule " + body
         requiresStr = ""
         ensuresStr  = ""
         attsStr     = prettyPrintKast(kast['att'], symbolTable)
         if kast["requires"] is not None:
             requiresStr = prettyPrintKast(kast["requires"], symbolTable)
-            requiresStr = "requires " + indent(requiresStr)
+            requiresStr = "requires " + "\n   ".join(requiresStr.split("\n"))
         if kast["ensures"] is not None:
             ensuresStr = prettyPrintKast(kast["ensures"], symbolTable)
-            ensuresStr = "ensures " + indent(ensuresStr)
+            ensuresStr = "ensures " + "\n  ".join(ensuresStr.split("\n"))
         return ruleStr + "\n  " + requiresStr + "\n  " + ensuresStr + "\n  " + attsStr
     if isKContext(kast):
         body        = indent(prettyPrintKast(kast["body"], symbolTable))
-        contexStr   = "context alias " + body
+        contextStr  = "context alias " + body
         requiresStr = ""
         attsStr     = prettyPrintKast(kast['att'], symbolTable)
         if kast['requires'] is not None:
             requiresStr = prettyPrintKast(kast['requires'], symbolTable)
             requiresStr = 'requires ' + indent(requiresStr)
-        return contextStr + "\n  " + requiresStr + "\n  " + attStr
+        return contextStr + "\n  " + requiresStr + "\n  " + attsStr
     if isKAtt(kast):
         if len(kast['att']) == 0:
             return ''
         attStrs = [ att + '(' + kast['att'][att] + ')' for att in kast['att'].keys() ]
-        return '[ ' + ' '.join(attStrs) + ' ]'
+        return '[' + ', '.join(attStrs) + ']'
     if isKSortSynonym(kast):
-        return 'sort ' + kast['newSort'] + ' = ' + kast['oldSort'] + ' ' + prettyPrintKast(kast['att'])
+        return 'sort ' + kast['newSort'] + ' = ' + kast['oldSort'] + ' ' + prettyPrintKast(kast['att'], symbolTable)
+    if isKModuleComment(kast):
+        return '// ' + kast['comment']
     if isKFlatModule(kast):
         name = kast["name"]
         imports = "\n".join(['import ' + kimport for kimport in kast["imports"]])

k-distribution/src/main/scripts/lib/pyk/kastManip.py

@@ -13,8 +13,7 @@ def match(pattern, kast):
     if isKToken(pattern) and isKToken(kast):
         return {} if pattern["token"] == kast["token"] else None
     if  isKApply(pattern) and isKApply(kast) \
-    and pattern["label"] == kast["label"] and pattern["arity"] == kast["arity"]:
-        subst = {}
+    and pattern["label"] == kast["label"] and len(pattern["args"]) == len(kast["args"]):
         for (patternArg, kastArg) in zip(pattern["args"], kast["args"]):
             argSubst = match(patternArg, kastArg)
             subst = combineDicts(subst, argSubst)
@@ -25,6 +24,13 @@ def match(pattern, kast):
         lhsSubst = match(pattern['lhs'], kast['lhs'])
         rhsSubst = match(pattern['rhs'], kast['rhs'])
         return combineDicts(lhsSubst, rhsSubst)
+    if isKSequence(pattern) and isKSequence(kast) and len(pattern['items']) == len(kast['items']):
+        for (patternItem, substItem) in zip(pattern['items'], kast['items']):
+            itemSubst = match(patternItem, substItem)
+            subst = combineDicts(subst, itemSubst)
+            if subst is None:
+                return None
+        return subst
     return None
 
 def onChildren(kast, effect):
@@ -262,6 +268,9 @@ def onAttributes(kast, effect):
     _fatal('No attributes for: ' + kast['node'] + '.')
 
 def minimizeRule(rule):
+    if not isKRule(rule):
+        return rule
+
     ruleBody     = rule["body"]
     ruleRequires = rule["requires"]
     ruleEnsures  = rule["ensures"]
@@ -293,11 +302,18 @@ def minimizeRule(rule):
     ruleBody = uselessVarsToDots(ruleBody, requires = ruleRequires, ensures = ruleEnsures)
     ruleBody = collapseDots(ruleBody)
 
-    if (ruleRequires == KToken("true", "Bool")):
+    if ruleRequires == KToken("true", "Bool"):
         ruleRequires = None
 
     return KRule(ruleBody, requires = ruleRequires, ensures = ruleEnsures, att = ruleAtts)
 
+def pushDownRewritesRule(rule):
+    if not isKRule(rule):
+        return rule
+
+    newRuleBody = pushDownRewrites(rule['body'])
+    return KRule(newRuleBody, requires = rule['requires'], ensures = rule['ensures'], att = rule['att'])
+
 def removeSourceMap(k):
     """Remove source map information from a given definition.
 

k-distribution/tests/pyk/.gitignore

@@ -2,3 +2,4 @@
 /kast-tests/*.gen
 /llvm
 /haskell
+/kpyk-tests/*.coverage