tests/make/test_rules.py

   1 import sys
   2 import os
   3 import subprocess
   4 import json
   5 from pathlib import Path
   6
   7 from required_tools import REQUIRED_TOOLS, found_tools
   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 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
  30 rules_file.parent.mkdir(exist_ok=True, parents=True)
  31
  32 with rules_file.open("w") as rules:
  33     name = str(sby_dir / sby_file.stem)
  34
  35     for task, info in taskinfo.items():
  36         target = name
  37         workdirname = sby_file.stem
  38         if task:
  39             target += f"_{task}"
  40             workdirname += f"_{task}"
  41
  42         engines = set()
  43         solvers = set()
  44         engine_solvers = set()
  45
  46         required_tools = set()
  47
  48         for engine in info["engines"]:
  49             engine, solver = parse_engine(engine)
  50             engines.add(engine)
  51             required_tools.update(
  52                 REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
  53             )
  54             if solver:
  55                 solvers.add(solver)
  56                 engine_solvers.add((engine, solver))
  57
  58         print(f".PHONY: {target}", file=rules)
  59         print(f"{target}:", file=rules)
  60
  61         shell_script = sby_dir / f"{sby_file.stem}.sh"
  62
  63         missing_tools = sorted(
  64             f"`{tool}`" for tool in required_tools if tool not in found_tools
  65         )
  66
  67         if missing_tools:
  68             print(
  69                 f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; $(SKIP_COMMAND)",
  70                 file=rules,
  71             )
  72
  73         elif shell_script.exists():
  74             print(
  75                 f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
  76                 file=rules,
  77             )
  78         else:
  79             print(
  80                 f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
  81                 file=rules,
  82             )
  83
  84         print(f".PHONY: clean-{target}", file=rules)
  85         print(f"clean-{target}:", file=rules)
  86         print(f"\trm -rf {target}", file=rules)
  87
  88         test_groups = []
  89
  90         mode = info["mode"]
  91
  92         test_groups.append(f"test_m_{mode}")
  93
  94         for engine in sorted(engines):
  95             test_groups.append(f"test_e_{engine}")
  96             test_groups.append(f"test_m_{mode}_e_{engine}")
  97
  98         for solver in sorted(solvers):
  99             test_groups.append(f"test_s_{solver}")
 100             test_groups.append(f"test_m_{mode}_s_{solver}")
 101
 102         for engine, solver in sorted(engine_solvers):
 103             test_groups.append(f"test_e_{engine}_s_{solver}")
 104             test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}")
 105
 106         prefix = ""
 107
 108         for part in [*sby_dir.parts, ""]:
 109             print(f".PHONY: {prefix}clean {prefix}test", file=rules)
 110             print(f"{prefix}clean: clean-{target}", file=rules)
 111             print(f"{prefix}test: {target}", file=rules)
 112
 113             for test_group in test_groups:
 114                 print(f".PHONY: {prefix}{test_group}", file=rules)
 115                 print(f"{prefix}{test_group}: {target}", file=rules)
 116             prefix += f"{part}/"
 117
 118     tasks = [task for task in taskinfo.keys() if task]
 119
 120     if tasks:
 121         print(f".PHONY: {name}", file=rules)
 122         print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules)