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         required_tools = sorted(required_tools)
  60
  61         print(f".PHONY: {target}", file=rules)
  62         print(f"{target}:", file=rules)
  63
  64         shell_script = sby_dir / f"{sby_file.stem}.sh"
  65
  66         if shell_script.exists():
  67             command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}"
  68         else:
  69             command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}"
  70
  71         print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules)
  72
  73         print(f".PHONY: clean-{target}", file=rules)
  74         print(f"clean-{target}:", file=rules)
  75         print(f"\trm -rf {target}", file=rules)
  76
  77         test_groups = []
  78
  79         mode = info["mode"]
  80
  81         test_groups.append(f"test_m_{mode}")
  82
  83         for engine in sorted(engines):
  84             test_groups.append(f"test_e_{engine}")
  85             test_groups.append(f"test_m_{mode}_e_{engine}")
  86
  87         for solver in sorted(solvers):
  88             test_groups.append(f"test_s_{solver}")
  89             test_groups.append(f"test_m_{mode}_s_{solver}")
  90
  91         for engine, solver in sorted(engine_solvers):
  92             test_groups.append(f"test_e_{engine}_s_{solver}")
  93             test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}")
  94
  95         prefix = ""
  96
  97         for part in [*sby_dir.parts, ""]:
  98             print(f".PHONY: {prefix}clean {prefix}test", file=rules)
  99             print(f"{prefix}clean: clean-{target}", file=rules)
 100             print(f"{prefix}test: {target}", file=rules)
 101
 102             for test_group in test_groups:
 103                 print(f".PHONY: {prefix}{test_group}", file=rules)
 104                 print(f"{prefix}{test_group}: {target}", file=rules)
 105             prefix += f"{part}/"
 106
 107     tasks = [task for task in taskinfo.keys() if task]
 108
 109     if tasks:
 110         print(f".PHONY: {name}", file=rules)
 111         print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules)