|
| 1 | +#!/usr/bin/env python3 |
| 2 | +import argparse |
| 3 | +import os |
| 4 | +import random |
| 5 | +import subprocess |
| 6 | +import concurrent.futures |
| 7 | +import shutil |
| 8 | +import multiprocessing |
| 9 | +import psutil |
| 10 | +import time |
| 11 | +import threading |
| 12 | +import platform |
| 13 | +from functools import partial |
| 14 | +from pathlib import Path |
| 15 | +import sys |
| 16 | +import liblimits |
| 17 | + |
| 18 | +configfile: "config.yaml" |
| 19 | + |
| 20 | +# get Git root |
| 21 | +GIT_ROOT = Path(subprocess.check_output( |
| 22 | + ["git", "rev-parse", "--show-toplevel"] |
| 23 | +).decode().strip()) |
| 24 | +print("Git root:", GIT_ROOT) |
| 25 | + |
| 26 | +HACKERSDELIGHT_FILE_NAMES, = glob_wildcards(GIT_ROOT / "SSA/Projects/InstCombine/HackersDelight/{file}.lean") |
| 27 | + |
| 28 | +SED = "gsed" if platform.system() == "Darwin" else "sed" |
| 29 | +hdel_nreps = config["hdel_nreps"] |
| 30 | + |
| 31 | +rule venv: |
| 32 | + output: |
| 33 | + GIT_ROOT / "venv/bin/activate" |
| 34 | + shell: |
| 35 | + """ |
| 36 | + python3 -m venv venv |
| 37 | + venv/bin/pip install -r {GIT_ROOT}/requirements.txt |
| 38 | + """ |
| 39 | + |
| 40 | +rule hdel_compare_make_lean: |
| 41 | + input: |
| 42 | + GIT_ROOT / "SSA/Projects/InstCombine/HackersDelight/{file}.lean" |
| 43 | + output: |
| 44 | + GIT_ROOT / "bv-evaluation/results/HackersDelight/{file}_{width}_{hdel_nreps}.lean" |
| 45 | + shell: |
| 46 | + "cp {input} {output} && " |
| 47 | + "{SED} -i -e \"s/all_goals sorry/all_goals bv_compare'/g\" -e \"s/WIDTH/{wildcards.width}/g\" {output} " |
| 48 | + |
| 49 | +rule hdel_compare_make_output: |
| 50 | + input: |
| 51 | + lambda wc: GIT_ROOT / f"bv-evaluation/results/HackersDelight/{wc.file}_{wc.width}_{hdel_nreps}.lean" |
| 52 | + output: |
| 53 | + GIT_ROOT / "bv-evaluation/results/HackersDelight/{file}_{width}_r{r}.txt" |
| 54 | + resources: |
| 55 | + # TODO: actually impose memory and time limit, using a python script. |
| 56 | + run: |
| 57 | + status, stdout, stderr = run_with_limits(cmd=["lake", "lean", input[0]], timeout=int(config["hdel_timeout_sec"]), memout_mb=int(config["hdel_memout_mb"])) |
| 58 | + with open(output[0], "w") as f: |
| 59 | + f.write(stdout) |
| 60 | + f.write(stderr) |
| 61 | + if not isinstance(status, int) or status != 0: |
| 62 | + raise Exception(f"rule failed with status '{status}'. See {output[0]} for possible more details.") |
| 63 | + |
| 64 | +# We can eventually split these, if we carefully understand the naming convention |
| 65 | +# of 'collect' for hacker's delight. |
| 66 | +# We currently make a monolithic job that runs both collect and plot, |
| 67 | +# Since the naming convention is a little opaque to @bollu. |
| 68 | +rule hdel_collect_and_plot: |
| 69 | + input: |
| 70 | + rules.venv.output, |
| 71 | + expand(GIT_ROOT / "bv-evaluation/results/HackersDelight/{file}_{width}_r{r}.txt", |
| 72 | + file=HACKERSDELIGHT_FILE_NAMES, |
| 73 | + width=config["hdel_bv_widths"], |
| 74 | + r=range(hdel_nreps)) |
| 75 | + params: |
| 76 | + nreps = lambda wc: hdel_nreps, |
| 77 | + nthreads = lambda wc: config["hdel_nthreads"] |
| 78 | + output: |
| 79 | + tex=GIT_ROOT / "bv-evaluation/performance-hackersdelight.tex", |
| 80 | + pdf_stacked=GIT_ROOT / "bv-evaluation/plots/bv_decide_stacked_perc_HackersDelight_bvw64.pdf" |
| 81 | + # TODO: track the exact files generated by 'collect.py'. |
| 82 | + # We currently just bother asking for the two outputs we care for. |
| 83 | + shell: |
| 84 | + "bash -c 'source venv/bin/activate && cd bv-evaluation && python3 collect.py hackersdelight' && " |
| 85 | + "bash -c 'source venv/bin/activate && cd bv-evaluation && python3 plot.py hackersdelight'" |
| 86 | + |
| 87 | +rule all: |
| 88 | + input: |
| 89 | + rules.hdel_collect_and_plot.output |
| 90 | + |
| 91 | + |
0 commit comments