tests/make/test_rules.py

   1 import shutil
   2 import sys
   3 import os
   4 import subprocess
   5 import json
   6 from pathlib import Path
   7
   8
   9 sby_file = Path(sys.argv[1])
  10 sby_dir = sby_file.parent
  11
  12
  13 taskinfo = json.loads(
  14     subprocess.check_output(
  15         [sys.executable, os.getenv("SBY_MAIN"), "--dumptaskinfo", sby_file]
  16     )
  17 )
  18
  19
  20 def parse_engine(engine):
  21     engine, *args = engine
  22     default_solvers = {"smtbmc": "yices"}
  23     for arg in args:
  24         if not arg.startswith("-"):
  25             return engine, arg
  26     return engine, default_solvers.get(engine)
  27
  28
  29 # When adding new tools, also update TOOL_LIST in Makefile to make sure we regenerate
  30 # the rules when the user installs or removes any of the tools
  31 REQUIRED_TOOLS = {
  32     ("smtbmc", "yices"): ["yices-smt2"],
  33     ("smtbmc", "z3"): ["z3"],
  34     ("smtbmc", "cvc4"): ["cvc4"],
  35     ("smtbmc", "mathsat"): ["mathsat"],
  36     ("smtbmc", "boolector"): ["boolector"],
  37     ("smtbmc", "bitwuzla"): ["bitwuzla"],
  38     ("smtbmc", "abc"): ["yosys-abc"],
  39     ("aiger", "suprove"): ["suprove", "yices"],
  40     ("aiger", "avy"): ["avy", "yices"],
  41     ("aiger", "aigbmc"): ["aigbmc", "yices"],
  42     ("btor", "btormc"): ["btormc", "btorsim"],
  43     ("btor", "pono"): ["pono", "btorsim"],
  44     ("abc"): ["yices"],
  45 }
  46
  47 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
  48 rules_file.parent.mkdir(exist_ok=True, parents=True)
  49
  50 with rules_file.open("w") as rules:
  51     name = str(sby_dir / sby_file.stem)
  52
  53     for task, info in taskinfo.items():
  54         target = name
  55         workdirname = sby_file.stem
  56         if task:
  57             target += f"_{task}"
  58             workdirname += f"_{task}"
  59
  60         engines = set()
  61         solvers = set()
  62         engine_solvers = set()
  63
  64         required_tools = set()
  65
  66         for engine in info["engines"]:
  67             engine, solver = parse_engine(engine)
  68             engines.add(engine)
  69             required_tools.update(
  70                 REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
  71             )
  72             if solver:
  73                 solvers.add(solver)
  74                 engine_solvers.add((engine, solver))
  75
  76         print(f".PHONY: {target}", file=rules)
  77         print(f"{target}:", file=rules)
  78
  79         shell_script = sby_dir / f"{sby_file.stem}.sh"
  80
  81         missing_tools = sorted(
  82             f"`{tool}`" for tool in required_tools if shutil.which(tool) is None
  83         )
  84
  85         if missing_tools:
  86             print(
  87                 f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo",
  88                 file=rules,
  89             )
  90
  91         elif shell_script.exists():
  92             print(
  93                 f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
  94                 file=rules,
  95             )
  96         else:
  97             print(
  98                 f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
  99                 file=rules,
 100             )
 101
 102         print(f".PHONY: clean-{target}", file=rules)
 103         print(f"clean-{target}:", file=rules)
 104         print(f"\trm -rf {target}", file=rules)
 105
 106         test_groups = []
 107
 108         mode = info["mode"]
 109
 110         test_groups.append(f"test_m_{mode}")
 111
 112         for engine in sorted(engines):
 113             test_groups.append(f"test_e_{engine}")
 114             test_groups.append(f"test_m_{mode}_e_{engine}")
 115
 116         for solver in sorted(solvers):
 117             test_groups.append(f"test_s_{solver}")
 118             test_groups.append(f"test_m_{mode}_s_{solver}")
 119
 120         for engine, solver in sorted(engine_solvers):
 121             test_groups.append(f"test_e_{engine}_s_{solver}")
 122             test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}")
 123
 124         prefix = ""
 125
 126         for part in [*sby_dir.parts, ""]:
 127             print(f".PHONY: {prefix}clean {prefix}test", file=rules)
 128             print(f"{prefix}clean: clean-{target}", file=rules)
 129             print(f"{prefix}test: {target}", file=rules)
 130
 131             for test_group in test_groups:
 132                 print(f".PHONY: {prefix}{test_group}", file=rules)
 133                 print(f"{prefix}{test_group}: {target}", file=rules)
 134             prefix += f"{part}/"
 135
 136     tasks = [task for task in taskinfo.keys() if task]
 137
 138     if tasks:
 139         print(f".PHONY: {name}", file=rules)
 140         print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules)