tests/make/test_rules.py

   1 import sys
   2 import os
   3 import subprocess
   4 import json
   5 import shlex
   6 from pathlib import Path
   7
   8 from required_tools import REQUIRED_TOOLS
   9
  10 sby_file = Path(sys.argv[1])
  11 sby_dir = sby_file.parent
  12
  13
  14 taskinfo = json.loads(
  15     subprocess.check_output(
  16         [sys.executable, os.getenv("SBY_MAIN"), "--dumptaskinfo", sby_file]
  17     )
  18 )
  19
  20
  21 def parse_engine(engine):
  22     engine, *args = engine
  23     default_solvers = {"smtbmc": "yices"}
  24     for arg in args:
  25         if not arg.startswith("-"):
  26             return engine, arg
  27     return engine, default_solvers.get(engine)
  28
  29
  30 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
  31 rules_file.parent.mkdir(exist_ok=True, parents=True)
  32
  33 with rules_file.open("w") as rules:
  34     name = str(sby_dir / sby_file.stem)
  35
  36     for task, info in taskinfo.items():
  37         target = name
  38         workdirname = sby_file.stem
  39         if task:
  40             target += f"_{task}"
  41             workdirname += f"_{task}"
  42
  43         engines = set()
  44         solvers = set()
  45         engine_solvers = set()
  46
  47         required_tools = set()
  48
  49         for engine in info["engines"]:
  50             engine, solver = parse_engine(engine)
  51             engines.add(engine)
  52             required_tools.update(
  53                 REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
  54             )
  55             if solver:
  56                 solvers.add(solver)
  57                 engine_solvers.add((engine, solver))
  58
  59         if any(line.startswith("read -verific") or line.startswith("verific") for line in info["script"]):
  60             required_tools.add("verific")
  61
  62         required_tools = sorted(required_tools)
  63
  64         print(f".PHONY: {target}", file=rules)
  65         print(f"{target}:", file=rules)
  66
  67         shell_script = sby_dir / f"{sby_file.stem}.sh"
  68
  69         if shell_script.exists():
  70             command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}"
  71         else:
  72             command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}"
  73
  74         print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules)
  75
  76         print(f".PHONY: clean-{target}", file=rules)
  77         print(f"clean-{target}:", file=rules)
  78         print(f"\trm -rf {target}", file=rules)
  79
  80         test_groups = []
  81
  82         mode = info["mode"]
  83
  84         test_groups.append(f"test_m_{mode}")
  85
  86         for engine in sorted(engines):
  87             test_groups.append(f"test_e_{engine}")
  88             test_groups.append(f"test_m_{mode}_e_{engine}")
  89
  90         for solver in sorted(solvers):
  91             test_groups.append(f"test_s_{solver}")
  92             test_groups.append(f"test_m_{mode}_s_{solver}")
  93
  94         for engine, solver in sorted(engine_solvers):
  95             test_groups.append(f"test_e_{engine}_s_{solver}")
  96             test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}")
  97
  98         prefix = ""
  99
 100         for part in [*sby_dir.parts, ""]:
 101             print(f".PHONY: {prefix}clean {prefix}test", file=rules)
 102             print(f"{prefix}clean: clean-{target}", file=rules)
 103             print(f"{prefix}test: {target}", file=rules)
 104
 105             for test_group in test_groups:
 106                 print(f".PHONY: {prefix}{test_group}", file=rules)
 107                 print(f"{prefix}{test_group}: {target}", file=rules)
 108             prefix += f"{part}/"
 109
 110     tasks = [task for task in taskinfo.keys() if task]
 111
 112     if tasks:
 113         print(f".PHONY: {name}", file=rules)
 114         print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules)