Merge pull request #156 from jix/refactor-tests

Refactor tests

sbysrc/sby.py

@@ -17,9 +17,9 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import argparse, os, sys, shutil, tempfile, re
+import argparse, json, os, sys, shutil, tempfile, re
 ##yosys-sys-path##
-from sby_core import SbyTask, SbyAbort, process_filename
+from sby_core import SbyConfig, SbyTask, SbyAbort, process_filename
 import time, platform
 
 class DictAction(argparse.Action):
@@ -72,6 +72,8 @@ parser.add_argument("--dumptasks", action="store_true", dest="dump_tasks",
         help="print the list of tasks")
 parser.add_argument("--dumpdefaults", action="store_true", dest="dump_defaults",
         help="print the list of default tasks")
+parser.add_argument("--dumptaskinfo", action="store_true", dest="dump_taskinfo",
+        help="output a summary of tasks as JSON")
 parser.add_argument("--dumpfiles", action="store_true", dest="dump_files",
         help="print the list of source files")
 parser.add_argument("--setup", action="store_true", dest="setupmode",
@@ -102,6 +104,7 @@ dump_cfg = args.dump_cfg
 dump_tags = args.dump_tags
 dump_tasks = args.dump_tasks
 dump_defaults = args.dump_defaults
+dump_taskinfo = args.dump_taskinfo
 dump_files = args.dump_files
 reusedir = False
 setupmode = args.setupmode
@@ -367,6 +370,21 @@ if dump_tasks or dump_defaults or dump_tags:
             print(name)
     sys.exit(0)
 
+if dump_taskinfo:
+    _, _, tasknames, _ = read_sbyconfig(sbydata, None)
+    taskinfo = {}
+    for taskname in tasknames or [None]:
+        task_sbyconfig, _, _, _ = read_sbyconfig(sbydata, taskname)
+        taskinfo[taskname or ""] = info = {}
+        cfg = SbyConfig()
+        cfg.parse_config(task_sbyconfig)
+        taskinfo[taskname or ""] = {
+            "mode": cfg.options.get("mode"),
+            "engines": cfg.engines,
+        }
+    print(json.dumps(taskinfo, indent=2))
+    sys.exit(0)
+
 if len(tasknames) == 0:
     _, _, tasknames, _ = read_sbyconfig(sbydata, None)
     if len(tasknames) == 0:
@@ -415,6 +433,10 @@ def run_task(taskname):
         my_opt_tmpdir = True
         my_workdir = tempfile.mkdtemp()
 
+    if os.getenv("SBY_WORKDIR_GITIGNORE"):
+        with open(f"{my_workdir}/.gitignore", "w") as gitignore:
+            print("*", file=gitignore)
+
     junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin"
     junit_tc_name = taskname if taskname is not None else "default"
 

sbysrc/sby_core.py

@@ -209,14 +209,110 @@ class SbyAbort(BaseException):
     pass
 
 
-class SbyTask:
-    def __init__(self, sbyconfig, workdir, early_logs, reusedir):
+class SbyConfig:
+    def __init__(self):
         self.options = dict()
-        self.used_options = set()
         self.engines = list()
         self.script = list()
         self.files = dict()
         self.verbatim_files = dict()
+        pass
+
+    def parse_config(self, f):
+        mode = None
+
+        for line in f:
+            raw_line = line
+            if mode in ["options", "engines", "files"]:
+                line = re.sub(r"\s*(\s#.*)?$", "", line)
+                if line == "" or line[0] == "#":
+                    continue
+            else:
+                line = line.rstrip()
+            # print(line)
+            if mode is None and (len(line) == 0 or line[0] == "#"):
+                continue
+            match = re.match(r"^\s*\[(.*)\]\s*$", line)
+            if match:
+                entries = match.group(1).split()
+                if len(entries) == 0:
+                    self.error(f"sby file syntax error: {line}")
+
+                if entries[0] == "options":
+                    mode = "options"
+                    if len(self.options) != 0 or len(entries) != 1:
+                        self.error(f"sby file syntax error: {line}")
+                    continue
+
+                if entries[0] == "engines":
+                    mode = "engines"
+                    if len(self.engines) != 0 or len(entries) != 1:
+                        self.error(f"sby file syntax error: {line}")
+                    continue
+
+                if entries[0] == "script":
+                    mode = "script"
+                    if len(self.script) != 0 or len(entries) != 1:
+                        self.error(f"sby file syntax error: {line}")
+                    continue
+
+                if entries[0] == "file":
+                    mode = "file"
+                    if len(entries) != 2:
+                        self.error(f"sby file syntax error: {line}")
+                    current_verbatim_file = entries[1]
+                    if current_verbatim_file in self.verbatim_files:
+                        self.error(f"duplicate file: {entries[1]}")
+                    self.verbatim_files[current_verbatim_file] = list()
+                    continue
+
+                if entries[0] == "files":
+                    mode = "files"
+                    if len(entries) != 1:
+                        self.error(f"sby file syntax error: {line}")
+                    continue
+
+                self.error(f"sby file syntax error: {line}")
+
+            if mode == "options":
+                entries = line.split()
+                if len(entries) != 2:
+                    self.error(f"sby file syntax error: {line}")
+                self.options[entries[0]] = entries[1]
+                continue
+
+            if mode == "engines":
+                entries = line.split()
+                self.engines.append(entries)
+                continue
+
+            if mode == "script":
+                self.script.append(line)
+                continue
+
+            if mode == "files":
+                entries = line.split()
+                if len(entries) == 1:
+                    self.files[os.path.basename(entries[0])] = entries[0]
+                elif len(entries) == 2:
+                    self.files[entries[0]] = entries[1]
+                else:
+                    self.error(f"sby file syntax error: {line}")
+                continue
+
+            if mode == "file":
+                self.verbatim_files[current_verbatim_file].append(raw_line)
+                continue
+
+            self.error(f"sby file syntax error: {line}")
+
+    def error(self, logmessage):
+        raise SbyAbort(logmessage)
+
+class SbyTask(SbyConfig):
+    def __init__(self, sbyconfig, workdir, early_logs, reusedir):
+        super().__init__()
+        self.used_options = set()
         self.models = dict()
         self.workdir = workdir
         self.reusedir = reusedir
@@ -550,94 +646,8 @@ class SbyTask:
             assert 0
 
     def run(self, setupmode):
-        mode = None
-        key = None
-
         with open(f"{self.workdir}/config.sby", "r") as f:
-            for line in f:
-                raw_line = line
-                if mode in ["options", "engines", "files"]:
-                    line = re.sub(r"\s*(\s#.*)?$", "", line)
-                    if line == "" or line[0] == "#":
-                        continue
-                else:
-                    line = line.rstrip()
-                # print(line)
-                if mode is None and (len(line) == 0 or line[0] == "#"):
-                    continue
-                match = re.match(r"^\s*\[(.*)\]\s*$", line)
-                if match:
-                    entries = match.group(1).split()
-                    if len(entries) == 0:
-                        self.error(f"sby file syntax error: {line}")
-
-                    if entries[0] == "options":
-                        mode = "options"
-                        if len(self.options) != 0 or len(entries) != 1:
-                            self.error(f"sby file syntax error: {line}")
-                        continue
-
-                    if entries[0] == "engines":
-                        mode = "engines"
-                        if len(self.engines) != 0 or len(entries) != 1:
-                            self.error(f"sby file syntax error: {line}")
-                        continue
-
-                    if entries[0] == "script":
-                        mode = "script"
-                        if len(self.script) != 0 or len(entries) != 1:
-                            self.error(f"sby file syntax error: {line}")
-                        continue
-
-                    if entries[0] == "file":
-                        mode = "file"
-                        if len(entries) != 2:
-                            self.error(f"sby file syntax error: {line}")
-                        current_verbatim_file = entries[1]
-                        if current_verbatim_file in self.verbatim_files:
-                            self.error(f"duplicate file: {entries[1]}")
-                        self.verbatim_files[current_verbatim_file] = list()
-                        continue
-
-                    if entries[0] == "files":
-                        mode = "files"
-                        if len(entries) != 1:
-                            self.error(f"sby file syntax error: {line}")
-                        continue
-
-                    self.error(f"sby file syntax error: {line}")
-
-                if mode == "options":
-                    entries = line.split()
-                    if len(entries) != 2:
-                        self.error(f"sby file syntax error: {line}")
-                    self.options[entries[0]] = entries[1]
-                    continue
-
-                if mode == "engines":
-                    entries = line.split()
-                    self.engines.append(entries)
-                    continue
-
-                if mode == "script":
-                    self.script.append(line)
-                    continue
-
-                if mode == "files":
-                    entries = line.split()
-                    if len(entries) == 1:
-                        self.files[os.path.basename(entries[0])] = entries[0]
-                    elif len(entries) == 2:
-                        self.files[entries[0]] = entries[1]
-                    else:
-                        self.error(f"sby file syntax error: {line}")
-                    continue
-
-                if mode == "file":
-                    self.verbatim_files[current_verbatim_file].append(raw_line)
-                    continue
-
-                self.error(f"sby file syntax error: {line}")
+            self.parse_config(f)
 
         self.handle_str_option("mode", None)
 

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__

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

tests/junit/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=junit
+include ../make/subdir.mk

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

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

tests/junit/junit_expect.sh

@@ -0,0 +1,4 @@
+#!/bin/bash
+set -e
+! python3 $SBY_MAIN -f $SBY_FILE $TASK
+grep '<failure type="EXPECT" message="Task returned status PASS. Expected values were: FAIL TIMEOUT" />' $WORKDIR/$WORKDIR.xml

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

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

tests/keepgoing/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=keepgoing
+include ../make/subdir.mk

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())

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

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

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

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

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

tests/keepgoing_multi_step.check.py

@@ -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())

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)

tests/make/help.txt

@@ -0,0 +1,20 @@
+make test:
+    run all tests (default)
+
+make clean:
+    remove all sby workdirs
+
+make test[_m_<mode>][_e_<engine>][_s_<solver>]:
+    run all tests that use a specific mode, engine and solver
+
+make <name>:
+    run the test for <name>.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

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)/$@

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)

tests/regression/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=regression
+include ../make/subdir.mk

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

tests/scripted/.gitignore

@@ -1 +0,0 @@
-/junit_*/

tests/scripted/Makefile

@@ -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

tests/scripted/junit_expect.sh

@@ -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 '<failure type="EXPECT" message="Task returned status PASS. Expected values were: FAIL TIMEOUT" />' junit_expect/junit_expect.xml

tests/unsorted/Makefile

@@ -0,0 +1,2 @@
+SUBDIR=unsorted
+include ../make/subdir.mk

tests/unsorted/prv32fmcmp.sby

@@ -17,5 +17,5 @@ read -sv prv32fmcmp.v
 prep -top prv32fmcmp
 
 [files]
-../extern/picorv32.v
+../../extern/picorv32.v
 prv32fmcmp.v