From 30db060f50832ad1b2a520120f85d7a71a993dde Mon Sep 17 00:00:00 2001 From: ehildenb Date: Thu, 26 Mar 2020 18:51:11 +0100 Subject: [PATCH] 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 --- .../src/main/scripts/lib/pyk/__init__.py | 7 +- .../src/main/scripts/lib/pyk/__main__.py | 123 ++++++++++-------- .../src/main/scripts/lib/pyk/definition.py | 54 ++++++++ .../src/main/scripts/lib/pyk/kast.py | 72 ++++++++-- .../src/main/scripts/lib/pyk/kastManip.py | 22 +++- k-distribution/tests/pyk/.gitignore | 1 + k-distribution/tests/pyk/Makefile | 12 +- .../org/kframework/definition/outer.scala | 2 +- 8 files changed, 220 insertions(+), 73 deletions(-) create mode 100644 k-distribution/src/main/scripts/lib/pyk/definition.py diff --git a/k-distribution/src/main/scripts/lib/pyk/__init__.py b/k-distribution/src/main/scripts/lib/pyk/__init__.py index 740b5db9a42..f9672b7cc1a 100755 --- a/k-distribution/src/main/scripts/lib/pyk/__init__.py +++ b/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) diff --git a/k-distribution/src/main/scripts/lib/pyk/__main__.py b/k-distribution/src/main/scripts/lib/pyk/__main__.py index b51d0e1b908..ee5b0fa7648 100644 --- a/k-distribution/src/main/scripts/lib/pyk/__main__.py +++ b/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 == '': + 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) diff --git a/k-distribution/src/main/scripts/lib/pyk/definition.py b/k-distribution/src/main/scripts/lib/pyk/definition.py new file mode 100644 index 00000000000..7022a763b50 --- /dev/null +++ b/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 diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 497add97629..ced7a3bfc7c 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/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"]]) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index a0402a87b73..eef8cd6ac9a 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/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. diff --git a/k-distribution/tests/pyk/.gitignore b/k-distribution/tests/pyk/.gitignore index 081a0710e37..ec448ac54cb 100644 --- a/k-distribution/tests/pyk/.gitignore +++ b/k-distribution/tests/pyk/.gitignore @@ -2,3 +2,4 @@ /kast-tests/*.gen /llvm /haskell +/kpyk-tests/*.coverage diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index b9250488d1f..457fe70d48c 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/k-distribution/tests/pyk/Makefile @@ -12,7 +12,8 @@ PYTHONPATH := $(K_LIB) export PYTHONPATH .PHONY: all clean pyk \ - test test-defn test-defn-kast test-defn-prove + test test-defn test-defn-kast test-defn-prove \ + test-kpyk test-kpyk-coverage-log all: test @@ -78,9 +79,14 @@ $(defn_tests)/proof-tests/%-spec.json.prove: $(defn_tests)/proof-tests/%-spec.k ## kpyk runner tests +sum_to_n_coverage := kpyk-tests/sum-to-n.imp.coverage + test-kpyk: test-kpyk-coverage-log -test-kpyk-coverage-log: $(llvm_imp_kompiled) +$(sum_to_n_coverage): $(llvm_imp_kompiled) kpyk-tests/sum-to-n.imp rm -rf $(llvm_dir)/imp-kompiled/*_coverage.txt $(KRUN) --directory $(llvm_dir) kpyk-tests/sum-to-n.imp - $(KPYK) coverage-log --coverage-file $(llvm_dir)/imp-kompiled/*_coverage.txt --definition $(llvm_dir)/imp-kompiled + mv $(llvm_dir)/imp-kompiled/*_coverage.txt $@ + +test-kpyk-coverage-log: $(sum_to_n_coverage) + $(KPYK) $(llvm_dir)/imp-kompiled coverage $(sum_to_n_coverage) diff --git a/kore/src/main/scala/org/kframework/definition/outer.scala b/kore/src/main/scala/org/kframework/definition/outer.scala index 2c4f52a1415..d0a2e845198 100644 --- a/kore/src/main/scala/org/kframework/definition/outer.scala +++ b/kore/src/main/scala/org/kframework/definition/outer.scala @@ -330,7 +330,7 @@ case class Module(val name: String, val imports: Set[Module], localSentences: Se case m: Module => m.name == name && m.sentences == sentences } - def flattened() : FlatModule = new FlatModule(name, imports.map(m => m.name), sentences, att) + def flattened() : FlatModule = new FlatModule(name, imports.map(m => m.name), localSentences, att) def flatModules() : (String, Set[FlatModule]) = (name, Set(flattened) ++ imports.map(m => m.flatModules._2).flatten) }