From 8da6f07cb3c11375ac59b625aee4f75b40ca8464 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 11 Apr 2022 17:39:05 +0200 Subject: [PATCH] Refactor tests Organize tests into subdirectories and use a new makefile that scans .sby files and allows selecting tests by mode, engine, solver and/or subdirectory. Automatically skips tests that use engines/solvers that are not found in the PATH. See `cd tests; make help` for a description of supported make targets. --- tests/.gitignore | 18 +-- tests/Makefile | 32 ++--- tests/{ => junit}/JUnit.xsd | 0 tests/junit/Makefile | 2 + tests/{ => junit}/junit_assert.sby | 0 tests/junit/junit_assert.sh | 4 + tests/{ => junit}/junit_cover.sby | 0 tests/junit/junit_cover.sh | 4 + tests/{scripted => junit}/junit_expect.sby | 0 tests/junit/junit_expect.sh | 4 + tests/{ => junit}/junit_nocodeloc.sby | 0 tests/junit/junit_nocodeloc.sh | 4 + tests/{ => junit}/junit_timeout_error.sby | 0 tests/junit/junit_timeout_error.sh | 4 + tests/{ => junit}/validate_junit.py | 0 tests/keepgoing/Makefile | 2 + tests/{ => keepgoing}/check_output.py | 0 tests/keepgoing/keepgoing_multi_step.py | 31 ++++ .../{ => keepgoing}/keepgoing_multi_step.sby | 0 tests/keepgoing/keepgoing_multi_step.sh | 4 + tests/{ => keepgoing}/keepgoing_multi_step.sv | 0 .../keepgoing_same_step.py} | 11 +- tests/{ => keepgoing}/keepgoing_same_step.sby | 0 tests/keepgoing/keepgoing_same_step.sh | 4 + tests/{ => keepgoing}/keepgoing_same_step.sv | 0 .../keepgoing_smtc.py} | 15 +- tests/{ => keepgoing}/keepgoing_smtc.sby | 0 tests/keepgoing/keepgoing_smtc.sh | 4 + tests/keepgoing_multi_step.check.py | 29 ---- tests/make/collect_tests.py | 47 ++++++ tests/make/help.txt | 20 +++ tests/make/subdir.mk | 15 ++ tests/make/test_rules.py | 135 ++++++++++++++++++ tests/regression/Makefile | 2 + .../aim_vs_smt2_nonzero_start_offset.sby | 17 ++- .../invalid_ff_dcinit_merge.sby | 0 tests/scripted/.gitignore | 1 - tests/scripted/Makefile | 11 -- tests/scripted/junit_expect.sh | 5 - tests/{ => unsorted}/2props1trace.sby | 0 tests/unsorted/Makefile | 2 + tests/{ => unsorted}/both_ex.sby | 0 tests/{ => unsorted}/both_ex.v | 0 tests/{ => unsorted}/cover.sby | 0 tests/{ => unsorted}/cover.sv | 0 tests/{ => unsorted}/cover_fail.sby | 0 tests/{ => unsorted}/demo.sby | 0 tests/{ => unsorted}/demo.sv | 0 tests/{ => unsorted}/memory.sby | 0 tests/{ => unsorted}/memory.sv | 0 tests/{ => unsorted}/mixed.sby | 0 tests/{ => unsorted}/mixed.v | 0 tests/{ => unsorted}/multi_assert.sby | 0 tests/{ => unsorted}/preunsat.sby | 0 tests/{ => unsorted}/prv32fmcmp.sby | 2 +- tests/{ => unsorted}/prv32fmcmp.v | 0 tests/{ => unsorted}/redxor.sby | 0 tests/{ => unsorted}/redxor.v | 0 tests/{ => unsorted}/stopfirst.sby | 0 tests/{ => unsorted}/submod_props.sby | 0 60 files changed, 328 insertions(+), 101 deletions(-) rename tests/{ => junit}/JUnit.xsd (100%) create mode 100644 tests/junit/Makefile rename tests/{ => junit}/junit_assert.sby (100%) create mode 100644 tests/junit/junit_assert.sh rename tests/{ => junit}/junit_cover.sby (100%) create mode 100644 tests/junit/junit_cover.sh rename tests/{scripted => junit}/junit_expect.sby (100%) create mode 100644 tests/junit/junit_expect.sh rename tests/{ => junit}/junit_nocodeloc.sby (100%) create mode 100644 tests/junit/junit_nocodeloc.sh rename tests/{ => junit}/junit_timeout_error.sby (100%) create mode 100644 tests/junit/junit_timeout_error.sh rename tests/{ => junit}/validate_junit.py (100%) create mode 100644 tests/keepgoing/Makefile rename tests/{ => keepgoing}/check_output.py (100%) create mode 100644 tests/keepgoing/keepgoing_multi_step.py rename tests/{ => keepgoing}/keepgoing_multi_step.sby (100%) create mode 100644 tests/keepgoing/keepgoing_multi_step.sh rename tests/{ => keepgoing}/keepgoing_multi_step.sv (100%) rename tests/{keepgoing_same_step.check.py => keepgoing/keepgoing_same_step.py} (69%) rename tests/{ => keepgoing}/keepgoing_same_step.sby (100%) create mode 100644 tests/keepgoing/keepgoing_same_step.sh rename tests/{ => keepgoing}/keepgoing_same_step.sv (100%) rename tests/{keepgoing_smtc.check.py => keepgoing/keepgoing_smtc.py} (66%) rename tests/{ => keepgoing}/keepgoing_smtc.sby (100%) create mode 100644 tests/keepgoing/keepgoing_smtc.sh delete mode 100644 tests/keepgoing_multi_step.check.py create mode 100644 tests/make/collect_tests.py create mode 100644 tests/make/help.txt create mode 100644 tests/make/subdir.mk create mode 100644 tests/make/test_rules.py create mode 100644 tests/regression/Makefile rename tests/{ => regression}/aim_vs_smt2_nonzero_start_offset.sby (66%) rename tests/{ => regression}/invalid_ff_dcinit_merge.sby (100%) delete mode 100644 tests/scripted/.gitignore delete mode 100644 tests/scripted/Makefile delete mode 100644 tests/scripted/junit_expect.sh rename tests/{ => unsorted}/2props1trace.sby (100%) create mode 100644 tests/unsorted/Makefile rename tests/{ => unsorted}/both_ex.sby (100%) rename tests/{ => unsorted}/both_ex.v (100%) rename tests/{ => unsorted}/cover.sby (100%) rename tests/{ => unsorted}/cover.sv (100%) rename tests/{ => unsorted}/cover_fail.sby (100%) rename tests/{ => unsorted}/demo.sby (100%) rename tests/{ => unsorted}/demo.sv (100%) rename tests/{ => unsorted}/memory.sby (100%) rename tests/{ => unsorted}/memory.sv (100%) rename tests/{ => unsorted}/mixed.sby (100%) rename tests/{ => unsorted}/mixed.v (100%) rename tests/{ => unsorted}/multi_assert.sby (100%) rename tests/{ => unsorted}/preunsat.sby (100%) rename tests/{ => unsorted}/prv32fmcmp.sby (89%) rename tests/{ => unsorted}/prv32fmcmp.v (100%) rename tests/{ => unsorted}/redxor.sby (100%) rename tests/{ => unsorted}/redxor.v (100%) rename tests/{ => unsorted}/stopfirst.sby (100%) rename tests/{ => unsorted}/submod_props.sby (100%) diff --git a/tests/.gitignore b/tests/.gitignore index f91f05a..9737325 100644 --- a/tests/.gitignore +++ b/tests/.gitignore @@ -1,16 +1,2 @@ -/both_ex*/ -/cover*/ -/demo*/ -/memory*/ -/mixed*/ -/preunsat*/ -/prv32fmcmp*/ -/redxor*/ -/stopfirst*/ -/junit_*/ -/keepgoing_*/ -/submod_props*/ -/multi_assert*/ -/aim_vs_smt2_nonzero_start_offset*/ -/invalid_ff_dcinit_merge*/ -/2props1trace*/ +/make/rules +__pycache__ diff --git a/tests/Makefile b/tests/Makefile index 177688c..eb941e2 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -1,25 +1,19 @@ -SBY_FILES=$(wildcard *.sby) -SBY_TESTS=$(addprefix test_,$(SBY_FILES:.sby=)) -CHECK_PY_FILES=$(wildcard *.check.py) -CHECK_PY_TASKS=$(addprefix check_,$(CHECK_PY_FILES:.check.py=)) -JUNIT_TESTS=junit_assert_pass junit_assert_fail junit_assert_preunsat \ -junit_cover_pass junit_cover_uncovered junit_cover_assert junit_cover_preunsat \ -junit_timeout_error_timeout junit_timeout_error_syntax junit_timeout_error_solver +test: -.PHONY: test validate_junit scripted +.PHONY: test clean refresh help -test: $(JUNIT_TESTS) $(CHECK_PY_TASKS) +help: + @cat make/help.txt -test_%: %.sby FORCE - python3 ../sbysrc/sby.py -f $< +export SBY_WORKDIR_GITIGNORE=1 +export SBY_MAIN=$(realpath $(dir $(firstword $(MAKEFILE_LIST)))/../sbysrc/sby.py) -$(CHECK_PY_TASKS): check_%: %.check.py test_% - python3 $< +make/rules/collect.mk: make/collect_tests.py + python3 make/collect_tests.py -$(JUNIT_TESTS): $(SBY_TESTS) - python3 validate_junit.py $@/$@.xml +make/rules/test/%.mk: + python3 make/test_rules.py $< -scripted: - make -C scripted - -FORCE: +ifneq (help,$(MAKECMDGOALS)) +include make/rules/collect.mk +endif diff --git a/tests/JUnit.xsd b/tests/junit/JUnit.xsd similarity index 100% rename from tests/JUnit.xsd rename to tests/junit/JUnit.xsd diff --git a/tests/junit/Makefile b/tests/junit/Makefile new file mode 100644 index 0000000..dd89403 --- /dev/null +++ b/tests/junit/Makefile @@ -0,0 +1,2 @@ +SUBDIR=junit +include ../make/subdir.mk diff --git a/tests/junit_assert.sby b/tests/junit/junit_assert.sby similarity index 100% rename from tests/junit_assert.sby rename to tests/junit/junit_assert.sby diff --git a/tests/junit/junit_assert.sh b/tests/junit/junit_assert.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_assert.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit_cover.sby b/tests/junit/junit_cover.sby similarity index 100% rename from tests/junit_cover.sby rename to tests/junit/junit_cover.sby diff --git a/tests/junit/junit_cover.sh b/tests/junit/junit_cover.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_cover.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/scripted/junit_expect.sby b/tests/junit/junit_expect.sby similarity index 100% rename from tests/scripted/junit_expect.sby rename to tests/junit/junit_expect.sby diff --git a/tests/junit/junit_expect.sh b/tests/junit/junit_expect.sh new file mode 100644 index 0000000..cb66b10 --- /dev/null +++ b/tests/junit/junit_expect.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +! python3 $SBY_MAIN -f $SBY_FILE $TASK +grep '' $WORKDIR/$WORKDIR.xml diff --git a/tests/junit_nocodeloc.sby b/tests/junit/junit_nocodeloc.sby similarity index 100% rename from tests/junit_nocodeloc.sby rename to tests/junit/junit_nocodeloc.sby diff --git a/tests/junit/junit_nocodeloc.sh b/tests/junit/junit_nocodeloc.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_nocodeloc.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/junit_timeout_error.sby b/tests/junit/junit_timeout_error.sby similarity index 100% rename from tests/junit_timeout_error.sby rename to tests/junit/junit_timeout_error.sby diff --git a/tests/junit/junit_timeout_error.sh b/tests/junit/junit_timeout_error.sh new file mode 100644 index 0000000..f18d8ca --- /dev/null +++ b/tests/junit/junit_timeout_error.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 validate_junit.py $WORKDIR/$WORKDIR.xml diff --git a/tests/validate_junit.py b/tests/junit/validate_junit.py similarity index 100% rename from tests/validate_junit.py rename to tests/junit/validate_junit.py diff --git a/tests/keepgoing/Makefile b/tests/keepgoing/Makefile new file mode 100644 index 0000000..0727e8b --- /dev/null +++ b/tests/keepgoing/Makefile @@ -0,0 +1,2 @@ +SUBDIR=keepgoing +include ../make/subdir.mk diff --git a/tests/check_output.py b/tests/keepgoing/check_output.py similarity index 100% rename from tests/check_output.py rename to tests/keepgoing/check_output.py diff --git a/tests/keepgoing/keepgoing_multi_step.py b/tests/keepgoing/keepgoing_multi_step.py new file mode 100644 index 0000000..c724c66 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.py @@ -0,0 +1,31 @@ +import sys +from check_output import * + +src = "keepgoing_multi_step.sv" + +workdir = sys.argv[1] + +assert_0 = line_ref(workdir, src, "assert(0)") +step_3_7 = line_ref(workdir, src, "step 3,7") +step_5 = line_ref(workdir, src, "step 5") +step_7 = line_ref(workdir, src, "step 7") + +log = open(workdir + "/logfile.txt").read() +log_per_trace = log.split("Writing trace to VCD file")[:-1] + +assert len(log_per_trace) == 4 + + +assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) + +for i in range(1, 4): + assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) + + +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) +assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) +assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) + +pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd" +assert re.search(pattern, open(f"{workdir}/{workdir}.xml").read()) diff --git a/tests/keepgoing_multi_step.sby b/tests/keepgoing/keepgoing_multi_step.sby similarity index 100% rename from tests/keepgoing_multi_step.sby rename to tests/keepgoing/keepgoing_multi_step.sby diff --git a/tests/keepgoing/keepgoing_multi_step.sh b/tests/keepgoing/keepgoing_multi_step.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_multi_step.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing_multi_step.sv b/tests/keepgoing/keepgoing_multi_step.sv similarity index 100% rename from tests/keepgoing_multi_step.sv rename to tests/keepgoing/keepgoing_multi_step.sv diff --git a/tests/keepgoing_same_step.check.py b/tests/keepgoing/keepgoing_same_step.py similarity index 69% rename from tests/keepgoing_same_step.check.py rename to tests/keepgoing/keepgoing_same_step.py index 35cd314..e273916 100644 --- a/tests/keepgoing_same_step.check.py +++ b/tests/keepgoing/keepgoing_same_step.py @@ -1,13 +1,14 @@ +import sys from check_output import * -task = "keepgoing_same_step" +workdir = sys.argv[1] src = "keepgoing_same_step.sv" -assert_a = line_ref(task, src, "assert(a)") -assert_not_a = line_ref(task, src, "assert(!a)") -assert_0 = line_ref(task, src, "assert(0)") +assert_a = line_ref(workdir, src, "assert(a)") +assert_not_a = line_ref(workdir, src, "assert(!a)") +assert_0 = line_ref(workdir, src, "assert(0)") -log = open(task + "/logfile.txt").read() +log = open(workdir + "/logfile.txt").read() log_per_trace = log.split("Writing trace to VCD file")[:-1] assert len(log_per_trace) == 2 diff --git a/tests/keepgoing_same_step.sby b/tests/keepgoing/keepgoing_same_step.sby similarity index 100% rename from tests/keepgoing_same_step.sby rename to tests/keepgoing/keepgoing_same_step.sby diff --git a/tests/keepgoing/keepgoing_same_step.sh b/tests/keepgoing/keepgoing_same_step.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_same_step.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing_same_step.sv b/tests/keepgoing/keepgoing_same_step.sv similarity index 100% rename from tests/keepgoing_same_step.sv rename to tests/keepgoing/keepgoing_same_step.sv diff --git a/tests/keepgoing_smtc.check.py b/tests/keepgoing/keepgoing_smtc.py similarity index 66% rename from tests/keepgoing_smtc.check.py rename to tests/keepgoing/keepgoing_smtc.py index 5749e3f..e0fd27d 100644 --- a/tests/keepgoing_smtc.check.py +++ b/tests/keepgoing/keepgoing_smtc.py @@ -1,16 +1,17 @@ +import sys from check_output import * -task = "keepgoing_smtc" +workdir = sys.argv[1] src = "keepgoing_same_step.sv" -assert_a = line_ref(task, src, "assert(a)") -assert_not_a = line_ref(task, src, "assert(!a)") -assert_0 = line_ref(task, src, "assert(0)") +assert_a = line_ref(workdir, src, "assert(a)") +assert_not_a = line_ref(workdir, src, "assert(!a)") +assert_0 = line_ref(workdir, src, "assert(0)") -assert_false = line_ref(task, "extra.smtc", "assert false") -assert_distinct = line_ref(task, "extra.smtc", "assert (distinct") +assert_false = line_ref(workdir, "extra.smtc", "assert false") +assert_distinct = line_ref(workdir, "extra.smtc", "assert (distinct") -log = open(task + "/logfile.txt").read() +log = open(workdir + "/logfile.txt").read() log_per_trace = log.split("Writing trace to VCD file")[:-1] assert len(log_per_trace) == 4 diff --git a/tests/keepgoing_smtc.sby b/tests/keepgoing/keepgoing_smtc.sby similarity index 100% rename from tests/keepgoing_smtc.sby rename to tests/keepgoing/keepgoing_smtc.sby diff --git a/tests/keepgoing/keepgoing_smtc.sh b/tests/keepgoing/keepgoing_smtc.sh new file mode 100644 index 0000000..aca8be6 --- /dev/null +++ b/tests/keepgoing/keepgoing_smtc.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -e +python3 $SBY_MAIN -f $SBY_FILE $TASK +python3 ${SBY_FILE%.sby}.py $WORKDIR diff --git a/tests/keepgoing_multi_step.check.py b/tests/keepgoing_multi_step.check.py deleted file mode 100644 index 78c713f..0000000 --- a/tests/keepgoing_multi_step.check.py +++ /dev/null @@ -1,29 +0,0 @@ -from check_output import * - -src = "keepgoing_multi_step.sv" - -for task in ["keepgoing_multi_step_bmc", "keepgoing_multi_step_prove"]: - assert_0 = line_ref(task, src, "assert(0)") - step_3_7 = line_ref(task, src, "step 3,7") - step_5 = line_ref(task, src, "step 5") - step_7 = line_ref(task, src, "step 7") - - log = open(task + "/logfile.txt").read() - log_per_trace = log.split("Writing trace to VCD file")[:-1] - - assert len(log_per_trace) == 4 - - - assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) - - for i in range(1, 4): - assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) - - - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) - assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) - assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) - - pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.vcd" - assert re.search(pattern, open(f"{task}/{task}.xml").read()) diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py new file mode 100644 index 0000000..cf782b9 --- /dev/null +++ b/tests/make/collect_tests.py @@ -0,0 +1,47 @@ +from pathlib import Path +import re + +tests = [] +checked_dirs = [] + +SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./]*$") + +def collect(path): + # don't pick up any paths that need escaping nor any sby workdirs + if not SAFE_PATH.match(str(path)) or (path / "config.sby").exists(): + return + + checked_dirs.append(path) + for entry in path.glob("*.sby"): + filename = str(entry) + if not SAFE_PATH.match(filename): + continue + if not re.match(r"^[a-zA-Z0-9_./]*$", filename): + print(f"skipping {filename!r}, use only [a-zA-Z0-9_./] in filenames") + continue + tests.append(entry) + for entry in path.glob("*"): + if entry.is_dir(): + collect(entry) + + +collect(Path(".")) + +out_file = Path("make/rules/collect.mk") +out_file.parent.mkdir(exist_ok=True) + +with out_file.open("w") as output: + + + for checked_dir in checked_dirs: + print(f"{out_file}: {checked_dir}", file=output) + + for test in tests: + 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(): + print(f"make/rules/test/{test}.mk: {script_file}", file=output) + print(f"make/rules/test/{test}.mk: make/test_rules.py", file=output) + for test in tests: + print(f"-include make/rules/test/{test}.mk", file=output) diff --git a/tests/make/help.txt b/tests/make/help.txt new file mode 100644 index 0000000..c840c4c --- /dev/null +++ b/tests/make/help.txt @@ -0,0 +1,20 @@ +make test: + run all tests (default) + +make clean: + remove all sby workdirs + +make test[_m_][_e_][_s_]: + run all tests that use a specific mode, engine and solver + +make : + run the test for .sby + +make refresh: + do nothing apart from refreshing generated make rules + +make help: + show this help + +running make in a subdirectory or prefixing the target with the subdirectory +limits the test selection to that directory diff --git a/tests/make/subdir.mk b/tests/make/subdir.mk new file mode 100644 index 0000000..b1f367a --- /dev/null +++ b/tests/make/subdir.mk @@ -0,0 +1,15 @@ +test: + @$(MAKE) -C .. $(SUBDIR)/$@ + +.PHONY: test refresh IMPLICIT_PHONY + +IMPLICIT_PHONY: + +refresh: + @$(MAKE) -C .. refresh + +help: + @$(MAKE) -C .. help + +%: IMPLICIT_PHONY + @$(MAKE) -C .. $(SUBDIR)/$@ diff --git a/tests/make/test_rules.py b/tests/make/test_rules.py new file mode 100644 index 0000000..1ad49ba --- /dev/null +++ b/tests/make/test_rules.py @@ -0,0 +1,135 @@ +import shutil +import sys +import os +import subprocess +import json +from pathlib import Path + + +sby_file = Path(sys.argv[1]) +sby_dir = sby_file.parent + + +taskinfo = json.loads( + subprocess.check_output( + [sys.executable, os.getenv("SBY_MAIN"), "--dumptaskinfo", sby_file] + ) +) + + +def parse_engine(engine): + engine, *args = engine + default_solvers = {"smtbmc": "yices"} + for arg in args: + if not arg.startswith("-"): + return engine, arg + 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) + +with rules_file.open("w") as rules: + name = str(sby_dir / sby_file.stem) + + for task, info in taskinfo.items(): + target = name + workdirname = sby_file.stem + if task: + target += f"_{task}" + workdirname += f"_{task}" + + engines = set() + solvers = set() + engine_solvers = set() + + required_tools = set() + + for engine in info["engines"]: + engine, solver = parse_engine(engine) + engines.add(engine) + required_tools.update(REQUIRED_TOOLS.get((engine, solver), ())) + if solver: + solvers.add(solver) + engine_solvers.add((engine, solver)) + + 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, + ) + else: + print( + f"\tcd {sby_dir} && python3 $(SBY_MAIN) -f {sby_file.name} {task}", + file=rules, + ) + + print(f".PHONY: clean-{target}", file=rules) + print(f"clean-{target}:", file=rules) + print(f"\trm -rf {target}", file=rules) + + test_groups = [] + + mode = info["mode"] + + test_groups.append(f"test_m_{mode}") + + for engine in sorted(engines): + test_groups.append(f"test_e_{engine}") + test_groups.append(f"test_m_{mode}_e_{engine}") + + for solver in sorted(solvers): + test_groups.append(f"test_s_{solver}") + test_groups.append(f"test_m_{mode}_s_{solver}") + + for engine, solver in sorted(engine_solvers): + test_groups.append(f"test_e_{engine}_s_{solver}") + test_groups.append(f"test_m_{mode}_e_{engine}_s_{solver}") + + prefix = "" + + for part in [*sby_dir.parts, ""]: + print(f".PHONY: {prefix}clean {prefix}test", file=rules) + print(f"{prefix}clean: clean-{target}", file=rules) + print(f"{prefix}test: {target}", file=rules) + + for test_group in test_groups: + print(f".PHONY: {prefix}{test_group}", file=rules) + print(f"{prefix}{test_group}: {target}", file=rules) + prefix += f"{part}/" + + tasks = [task for task in taskinfo.keys() if task] + + if tasks: + print(f".PHONY: {name}", file=rules) + print(f"{name}:", *(f"{name}_{task}" for task in tasks), file=rules) diff --git a/tests/regression/Makefile b/tests/regression/Makefile new file mode 100644 index 0000000..0d9b684 --- /dev/null +++ b/tests/regression/Makefile @@ -0,0 +1,2 @@ +SUBDIR=regression +include ../make/subdir.mk diff --git a/tests/aim_vs_smt2_nonzero_start_offset.sby b/tests/regression/aim_vs_smt2_nonzero_start_offset.sby similarity index 66% rename from tests/aim_vs_smt2_nonzero_start_offset.sby rename to tests/regression/aim_vs_smt2_nonzero_start_offset.sby index 4309551..94591d7 100644 --- a/tests/aim_vs_smt2_nonzero_start_offset.sby +++ b/tests/regression/aim_vs_smt2_nonzero_start_offset.sby @@ -1,6 +1,9 @@ [tasks] -bmc -prove +abc_bmc3 bmc +abc_sim3 bmc +aiger_avy prove +aiger_suprove prove +abc_pdr prove [options] bmc: mode bmc @@ -9,11 +12,11 @@ expect fail wait on [engines] -bmc: abc bmc3 -bmc: abc sim3 -prove: aiger avy -prove: aiger suprove -prove: abc pdr +abc_bmc3: abc bmc3 +abc_sim3: abc sim3 +aiger_avy: aiger avy +aiger_suprove: aiger suprove +abc_pdr: abc pdr [script] read -sv test.sv diff --git a/tests/invalid_ff_dcinit_merge.sby b/tests/regression/invalid_ff_dcinit_merge.sby similarity index 100% rename from tests/invalid_ff_dcinit_merge.sby rename to tests/regression/invalid_ff_dcinit_merge.sby diff --git a/tests/scripted/.gitignore b/tests/scripted/.gitignore deleted file mode 100644 index 6403b85..0000000 --- a/tests/scripted/.gitignore +++ /dev/null @@ -1 +0,0 @@ -/junit_*/ diff --git a/tests/scripted/Makefile b/tests/scripted/Makefile deleted file mode 100644 index ca27199..0000000 --- a/tests/scripted/Makefile +++ /dev/null @@ -1,11 +0,0 @@ -SH_FILES=$(wildcard *.sh) -SH_TESTS=$(addprefix test_,$(SH_FILES:.sh=)) - -test: $(SH_TESTS) - -test_%: %.sh FORCE - bash $< - -FORCE: - -.PHONY: test FORCE diff --git a/tests/scripted/junit_expect.sh b/tests/scripted/junit_expect.sh deleted file mode 100644 index 27b972d..0000000 --- a/tests/scripted/junit_expect.sh +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/bash - -# this is expected to return 1 so don't use 'set -e' -python3 ../../sbysrc/sby.py -f junit_expect.sby -grep '' junit_expect/junit_expect.xml diff --git a/tests/2props1trace.sby b/tests/unsorted/2props1trace.sby similarity index 100% rename from tests/2props1trace.sby rename to tests/unsorted/2props1trace.sby diff --git a/tests/unsorted/Makefile b/tests/unsorted/Makefile new file mode 100644 index 0000000..61c3a6f --- /dev/null +++ b/tests/unsorted/Makefile @@ -0,0 +1,2 @@ +SUBDIR=unsorted +include ../make/subdir.mk diff --git a/tests/both_ex.sby b/tests/unsorted/both_ex.sby similarity index 100% rename from tests/both_ex.sby rename to tests/unsorted/both_ex.sby diff --git a/tests/both_ex.v b/tests/unsorted/both_ex.v similarity index 100% rename from tests/both_ex.v rename to tests/unsorted/both_ex.v diff --git a/tests/cover.sby b/tests/unsorted/cover.sby similarity index 100% rename from tests/cover.sby rename to tests/unsorted/cover.sby diff --git a/tests/cover.sv b/tests/unsorted/cover.sv similarity index 100% rename from tests/cover.sv rename to tests/unsorted/cover.sv diff --git a/tests/cover_fail.sby b/tests/unsorted/cover_fail.sby similarity index 100% rename from tests/cover_fail.sby rename to tests/unsorted/cover_fail.sby diff --git a/tests/demo.sby b/tests/unsorted/demo.sby similarity index 100% rename from tests/demo.sby rename to tests/unsorted/demo.sby diff --git a/tests/demo.sv b/tests/unsorted/demo.sv similarity index 100% rename from tests/demo.sv rename to tests/unsorted/demo.sv diff --git a/tests/memory.sby b/tests/unsorted/memory.sby similarity index 100% rename from tests/memory.sby rename to tests/unsorted/memory.sby diff --git a/tests/memory.sv b/tests/unsorted/memory.sv similarity index 100% rename from tests/memory.sv rename to tests/unsorted/memory.sv diff --git a/tests/mixed.sby b/tests/unsorted/mixed.sby similarity index 100% rename from tests/mixed.sby rename to tests/unsorted/mixed.sby diff --git a/tests/mixed.v b/tests/unsorted/mixed.v similarity index 100% rename from tests/mixed.v rename to tests/unsorted/mixed.v diff --git a/tests/multi_assert.sby b/tests/unsorted/multi_assert.sby similarity index 100% rename from tests/multi_assert.sby rename to tests/unsorted/multi_assert.sby diff --git a/tests/preunsat.sby b/tests/unsorted/preunsat.sby similarity index 100% rename from tests/preunsat.sby rename to tests/unsorted/preunsat.sby diff --git a/tests/prv32fmcmp.sby b/tests/unsorted/prv32fmcmp.sby similarity index 89% rename from tests/prv32fmcmp.sby rename to tests/unsorted/prv32fmcmp.sby index 2412eb8..bd4e096 100644 --- a/tests/prv32fmcmp.sby +++ b/tests/unsorted/prv32fmcmp.sby @@ -17,5 +17,5 @@ read -sv prv32fmcmp.v prep -top prv32fmcmp [files] -../extern/picorv32.v +../../extern/picorv32.v prv32fmcmp.v diff --git a/tests/prv32fmcmp.v b/tests/unsorted/prv32fmcmp.v similarity index 100% rename from tests/prv32fmcmp.v rename to tests/unsorted/prv32fmcmp.v diff --git a/tests/redxor.sby b/tests/unsorted/redxor.sby similarity index 100% rename from tests/redxor.sby rename to tests/unsorted/redxor.sby diff --git a/tests/redxor.v b/tests/unsorted/redxor.v similarity index 100% rename from tests/redxor.v rename to tests/unsorted/redxor.v diff --git a/tests/stopfirst.sby b/tests/unsorted/stopfirst.sby similarity index 100% rename from tests/stopfirst.sby rename to tests/unsorted/stopfirst.sby diff --git a/tests/submod_props.sby b/tests/unsorted/submod_props.sby similarity index 100% rename from tests/submod_props.sby rename to tests/unsorted/submod_props.sby -- 2.30.2