tests: Check for btorsim --vcd

tests/Makefile

@@ -33,10 +33,19 @@ make/rules/test/%.mk:
 
 ifneq (help,$(MAKECMDGOALS))
 
-FIND_TOOLS := $(shell \
-	TOOLS=$$(which $(TOOL_LIST) 2>/dev/null || true); \
-	echo $$TOOLS | cmp -s make/rules/found_tools || echo $$TOOLS > make/rules/found_tools \
-)
+# This should run every time but only trigger anything depending on it whenever
+# the script overwrites make/rules/found_tools. This doesn't really match how
+# make targets usually work, so we manually shell out here.
+
+FIND_TOOLS := $(shell python3 make/required_tools.py || echo error)
+
+ifneq (,$(findstring error,$(FIND_TOOLS)))
+$(error could not run 'python3 make/required_tools.py')
+endif
+
+ifneq (,$(FIND_TOOLS))
+$(warning $(FIND_TOOLS))
+endif
 
 include make/rules/collect.mk
 

tests/make/required_tools.py

@@ -0,0 +1,64 @@
+import shutil
+
+REQUIRED_TOOLS = {
+    ("smtbmc", "yices"): ["yices-smt2"],
+    ("smtbmc", "z3"): ["z3"],
+    ("smtbmc", "cvc4"): ["cvc4"],
+    ("smtbmc", "mathsat"): ["mathsat"],
+    ("smtbmc", "boolector"): ["boolector"],
+    ("smtbmc", "bitwuzla"): ["bitwuzla"],
+    ("smtbmc", "abc"): ["yosys-abc"],
+    ("aiger", "suprove"): ["suprove", "yices"],
+    ("aiger", "avy"): ["avy", "yices"],
+    ("aiger", "aigbmc"): ["aigbmc", "yices"],
+    ("btor", "btormc"): ["btormc", "btorsim"],
+    ("btor", "pono"): ["pono", "btorsim"],
+    ("abc"): ["yices"],
+}
+
+
+if __name__ == "__main__":
+    import subprocess
+    import sys
+    from pathlib import Path
+
+    found_tools = []
+    check_tools = set()
+    for tools in REQUIRED_TOOLS.values():
+        check_tools.update(tools)
+
+    for tool in sorted(check_tools):
+        if not shutil.which(tool):
+            continue
+
+        if tool == "btorsim":
+            error_msg = subprocess.run(
+                ["btorsim", "--vcd"],
+                capture_output=True,
+                text=True,
+            ).stderr
+            if "invalid command line option" in error_msg:
+                print(
+                    "found `btorsim` binary is too old "
+                    "to support the `--vcd` option, ignoring"
+                )
+                continue
+
+        found_tools.append(tool)
+
+    found_tools = "\n".join(found_tools + [""])
+
+    try:
+        with open("make/rules/found_tools") as found_tools_file:
+            if found_tools_file.read() == found_tools:
+                exit(0)
+    except FileNotFoundError:
+        pass
+
+    Path("make/rules").mkdir(exist_ok=True)
+
+    with open("make/rules/found_tools", "w") as found_tools_file:
+        found_tools_file.write(found_tools)
+else:
+    with open("make/rules/found_tools") as found_tools_file:
+        found_tools = [tool.strip() for tool in found_tools_file.readlines()]

tests/make/test_rules.py

@@ -1,10 +1,10 @@
-import shutil
 import sys
 import os
 import subprocess
 import json
 from pathlib import Path
 
+from required_tools import REQUIRED_TOOLS, found_tools
 
 sby_file = Path(sys.argv[1])
 sby_dir = sby_file.parent
@@ -26,24 +26,6 @@ def parse_engine(engine):
     return engine, default_solvers.get(engine)
 
 
-# When adding new tools, also update TOOL_LIST in Makefile to make sure we regenerate
-# the rules when the user installs or removes any of the tools
-REQUIRED_TOOLS = {
-    ("smtbmc", "yices"): ["yices-smt2"],
-    ("smtbmc", "z3"): ["z3"],
-    ("smtbmc", "cvc4"): ["cvc4"],
-    ("smtbmc", "mathsat"): ["mathsat"],
-    ("smtbmc", "boolector"): ["boolector"],
-    ("smtbmc", "bitwuzla"): ["bitwuzla"],
-    ("smtbmc", "abc"): ["yosys-abc"],
-    ("aiger", "suprove"): ["suprove", "yices"],
-    ("aiger", "avy"): ["avy", "yices"],
-    ("aiger", "aigbmc"): ["aigbmc", "yices"],
-    ("btor", "btormc"): ["btormc", "btorsim"],
-    ("btor", "pono"): ["pono", "btorsim"],
-    ("abc"): ["yices"],
-}
-
 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
 rules_file.parent.mkdir(exist_ok=True, parents=True)
 
@@ -79,7 +61,7 @@ with rules_file.open("w") as rules:
         shell_script = sby_dir / f"{sby_file.stem}.sh"
 
         missing_tools = sorted(
-            f"`{tool}`" for tool in required_tools if shutil.which(tool) is None
+            f"`{tool}`" for tool in required_tools if tool not in found_tools
         )
 
         if missing_tools: