Organize pyk utils

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

@@ -5,7 +5,6 @@
 import sys
 import tempfile
 
-from .util      import *
 from .kast      import *
 from .kastManip import *
 from .coverage  import *

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

@@ -7,6 +7,7 @@
 import sys
 
 from .      import *
+from .cli_utils import notif, warning
 from .ktool import KPrint, KProve
 
 pykArgs = argparse.ArgumentParser()

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

@@ -0,0 +1,54 @@
+import sys
+import time
+from datetime import datetime
+from pathlib import Path
+
+_last_time = time.time()
+
+
+def check_dir_path(path: Path) -> None:
+    if not path.exists():
+        raise ValueError(f'Directory does not exist: {path}')
+    if not path.is_dir():
+        raise ValueError(f'Path is not a directory: {path}')
+
+
+def dir_path(s: str) -> Path:
+    path = Path(s)
+    check_dir_path(path)
+    return path
+
+
+def check_file_path(path: Path) -> None:
+    if not path.exists():
+        raise ValueError(f'File does not exist: {path}')
+    if not path.is_file():
+        raise ValueError(f'Path is not a file: {path}')
+
+
+def file_path(s: str) -> Path:
+    path = Path(s)
+    check_file_path(path)
+    return path
+
+
+def notif(msg: str):
+    global _last_time
+    curr_time = time.time()
+    time_diff = curr_time - _last_time
+    _last_time = curr_time
+    sys.stderr.write('== ' + sys.argv[0].split('/')[-1] + ' [+' + '{0:8.2f}'.format(time_diff) + ']: ' + msg + '\n')
+    sys.stderr.flush()
+
+
+def warning(msg: str):
+    notif('[WARNING] ' + msg)
+
+
+def fatal(msg: str):
+    notif('[FATAL] ' + msg)
+    sys.exit('Quitting')
+
+
+def gen_file_timestamp(comment='//'):
+    return comment + ' This file generated by: ' + sys.argv[0] + '\n' + comment + ' ' + str(datetime.now()) + '\n'

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

@@ -3,7 +3,7 @@
 import json
 import sys
 
-from .util      import *
+from .cli_utils import fatal
 from .kast      import *
 from .kastManip import *
 

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

@@ -3,7 +3,8 @@
 import sys
 import json
 
