diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ea48d06..67abe1f 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/Makefile b/Makefile index 3b58d87..07f85a4 100644 --- a/Makefile +++ b/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: diff --git a/tests/Makefile b/tests/Makefile index eb941e2..ccb983c 100644 --- a/tests/Makefile +++ b/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 diff --git a/tests/junit/validate_junit.py b/tests/junit/validate_junit.py index c1c0573..1999551 100644 --- a/tests/junit/validate_junit.py +++ b/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(): diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py new file mode 100644 index 0000000..67b5d2b --- /dev/null +++ b/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) diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 1ad49ba..04d2226 100644 --- a/tests/make/test_rules.py +++ b/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)