Merge pull request #163 from jix/make_improvements

Test makefile improvements

.github/workflows/ci.yml

@@ -9,4 +9,4 @@ jobs:
       - uses: actions/checkout@v2
       - uses: YosysHQ/setup-oss-cad-suite@v1
       - name: Run checks
-        run: tabbypip install xmlschema && make ci
+        run: tabbypip install xmlschema && make ci NOSKIP=1

Makefile

@@ -10,6 +10,8 @@ ifeq ($(OS), Windows_NT)
 PYTHON = $(shell cygpath -w -m $(PREFIX)/bin/python3)
 endif
 
+.PHONY: help install ci test html clean
+
 help:
 	@echo ""
 	@echo "sudo make install"
@@ -19,7 +21,11 @@ help:
 	@echo "    build documentation in docs/build/html/"
 	@echo ""
 	@echo "make test"
-	@echo "    run examples"
+	@echo "    run tests"
+	@echo ""
+	@echo "make ci"
+	@echo "    run tests and check examples"
+	@echo "    note: this requires a full Tabby CAD Suite or OSS CAD Suite install"
 	@echo ""
 	@echo "make clean"
 	@echo "    cleanup"
@@ -39,7 +45,12 @@ else
 	chmod +x $(DESTDIR)$(PREFIX)/bin/sby
 endif
 
-ci: \
+.PHONY: check_cad_suite run_ci
+
+ci: check_cad_suite
+	@$(MAKE) run_ci
+
+run_ci: \
   test_demo1 test_demo2 test_demo3 \
   test_abstract_abstr test_abstract_props \
   test_demos_fib_cover test_demos_fib_prove test_demos_fib_live \
@@ -47,9 +58,16 @@ ci: \
   test_puzzles_djb2hash test_puzzles_pour853to4 test_puzzles_wolfgoatcabbage \
   test_puzzles_primegen_primegen test_puzzles_primegen_primes_pass test_puzzles_primegen_primes_fail \
   test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \
-  run_tests
+  test
 	if yosys -qp 'read -verific' 2> /dev/null; then set -x; \
-		YOSYS_NOVERIFIC=1 $(MAKE) ci; \
+		YOSYS_NOVERIFIC=1 $(MAKE) run_ci; \
+	fi
+
+check_cad_suite:
+	@if ! which tabbypip >/dev/null 2>&1; then \
+		echo "'make ci' requries the Tabby CAD Suite or the OSS CAD Suite"; \
+		echo "try 'make test' instead or run 'make run_ci' to proceed anyway."; \
+		exit 1; \
 	fi
 
 test_demo1:
@@ -113,7 +131,7 @@ test_quickstart_prove:
 test_quickstart_memory:
 	cd docs/examples/quickstart && python3 ../../../sbysrc/sby.py -f memory.sby
 
-run_tests:
+test:
 	$(MAKE) -C tests test
 
 html:

tests/Makefile

@@ -2,6 +2,23 @@ test:
 
 .PHONY: test clean refresh help
 
+TOOL_LIST := \
+	btorsim \
+	yices \
+	aigbmc \
+	avy \
+	bitwuzla \
+	boolector \
+	btormc \
+	cvc4 \
+	mathsat \
+	pono \
+	suprove \
+	yices-smt2 \
+	yices \
+	yosys-abc \
+	z3
+
 help:
 	@cat make/help.txt
 
@@ -15,5 +32,21 @@ make/rules/test/%.mk:
 	python3 make/test_rules.py $<
 
 ifneq (help,$(MAKECMDGOALS))
-include make/rules/collect.mk
+
+# 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
+
 endif

tests/junit/validate_junit.py

@@ -1,4 +1,13 @@
-from xmlschema import XMLSchema, XMLSchemaValidationError
+try:
+    from xmlschema import XMLSchema, XMLSchemaValidationError
+except ImportError:
+    import os
+    if "NOSKIP" not in os.environ.get("MAKEFLAGS", ""):
+        print()
+        print("SKIPPING python library xmlschema not found, skipping JUnit output validation")
+        print()
+        exit(0)
+
 import argparse
 
 def main():

tests/make/required_tools.py

@@ -0,0 +1,90 @@
+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"],
+}
+
+
+def found_tools():
+    with open("make/rules/found_tools") as found_tools_file:
+        return [tool.strip() for tool in found_tools_file.readlines()]
+
+
+if __name__ == "__main__":
+    import subprocess
+    import sys
+    import os
+    from pathlib import Path
+
+    args = sys.argv[1:]
+
+    if args and args[0] == "run":
+        target, command, *required_tools = args[1:]
+
+        with open("make/rules/found_tools") as found_tools_file:
+            found_tools = set(tool.strip() for tool in found_tools_file.readlines())
+
+        missing_tools = sorted(
+            f"`{tool}`" for tool in required_tools if tool not in found_tools
+        )
+        if missing_tools:
+            noskip = "NOSKIP" in os.environ.get("MAKEFLAGS", "")
+            print()
+            print(f"SKIPPING {target}: {', '.join(missing_tools)} not found")
+            if noskip:
+                print("NOSKIP was set, treating this as an error")
+            print()
+            exit(noskip)
+
+        print(command, flush=True)
+        exit(subprocess.call(command, shell=True))
+
+    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)

tests/make/test_rules.py

@@ -1,10 +1,11 @@
-import shutil
 import sys
 import os
 import subprocess
 import json
+import shlex
 from pathlib import Path
 
+from required_tools import REQUIRED_TOOLS
 
 sby_file = Path(sys.argv[1])
 sby_dir = sby_file.parent
@@ -26,21 +27,6 @@ def parse_engine(engine):
     return engine, default_solvers.get(engine)
 
 
-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"],
-    ("aiger", "avy"): ["avy"],
-    ("aiger", "aigbmc"): ["aigbmc"],
-    ("btor", "btormc"): ["btormc"],
-    ("btor", "pono"): ["pono"],
-}
-
 rules_file = Path("make/rules/test") / sby_dir / (sby_file.name + ".mk")
 rules_file.parent.mkdir(exist_ok=True, parents=True)
 
@@ -63,36 +49,26 @@ with rules_file.open("w") as rules:
         for engine in info["engines"]:
             engine, solver = parse_engine(engine)
             engines.add(engine)
-            required_tools.update(REQUIRED_TOOLS.get((engine, solver), ()))
+            required_tools.update(
+                REQUIRED_TOOLS.get((engine, solver), REQUIRED_TOOLS.get(engine, ()))
+            )
             if solver:
                 solvers.add(solver)
                 engine_solvers.add((engine, solver))
 
+        required_tools = sorted(required_tools)
+
         print(f".PHONY: {target}", file=rules)
         print(f"{target}:", file=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
-        )
-
-        if missing_tools:
-            print(
-                f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo",
-                file=rules,
-            )
-
-        elif shell_script.exists():
-            print(
-                f"\tcd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}",
-                file=rules,
-            )
+        if shell_script.exists():
+            command = f"cd {sby_dir} && SBY_FILE={sby_file.name} WORKDIR={workdirname} TASK={task} bash {shell_script.name}"
         else:
-            print(
-                f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}",
-                file=rules,
-            )
+            command = f"cd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}"
+
+        print(f"\t@python3 make/required_tools.py run {target} {shlex.quote(command)} {shlex.join(required_tools)}", file=rules)
 
         print(f".PHONY: clean-{target}", file=rules)
         print(f"clean-{target}:", file=rules)