-from .util import *
+from .cli_utils import fatal, notif, warning
+from .utils import combine_dicts
 
 def KApply(label, args):
     return { 'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args }
@@ -183,7 +184,7 @@ def addAttributes(kast, att):
     -   Output: Same Kast term, with the attributes overwritten/added.
     """
     if isKAtt(kast):
-        return KAtt(combineDicts(att, kast['att']))
+        return KAtt(combine_dicts(att, kast['att']))
     newAtt = KAtt(att) if not ('att' in kast and kast['att'] is not None and isKAtt(kast['att'])) else addAttributes(kast['att'], att)
     if isKRule(kast):
         return KRule(kast['body'], requires = kast['requires'], ensures = kast['ensures'], att = newAtt)

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

@@ -3,6 +3,8 @@
 import sys
 import subprocess
 
+from .cli_utils import fatal
+from .utils import combine_dicts, dedupe, find_common_items
 from .kast import *
 
 def buildAssoc(unit, join, ls):
@@ -45,18 +47,18 @@ def match(pattern, kast):
     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)
+            subst = combine_dicts(subst, argSubst)
             if subst is None:
                 return None
         return subst
     if isKRewrite(pattern) and isKRewrite(kast):
         lhsSubst = match(pattern['lhs'], kast['lhs'])
         rhsSubst = match(pattern['rhs'], kast['rhs'])
-        return combineDicts(lhsSubst, rhsSubst)
+        return combine_dicts(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)
+            subst = combine_dicts(subst, itemSubst)
             if subst is None:
                 return None
         return subst
@@ -241,8 +243,8 @@ def _propagateUpConstraints(_k):
             return _k
         conjuncts1        = flattenLabel('#And', _k['args'][0])
         conjuncts2        = flattenLabel('#And', _k['args'][1])
-        (common1, l1, r1) = findCommonItems(conjuncts1, conjuncts2)
-        (common2, r2, l2) = findCommonItems(r1, l1)
+        (common1, l1, r1) = find_common_items(conjuncts1, conjuncts2)
+        (common2, r2, l2) = find_common_items(r1, l1)
         common = common1 + common2
         if len(common) == 0:
             return _k

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

@@ -3,7 +3,10 @@
 import os
 from   pathlib    import Path
 import subprocess
+from typing import List
 
+from .cli_utils import gen_file_timestamp, notif
+from .utils import hash_str
 from .kastManip import *
 
 class KPrint:
@@ -14,7 +17,7 @@ def __init__(self, kompiledDirectory):
         self.kompiledDirectory = Path(kompiledDirectory)
         self.definition        = readKastTerm(self.kompiledDirectory / 'compiled.json')
         self.symbolTable       = buildSymbolTable(self.definition, opinionated = True)
-        self.definitionHash    = strHash(self.definition)
+        self.definitionHash    = hash_str(self.definition)
 
     def prettyPrint(self, kast, debug = False):
         """Given a KAST term, pretty-print it using the current definition.
@@ -67,7 +70,7 @@ def prove(self, specFile, specModuleName, args = [], haskellArgs = [], logAxioms
             sys.stderr.write(stdout + '\n')
             sys.stderr.write(stderr + '\n')
             fatal('Exiting...', exitCode = process.returncode)
-        if finalState == KConstant('#Top') and len(getAppliedAxiomList(logFile)) == 0 and not allowZeroStep:
+        if finalState == KConstant('#Top') and len(_getAppliedAxiomList(logFile)) == 0 and not allowZeroStep:
             fatal('Proof took zero steps, likely the LHS is invalid: ' + str(specFile))
         return finalState
 
@@ -89,7 +92,7 @@ def proveClaimNoBranching(self, claim, claimId, args = [], haskellArgs = [], log
         logFileName = logAxiomsFile if logAxiomsFile is not None else (self.useDirectory / claimId.lower()).with_suffix('.debug.log')
         nextState   = self.proveClaim(claim, claimId, args = (args + ['--branching-allowed', '1', '--depth', str(maxDepth)]), haskellArgs = haskellArgs, logAxiomsFile = logFileName, allowZeroStep = allowZeroStep)
         depth       = 0
-        for axioms in getAppliedAxiomList(str(logFileName)):
+        for axioms in _getAppliedAxiomList(str(logFileName)):
             depth += 1
             if len(axioms) > 1:
                 break
@@ -108,7 +111,21 @@ def _writeClaimDefinition(self, claim, claimId, lemmas = [], rule = False):
         with open(tmpClaim, 'w') as tc:
             claimModule     = KFlatModule(tmpModuleName, [KImport(self.mainModule, True)], lemmas + [claim])
             claimDefinition = KDefinition(tmpModuleName, [claimModule], requires = [KRequire(self.mainFileName)])
-            tc.write(genFileTimestamp() + '\n')
+            tc.write(gen_file_timestamp() + '\n')
             tc.write(self.prettyPrint(claimDefinition) + '\n\n')
             tc.flush()
         notif('Wrote claim file: ' + str(tmpClaim) + '.')
+
+
+def _getAppliedAxiomList(debugLogFile: Path) -> List[List[str]]:
+    axioms = []
+    next_axioms = []
+    with open(debugLogFile, 'r') as logFile:
+        for line in logFile:
+            if line.find('DebugTransition') > 0:
+                if line.find('after  apply axioms:') > 0:
+                    next_axioms.append(line[line.find('after  apply axioms:') + len('after  apply axioms:'):])
+                elif len(next_axioms) > 0:
+                    axioms.append(next_axioms)
+                    next_axioms = []
+    return axioms

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

@@ -0,0 +1,75 @@
+import hashlib
+from typing import Any, Dict, Iterable, List, Mapping, Optional, Tuple, TypeVar
+
+T = TypeVar('T')
+
+
+def combine_dicts(*dicts: Mapping) -> Optional[Dict]:
+    if len(dicts) == 0:
+        return {}
+    if len(dicts) == 1:
+        return dict(dicts[0])
+    dict1 = dicts[0]
+    dict2 = dicts[1]
+    restDicts = dicts[2:]
+    if dict1 is None or dict2 is None:
+        return None
+    intersecting_keys = set(dict1.keys()).intersection(set(dict2.keys()))
+    for key in intersecting_keys:
+        if dict1[key] != dict2[key]:
+            return None
+    newDict = {key: dict1[key] for key in dict1}
+    for key in dict2.keys():
+        newDict[key] = dict2[key]
+    return combine_dicts(newDict, *restDicts)
+
+
+def merge_with(f, d1: Mapping, d2: Mapping) -> Dict:
+    res = dict(d1)
+    for k, v2 in d2.items():
+        if k in d1:
+            v1 = d1[k]
+            res[k] = f(v1, v2)
+        else:
+            res[k] = v2
+    return res
+
+
+def find_common_items(l1: Iterable[T], l2: Iterable[T]) -> Tuple[List[T], List[T], List[T]]:
+    common = []
+    for i in l1:
+        if i in l2:
+            common.append(i)
+    newL1 = []
+    newL2 = []
+    for i in l1:
+        if i not in common:
+            newL1.append(i)
+    for i in l2:
+        if i not in common:
+            newL2.append(i)
+    return (common, newL1, newL2)
+
+
+def dedupe(xs: Iterable[T]) -> List[T]:
+    res = []
+    for x in xs:
+        if x not in res:
+            res.append(x)
+    return res
+
+
+def hash_str(x: Any) -> str:
+    hash = hashlib.sha256()
+    hash.update(str(x).encode('utf-8'))
+    return str(hash.hexdigest())
+
+
+def nonempty_str(x: Any) -> str:
+    if x is None:
+        raise ValueError('Expected nonempty string, found: null.')
+    if type(x) is not str:
+        raise TypeError('Expected nonempty string, found: {type(x)}')
+    if x == '':
+        raise ValueError("Expected nonempty string, found: ''")
+    return x