From 46a6005bd5a6861d7fb0ca1c1d0371926a52385a Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Thu, 28 Oct 2021 14:39:31 -0400 Subject: [PATCH 1/3] Autoformat --- scripts/parse-logs.py | 174 ++++++++++++++++++++++++------------------ 1 file changed, 101 insertions(+), 73 deletions(-) diff --git a/scripts/parse-logs.py b/scripts/parse-logs.py index 4d61551..2eba03c 100755 --- a/scripts/parse-logs.py +++ b/scripts/parse-logs.py @@ -17,28 +17,42 @@ import re import sys -time_re = re.compile(r'elapsed_sec: (\d+)(|\.\d+) maxresident_kb: (\d+)') -timeout_re = re.compile(r'Command exited with non-zero status 124') -apalache_outcome_re = re.compile(r'The outcome is:\s*(.*)') -apalache_ntrans_re = re.compile(r'Found\s+(\d+)\s+initializing transitions and\s+(\d+)\s+next transitions') -apalache_depth_re = re.compile(r'Step\s+(\d+), level\s+\d+:') -tlc_no_error_re = re.compile(r'Model checking completed. No error has been found') -tlc_states_re = re.compile(r'\s(\d+)\s+distinct states found') -tlc_depth_re = re.compile(r'The depth of the complete state graph search is\s+(\d+)') -tlc_error_re = re.compile(r'Error:.* is violated') -tlc_progress_re =\ - re.compile(r'Progress\((\d+)\) at .*: (\d+) states generated (.*), (\d+) distinct states found') +time_re = re.compile(r"elapsed_sec: (\d+)(|\.\d+) maxresident_kb: (\d+)") +timeout_re = re.compile(r"Command exited with non-zero status 124") +apalache_outcome_re = re.compile(r"The outcome is:\s*(.*)") +apalache_ntrans_re = re.compile( + r"Found\s+(\d+)\s+initializing transitions and\s+(\d+)\s+next transitions" +) +apalache_depth_re = re.compile(r"Step\s+(\d+), level\s+\d+:") +tlc_no_error_re = re.compile(r"Model checking completed. No error has been found") +tlc_states_re = re.compile(r"\s(\d+)\s+distinct states found") +tlc_depth_re = re.compile(r"The depth of the complete state graph search is\s+(\d+)") +tlc_error_re = re.compile(r"Error:.* is violated") +tlc_progress_re = re.compile( + r"Progress\((\d+)\) at .*: (\d+) states generated (.*), (\d+) distinct states found" +) def parse_options(): parser = argparse.ArgumentParser( - description="Parse the logs that are produced by the Apalache tests.") - parser.add_argument("expDir", type=str, - help="The directory where the scripts and experiments logs can be found.") - parser.add_argument("--output", "-o", default='results.csv', - help="The filename of the output CSV file") - parser.add_argument("--human", action="store_true", - help="Make figures human-readable, e.g., convert 3610 seconds to 01H00M") + description="Parse the logs that are produced by the Apalache tests." + ) + parser.add_argument( + "expDir", + type=str, + help="The directory where the scripts and experiments logs can be found.", + ) + parser.add_argument( + "--output", + "-o", + default="results.csv", + help="The filename of the output CSV file", + ) + parser.add_argument( + "--human", + action="store_true", + help="Make figures human-readable, e.g., convert 3610 seconds to 01H00M", + ) args = parser.parse_args() args.expDir = os.path.realpath(args.expDir) return args @@ -52,33 +66,37 @@ def collect_dirs(args): files.sort() for f in files: exp_path = os.path.join(in_dir, f) - m = re.compile('\d+').match(f) + m = re.compile("\d+").match(f) if m and os.path.isdir(exp_path): - if os.path.exists(os.path.join(exp_path, 'apalache.out')): - print(' %3s -> apalache' % f) + if os.path.exists(os.path.join(exp_path, "apalache.out")): + print(" %3s -> apalache" % f) exp_descs.append({"no": int(f), "tool": "apalache", "path": exp_path}) - elif os.path.exists(os.path.join(exp_path, 'tlc.out')): - print(' %3s -> tlc' % f) + elif os.path.exists(os.path.join(exp_path, "tlc.out")): + print(" %3s -> tlc" % f) exp_descs.append({"no": int(f), "tool": "tlc", "path": exp_path}) else: - print(' %3s -> CORRUPTED' % f) + print(" %3s -> CORRUPTED" % f) return exp_descs def parse_time(ed): - entry = {'04:time_sec': None, '05:mem_kb': None, '03:status': 'Fail'} - with open(os.path.join(ed['path'], 'time.out'), "r") as f: + entry = {"04:time_sec": None, "05:mem_kb": None, "03:status": "Fail"} + with open(os.path.join(ed["path"], "time.out"), "r") as f: line = f.readline() while line: m = timeout_re.search(line) if m: - entry = { **entry, '03:status': 'Timeout' } + entry = {**entry, "03:status": "Timeout"} m = time_re.search(line) if m: - entry = { **entry, - '04:time_sec': int(math.ceil(float(m.group(1)) + float(m.group(2)))), - '05:mem_kb': m.group(3)} + entry = { + **entry, + "04:time_sec": int( + math.ceil(float(m.group(1)) + float(m.group(2))) + ), + "05:mem_kb": m.group(3), + } line = f.readline() @@ -86,26 +104,26 @@ def parse_time(ed): def parse_apalache(ed): - entry = {'05:depth': 0, '10:ninit_trans': 0, '11:ninit_trans': 0} - with open(os.path.join(ed['path'], 'detailed.log'), "r") as lf: + entry = {"05:depth": 0, "10:ninit_trans": 0, "11:ninit_trans": 0} + with open(os.path.join(ed["path"], "detailed.log"), "r") as lf: line = lf.readline() while line: m = apalache_outcome_re.search(line) if m: - entry['03:status'] = m.group(1) + entry["03:status"] = m.group(1) m = apalache_depth_re.search(line) if m: - entry['05:depth'] = int(m.group(1)) + entry["05:depth"] = int(m.group(1)) m = apalache_ntrans_re.search(line) if m: - entry['10:ninit_trans'] = m.group(1) - entry['11:ninit_trans'] = m.group(2) + entry["10:ninit_trans"] = m.group(1) + entry["11:ninit_trans"] = m.group(2) line = lf.readline() - prof_rule_re = re.compile(r'^(\w+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)') + prof_rule_re = re.compile(r"^(\w+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)") ncells, nclauses, nclause_prod = 0, 0, 0 - with open(os.path.join(ed['path'], 'profile-rules.txt'), "r") as pf: + with open(os.path.join(ed["path"], "profile-rules.txt"), "r") as pf: line = pf.readline() while line: m = prof_rule_re.match(line) @@ -115,39 +133,42 @@ def parse_apalache(ed): nclause_prod += int(m.group(5)) * int(m.group(6)) line = pf.readline() - avg_clause_len = \ - math.ceil(nclause_prod / nclauses) if (nclauses > 0) else 0 - entry = { **entry, '12:ncells': ncells, - '13:nclauses': nclauses, '14:navg_clause_len': avg_clause_len } + avg_clause_len = math.ceil(nclause_prod / nclauses) if (nclauses > 0) else 0 + entry = { + **entry, + "12:ncells": ncells, + "13:nclauses": nclauses, + "14:navg_clause_len": avg_clause_len, + } return entry def parse_tlc(ed): - entry = {'05:depth': 0, '20:nstates': 0} - with open(os.path.join(ed['path'], 'tlc.out'), "r") as lf: + entry = {"05:depth": 0, "20:nstates": 0} + with open(os.path.join(ed["path"], "tlc.out"), "r") as lf: line = lf.readline() while line: m = tlc_no_error_re.search(line) if m: - entry['03:status'] = "NoError" + entry["03:status"] = "NoError" m = tlc_error_re.search(line) if m: - entry['03:status'] = "Error" + entry["03:status"] = "Error" m = tlc_progress_re.search(line) if m: - entry['05:depth'] = int(m.group(1)) - entry['20:nstates'] = int(m.group(4)) + entry["05:depth"] = int(m.group(1)) + entry["20:nstates"] = int(m.group(4)) m = tlc_states_re.search(line) if m: - entry['20:nstates'] = int(m.group(1)) + entry["20:nstates"] = int(m.group(1)) m = tlc_depth_re.search(line) if m: - entry['05:depth'] = int(m.group(1)) + entry["05:depth"] = int(m.group(1)) line = lf.readline() @@ -165,6 +186,7 @@ def humanize_sec(sec): else: return "%2ds" % sec + def humanize_kb(kb): mb = int(kb / 1024) gb = int(mb / 1024) @@ -176,6 +198,7 @@ def humanize_kb(kb): else: return "%dK" % kb + def humanize_num(num): # shall we use round(..) instead of int(..)? thousands = int(num / 1000) @@ -202,19 +225,20 @@ def humanize(entry): def int_or_zero(name): return int(entry[name]) if name in entry and entry[name] else 0 - new_entry = { **entry, - '04:time_hum': humanize_sec(int_or_zero('04:time_sec')), - '05:mem_hum': humanize_kb(int_or_zero('05:mem_kb')), - '12:ncells_hum': humanize_num(int_or_zero('12:ncells')), - '13:nclauses_hum': humanize_num(int_or_zero('13:nclauses')), - '20:nstates_hum': humanize_num(int_or_zero('20:nstates')) - } + new_entry = { + **entry, + "04:time_hum": humanize_sec(int_or_zero("04:time_sec")), + "05:mem_hum": humanize_kb(int_or_zero("05:mem_kb")), + "12:ncells_hum": humanize_num(int_or_zero("12:ncells")), + "13:nclauses_hum": humanize_num(int_or_zero("13:nclauses")), + "20:nstates_hum": humanize_num(int_or_zero("20:nstates")), + } return new_entry if __name__ == "__main__": args = parse_options() - if not os.path.exists(args.expDir): + if not os.path.exists(args.expDir): print("Error: Directory %s not found." % args.expDir) sys.exit(1) @@ -222,21 +246,21 @@ def int_or_zero(name): eds = collect_dirs(args) entries = [] for ed in eds: - entry = { '01:no': ed['no'], '02:tool': ed['tool'] } + entry = {"01:no": ed["no"], "02:tool": ed["tool"]} try: - entry = { **entry, **parse_time(ed) } # merge - if ed['tool'] == 'apalache': - entry = { **entry, **parse_apalache(ed)} - elif ed['tool'] == 'tlc': - entry = { **entry, **parse_tlc(ed)} + entry = {**entry, **parse_time(ed)} # merge + if ed["tool"] == "apalache": + entry = {**entry, **parse_apalache(ed)} + elif ed["tool"] == "tlc": + entry = {**entry, **parse_tlc(ed)} else: - print('Unknown tool: ' + ed['tool']) - entry['03:status'] = 'Fail' + print("Unknown tool: " + ed["tool"]) + entry["03:status"] = "Fail" except FileNotFoundError as err: - print("Error in %s: %s" % (ed['no'], err)) - entry['03:status'] = 'Fail' + print("Error in %s: %s" % (ed["no"], err)) + entry["03:status"] = "Fail" - #print(entry) + # print(entry) entries.append(entry) # if the values must be human-readable, convert them @@ -252,12 +276,16 @@ def int_or_zero(name): sorted_keys.sort() # write the results to a csv file - with open(args.output, 'w', newline='') as csvfile: - writer = csv.DictWriter(csvfile, fieldnames=sorted_keys, delimiter=',', - quotechar="'", quoting=csv.QUOTE_MINIMAL) + with open(args.output, "w", newline="") as csvfile: + writer = csv.DictWriter( + csvfile, + fieldnames=sorted_keys, + delimiter=",", + quotechar="'", + quoting=csv.QUOTE_MINIMAL, + ) writer.writeheader() for e in entries: writer.writerow(e) print("\n%d entries are written to %s" % (len(entries), args.output)) - From 907a71b5672fa68c29c5528ab4a557469bda8da2 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 29 Oct 2021 12:49:20 -0400 Subject: [PATCH 2/3] Fix log parsing locations --- scripts/mk-run.py | 2 +- scripts/parse-logs.py | 17 +++++++++++++++-- 2 files changed, 16 insertions(+), 3 deletions(-) diff --git a/scripts/mk-run.py b/scripts/mk-run.py index 1f014dc..dbac50d 100755 --- a/scripts/mk-run.py +++ b/scripts/mk-run.py @@ -79,7 +79,7 @@ def kv(key): ctime = "%s -f 'elapsed_sec: %%e maxresident_kb: %%M' -o time.out" % os_cmds["time"] ctimeout = "%s --foreground %s" % (os_cmds["timeout"], csv_row["timeout"]) if tool == "apalache": - return "%s %s %s/bin/apalache-mc check %s %s %s %s %s %s | tee apalache.out" % ( + return "%s %s %s/bin/apalache-mc check --profiling=true %s %s %s %s %s %s | tee apalache.out" % ( ctime, ctimeout, args.apalacheDir, diff --git a/scripts/parse-logs.py b/scripts/parse-logs.py index 2eba03c..876beb9 100755 --- a/scripts/parse-logs.py +++ b/scripts/parse-logs.py @@ -17,6 +17,8 @@ import re import sys +from pathlib import Path + time_re = re.compile(r"elapsed_sec: (\d+)(|\.\d+) maxresident_kb: (\d+)") timeout_re = re.compile(r"Command exited with non-zero status 124") apalache_outcome_re = re.compile(r"The outcome is:\s*(.*)") @@ -103,9 +105,20 @@ def parse_time(ed): return entry +def get_experiment_log(ed: dict, fname: str) -> Path: + glob_pattern = "*/" + fname + out_dir = Path(ed["path"]) / "_apalache-out" + try: + return next(out_dir.glob(glob_pattern)) + except StopIteration: + raise RuntimeError( + f"Failed to find log file {fname} in experiment directory {out_dir}" + ) + + def parse_apalache(ed): entry = {"05:depth": 0, "10:ninit_trans": 0, "11:ninit_trans": 0} - with open(os.path.join(ed["path"], "detailed.log"), "r") as lf: + with get_experiment_log(ed, "detailed.log").open("r") as lf: line = lf.readline() while line: m = apalache_outcome_re.search(line) @@ -123,7 +136,7 @@ def parse_apalache(ed): prof_rule_re = re.compile(r"^(\w+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)\s+(\d+)") ncells, nclauses, nclause_prod = 0, 0, 0 - with open(os.path.join(ed["path"], "profile-rules.txt"), "r") as pf: + with get_experiment_log(ed, "profile-rules.txt").open("r") as pf: line = pf.readline() while line: m = prof_rule_re.match(line) From c7ffcb67ff2728ebe7acbbe714cac5a58ebc2f96 Mon Sep 17 00:00:00 2001 From: Shon Feder Date: Fri, 29 Oct 2021 12:56:04 -0400 Subject: [PATCH 3/3] Configure CI to run benchmarks on PRs We don't have to wait for these, but it'd be nice to actually see if the changes we make still let the benchmarks run and complete, if we want. --- .github/workflows/benchmarks.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/benchmarks.yml b/.github/workflows/benchmarks.yml index a063c06..cda275e 100644 --- a/.github/workflows/benchmarks.yml +++ b/.github/workflows/benchmarks.yml @@ -13,6 +13,7 @@ on: # Automatically prepare a minor version release every Saturday # See https://crontab.guru/#0_0_*_*_6 - cron: "0 0 * * 6" + pull_request: env: VERSION: ${{ github.event.inputs.release_version || 'unreleased' }}