From 939e000036e8293a67baf6a359554c8189244fe5 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 30 May 2022 13:35:57 +0200 Subject: [PATCH 1/7] Makefile: Rename run_tests to test, update help, use .PHONY --- Makefile | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 3b58d87..56824a8 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" @@ -47,7 +53,7 @@ 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; \ fi @@ -113,7 +119,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: From dc22d97362162c39bd826df2600f34c6b9ba7fbe Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 30 May 2022 14:37:20 +0200 Subject: [PATCH 2/7] Better checking of available solvers Check for required auxiliary tools and always regenerate the make rules when the set of available tools changes. --- tests/Makefile | 24 ++++++++++++++++++++++++ tests/make/collect_tests.py | 2 +- tests/make/test_rules.py | 17 +++++++++++------ 3 files changed, 36 insertions(+), 7 deletions(-) diff --git a/tests/Makefile b/tests/Makefile index eb941e2..6992f92 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,12 @@ make/rules/test/%.mk: python3 make/test_rules.py $< 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 \ +) + include make/rules/collect.mk + endif diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index cf782b9..7b0cda3 100644 --- a/tests/make/collect_tests.py +++ b/tests/make/collect_tests.py @@ -37,7 +37,7 @@ with out_file.open("w") as output: print(f"{out_file}: {checked_dir}", file=output) for test in tests: - print(f"make/rules/test/{test}.mk: {test}", file=output) + print(f"make/rules/test/{test}.mk: {test} make/rules/found_tools", file=output) for ext in [".sh", ".py"]: script_file = test.parent / (test.stem + ext) if script_file.exists(): diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 1ad49ba..149e524 100644 --- a/tests/make/test_rules.py +++ b/tests/make/test_rules.py @@ -26,6 +26,8 @@ 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"], @@ -34,11 +36,12 @@ REQUIRED_TOOLS = { ("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"], + ("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") @@ -63,7 +66,9 @@ 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)) From 206562e5de2d9f6bd976d239f1f7e4a25abee033 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 30 May 2022 15:27:14 +0200 Subject: [PATCH 3/7] Check for the tabby/oss cad suite before running make ci checks --- Makefile | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 56824a8..07f85a4 100644 --- a/Makefile +++ b/Makefile @@ -45,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 \ @@ -55,7 +60,14 @@ ci: \ test_quickstart_demo test_quickstart_cover test_quickstart_prove test_quickstart_memory \ 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: From 00efdecb4bdb06adecf07ad09c096c5883171697 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 2 Jun 2022 16:24:30 +0200 Subject: [PATCH 4/7] tests: Check for btorsim --vcd --- tests/Makefile | 17 +++++++--- tests/make/required_tools.py | 64 ++++++++++++++++++++++++++++++++++++ tests/make/test_rules.py | 22 ++----------- 3 files changed, 79 insertions(+), 24 deletions(-) create mode 100644 tests/make/required_tools.py diff --git a/tests/Makefile b/tests/Makefile index 6992f92..ccb983c 100644 --- a/tests/Makefile +++ b/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 diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py new file mode 100644 index 0000000..4d06e10 --- /dev/null +++ b/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()] diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 149e524..d03fc6c 100644 --- a/tests/make/test_rules.py +++ b/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: From d398a3c2df7b3761cda5e768b6881ca6186f0429 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 2 Jun 2022 16:25:11 +0200 Subject: [PATCH 5/7] tests: Fail on CI when any required tool is missing --- .github/workflows/ci.yml | 2 +- tests/Makefile | 6 ++++++ tests/make/test_rules.py | 2 +- 3 files changed, 8 insertions(+), 2 deletions(-) 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/tests/Makefile b/tests/Makefile index ccb983c..6b02872 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -31,6 +31,12 @@ make/rules/collect.mk: make/collect_tests.py make/rules/test/%.mk: python3 make/test_rules.py $< +ifdef NOSKIP +SKIP_COMMAND := echo "NOSKIP was set, treating this as an error"; echo; false +else +SKIP_COMMAND := echo +endif + ifneq (help,$(MAKECMDGOALS)) # This should run every time but only trigger anything depending on it whenever diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index d03fc6c..4871b11 100644 --- a/tests/make/test_rules.py +++ b/tests/make/test_rules.py @@ -66,7 +66,7 @@ with rules_file.open("w") as rules: if missing_tools: print( - f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; echo", + f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; $(SKIP_COMMAND)", file=rules, ) From 80eacf34ca575c0c458fef845a046d76d2cd1b33 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 3 Jun 2022 17:16:01 +0200 Subject: [PATCH 6/7] Don't fail tests when xmlschema is missing --- tests/junit/validate_junit.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) 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(): From 34d6adf098ff03d63818ec20d59f7c9554336133 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 7 Jun 2022 14:29:25 +0200 Subject: [PATCH 7/7] tests: Move required tool checks from rule generation to execution This avoids regenerating the test makefile rules when the set of installed tools changes and is a bit simpler overall. --- tests/Makefile | 6 ------ tests/make/collect_tests.py | 2 +- tests/make/required_tools.py | 32 +++++++++++++++++++++++++++++--- tests/make/test_rules.py | 29 +++++++++-------------------- 4 files changed, 39 insertions(+), 30 deletions(-) diff --git a/tests/Makefile b/tests/Makefile index 6b02872..ccb983c 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -31,12 +31,6 @@ make/rules/collect.mk: make/collect_tests.py make/rules/test/%.mk: python3 make/test_rules.py $< -ifdef NOSKIP -SKIP_COMMAND := echo "NOSKIP was set, treating this as an error"; echo; false -else -SKIP_COMMAND := echo -endif - ifneq (help,$(MAKECMDGOALS)) # This should run every time but only trigger anything depending on it whenever diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index 7b0cda3..cf782b9 100644 --- a/tests/make/collect_tests.py +++ b/tests/make/collect_tests.py @@ -37,7 +37,7 @@ with out_file.open("w") as output: print(f"{out_file}: {checked_dir}", file=output) for test in tests: - print(f"make/rules/test/{test}.mk: {test} make/rules/found_tools", file=output) + print(f"make/rules/test/{test}.mk: {test}", file=output) for ext in [".sh", ".py"]: script_file = test.parent / (test.stem + ext) if script_file.exists(): diff --git a/tests/make/required_tools.py b/tests/make/required_tools.py index 4d06e10..67b5d2b 100644 --- a/tests/make/required_tools.py +++ b/tests/make/required_tools.py @@ -17,11 +17,40 @@ REQUIRED_TOOLS = { } +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(): @@ -59,6 +88,3 @@ if __name__ == "__main__": 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()] diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py index 4871b11..04d2226 100644 --- a/tests/make/test_rules.py +++ b/tests/make/test_rules.py @@ -2,9 +2,10 @@ import sys import os import subprocess import json +import shlex from pathlib import Path -from required_tools import REQUIRED_TOOLS, found_tools +from required_tools import REQUIRED_TOOLS sby_file = Path(sys.argv[1]) sby_dir = sby_file.parent @@ -55,31 +56,19 @@ with rules_file.open("w") as rules: 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 tool not in found_tools - ) - - if missing_tools: - print( - f"\t@echo; echo 'SKIPPING {target}: {', '.join(missing_tools)} not found'; $(SKIP_COMMAND)", - 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)