Upstream Summarizer utils

k-distribution/src/main/scripts/lib/.isort.cfg

@@ -0,0 +1,4 @@
+[settings]
+multi_line_output=3
+include_trailing_comma=true
+ensure_newline_before_comments=true

k-distribution/src/main/scripts/lib/Makefile

@@ -0,0 +1,16 @@
+.PHONY: all test test-code-style test-flake8 test-isort isort
+
+all: test
+
+test: test-code-style
+
+test-code-style: test-flake8 test-isort
+
+test-flake8:
+	flake8 . --ignore=E501
+
+test-isort:
+	isort . --check
+
+isort:
+	isort .

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

@@ -1,11 +0,0 @@
-#!/usr/bin/env python3
-
-import os
-import subprocess
-import sys
-import tempfile
-
-from .kast      import *
-from .kastManip import *
-from .coverage  import *
-from .ktool     import *

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

@@ -1,62 +1,80 @@
-#!/usr/bin/env python3
-
 import argparse
-from   graphviz import Digraph
-import tempfile
+import json
 import os.path as path
 import sys
-
-from .      import *
-from .cli_utils import notif, warning
+from pathlib import Path
+
+from graphviz import Digraph
+
+from .cli_utils import fatal, notif, warning
+from .coverage import getRuleById, stripCoverageLogger
+from .kast import (
+    KApply,
+    KConstant,
+    buildSymbolTable,
+    flattenLabel,
+    prettyPrintKast,
+    readKastTerm,
+)
+from .kastManip import (
+    minimizeRule,
+    minimizeTerm,
+    propagateUpConstraints,
+    removeSourceMap,
+    splitConfigAndConstraints,
+)
 from .ktool import KPrint, KProve
+from .prelude import buildAssoc
 
 pykArgs = argparse.ArgumentParser()
-pykArgs.add_argument('kompiled-dir', type = str, help = 'Kompiled directory for definition.')
+pykArgs.add_argument('kompiled-dir', type=str, help='Kompiled directory for definition.')
+
+pykCommandParsers = pykArgs.add_subparsers(dest='command')
 
-pykCommandParsers = pykArgs.add_subparsers(dest = 'command')
+kprintArgs = pykCommandParsers.add_parser('print', help='Pretty print a term.')
+kprintArgs.add_argument('term', type=argparse.FileType('r'), help='Input term (in JSON).')
+kprintArgs.add_argument('--minimize', default=True, action='store_true', help='Minimize the JSON configuration before printing.')
+kprintArgs.add_argument('--no-minimize', dest='minimize', action='store_false', help='Do not minimize the JSON configuration before printing.')
+kprintArgs.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.')
+kprintArgs.add_argument('--output-file', type=argparse.FileType('w'), default='-')
 
-kprintArgs = pykCommandParsers.add_parser('print', help = 'Pretty print a term.')
-kprintArgs.add_argument('term', type = argparse.FileType('r'), help = 'Input term (in JSON).')
-kprintArgs.add_argument('--minimize', default = True, action = 'store_true', help = 'Minimize the JSON configuration before printing.')
-kprintArgs.add_argument('--no-minimize', dest = 'minimize', action = 'store_false', help = 'Do not minimize the JSON configuration before printing.')
-kprintArgs.add_argument('--omit-labels', default = '', nargs = '?', help = 'List of labels to omit from output.')
-kprintArgs.add_argument('--output-file', type = argparse.FileType('w'), default = '-')
+kproveArgs = pykCommandParsers.add_parser('prove', help='Prove an input specification (using kprovex).')
+kproveArgs.add_argument('main-file', type=str, help='Main file used for kompilation.')
+kproveArgs.add_argument('spec-file', type=str, help='File with the specification module.')
+kproveArgs.add_argument('spec-module', type=str, help='Module with claims to be proven.')
+kproveArgs.add_argument('--output-file', type=argparse.FileType('w'), default='-')
+kproveArgs.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
 
-kproveArgs = pykCommandParsers.add_parser('prove', help = 'Prove an input specification (using kprovex).')
-kproveArgs.add_argument('main-file', type = str, help = 'Main file used for kompilation.')
-kproveArgs.add_argument('spec-file', type = str, help = 'File with the specification module.')
-kproveArgs.add_argument('spec-module', type = str, help = 'Module with claims to be proven.')
-kproveArgs.add_argument('--output-file', type = argparse.FileType('w'), default = '-')
-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.')
 
-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='-')
 
-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))
 
-def main(commandLineArgs, extraMain = None):
+
+def main(commandLineArgs, extraMain=None):
     returncode = 0
     args = vars(commandLineArgs.parse_args())
     kompiled_dir = Path(args['kompiled-dir'])
 
     if args['command'] == 'print':
         printer = KPrint(kompiled_dir)
-        term    = json.loads(args['term'].read())
+        term = json.loads(args['term'].read())
         if 'term' in term:
             term = term['term']
         if term == KConstant('#Top'):
             args['output_file'].write(printer.prettyPrint(term))
         else:
             if args['minimize']:
-                abstractLabels     = [] if args['omit_labels'] is None else args['omit_labels'].split(',')
+                abstractLabels = [] if args['omit_labels'] is None else args['omit_labels'].split(',')
                 minimizedDisjuncts = []
                 for d in flattenLabel('#Or', term):
-                    dMinimized = minimizeTerm(d, abstractLabels = abstractLabels)
-                    (dConfig, dConstraint) = splitConfigAndConstraints(dMinimized)
+                    dMinimized = minimizeTerm(d, abstractLabels=abstractLabels)
+                    dConfig, dConstraint = splitConfigAndConstraints(dMinimized)
                     if dConstraint != KConstant('#Top'):
                         minimizedDisjuncts.append(KApply('#And', [dConfig, dConstraint]))
                     else:
@@ -65,17 +83,17 @@ def main(commandLineArgs, extraMain = None):
             args['output_file'].write(printer.prettyPrint(term))
 
     elif args['command'] == 'prove':
-        kprover    = KProve(kompiled_dir, args['main-file'])
-        finalState = kprover.prove(Path(args['spec-file']), args['spec-module'], args = args['kArgs'])
+        kprover = KProve(kompiled_dir, args['main-file'])
+        finalState = kprover.prove(Path(args['spec-file']), args['spec-module'], args=args['kArgs'])
         args['output_file'].write(json.dumps(finalState))
         if finalState != KConstant('#Top'):
             warning('Proof failed!')
 
     elif args['command'] == 'graph-imports':
-        kprinter    = KPrint(kompiled_dir)
-        kDefn       = kprinter.definition
+        kprinter = KPrint(kompiled_dir)
+        kDefn = kprinter.definition
         importGraph = Digraph()
-        graphFile   = kompiled_dir / 'import-graph'
+        graphFile = kompiled_dir / 'import-graph'
         for module in kDefn['modules']:
             modName = module['name']
             importGraph.node(modName)
@@ -98,7 +116,8 @@ def main(commandLineArgs, extraMain = None):
         extraMain(args, kompiled_dir)
 
     if returncode != 0:
-        _fatal('Non-zero exit code (' + str(returncode) + '): ' + str(kCommand), code = returncode)
+        fatal('Non-zero exit code (' + str(returncode) + '): ' + str(args['command']))
+
 
 if __name__ == '__main__':
     # KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...).

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

@@ -1,11 +1,14 @@
-#!/usr/bin/env python3
-
-import json
-import sys
-
 from .cli_utils import fatal
-from .kast      import *
-from .kastManip import *
+from .kast import (
+    KRewrite,
+    KRule,
+    isKApply,
+    isKRewrite,
+    isKRule,
+    isKSequence,
+    readKastTerm,
+)
+
 
 def getRuleById(definition, rule_id):
     """Get a rule from the definition by coverage rule id.
@@ -26,11 +29,12 @@ def getRuleById(definition, rule_id):
                     return sentence
     fatal('Could not find rule with ID: ' + rule_id)
 
+
 def stripCoverageLogger(rule):
-    ruleBody     = rule['body']
+    ruleBody = rule['body']
     ruleRequires = rule['requires']
-    ruleEnsures  = rule['ensures']
-    ruleAtts     = rule['att']
+    ruleEnsures = rule['ensures']
+    ruleAtts = rule['att']
 
     if isKRewrite(ruleBody):
         ruleLHS = ruleBody['lhs']
@@ -39,7 +43,8 @@ def stripCoverageLogger(rule):
             ruleRHSseq = ruleRHS['args'][0]
             if isKSequence(ruleRHSseq) and len(ruleRHSseq['items']) == 2:
                 ruleBody = KRewrite(ruleLHS, ruleRHSseq['items'][1])
-    return KRule(ruleBody, requires = ruleRequires, ensures = ruleEnsures, att = ruleAtts)
+    return KRule(ruleBody, requires=ruleRequires, ensures=ruleEnsures, att=ruleAtts)
+
 
 def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_list):
     """Translate the coverage data from one kompiled definition to another.
@@ -57,28 +62,28 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li
     # Load the src_rule_id -> src_source_location rule map from the src kompiled directory
     src_rule_map = {}
     for line in src_all_rules:
-        [ src_rule_hash, src_rule_loc ] = line.split(' ')
+        src_rule_hash, src_rule_loc = line.split(' ')
         src_rule_loc = src_rule_loc.split('/')[-1]
         src_rule_map[src_rule_hash.strip()] = src_rule_loc.strip()
 
     # Load the dst_rule_id -> dst_source_location rule map (and inverts it) from the dst kompiled directory
     dst_rule_map = {}
     for line in dst_all_rules:
-        [ dst_rule_hash, dst_rule_loc ] = line.split(' ')
+        dst_rule_hash, dst_rule_loc = line.split(' ')
         dst_rule_loc = dst_rule_loc.split('/')[-1]
         dst_rule_map[dst_rule_loc.strip()] = dst_rule_hash.strip()
 
-    src_rule_list = [ rule_hash.strip() for rule_hash in src_rules_list ]
+    src_rule_list = [rule_hash.strip() for rule_hash in src_rules_list]
 
     # Filter out non-functional rules from rule map (determining if they are functional via the top symbol in the rule being `<generatedTop>`)
     dst_non_function_rules = []
     for module in dst_definition['modules']:
         for sentence in module['localSentences']:
             if isKRule(sentence):
                 ruleBody = sentence['body']
-                ruleAtt  = sentence['att']['att']
-                if    (isKApply(ruleBody)                                 and ruleBody['label']        == '<generatedTop>') \
-                   or (isKRewrite(ruleBody) and isKApply(ruleBody['lhs']) and ruleBody['lhs']['label'] == '<generatedTop>'):
+                ruleAtt = sentence['att']['att']
+                if (isKApply(ruleBody) and ruleBody['label'] == '<generatedTop>') \
+                        or (isKRewrite(ruleBody) and isKApply(ruleBody['lhs']) and ruleBody['lhs']['label'] == '<generatedTop>'):
                     if 'UNIQUE_ID' in ruleAtt:
                         dst_non_function_rules.append(ruleAtt['UNIQUE_ID'])
 
@@ -98,6 +103,7 @@ def translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_li
 
     return dst_rule_list
 
+
 def translateCoverageFromPaths(src_kompiled_dir, dst_kompiled_dir, src_rules_file):
     """Translate coverage information given paths to needed files.
 
@@ -111,16 +117,16 @@ def translateCoverageFromPaths(src_kompiled_dir, dst_kompiled_dir, src_rules_fil
     """
     src_all_rules = []
     with open(src_kompiled_dir + '/allRules.txt', 'r') as src_all_rules_file:
-        src_all_rules = [ line.strip() for line in src_all_rules_file ]
+        src_all_rules = [line.strip() for line in src_all_rules_file]
 
     dst_all_rules = []
     with open(dst_kompiled_dir + '/allRules.txt', 'r') as dst_all_rules_file:
-        dst_all_rules = [ line.strip() for line in dst_all_rules_file ]
+        dst_all_rules = [line.strip() for line in dst_all_rules_file]
 
     dst_definition = readKastTerm(dst_kompiled_dir + '/compiled.json')
 
     src_rules_list = []
     with open(src_rules_file, 'r') as src_rules:
-        src_rules_list = [ line.strip() for line in src_rules ]
+        src_rules_list = [line.strip() for line in src_rules]
 
     return translateCoverage(src_all_rules, dst_all_rules, dst_definition, src_rules_list)