diff --git a/sbysrc/sby.py b/sbysrc/sby.py
index 5616bc0..d13960c 100644
--- a/sbysrc/sby.py
+++ b/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"
diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 3908f65..ab10614 100644
--- a/sbysrc/sby_core.py
+++ b/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)
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