From a52c12219eb512df55ed4d483681ea3f7235b78d Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 10:22:24 +0100 Subject: [PATCH 01/14] Add module cli_utils --- .../src/main/scripts/lib/pyk/cli_utils.py | 27 +++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 k-distribution/src/main/scripts/lib/pyk/cli_utils.py diff --git a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py new file mode 100644 index 00000000000..1151bd9f26b --- /dev/null +++ b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py @@ -0,0 +1,27 @@ +from pathlib import Path + + +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 From 726b5f9949f95ab63a756dc7caa2b5773f923b51 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 10:54:42 +0100 Subject: [PATCH 02/14] Move some functions from util to cli_utils --- .../src/main/scripts/lib/pyk/__main__.py | 1 + .../src/main/scripts/lib/pyk/cli_utils.py | 28 +++++++++++++++++++ .../src/main/scripts/lib/pyk/coverage.py | 1 + .../src/main/scripts/lib/pyk/kast.py | 1 + .../src/main/scripts/lib/pyk/kastManip.py | 1 + .../src/main/scripts/lib/pyk/ktool.py | 1 + .../src/main/scripts/lib/pyk/util.py | 22 --------------- 7 files changed, 33 insertions(+), 22 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__main__.py b/k-distribution/src/main/scripts/lib/pyk/__main__.py index 184163a9aea..48a9d01e769 100644 --- a/k-distribution/src/main/scripts/lib/pyk/__main__.py +++ b/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() diff --git a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py index 1151bd9f26b..b476ceecb97 100644 --- a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py @@ -1,6 +1,12 @@ +import sys +import time +from datetime import datetime from pathlib import Path +_lastTime = time.time() + + def check_dir_path(path: Path) -> None: if not path.exists(): raise ValueError(f'Directory does not exist: {path}') @@ -25,3 +31,25 @@ def file_path(s: str) -> Path: path = Path(s) check_file_path(path) return path + + +def notif(msg): + global _lastTime + curTime = time.time() + diffTime = curTime - _lastTime + _lastTime = curTime + sys.stderr.write('== ' + sys.argv[0].split('/')[-1] + ' [+' + '{0:8.2f}'.format(diffTime) + ']: ' + msg + '\n') + sys.stderr.flush() + + +def warning(msg): + notif('[WARNING] ' + msg) + + +def fatal(msg, exitCode = 1): + notif('[FATAL] ' + msg) + raise('Quitting') + + +def genFileTimestamp(comment = '//'): + return comment + ' This file generated by: ' + sys.argv[0] + '\n' + comment + ' ' + str(datetime.now()) + '\n' diff --git a/k-distribution/src/main/scripts/lib/pyk/coverage.py b/k-distribution/src/main/scripts/lib/pyk/coverage.py index 63ef69bb618..cfba1549777 100755 --- a/k-distribution/src/main/scripts/lib/pyk/coverage.py +++ b/k-distribution/src/main/scripts/lib/pyk/coverage.py @@ -3,6 +3,7 @@ import json import sys +from .cli_utils import fatal from .util import * from .kast import * from .kastManip import * diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 57fe68d7559..86dcb29146f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/k-distribution/src/main/scripts/lib/pyk/kast.py @@ -3,6 +3,7 @@ import sys import json +from .cli_utils import fatal, notif, warning from .util import * def KApply(label, args): diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index c159f82fe99..b48635f432f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -3,6 +3,7 @@ import sys import subprocess +from .cli_utils import fatal from .kast import * def buildAssoc(unit, join, ls): diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 2e4e400427a..8662e6aa7c0 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -4,6 +4,7 @@ from pathlib import Path import subprocess +from .cli_utils import genFileTimestamp, notif from .kastManip import * class KPrint: diff --git a/k-distribution/src/main/scripts/lib/pyk/util.py b/k-distribution/src/main/scripts/lib/pyk/util.py index d0cb15ee079..e2740da213f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/util.py +++ b/k-distribution/src/main/scripts/lib/pyk/util.py @@ -1,11 +1,7 @@ #!/usr/bin/env python3 -from datetime import datetime import hashlib -import sys -import time -_lastTime = time.time() def combineDicts(*dicts): if len(dicts) == 0: @@ -48,24 +44,6 @@ def dedupe(ls): newL.append(l) return newL -def notif(msg): - global _lastTime - curTime = time.time() - diffTime = curTime - _lastTime - _lastTime = curTime - sys.stderr.write('== ' + sys.argv[0].split('/')[-1] + ' [+' + '{0:8.2f}'.format(diffTime) + ']: ' + msg + '\n') - sys.stderr.flush() - -def warning(msg): - notif('[WARNING] ' + msg) - -def fatal(msg, exitCode = 1): - notif('[FATAL] ' + msg) - raise('Quitting') - -def genFileTimestamp(comment = '//'): - return comment + ' This file generated by: ' + sys.argv[0] + '\n' + comment + ' ' + str(datetime.now()) + '\n' - def getAppliedAxiomList(debugLogFile): axioms = [] next_axioms = [] From ab2fcb39a7e4f0daa7407946afe47ea64574d78b Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 10:58:20 +0100 Subject: [PATCH 03/14] Rename genFileTimestamp to gen_file_timestamp --- k-distribution/src/main/scripts/lib/pyk/cli_utils.py | 2 +- k-distribution/src/main/scripts/lib/pyk/ktool.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py index b476ceecb97..813ce91e5ee 100644 --- a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py @@ -51,5 +51,5 @@ def fatal(msg, exitCode = 1): raise('Quitting') -def genFileTimestamp(comment = '//'): +def gen_file_timestamp(comment='//'): return comment + ' This file generated by: ' + sys.argv[0] + '\n' + comment + ' ' + str(datetime.now()) + '\n' diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 8662e6aa7c0..aa0dc8a1fbb 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -4,7 +4,7 @@ from pathlib import Path import subprocess -from .cli_utils import genFileTimestamp, notif +from .cli_utils import gen_file_timestamp, notif from .kastManip import * class KPrint: @@ -109,7 +109,7 @@ 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) + '.') From 275611bf3f92865e237c6e6d079f5db2d7766a4a Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 11:03:28 +0100 Subject: [PATCH 04/14] Fix styling issues in cli_utils --- .../src/main/scripts/lib/pyk/cli_utils.py | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py index 813ce91e5ee..9e9bb76e4a0 100644 --- a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py @@ -3,8 +3,7 @@ from datetime import datetime from pathlib import Path - -_lastTime = time.time() +_last_time = time.time() def check_dir_path(path: Path) -> None: @@ -33,20 +32,20 @@ def file_path(s: str) -> Path: return path -def notif(msg): - global _lastTime - curTime = time.time() - diffTime = curTime - _lastTime - _lastTime = curTime - sys.stderr.write('== ' + sys.argv[0].split('/')[-1] + ' [+' + '{0:8.2f}'.format(diffTime) + ']: ' + msg + '\n') +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): +def warning(msg: str): notif('[WARNING] ' + msg) -def fatal(msg, exitCode = 1): +def fatal(msg: str, exit_code=1): notif('[FATAL] ' + msg) raise('Quitting') From 50c125c45c00d1280466e447106f3702f0967f11 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 11:15:23 +0100 Subject: [PATCH 05/14] Fix fatal --- k-distribution/src/main/scripts/lib/pyk/cli_utils.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py index 9e9bb76e4a0..70754ed5a2f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/cli_utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/cli_utils.py @@ -45,9 +45,9 @@ def warning(msg: str): notif('[WARNING] ' + msg) -def fatal(msg: str, exit_code=1): +def fatal(msg: str): notif('[FATAL] ' + msg) - raise('Quitting') + sys.exit('Quitting') def gen_file_timestamp(comment='//'): From dfd064e76acffa3e3f4ee250bffaae52c8f32b35 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 11:32:39 +0100 Subject: [PATCH 06/14] Resolve wildcard imports from util --- k-distribution/src/main/scripts/lib/pyk/__init__.py | 1 - k-distribution/src/main/scripts/lib/pyk/coverage.py | 1 - k-distribution/src/main/scripts/lib/pyk/kast.py | 2 +- k-distribution/src/main/scripts/lib/pyk/kastManip.py | 1 + k-distribution/src/main/scripts/lib/pyk/ktool.py | 1 + 5 files changed, 3 insertions(+), 3 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/__init__.py b/k-distribution/src/main/scripts/lib/pyk/__init__.py index 039c8838b01..6160b0daec9 100755 --- a/k-distribution/src/main/scripts/lib/pyk/__init__.py +++ b/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 * diff --git a/k-distribution/src/main/scripts/lib/pyk/coverage.py b/k-distribution/src/main/scripts/lib/pyk/coverage.py index cfba1549777..a1bdfc369ab 100755 --- a/k-distribution/src/main/scripts/lib/pyk/coverage.py +++ b/k-distribution/src/main/scripts/lib/pyk/coverage.py @@ -4,7 +4,6 @@ import sys from .cli_utils import fatal -from .util import * from .kast import * from .kastManip import * diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 86dcb29146f..4eb1a2240a7 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/k-distribution/src/main/scripts/lib/pyk/kast.py @@ -4,7 +4,7 @@ import json from .cli_utils import fatal, notif, warning -from .util import * +from .util import combineDicts def KApply(label, args): return { 'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args } diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index b48635f432f..420d0869117 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -4,6 +4,7 @@ import subprocess from .cli_utils import fatal +from .util import combineDicts, dedupe, findCommonItems from .kast import * def buildAssoc(unit, join, ls): diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index aa0dc8a1fbb..9c6ec194e44 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -5,6 +5,7 @@ import subprocess from .cli_utils import gen_file_timestamp, notif +from .util import getAppliedAxiomList, strHash from .kastManip import * class KPrint: From 7a89ec92bb81d3c3e9a62b517b0f59064dafd589 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 11:37:46 +0100 Subject: [PATCH 07/14] Rename util to utils --- k-distribution/src/main/scripts/lib/pyk/kast.py | 2 +- k-distribution/src/main/scripts/lib/pyk/kastManip.py | 2 +- k-distribution/src/main/scripts/lib/pyk/ktool.py | 2 +- k-distribution/src/main/scripts/lib/pyk/{util.py => utils.py} | 0 4 files changed, 3 insertions(+), 3 deletions(-) rename k-distribution/src/main/scripts/lib/pyk/{util.py => utils.py} (100%) diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 4eb1a2240a7..7fb047fbc81 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/k-distribution/src/main/scripts/lib/pyk/kast.py @@ -4,7 +4,7 @@ import json from .cli_utils import fatal, notif, warning -from .util import combineDicts +from .utils import combineDicts def KApply(label, args): return { 'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args } diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 420d0869117..efbb96d7027 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -4,7 +4,7 @@ import subprocess from .cli_utils import fatal -from .util import combineDicts, dedupe, findCommonItems +from .utils import combineDicts, dedupe, findCommonItems from .kast import * def buildAssoc(unit, join, ls): diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 9c6ec194e44..7f7fc930c1b 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -5,7 +5,7 @@ import subprocess from .cli_utils import gen_file_timestamp, notif -from .util import getAppliedAxiomList, strHash +from .utils import getAppliedAxiomList, strHash from .kastManip import * class KPrint: diff --git a/k-distribution/src/main/scripts/lib/pyk/util.py b/k-distribution/src/main/scripts/lib/pyk/utils.py similarity index 100% rename from k-distribution/src/main/scripts/lib/pyk/util.py rename to k-distribution/src/main/scripts/lib/pyk/utils.py From 9b39248c2ce8361f9b7bca3395ebe3c731cf399f Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 11:42:39 +0100 Subject: [PATCH 08/14] Fix styling issues in utils --- .../src/main/scripts/lib/pyk/utils.py | 26 ++++++++++--------- 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index e2740da213f..ec4008956e8 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -1,5 +1,3 @@ -#!/usr/bin/env python3 - import hashlib @@ -17,11 +15,12 @@ def combineDicts(*dicts): for key in intersecting_keys: if dict1[key] != dict2[key]: return None - newDict = { key : dict1[key] for key in dict1 } + newDict = {key: dict1[key] for key in dict1} for key in dict2.keys(): newDict[key] = dict2[key] return combineDicts(newDict, *restDicts) + def findCommonItems(l1, l2): common = [] for i in l1: @@ -30,22 +29,24 @@ def findCommonItems(l1, l2): newL1 = [] newL2 = [] for i in l1: - if not i in common: + if i not in common: newL1.append(i) for i in l2: - if not i in common: + if i not in common: newL2.append(i) return (common, newL1, newL2) -def dedupe(ls): - newL = [] - for l in ls: - if l not in newL: - newL.append(l) - return newL + +def dedupe(xs): + res = [] + for x in xs: + if x not in res: + res.append(x) + return res + def getAppliedAxiomList(debugLogFile): - axioms = [] + axioms = [] next_axioms = [] with open(debugLogFile, 'r') as logFile: for line in logFile: @@ -57,6 +58,7 @@ def getAppliedAxiomList(debugLogFile): next_axioms = [] return axioms + def strHash(k): hash = hashlib.sha256() hash.update(str(k).encode('utf-8')) From 4acbb8c9b63b595db03d5676b781b25efc7e7d9c Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 12:00:36 +0100 Subject: [PATCH 09/14] Add type hints to utils --- k-distribution/src/main/scripts/lib/pyk/utils.py | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index ec4008956e8..9058bd74f25 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -1,11 +1,15 @@ import hashlib +from pathlib import Path +from typing import Any, Dict, Iterable, List, Mapping, Optional, Tuple, TypeVar +T = TypeVar('T') -def combineDicts(*dicts): + +def combineDicts(*dicts: Mapping) -> Optional[Dict]: if len(dicts) == 0: return {} if len(dicts) == 1: - return dicts[0] + return dict(dicts[0]) dict1 = dicts[0] dict2 = dicts[1] restDicts = dicts[2:] @@ -21,7 +25,7 @@ def combineDicts(*dicts): return combineDicts(newDict, *restDicts) -def findCommonItems(l1, l2): +def findCommonItems(l1: Iterable[T], l2: Iterable[T]) -> Tuple[List[T], List[T], List[T]]: common = [] for i in l1: if i in l2: @@ -37,7 +41,7 @@ def findCommonItems(l1, l2): return (common, newL1, newL2) -def dedupe(xs): +def dedupe(xs: Iterable[T]) -> List[T]: res = [] for x in xs: if x not in res: @@ -45,7 +49,7 @@ def dedupe(xs): return res -def getAppliedAxiomList(debugLogFile): +def getAppliedAxiomList(debugLogFile: Path) -> List[List[str]]: axioms = [] next_axioms = [] with open(debugLogFile, 'r') as logFile: @@ -59,7 +63,7 @@ def getAppliedAxiomList(debugLogFile): return axioms -def strHash(k): +def strHash(k: Any) -> str: hash = hashlib.sha256() hash.update(str(k).encode('utf-8')) return str(hash.hexdigest()) From 4733eaed757995ec0ffd0462c3c0d196b9c32834 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 12:03:25 +0100 Subject: [PATCH 10/14] Rename strHash to hash_str --- k-distribution/src/main/scripts/lib/pyk/ktool.py | 4 ++-- k-distribution/src/main/scripts/lib/pyk/utils.py | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index 7f7fc930c1b..fd5939f0026 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -5,7 +5,7 @@ import subprocess from .cli_utils import gen_file_timestamp, notif -from .utils import getAppliedAxiomList, strHash +from .utils import getAppliedAxiomList, hash_str from .kastManip import * class KPrint: @@ -16,7 +16,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. diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index 9058bd74f25..cde76a1f014 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -63,7 +63,7 @@ def getAppliedAxiomList(debugLogFile: Path) -> List[List[str]]: return axioms -def strHash(k: Any) -> str: +def hash_str(x: Any) -> str: hash = hashlib.sha256() - hash.update(str(k).encode('utf-8')) + hash.update(str(x).encode('utf-8')) return str(hash.hexdigest()) From 5f147169689acb9bed3d0a6b9dbaf6d365dd13c7 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 12:52:14 +0100 Subject: [PATCH 11/14] Rename combineDicts to combine_dicts --- k-distribution/src/main/scripts/lib/pyk/kast.py | 4 ++-- k-distribution/src/main/scripts/lib/pyk/kastManip.py | 8 ++++---- k-distribution/src/main/scripts/lib/pyk/utils.py | 4 ++-- 3 files changed, 8 insertions(+), 8 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kast.py b/k-distribution/src/main/scripts/lib/pyk/kast.py index 7fb047fbc81..fccca75a03f 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kast.py +++ b/k-distribution/src/main/scripts/lib/pyk/kast.py @@ -4,7 +4,7 @@ import json from .cli_utils import fatal, notif, warning -from .utils import combineDicts +from .utils import combine_dicts def KApply(label, args): return { 'node': 'KApply', 'label': label, 'variable': False, 'arity': len(args), 'args': args } @@ -184,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) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index efbb96d7027..3c022f44129 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -4,7 +4,7 @@ import subprocess from .cli_utils import fatal -from .utils import combineDicts, dedupe, findCommonItems +from .utils import combine_dicts, dedupe, findCommonItems from .kast import * def buildAssoc(unit, join, ls): @@ -47,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 diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index cde76a1f014..0fc93310f5c 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -5,7 +5,7 @@ T = TypeVar('T') -def combineDicts(*dicts: Mapping) -> Optional[Dict]: +def combine_dicts(*dicts: Mapping) -> Optional[Dict]: if len(dicts) == 0: return {} if len(dicts) == 1: @@ -22,7 +22,7 @@ def combineDicts(*dicts: Mapping) -> Optional[Dict]: newDict = {key: dict1[key] for key in dict1} for key in dict2.keys(): newDict[key] = dict2[key] - return combineDicts(newDict, *restDicts) + return combine_dicts(newDict, *restDicts) def findCommonItems(l1: Iterable[T], l2: Iterable[T]) -> Tuple[List[T], List[T], List[T]]: From f998767d6b8f1ced40fd99710cd5951906908ffc Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 12:57:12 +0100 Subject: [PATCH 12/14] Rename findCommonItems to find_common_items --- k-distribution/src/main/scripts/lib/pyk/kastManip.py | 6 +++--- k-distribution/src/main/scripts/lib/pyk/utils.py | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/kastManip.py b/k-distribution/src/main/scripts/lib/pyk/kastManip.py index 3c022f44129..42f652780b4 100644 --- a/k-distribution/src/main/scripts/lib/pyk/kastManip.py +++ b/k-distribution/src/main/scripts/lib/pyk/kastManip.py @@ -4,7 +4,7 @@ import subprocess from .cli_utils import fatal -from .utils import combine_dicts, dedupe, findCommonItems +from .utils import combine_dicts, dedupe, find_common_items from .kast import * def buildAssoc(unit, join, ls): @@ -243,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 diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index 0fc93310f5c..cee2d5d80b9 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -25,7 +25,7 @@ def combine_dicts(*dicts: Mapping) -> Optional[Dict]: return combine_dicts(newDict, *restDicts) -def findCommonItems(l1: Iterable[T], l2: Iterable[T]) -> Tuple[List[T], List[T], List[T]]: +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: From 7652f658acaf2299ac745bb7b2fdec9853f5a3d3 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 13:01:07 +0100 Subject: [PATCH 13/14] Move getAppliedAxiomList from utils to ktool --- .../src/main/scripts/lib/pyk/ktool.py | 21 ++++++++++++++++--- .../src/main/scripts/lib/pyk/utils.py | 15 ------------- 2 files changed, 18 insertions(+), 18 deletions(-) diff --git a/k-distribution/src/main/scripts/lib/pyk/ktool.py b/k-distribution/src/main/scripts/lib/pyk/ktool.py index fd5939f0026..757a06634be 100644 --- a/k-distribution/src/main/scripts/lib/pyk/ktool.py +++ b/k-distribution/src/main/scripts/lib/pyk/ktool.py @@ -3,9 +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 getAppliedAxiomList, hash_str +from .utils import hash_str from .kastManip import * class KPrint: @@ -69,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 @@ -91,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 @@ -114,3 +115,17 @@ def _writeClaimDefinition(self, claim, claimId, lemmas = [], rule = False): 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 diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index cee2d5d80b9..508667360c7 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -1,5 +1,4 @@ import hashlib -from pathlib import Path from typing import Any, Dict, Iterable, List, Mapping, Optional, Tuple, TypeVar T = TypeVar('T') @@ -49,20 +48,6 @@ def dedupe(xs: Iterable[T]) -> List[T]: return res -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 - - def hash_str(x: Any) -> str: hash = hashlib.sha256() hash.update(str(x).encode('utf-8')) From bb675fbd27312222b35156f89702a7542fca3f16 Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Thu, 17 Feb 2022 13:10:10 +0100 Subject: [PATCH 14/14] Add merge_with and nonempty_str to utils --- .../src/main/scripts/lib/pyk/utils.py | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/k-distribution/src/main/scripts/lib/pyk/utils.py b/k-distribution/src/main/scripts/lib/pyk/utils.py index 508667360c7..ae9ee0da338 100644 --- a/k-distribution/src/main/scripts/lib/pyk/utils.py +++ b/k-distribution/src/main/scripts/lib/pyk/utils.py @@ -24,6 +24,17 @@ def combine_dicts(*dicts: Mapping) -> Optional[Dict]: 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: @@ -52,3 +63,13 @@ 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