From f9b08bc64b1a190ca523d2707696791c483da461 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 22 Jul 2026 13:58:59 +0100 Subject: [PATCH 1/5] add: version support for specs and check-specs conflict checker --- formal_lib/__init__.py | 5 ++ formal_lib/__main__.py | 4 +- formal_lib/specs/__init__.py | 38 ++++++--- formal_lib/specs/base.py | 10 +++ formal_lib/specs/conflicts.py | 75 +++++++++++++++++ formal_lib/version.py | 106 +++++++++++++++++++++++ pyproject.toml | 1 + tests/test_version.py | 153 ++++++++++++++++++++++++++++++++++ 8 files changed, 380 insertions(+), 12 deletions(-) create mode 100644 formal_lib/specs/conflicts.py create mode 100644 formal_lib/version.py create mode 100644 tests/test_version.py diff --git a/formal_lib/__init__.py b/formal_lib/__init__.py index 6fd5328..84c476a 100644 --- a/formal_lib/__init__.py +++ b/formal_lib/__init__.py @@ -8,11 +8,13 @@ from formal_lib.specs import ( SPECS, detect_spec, + resolve_spec, cbmc_spec, clang_spec, esbmc_spec, pytest_spec, ) +from formal_lib.version import Version, VersionRange __all__ = [ "__version__", @@ -22,7 +24,10 @@ "Issue", "VerifierIssue", "SPECS", + "Version", + "VersionRange", "detect_spec", + "resolve_spec", "cbmc_spec", "clang_spec", "esbmc_spec", diff --git a/formal_lib/__main__.py b/formal_lib/__main__.py index 9156dfd..9ab8afd 100644 --- a/formal_lib/__main__.py +++ b/formal_lib/__main__.py @@ -9,7 +9,7 @@ from formal_lib.issue import VerifierIssue from formal_lib.issue_parser import IssueSpecOutputParser from formal_lib.verifier_output import VerifierOutput -from formal_lib.specs import SPECS, detect_spec +from formal_lib.specs import SPECS, detect_spec, resolve_spec def pretty_print(result: VerifierOutput) -> None: @@ -90,7 +90,7 @@ def main() -> None: duration = 0.0 try: - spec = SPECS[args.backend] if args.backend else detect_spec(output) + spec = resolve_spec(args.backend, output) if args.backend else detect_spec(output) except ValueError as e: parser.error(str(e)) diff --git a/formal_lib/specs/__init__.py b/formal_lib/specs/__init__.py index bc67caa..3caf18e 100644 --- a/formal_lib/specs/__init__.py +++ b/formal_lib/specs/__init__.py @@ -19,28 +19,43 @@ from .esbmc import esbmc_spec from .kani import kani_spec from .pytest import pytest_spec +from formal_lib.version import Version, VersionRange -SPECS: dict[str, IssueRegexSpec] = { - "esbmc": esbmc_spec, +SPECS: dict[str, list[IssueRegexSpec]] = { + "esbmc": [esbmc_spec], # kani must precede cbmc: Kani's `--output-format old` output also carries a # `CBMC version` banner, so cbmc_spec.detect would otherwise claim it first. - "kani": kani_spec, - "cbmc": cbmc_spec, - "clang": clang_spec, - "pytest": pytest_spec, + "kani": [kani_spec], + "cbmc": [cbmc_spec], + "clang": [clang_spec], + "pytest": [pytest_spec], } -"""Specs that the frontend currently supports.""" +"""Specs that the frontend currently supports, grouped by backend name. A backend +holds one spec per supported version range (list newest versions first); ranges +within a backend must not overlap (checked by ``hatch run check-specs``).""" def detect_spec(output: str) -> IssueRegexSpec: """Auto-detect which spec matches the output using each spec's detect pattern.""" - for _, spec in SPECS.items(): - if spec.detect and re.search(spec.detect, output, re.MULTILINE): - return spec + for specs in SPECS.values(): + for spec in specs: + if spec.detect and re.search(spec.detect, output, re.MULTILINE): + return spec names = ", ".join(SPECS) raise ValueError(f"could not detect backend from output (known: {names})") +def resolve_spec(backend: str, output: str) -> IssueRegexSpec: + """Pick the spec for a backend name. With several versioned specs, the first + whose ``detect`` pattern matches the output wins; when none match, fall back + to the first registered (the newest) spec.""" + specs = SPECS[backend] + for spec in specs: + if spec.detect and re.search(spec.detect, output, re.MULTILINE): + return spec + return specs[0] + + __all__ = [ "AnnotatedPattern", "CachePropertiesFn", @@ -49,6 +64,8 @@ def detect_spec(output: str) -> IssueRegexSpec: "IssueRegexSpec", "SPECS", "StackTraceRegexSpec", + "Version", + "VersionRange", "cbmc_spec", "clang_spec", "detect_spec", @@ -57,4 +74,5 @@ def detect_spec(output: str) -> IssueRegexSpec: "kani_spec", "missing_hint", "pytest_spec", + "resolve_spec", ] diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index 739c010..9ee8afc 100644 --- a/formal_lib/specs/base.py +++ b/formal_lib/specs/base.py @@ -7,6 +7,8 @@ from dataclasses import dataclass, field from pathlib import Path +from formal_lib.version import Version, VersionRange + class AnnotatedPattern(str): """A regex pattern string annotated with a hint for when it fails to match.""" @@ -236,6 +238,14 @@ class IssueRegexSpec: detect: str = "" """Regex pattern to detect if output was produced by this verifier. Matched against the full output with MULTILINE. Empty means no auto-detection.""" + versions: list[Version | VersionRange] = field(default_factory=lambda: [VersionRange()]) + """Verifier versions this spec's patterns are written for: exact ``Version`` + entries and/or inclusive ``VersionRange`` entries (a ``None`` bound means + unbounded on that side). The default single unbounded range means "all + versions". When a verifier changes its output format, register a second spec + under the same backend name in ``SPECS`` and constrain both specs' versions — + within one backend no two specs may support the same version (checked by + ``hatch run check-specs``).""" counterexample_spec: CounterexampleRegexSpec | None = None """Optional nested specification for parsing counterexample traces.""" error_location: ErrorLocationRegexSpec | None = None diff --git a/formal_lib/specs/conflicts.py b/formal_lib/specs/conflicts.py new file mode 100644 index 0000000..a3fcbe5 --- /dev/null +++ b/formal_lib/specs/conflicts.py @@ -0,0 +1,75 @@ +# Author: Yiannis Charalambous + +"""Spec version-conflict checker, run via ``hatch run check-specs``. + +Within one backend, each version must be handled by at most one spec — two +specs whose supported versions overlap is a spec conflict, because backend +resolution could no longer tell which spec owns output from that version. + +``check-specs -v`` additionally lists every spec and the versions it supports. +""" + +import argparse +import sys +from itertools import combinations + +from formal_lib.specs import SPECS +from formal_lib.specs.base import IssueRegexSpec +from formal_lib.version import Version, VersionRange, as_range + + +def _describe(versions: list[Version | VersionRange]) -> str: + """Render a supported-versions list; the all-unbounded default reads "any version".""" + return ", ".join( + "any version" if v == VersionRange() else str(v) for v in versions + ) + + +def find_conflicts(specs: dict[str, list[IssueRegexSpec]] = SPECS) -> list[str]: + """Return one message per pair of same-backend specs with overlapping versions.""" + conflicts: list[str] = [] + for backend, backend_specs in specs.items(): + for (i, first), (j, second) in combinations(enumerate(backend_specs), 2): + if any( + as_range(a).overlaps(b) + for a in first.versions + for b in second.versions + ): + conflicts.append( + f"{backend}: spec #{i} [{_describe(first.versions)}] overlaps " + f"spec #{j} [{_describe(second.versions)}]" + ) + return conflicts + + +def main() -> None: + parser = argparse.ArgumentParser( + prog="check-specs", + description="Check that no two specs of one backend support the same " + "verifier version.", + ) + parser.add_argument( + "-v", + "--verbose", + action="store_true", + help="list every spec and the versions it supports", + ) + args = parser.parse_args() + + if args.verbose: + for backend, backend_specs in SPECS.items(): + print(f"{backend}:") + for i, spec in enumerate(backend_specs): + print(f" spec #{i}: {_describe(spec.versions)}") + + conflicts = find_conflicts() + for conflict in conflicts: + print(f"spec conflict: {conflict}", file=sys.stderr) + if conflicts: + sys.exit(1) + spec_count = sum(len(specs) for specs in SPECS.values()) + print(f"OK: no version overlap across {spec_count} specs in {len(SPECS)} backends") + + +if __name__ == "__main__": + main() diff --git a/formal_lib/version.py b/formal_lib/version.py new file mode 100644 index 0000000..89ca2ab --- /dev/null +++ b/formal_lib/version.py @@ -0,0 +1,106 @@ +# Author: Yiannis Charalambous + +"""Version datatypes for declaring which verifier versions a spec supports. + +A spec's ``versions`` list holds exact :class:`Version` entries and inclusive +:class:`VersionRange` entries. A range with ``lower=None`` extends back to the +earliest version, ``upper=None`` forward to the latest. + +Regression-sample category directories use the same grammar, matched by +``VERSION_RANGE_PATTERN``: ``v6.7.0-v6.10.0`` (bounded), ``v6.7.0-`` (no upper +bound), ``-v6.10.0`` (no lower bound), or ``v6.7.1`` (exact version). +""" + +import re +from dataclasses import dataclass + +_VERSION = r"v\d+(?:\.\d+)*" +VERSION_RANGE_PATTERN = re.compile(rf"{_VERSION}-(?:{_VERSION})?|-{_VERSION}|{_VERSION}") +"""Grammar for a version-range category name; use with ``fullmatch``. A bare +``-`` (unbounded on both sides) is deliberately rejected — an unconstrained +category is expressed by not using a version directory at all.""" + + +@dataclass(frozen=True, order=True) +class Version: + """A dotted numeric version, compared numerically part by part. + + Trailing zero parts are normalized away so ``6.7.0 == 6.7``. + """ + + parts: tuple[int, ...] + + def __post_init__(self) -> None: + if not self.parts: + raise ValueError("version needs at least one part") + parts = self.parts + while len(parts) > 1 and parts[-1] == 0: + parts = parts[:-1] + object.__setattr__(self, "parts", parts) + + @classmethod + def parse(cls, text: str) -> "Version": + """Parse ``6.7.1`` or ``v6.7.1`` into a Version.""" + body = text.removeprefix("v") + if not re.fullmatch(r"\d+(?:\.\d+)*", body): + raise ValueError(f"invalid version: {text!r}") + return cls(tuple(int(part) for part in body.split("."))) + + def __str__(self) -> str: + return ".".join(str(part) for part in self.parts) + + +@dataclass(frozen=True) +class VersionRange: + """An inclusive version range; a ``None`` bound means unbounded on that side. + + The default ``VersionRange()`` is unbounded on both sides — "all versions". + """ + + lower: Version | None = None + upper: Version | None = None + + def __post_init__(self) -> None: + if self.lower is not None and self.upper is not None and self.lower > self.upper: + raise ValueError(f"range lower bound {self.lower} exceeds upper bound {self.upper}") + + @classmethod + def parse(cls, text: str) -> "VersionRange": + """Parse a category name matching ``VERSION_RANGE_PATTERN``. + + ``v6.7.0-v6.10.0`` | ``v6.7.0-`` | ``-v6.10.0`` | ``v6.7.1`` (exact). + """ + if not VERSION_RANGE_PATTERN.fullmatch(text): + raise ValueError(f"invalid version range: {text!r}") + if "-" not in text: + exact = Version.parse(text) + return cls(exact, exact) + lower_text, upper_text = text.split("-", 1) + return cls( + Version.parse(lower_text) if lower_text else None, + Version.parse(upper_text) if upper_text else None, + ) + + def __contains__(self, version: Version) -> bool: + return (self.lower is None or self.lower <= version) and ( + self.upper is None or version <= self.upper + ) + + def overlaps(self, other: "Version | VersionRange") -> bool: + """Whether at least one version falls in both ranges (bounds inclusive).""" + other = as_range(other) + return (self.lower is None or other.upper is None or self.lower <= other.upper) and ( + other.lower is None or self.upper is None or other.lower <= self.upper + ) + + def __str__(self) -> str: + if self.lower is not None and self.lower == self.upper: + return f"v{self.lower}" + lower = f"v{self.lower}" if self.lower is not None else "" + upper = f"v{self.upper}" if self.upper is not None else "" + return f"{lower}-{upper}" + + +def as_range(value: Version | VersionRange) -> VersionRange: + """Normalize a supported-versions entry: an exact Version becomes ``[v, v]``.""" + return value if isinstance(value, VersionRange) else VersionRange(value, value) diff --git a/pyproject.toml b/pyproject.toml index d18dfe1..b29d081 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -36,6 +36,7 @@ urls.Source = "https://github.com/ByteRepair/formal-lib" scripts.pf = "formal_lib.__main__:main" [tool.hatch] +envs.default.scripts.check-specs = "python -m formal_lib.specs.conflicts {args}" envs.types.extra-dependencies = [ "mypy>=1.0.0", "pytest", diff --git a/tests/test_version.py b/tests/test_version.py new file mode 100644 index 0000000..6314013 --- /dev/null +++ b/tests/test_version.py @@ -0,0 +1,153 @@ +# Author: Yiannis Charalambous + +"""Tests for the Version/VersionRange datatypes and the spec conflict checker.""" + +import pytest + +from formal_lib.specs import SPECS +from formal_lib.specs.base import IssueRegexSpec, StackTraceRegexSpec +from formal_lib.specs.conflicts import find_conflicts +from formal_lib.version import VERSION_RANGE_PATTERN, Version, VersionRange, as_range + + +# --- Version --- + +def test_version_parse() -> None: + assert Version.parse("6.7.1") == Version((6, 7, 1)) + assert Version.parse("v6.7.1") == Version((6, 7, 1)) + assert Version.parse("8") == Version((8,)) + + +def test_version_parse_rejects_garbage() -> None: + for text in ("", "v", "6.", "6.x", "6-7"): + with pytest.raises(ValueError): + Version.parse(text) + + +def test_version_ordering_is_numeric() -> None: + assert Version.parse("6.10") > Version.parse("6.7") + assert Version.parse("6.7") < Version.parse("6.7.1") + + +def test_version_normalizes_trailing_zeros() -> None: + assert Version.parse("6.7.0") == Version.parse("6.7") + assert str(Version.parse("1.0.0")) == "1" + + +# --- VersionRange --- + +def test_range_parse_bounded() -> None: + r = VersionRange.parse("v6.7.0-v6.10.0") + assert r.lower == Version.parse("6.7") + assert r.upper == Version.parse("6.10") + + +def test_range_parse_unbounded_sides() -> None: + assert VersionRange.parse("v6.7.0-").upper is None + assert VersionRange.parse("-v6.10.0").lower is None + + +def test_range_parse_exact_version() -> None: + r = VersionRange.parse("v6.7.1") + assert r.lower == r.upper == Version.parse("6.7.1") + + +def test_range_parse_rejects_non_ranges() -> None: + # Plain category names must never parse as version ranges. + for text in ("contracts", "esbmc-cpp", "linux", "-", "v6.7-x"): + assert not VERSION_RANGE_PATTERN.fullmatch(text) + with pytest.raises(ValueError): + VersionRange.parse(text) + + +def test_range_rejects_inverted_bounds() -> None: + with pytest.raises(ValueError): + VersionRange(Version.parse("2"), Version.parse("1")) + + +def test_range_contains_inclusive_bounds() -> None: + r = VersionRange.parse("v6.7.0-v6.10.0") + assert Version.parse("6.7.0") in r + assert Version.parse("6.10.0") in r + assert Version.parse("6.8.2") in r + assert Version.parse("6.6.9") not in r + assert Version.parse("6.10.1") not in r + + +def test_unbounded_range_contains_everything() -> None: + assert Version.parse("0.0.1") in VersionRange() + assert Version.parse("999") in VersionRange() + + +def test_overlaps() -> None: + assert VersionRange.parse("v1-v3").overlaps(VersionRange.parse("v3-v5")) # touching, inclusive + assert not VersionRange.parse("v1-v3").overlaps(VersionRange.parse("v3.0.1-v5")) + assert VersionRange.parse("v4-").overlaps(VersionRange()) # unbounded overlaps all + assert VersionRange.parse("-v3").overlaps(Version.parse("2.5")) + assert not VersionRange.parse("-v3").overlaps(Version.parse("3.1")) + + +def test_as_range() -> None: + assert as_range(Version.parse("2")) == VersionRange.parse("v2") + r = VersionRange.parse("v1-v2") + assert as_range(r) is r + + +# --- spec conflict checker --- + +_NO_TRACE = StackTraceRegexSpec( + block=r"ZZZ_NOMATCH", trace_entry=r"ZZZ", trace_index=r"ZZZ", + path=r"ZZZ", name=r"ZZZ", line_index=r"ZZZ", +) + + +def _spec(*versions: Version | VersionRange) -> IssueRegexSpec: + spec = IssueRegexSpec( + block=r"ZZZ", + error_type=r"ZZZ", + message=r"ZZZ", + severity=r"ZZZ", + stack_trace_spec=_NO_TRACE, + ) + if versions: # no args -> keep the default all-versions range + spec.versions = list(versions) + return spec + + +def test_disjoint_specs_do_not_conflict() -> None: + specs = { + "tool": [ + _spec(VersionRange.parse("v8-")), + _spec(VersionRange.parse("-v7.99")), + ] + } + assert find_conflicts(specs) == [] + + +def test_overlapping_specs_conflict() -> None: + specs = { + "tool": [ + _spec(VersionRange.parse("v7-")), + _spec(VersionRange.parse("-v7.5")), + ] + } + conflicts = find_conflicts(specs) + assert len(conflicts) == 1 + assert "tool" in conflicts[0] + + +def test_default_all_versions_specs_conflict() -> None: + # Two specs left on the default unbounded range must be flagged. + assert len(find_conflicts({"tool": [_spec(), _spec()]})) == 1 + + +def test_same_versions_in_different_backends_do_not_conflict() -> None: + specs = { + "tool_a": [_spec(VersionRange.parse("v1-v2"))], + "tool_b": [_spec(VersionRange.parse("v1-v2"))], + } + assert find_conflicts(specs) == [] + + +def test_registered_specs_have_no_conflicts() -> None: + assert find_conflicts(SPECS) == [] From 057c44f01c985fcb2a3cb57b5793ca9fa7d936c4 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 22 Jul 2026 13:58:59 +0100 Subject: [PATCH 2/5] test: move regression samples into version-range categories --- .../{ => v6.7.1}/esbmc/00_bitshift_01.json | 0 .../{ => v6.7.1}/esbmc/00_bitshift_01.log | 0 .../cbmc/{ => v6.7.1}/esbmc/fam_false_0.json | 0 .../cbmc/{ => v6.7.1}/esbmc/fam_false_0.log | 0 .../{ => v6.7.1}/esbmc/github_1175_10.json | 0 .../{ => v6.7.1}/esbmc/github_1175_10.log | 0 .../{ => v6.7.1}/esbmc/github_1890_1.json | 0 .../cbmc/{ => v6.7.1}/esbmc/github_1890_1.log | 0 .../esbmc/overflow_01_addition.json | 0 .../esbmc/overflow_01_addition.log | 0 .../unordered_map/basic_insert2_fail.json | 0 .../unordered_map/basic_insert2_fail.log | 0 .../linux/kernel_from_user_copy_invalid.json | 0 .../linux/kernel_from_user_copy_invalid.log | 0 .../copy_mem_same_object_no_stacktrace.json | 0 .../copy_mem_same_object_no_stacktrace.log | 0 .../strlen_enforce_array_bounds.json | 0 .../contracts/strlen_enforce_array_bounds.log | 0 .../kani/{ => v0.67.0}/arith_overflow.json | 0 .../kani/{ => v0.67.0}/arith_overflow.log | 0 .../kani/{ => v0.67.0}/array_success.json | 0 .../kani/{ => v0.67.0}/array_success.log | 0 .../samples/kani/{ => v0.67.0}/assert_eq.json | 0 .../samples/kani/{ => v0.67.0}/assert_eq.log | 0 .../kani/{ => v0.67.0}/assert_success.json | 0 .../kani/{ => v0.67.0}/assert_success.log | 0 .../kani/{ => v0.67.0}/cast_success.json | 0 .../kani/{ => v0.67.0}/cast_success.log | 0 .../kani/{ => v0.67.0}/division_by_zero.json | 0 .../kani/{ => v0.67.0}/division_by_zero.log | 0 .../samples/kani/{ => v0.67.0}/float_nan.json | 0 .../samples/kani/{ => v0.67.0}/float_nan.log | 0 .../kani/{ => v0.67.0}/multiple_asserts.json | 0 .../kani/{ => v0.67.0}/multiple_asserts.log | 0 .../{ => v0.67.0}/native_format_no_trace.json | 0 .../{ => v0.67.0}/native_format_no_trace.log | 0 .../pointer_offset_overflow.json | 0 .../{ => v0.67.0}/pointer_offset_overflow.log | 0 .../kani/{ => v0.67.0}/slice_from_raw.json | 0 .../kani/{ => v0.67.0}/slice_from_raw.log | 0 .../{ => v0.67.0}/slice_out_of_bounds.json | 0 .../{ => v0.67.0}/slice_out_of_bounds.log | 0 .../kani/{ => v0.67.0}/unreachable.json | 0 .../kani/{ => v0.67.0}/unreachable.log | 0 .../samples/pytest/{ => v8.4.2}/multiple.json | 0 .../samples/pytest/{ => v8.4.2}/multiple.log | 0 .../multiple_collection_error.json | 0 .../multiple_collection_error.log | 0 .../pytest/{ => v8.4.2}/successful.json | 0 .../pytest/{ => v8.4.2}/successful.log | 0 tests/regressions/test_sample_regression.py | 94 ++++++++++++++----- 51 files changed, 68 insertions(+), 26 deletions(-) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/00_bitshift_01.json (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/00_bitshift_01.log (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/fam_false_0.json (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/fam_false_0.log (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/github_1175_10.json (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/github_1175_10.log (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/github_1890_1.json (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/github_1890_1.log (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/overflow_01_addition.json (100%) rename tests/regressions/samples/cbmc/{ => v6.7.1}/esbmc/overflow_01_addition.log (100%) rename tests/regressions/samples/esbmc/{ => v8.1.0}/esbmc-cpp/unordered_map/basic_insert2_fail.json (100%) rename tests/regressions/samples/esbmc/{ => v8.1.0}/esbmc-cpp/unordered_map/basic_insert2_fail.log (100%) rename tests/regressions/samples/esbmc/{ => v8.1.0}/linux/kernel_from_user_copy_invalid.json (100%) rename tests/regressions/samples/esbmc/{ => v8.1.0}/linux/kernel_from_user_copy_invalid.log (100%) rename tests/regressions/samples/esbmc/{ => v8.2.0}/contracts/copy_mem_same_object_no_stacktrace.json (100%) rename tests/regressions/samples/esbmc/{ => v8.2.0}/contracts/copy_mem_same_object_no_stacktrace.log (100%) rename tests/regressions/samples/esbmc/{ => v8.2.0}/contracts/strlen_enforce_array_bounds.json (100%) rename tests/regressions/samples/esbmc/{ => v8.2.0}/contracts/strlen_enforce_array_bounds.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/arith_overflow.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/arith_overflow.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/array_success.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/array_success.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/assert_eq.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/assert_eq.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/assert_success.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/assert_success.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/cast_success.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/cast_success.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/division_by_zero.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/division_by_zero.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/float_nan.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/float_nan.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/multiple_asserts.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/multiple_asserts.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/native_format_no_trace.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/native_format_no_trace.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/pointer_offset_overflow.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/pointer_offset_overflow.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/slice_from_raw.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/slice_from_raw.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/slice_out_of_bounds.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/slice_out_of_bounds.log (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/unreachable.json (100%) rename tests/regressions/samples/kani/{ => v0.67.0}/unreachable.log (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/multiple.json (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/multiple.log (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/multiple_collection_error.json (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/multiple_collection_error.log (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/successful.json (100%) rename tests/regressions/samples/pytest/{ => v8.4.2}/successful.log (100%) diff --git a/tests/regressions/samples/cbmc/esbmc/00_bitshift_01.json b/tests/regressions/samples/cbmc/v6.7.1/esbmc/00_bitshift_01.json similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/00_bitshift_01.json rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/00_bitshift_01.json diff --git a/tests/regressions/samples/cbmc/esbmc/00_bitshift_01.log b/tests/regressions/samples/cbmc/v6.7.1/esbmc/00_bitshift_01.log similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/00_bitshift_01.log rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/00_bitshift_01.log diff --git a/tests/regressions/samples/cbmc/esbmc/fam_false_0.json b/tests/regressions/samples/cbmc/v6.7.1/esbmc/fam_false_0.json similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/fam_false_0.json rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/fam_false_0.json diff --git a/tests/regressions/samples/cbmc/esbmc/fam_false_0.log b/tests/regressions/samples/cbmc/v6.7.1/esbmc/fam_false_0.log similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/fam_false_0.log rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/fam_false_0.log diff --git a/tests/regressions/samples/cbmc/esbmc/github_1175_10.json b/tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1175_10.json similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/github_1175_10.json rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1175_10.json diff --git a/tests/regressions/samples/cbmc/esbmc/github_1175_10.log b/tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1175_10.log similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/github_1175_10.log rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1175_10.log diff --git a/tests/regressions/samples/cbmc/esbmc/github_1890_1.json b/tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1890_1.json similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/github_1890_1.json rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1890_1.json diff --git a/tests/regressions/samples/cbmc/esbmc/github_1890_1.log b/tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1890_1.log similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/github_1890_1.log rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/github_1890_1.log diff --git a/tests/regressions/samples/cbmc/esbmc/overflow_01_addition.json b/tests/regressions/samples/cbmc/v6.7.1/esbmc/overflow_01_addition.json similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/overflow_01_addition.json rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/overflow_01_addition.json diff --git a/tests/regressions/samples/cbmc/esbmc/overflow_01_addition.log b/tests/regressions/samples/cbmc/v6.7.1/esbmc/overflow_01_addition.log similarity index 100% rename from tests/regressions/samples/cbmc/esbmc/overflow_01_addition.log rename to tests/regressions/samples/cbmc/v6.7.1/esbmc/overflow_01_addition.log diff --git a/tests/regressions/samples/esbmc/esbmc-cpp/unordered_map/basic_insert2_fail.json b/tests/regressions/samples/esbmc/v8.1.0/esbmc-cpp/unordered_map/basic_insert2_fail.json similarity index 100% rename from tests/regressions/samples/esbmc/esbmc-cpp/unordered_map/basic_insert2_fail.json rename to tests/regressions/samples/esbmc/v8.1.0/esbmc-cpp/unordered_map/basic_insert2_fail.json diff --git a/tests/regressions/samples/esbmc/esbmc-cpp/unordered_map/basic_insert2_fail.log b/tests/regressions/samples/esbmc/v8.1.0/esbmc-cpp/unordered_map/basic_insert2_fail.log similarity index 100% rename from tests/regressions/samples/esbmc/esbmc-cpp/unordered_map/basic_insert2_fail.log rename to tests/regressions/samples/esbmc/v8.1.0/esbmc-cpp/unordered_map/basic_insert2_fail.log diff --git a/tests/regressions/samples/esbmc/linux/kernel_from_user_copy_invalid.json b/tests/regressions/samples/esbmc/v8.1.0/linux/kernel_from_user_copy_invalid.json similarity index 100% rename from tests/regressions/samples/esbmc/linux/kernel_from_user_copy_invalid.json rename to tests/regressions/samples/esbmc/v8.1.0/linux/kernel_from_user_copy_invalid.json diff --git a/tests/regressions/samples/esbmc/linux/kernel_from_user_copy_invalid.log b/tests/regressions/samples/esbmc/v8.1.0/linux/kernel_from_user_copy_invalid.log similarity index 100% rename from tests/regressions/samples/esbmc/linux/kernel_from_user_copy_invalid.log rename to tests/regressions/samples/esbmc/v8.1.0/linux/kernel_from_user_copy_invalid.log diff --git a/tests/regressions/samples/esbmc/contracts/copy_mem_same_object_no_stacktrace.json b/tests/regressions/samples/esbmc/v8.2.0/contracts/copy_mem_same_object_no_stacktrace.json similarity index 100% rename from tests/regressions/samples/esbmc/contracts/copy_mem_same_object_no_stacktrace.json rename to tests/regressions/samples/esbmc/v8.2.0/contracts/copy_mem_same_object_no_stacktrace.json diff --git a/tests/regressions/samples/esbmc/contracts/copy_mem_same_object_no_stacktrace.log b/tests/regressions/samples/esbmc/v8.2.0/contracts/copy_mem_same_object_no_stacktrace.log similarity index 100% rename from tests/regressions/samples/esbmc/contracts/copy_mem_same_object_no_stacktrace.log rename to tests/regressions/samples/esbmc/v8.2.0/contracts/copy_mem_same_object_no_stacktrace.log diff --git a/tests/regressions/samples/esbmc/contracts/strlen_enforce_array_bounds.json b/tests/regressions/samples/esbmc/v8.2.0/contracts/strlen_enforce_array_bounds.json similarity index 100% rename from tests/regressions/samples/esbmc/contracts/strlen_enforce_array_bounds.json rename to tests/regressions/samples/esbmc/v8.2.0/contracts/strlen_enforce_array_bounds.json diff --git a/tests/regressions/samples/esbmc/contracts/strlen_enforce_array_bounds.log b/tests/regressions/samples/esbmc/v8.2.0/contracts/strlen_enforce_array_bounds.log similarity index 100% rename from tests/regressions/samples/esbmc/contracts/strlen_enforce_array_bounds.log rename to tests/regressions/samples/esbmc/v8.2.0/contracts/strlen_enforce_array_bounds.log diff --git a/tests/regressions/samples/kani/arith_overflow.json b/tests/regressions/samples/kani/v0.67.0/arith_overflow.json similarity index 100% rename from tests/regressions/samples/kani/arith_overflow.json rename to tests/regressions/samples/kani/v0.67.0/arith_overflow.json diff --git a/tests/regressions/samples/kani/arith_overflow.log b/tests/regressions/samples/kani/v0.67.0/arith_overflow.log similarity index 100% rename from tests/regressions/samples/kani/arith_overflow.log rename to tests/regressions/samples/kani/v0.67.0/arith_overflow.log diff --git a/tests/regressions/samples/kani/array_success.json b/tests/regressions/samples/kani/v0.67.0/array_success.json similarity index 100% rename from tests/regressions/samples/kani/array_success.json rename to tests/regressions/samples/kani/v0.67.0/array_success.json diff --git a/tests/regressions/samples/kani/array_success.log b/tests/regressions/samples/kani/v0.67.0/array_success.log similarity index 100% rename from tests/regressions/samples/kani/array_success.log rename to tests/regressions/samples/kani/v0.67.0/array_success.log diff --git a/tests/regressions/samples/kani/assert_eq.json b/tests/regressions/samples/kani/v0.67.0/assert_eq.json similarity index 100% rename from tests/regressions/samples/kani/assert_eq.json rename to tests/regressions/samples/kani/v0.67.0/assert_eq.json diff --git a/tests/regressions/samples/kani/assert_eq.log b/tests/regressions/samples/kani/v0.67.0/assert_eq.log similarity index 100% rename from tests/regressions/samples/kani/assert_eq.log rename to tests/regressions/samples/kani/v0.67.0/assert_eq.log diff --git a/tests/regressions/samples/kani/assert_success.json b/tests/regressions/samples/kani/v0.67.0/assert_success.json similarity index 100% rename from tests/regressions/samples/kani/assert_success.json rename to tests/regressions/samples/kani/v0.67.0/assert_success.json diff --git a/tests/regressions/samples/kani/assert_success.log b/tests/regressions/samples/kani/v0.67.0/assert_success.log similarity index 100% rename from tests/regressions/samples/kani/assert_success.log rename to tests/regressions/samples/kani/v0.67.0/assert_success.log diff --git a/tests/regressions/samples/kani/cast_success.json b/tests/regressions/samples/kani/v0.67.0/cast_success.json similarity index 100% rename from tests/regressions/samples/kani/cast_success.json rename to tests/regressions/samples/kani/v0.67.0/cast_success.json diff --git a/tests/regressions/samples/kani/cast_success.log b/tests/regressions/samples/kani/v0.67.0/cast_success.log similarity index 100% rename from tests/regressions/samples/kani/cast_success.log rename to tests/regressions/samples/kani/v0.67.0/cast_success.log diff --git a/tests/regressions/samples/kani/division_by_zero.json b/tests/regressions/samples/kani/v0.67.0/division_by_zero.json similarity index 100% rename from tests/regressions/samples/kani/division_by_zero.json rename to tests/regressions/samples/kani/v0.67.0/division_by_zero.json diff --git a/tests/regressions/samples/kani/division_by_zero.log b/tests/regressions/samples/kani/v0.67.0/division_by_zero.log similarity index 100% rename from tests/regressions/samples/kani/division_by_zero.log rename to tests/regressions/samples/kani/v0.67.0/division_by_zero.log diff --git a/tests/regressions/samples/kani/float_nan.json b/tests/regressions/samples/kani/v0.67.0/float_nan.json similarity index 100% rename from tests/regressions/samples/kani/float_nan.json rename to tests/regressions/samples/kani/v0.67.0/float_nan.json diff --git a/tests/regressions/samples/kani/float_nan.log b/tests/regressions/samples/kani/v0.67.0/float_nan.log similarity index 100% rename from tests/regressions/samples/kani/float_nan.log rename to tests/regressions/samples/kani/v0.67.0/float_nan.log diff --git a/tests/regressions/samples/kani/multiple_asserts.json b/tests/regressions/samples/kani/v0.67.0/multiple_asserts.json similarity index 100% rename from tests/regressions/samples/kani/multiple_asserts.json rename to tests/regressions/samples/kani/v0.67.0/multiple_asserts.json diff --git a/tests/regressions/samples/kani/multiple_asserts.log b/tests/regressions/samples/kani/v0.67.0/multiple_asserts.log similarity index 100% rename from tests/regressions/samples/kani/multiple_asserts.log rename to tests/regressions/samples/kani/v0.67.0/multiple_asserts.log diff --git a/tests/regressions/samples/kani/native_format_no_trace.json b/tests/regressions/samples/kani/v0.67.0/native_format_no_trace.json similarity index 100% rename from tests/regressions/samples/kani/native_format_no_trace.json rename to tests/regressions/samples/kani/v0.67.0/native_format_no_trace.json diff --git a/tests/regressions/samples/kani/native_format_no_trace.log b/tests/regressions/samples/kani/v0.67.0/native_format_no_trace.log similarity index 100% rename from tests/regressions/samples/kani/native_format_no_trace.log rename to tests/regressions/samples/kani/v0.67.0/native_format_no_trace.log diff --git a/tests/regressions/samples/kani/pointer_offset_overflow.json b/tests/regressions/samples/kani/v0.67.0/pointer_offset_overflow.json similarity index 100% rename from tests/regressions/samples/kani/pointer_offset_overflow.json rename to tests/regressions/samples/kani/v0.67.0/pointer_offset_overflow.json diff --git a/tests/regressions/samples/kani/pointer_offset_overflow.log b/tests/regressions/samples/kani/v0.67.0/pointer_offset_overflow.log similarity index 100% rename from tests/regressions/samples/kani/pointer_offset_overflow.log rename to tests/regressions/samples/kani/v0.67.0/pointer_offset_overflow.log diff --git a/tests/regressions/samples/kani/slice_from_raw.json b/tests/regressions/samples/kani/v0.67.0/slice_from_raw.json similarity index 100% rename from tests/regressions/samples/kani/slice_from_raw.json rename to tests/regressions/samples/kani/v0.67.0/slice_from_raw.json diff --git a/tests/regressions/samples/kani/slice_from_raw.log b/tests/regressions/samples/kani/v0.67.0/slice_from_raw.log similarity index 100% rename from tests/regressions/samples/kani/slice_from_raw.log rename to tests/regressions/samples/kani/v0.67.0/slice_from_raw.log diff --git a/tests/regressions/samples/kani/slice_out_of_bounds.json b/tests/regressions/samples/kani/v0.67.0/slice_out_of_bounds.json similarity index 100% rename from tests/regressions/samples/kani/slice_out_of_bounds.json rename to tests/regressions/samples/kani/v0.67.0/slice_out_of_bounds.json diff --git a/tests/regressions/samples/kani/slice_out_of_bounds.log b/tests/regressions/samples/kani/v0.67.0/slice_out_of_bounds.log similarity index 100% rename from tests/regressions/samples/kani/slice_out_of_bounds.log rename to tests/regressions/samples/kani/v0.67.0/slice_out_of_bounds.log diff --git a/tests/regressions/samples/kani/unreachable.json b/tests/regressions/samples/kani/v0.67.0/unreachable.json similarity index 100% rename from tests/regressions/samples/kani/unreachable.json rename to tests/regressions/samples/kani/v0.67.0/unreachable.json diff --git a/tests/regressions/samples/kani/unreachable.log b/tests/regressions/samples/kani/v0.67.0/unreachable.log similarity index 100% rename from tests/regressions/samples/kani/unreachable.log rename to tests/regressions/samples/kani/v0.67.0/unreachable.log diff --git a/tests/regressions/samples/pytest/multiple.json b/tests/regressions/samples/pytest/v8.4.2/multiple.json similarity index 100% rename from tests/regressions/samples/pytest/multiple.json rename to tests/regressions/samples/pytest/v8.4.2/multiple.json diff --git a/tests/regressions/samples/pytest/multiple.log b/tests/regressions/samples/pytest/v8.4.2/multiple.log similarity index 100% rename from tests/regressions/samples/pytest/multiple.log rename to tests/regressions/samples/pytest/v8.4.2/multiple.log diff --git a/tests/regressions/samples/pytest/multiple_collection_error.json b/tests/regressions/samples/pytest/v8.4.2/multiple_collection_error.json similarity index 100% rename from tests/regressions/samples/pytest/multiple_collection_error.json rename to tests/regressions/samples/pytest/v8.4.2/multiple_collection_error.json diff --git a/tests/regressions/samples/pytest/multiple_collection_error.log b/tests/regressions/samples/pytest/v8.4.2/multiple_collection_error.log similarity index 100% rename from tests/regressions/samples/pytest/multiple_collection_error.log rename to tests/regressions/samples/pytest/v8.4.2/multiple_collection_error.log diff --git a/tests/regressions/samples/pytest/successful.json b/tests/regressions/samples/pytest/v8.4.2/successful.json similarity index 100% rename from tests/regressions/samples/pytest/successful.json rename to tests/regressions/samples/pytest/v8.4.2/successful.json diff --git a/tests/regressions/samples/pytest/successful.log b/tests/regressions/samples/pytest/v8.4.2/successful.log similarity index 100% rename from tests/regressions/samples/pytest/successful.log rename to tests/regressions/samples/pytest/v8.4.2/successful.log diff --git a/tests/regressions/test_sample_regression.py b/tests/regressions/test_sample_regression.py index ad23ff6..9505dad 100644 --- a/tests/regressions/test_sample_regression.py +++ b/tests/regressions/test_sample_regression.py @@ -2,56 +2,98 @@ """Data-driven regression tests for verifier spec parsing. -Drop a .log and .json pair into tests/regressions/samples// and the test -runner will automatically pick it up. The .json file should contain the expected -JSON output from `formal-lib -- --format json-compact`, minus the `output` -field (which is just the raw log content). +Drop a .log and .json pair into tests/regressions/samples// and the +test runner will automatically pick it up. The .json file should contain the +expected JSON output from `pf --backend --format json-compact`, minus +the `output` field (which is just the raw log content). + +A directory component whose name matches the version-range grammar +(``v6.7.0-v6.10.0``, ``v6.7.0-``, ``-v6.10.0``, or exact ``v6.7.1``) constrains +the samples beneath it: they only run against the backend's specs whose +supported versions overlap that range. Samples outside a version directory run +against every spec of their backend. """ import json -import subprocess from pathlib import Path import pytest +from formal_lib.issue_parser import IssueSpecOutputParser +from formal_lib.specs import SPECS +from formal_lib.specs.base import IssueRegexSpec +from formal_lib.version import VERSION_RANGE_PATTERN, VersionRange, as_range + SAMPLES_DIR = Path(__file__).parent / "samples" -KNOWN_SPECS = {"esbmc", "clang", "pytest", "cbmc", "kani"} -def discover_samples() -> list[tuple[str, Path, Path]]: - """Discover all .log/.json pairs under samples//.""" - pairs = [] - for spec_dir in sorted(SAMPLES_DIR.iterdir()): - if not spec_dir.is_dir() or spec_dir.name not in KNOWN_SPECS: +ORPHANED: list[str] = [] +"""Version-constrained samples whose range overlaps no spec of their backend — +silently dropping them would shrink the suite, so a test asserts this is empty.""" + + +def discover_samples() -> list[tuple[str, IssueRegexSpec, Path, Path]]: + """Discover .log/.json pairs and pair each with the specs it applies to.""" + cases = [] + for backend_dir in sorted(SAMPLES_DIR.iterdir()): + specs = SPECS.get(backend_dir.name) + if not backend_dir.is_dir() or not specs: continue - spec = spec_dir.name - for log_file in sorted(spec_dir.glob("**/*.log")): + for log_file in sorted(backend_dir.glob("**/*.log")): json_file = log_file.with_suffix(".json") - if json_file.exists(): - pairs.append((spec, log_file, json_file)) - return pairs + if not json_file.exists(): + continue + relative = log_file.relative_to(backend_dir) + constraint = next( + ( + VersionRange.parse(part) + for part in relative.parts[:-1] + if VERSION_RANGE_PATTERN.fullmatch(part) + ), + None, + ) + matched = [ + spec + for spec in specs + if constraint is None + or any(as_range(v).overlaps(constraint) for v in spec.versions) + ] + if not matched: + ORPHANED.append(f"{backend_dir.name}/{relative}") + continue + for spec in matched: + sample_id = f"{backend_dir.name}/{relative.with_suffix('')}" + if len(matched) > 1: + versions = ",".join(str(v) for v in spec.versions) + sample_id += f"@{versions}" + cases.append((sample_id, spec, log_file, json_file)) + return cases SAMPLES = discover_samples() -SAMPLE_IDS = [f"{spec}/{log.stem}" for spec, log, _ in SAMPLES] @pytest.mark.regression -@pytest.mark.parametrize("spec, log_file, json_file", SAMPLES, ids=SAMPLE_IDS) +def test_no_orphaned_samples() -> None: + """Every version-constrained sample overlaps at least one spec's versions.""" + assert not ORPHANED + + +@pytest.mark.regression +@pytest.mark.parametrize( + "spec, log_file, json_file", + [case[1:] for case in SAMPLES], + ids=[case[0] for case in SAMPLES], +) def test_sample_output_matches_expected( - spec: str, log_file: Path, json_file: Path + spec: IssueRegexSpec, log_file: Path, json_file: Path ) -> None: log_content = log_file.read_text() expected = json.loads(json_file.read_text()) - result = subprocess.run( - ["python", "-m", "formal_lib", "--backend", spec, "--format", "json-compact"], - input=log_content, - capture_output=True, - text=True, - ) + result = IssueSpecOutputParser(spec).parse_output(log_content) - actual = json.loads(result.stdout) + actual = result.model_dump(mode="json") actual.pop("output", None) assert actual == expected From 67d6d6d06ce70cbbcc5adb134b54aac8d470fd73 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 22 Jul 2026 13:58:59 +0100 Subject: [PATCH 3/5] ci: check spec conflicts in test workflow --- .github/workflows/test.yml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 910e61d..15ff2ef 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -26,3 +26,11 @@ jobs: - uses: ./.github/actions/setup-hatch - name: Run regression tests run: hatch test -- tests/regressions/ -m regression -o "addopts=" + + spec-conflicts: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v7.0.0 + - uses: ./.github/actions/setup-hatch + - name: Check spec version conflicts + run: hatch run check-specs -v From d1e943755e7ebc990b55d88ac2ce5be7773471a0 Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 22 Jul 2026 13:58:59 +0100 Subject: [PATCH 4/5] docs: document spec versioning in CLAUDE.md and README --- CLAUDE.md | 15 ++++++++++++--- README.md | 14 ++++++++++++++ 2 files changed, 26 insertions(+), 3 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 7c04f6d..c6d1cc7 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -24,15 +24,21 @@ hatch test -- tests/regressions/ -m regression -o "addopts=" # Type checking hatch run types:check +# Check that no two specs of one backend support the same verifier version +# (-v also lists every spec and the versions it supports) +hatch run check-specs + # Build hatch build ``` +Hatch scripts only forward extra CLI arguments when their definition in `pyproject.toml` contains an explicit `{args}` placeholder (e.g. `check-specs = "python -m formal_lib.specs.conflicts {args}"`) — without it, hatch silently swallows flags like `-v`. + ## Architecture The library uses a **specification-driven regex parsing** pattern with three layers: -1. **Specs** (`formal_lib/specs/`) — Each verifier backend defines an `IssueRegexSpec` containing regex patterns for extracting issue blocks, error types, messages, severity, and nested `StackTraceRegexSpec`/`CounterexampleRegexSpec` for traces. The verification outcome is a data-driven baseline — a run passes when it has no error-severity issue — that a spec can gate with an optional positive `success` pattern (fail-closed: it must match to pass, e.g. ESBMC/CBMC's `VERIFICATION SUCCESSFUL`) and/or a `failure` pattern (a match forces failure — the gate for backends whose failures don't surface as issues by default, e.g. Kani without `--trace`). Specs are plain dataclass instances (e.g., `esbmc_spec`, `cbmc_spec`, `clang_spec`, `pytest_spec`). Any `block` pattern can be wrapped with `missing_hint("Needs --flag")(pattern)` to annotate it — when the block fails to match and verification failed, the hint is collected into `VerifierOutput.hints` and displayed by the CLI. +1. **Specs** (`formal_lib/specs/`) — Each verifier backend defines an `IssueRegexSpec` containing regex patterns for extracting issue blocks, error types, messages, severity, and nested `StackTraceRegexSpec`/`CounterexampleRegexSpec` for traces. The verification outcome is a data-driven baseline — a run passes when it has no error-severity issue — that a spec can gate with an optional positive `success` pattern (fail-closed: it must match to pass, e.g. ESBMC/CBMC's `VERIFICATION SUCCESSFUL`) and/or a `failure` pattern (a match forces failure — the gate for backends whose failures don't surface as issues by default, e.g. Kani without `--trace`). Specs are plain dataclass instances (e.g., `esbmc_spec`, `cbmc_spec`, `clang_spec`, `pytest_spec`). Each spec declares the verifier `versions` it supports — a list of exact `Version` and/or inclusive `VersionRange` entries (`formal_lib/version.py`; a `None` bound means unbounded, default is a single all-versions range). Any `block` pattern can be wrapped with `missing_hint("Needs --flag")(pattern)` to annotate it — when the block fails to match and verification failed, the hint is collected into `VerifierOutput.hints` and displayed by the CLI. 2. **Parser** (`formal_lib/issue_parser.py`) — `IssueSpecOutputParser` applies a spec's regex hierarchy to raw output: the block pattern finds issue boundaries and field patterns extract structured data from each block, then `_is_successful` computes the `successful` flag from the parsed issues' severities gated by the spec's `success`/`failure` patterns. Traces are parsed via a nested block→entry→fields hierarchy. @@ -48,9 +54,12 @@ The library uses a **specification-driven regex parsing** pattern with three lay ## Testing - **Unit tests** in `tests/test_specs/` — cover only behaviour a regression fixture can't express: auto-detection, missing-flag hints (excluded from serialized output), derived-property logic (`function_name`/`error_location` precedence), and verdict combinations driven by synthetic specs. Anything that's "parse a real log with a registered backend and check the structured output" belongs in the regression suite, not here. -- **Regression tests** in `tests/regressions/` — data-driven: drop a `.log` and matching `.json` into `tests/regressions/samples//` and the test auto-discovers them. The `.json` is the expected CLI JSON output minus the `output` field. Marked with `@pytest.mark.regression`, excluded from default pytest runs. +- **Regression tests** in `tests/regressions/` — data-driven: drop a `.log` and matching `.json` into `tests/regressions/samples//` and the test auto-discovers them. The `.json` is the expected CLI JSON output minus the `output` field. Marked with `@pytest.mark.regression`, excluded from default pytest runs. + - A directory component named as a version range (`v6.7.0-v6.10.0`, `v6.7.0-`, `-v6.10.0`, or exact `v6.7.1` — see `VERSION_RANGE_PATTERN`) constrains the samples beneath it: they run only against the backend's specs whose `versions` overlap that range. Samples outside a version directory run against every spec of their backend. Name version directories after the tool version the `.log` itself proves (its version banner) — don't invent ranges the log doesn't evidence. - The `.log` must be **genuine verifier output** (captured from a real run), and the `.json` must be the **exact** structured output the parser produces from that log — generate it by running `pf` (`python -m formal_lib --backend --format json-compact`) against the log and stripping the `output` field, then read it to confirm it faithfully reflects the log. Never hand-write or hallucinate field values (messages, line numbers, trace entries, severities): every value in the `.json` must be traceable to something actually present in the `.log`. If the generated output looks wrong, the fix is in the spec/parser, not in editing the `.json` to what you wish it said. ## Adding a New Verifier Backend -Create a new `IssueRegexSpec` instance in `formal_lib/specs/`. The verdict defaults to "no error-severity issue"; add a `success` pattern (positive verdict line) and/or a `failure` pattern (forces failure) only if the backend needs one. Wrap any `block` pattern with `missing_hint("Needs --flag")(pattern)` when the verifier requires a specific flag for that data. Export it from `formal_lib/specs/__init__.py` and add it to the `SPECS` dict (which also registers the `--backend` choice in `__main__.py`). +Create a new `IssueRegexSpec` instance in `formal_lib/specs/`. The verdict defaults to "no error-severity issue"; add a `success` pattern (positive verdict line) and/or a `failure` pattern (forces failure) only if the backend needs one. Wrap any `block` pattern with `missing_hint("Needs --flag")(pattern)` when the verifier requires a specific flag for that data. Export it from `formal_lib/specs/__init__.py` and add it to the `SPECS` dict, which maps each backend name (the `--backend` choice in `__main__.py`) to a list of versioned specs. + +When a verifier changes its output format in a new version, add a second spec to the same backend's list (newest first) and constrain both specs' `versions` so their ranges don't overlap — `hatch run check-specs` fails on any same-backend overlap (a spec conflict). `resolve_spec` picks within a backend by trying each spec's `detect` pattern, falling back to the first listed. diff --git a/README.md b/README.md index a456932..03c4c09 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,20 @@ The following backends are supported: - PyTest - Kani +### Spec Versioning + +Each backend is parsed by a spec that declares which verifier versions it +supports, as exact versions and/or inclusive version ranges (a missing bound +means the range is unbounded on that side; the default is all versions). When +a verifier changes its output format, a new spec is added for the new versions +alongside the old one. Within a backend, no two specs may support the same +version (a spec conflict). Check this with: + +```bash +hatch run check-specs # fails on any spec conflict +hatch run check-specs -v # also lists every spec and the versions it supports +``` + ## Frontend `pf` (Pretty Format) is a CLI frontend for `formal-lib`. It can be invoked from From 89ccde13767565cafc3b9159e837a0b9a4c01cba Mon Sep 17 00:00:00 2001 From: Yiannis Charalambous Date: Wed, 22 Jul 2026 14:11:03 +0100 Subject: [PATCH 5/5] refactor: apply cleanup review to version support internals --- formal_lib/specs/__init__.py | 27 +++++++++------ formal_lib/specs/base.py | 10 +++++- formal_lib/specs/conflicts.py | 24 +++++-------- formal_lib/version.py | 7 ++-- tests/regressions/test_sample_regression.py | 38 +++++++++------------ tests/test_version.py | 14 ++++++++ 6 files changed, 70 insertions(+), 50 deletions(-) diff --git a/formal_lib/specs/__init__.py b/formal_lib/specs/__init__.py index 3caf18e..64c0588 100644 --- a/formal_lib/specs/__init__.py +++ b/formal_lib/specs/__init__.py @@ -19,7 +19,6 @@ from .esbmc import esbmc_spec from .kani import kani_spec from .pytest import pytest_spec -from formal_lib.version import Version, VersionRange SPECS: dict[str, list[IssueRegexSpec]] = { "esbmc": [esbmc_spec], @@ -35,12 +34,23 @@ within a backend must not overlap (checked by ``hatch run check-specs``).""" +def _first_detected(specs: list[IssueRegexSpec], output: str) -> IssueRegexSpec | None: + """First spec whose ``detect`` pattern matches the output, or None. + + The one definition of detect-matching, so auto-detection and backend-scoped + resolution can never pick different specs for the same log.""" + for spec in specs: + if spec.detect and re.search(spec.detect, output, re.MULTILINE): + return spec + return None + + def detect_spec(output: str) -> IssueRegexSpec: """Auto-detect which spec matches the output using each spec's detect pattern.""" for specs in SPECS.values(): - for spec in specs: - if spec.detect and re.search(spec.detect, output, re.MULTILINE): - return spec + spec = _first_detected(specs, output) + if spec is not None: + return spec names = ", ".join(SPECS) raise ValueError(f"could not detect backend from output (known: {names})") @@ -50,10 +60,9 @@ def resolve_spec(backend: str, output: str) -> IssueRegexSpec: whose ``detect`` pattern matches the output wins; when none match, fall back to the first registered (the newest) spec.""" specs = SPECS[backend] - for spec in specs: - if spec.detect and re.search(spec.detect, output, re.MULTILINE): - return spec - return specs[0] + if len(specs) == 1: + return specs[0] + return _first_detected(specs, output) or specs[0] __all__ = [ @@ -64,8 +73,6 @@ def resolve_spec(backend: str, output: str) -> IssueRegexSpec: "IssueRegexSpec", "SPECS", "StackTraceRegexSpec", - "Version", - "VersionRange", "cbmc_spec", "clang_spec", "detect_spec", diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index 9ee8afc..17ea7c3 100644 --- a/formal_lib/specs/base.py +++ b/formal_lib/specs/base.py @@ -7,7 +7,7 @@ from dataclasses import dataclass, field from pathlib import Path -from formal_lib.version import Version, VersionRange +from formal_lib.version import Version, VersionRange, as_range class AnnotatedPattern(str): @@ -268,3 +268,11 @@ class IssueRegexSpec: cache_properties: CachePropertiesFn | None = field(default=None) """Optional function to compute cache properties from verify_source args. When None, default properties are used.""" + + def supports(self, target: Version | VersionRange) -> bool: + """Whether any entry in ``versions`` overlaps ``target``. + + The single interpretation of the ``versions`` field — shared by the + conflict checker and the regression suite's version-directory scoping + so the two can never disagree about which specs a version maps to.""" + return any(as_range(v).overlaps(target) for v in self.versions) diff --git a/formal_lib/specs/conflicts.py b/formal_lib/specs/conflicts.py index a3fcbe5..021bfc1 100644 --- a/formal_lib/specs/conflicts.py +++ b/formal_lib/specs/conflicts.py @@ -15,29 +15,21 @@ from formal_lib.specs import SPECS from formal_lib.specs.base import IssueRegexSpec -from formal_lib.version import Version, VersionRange, as_range -def _describe(versions: list[Version | VersionRange]) -> str: - """Render a supported-versions list; the all-unbounded default reads "any version".""" - return ", ".join( - "any version" if v == VersionRange() else str(v) for v in versions - ) +def _versions(spec: IssueRegexSpec) -> str: + return ", ".join(str(v) for v in spec.versions) -def find_conflicts(specs: dict[str, list[IssueRegexSpec]] = SPECS) -> list[str]: +def find_conflicts(specs: dict[str, list[IssueRegexSpec]]) -> list[str]: """Return one message per pair of same-backend specs with overlapping versions.""" conflicts: list[str] = [] for backend, backend_specs in specs.items(): for (i, first), (j, second) in combinations(enumerate(backend_specs), 2): - if any( - as_range(a).overlaps(b) - for a in first.versions - for b in second.versions - ): + if any(first.supports(v) for v in second.versions): conflicts.append( - f"{backend}: spec #{i} [{_describe(first.versions)}] overlaps " - f"spec #{j} [{_describe(second.versions)}]" + f"{backend}: spec #{i} [{_versions(first)}] overlaps " + f"spec #{j} [{_versions(second)}]" ) return conflicts @@ -60,9 +52,9 @@ def main() -> None: for backend, backend_specs in SPECS.items(): print(f"{backend}:") for i, spec in enumerate(backend_specs): - print(f" spec #{i}: {_describe(spec.versions)}") + print(f" spec #{i}: {_versions(spec)}") - conflicts = find_conflicts() + conflicts = find_conflicts(SPECS) for conflict in conflicts: print(f"spec conflict: {conflict}", file=sys.stderr) if conflicts: diff --git a/formal_lib/version.py b/formal_lib/version.py index 89ca2ab..5768988 100644 --- a/formal_lib/version.py +++ b/formal_lib/version.py @@ -14,7 +14,8 @@ import re from dataclasses import dataclass -_VERSION = r"v\d+(?:\.\d+)*" +_VERSION_BODY = r"\d+(?:\.\d+)*" +_VERSION = rf"v{_VERSION_BODY}" VERSION_RANGE_PATTERN = re.compile(rf"{_VERSION}-(?:{_VERSION})?|-{_VERSION}|{_VERSION}") """Grammar for a version-range category name; use with ``fullmatch``. A bare ``-`` (unbounded on both sides) is deliberately rejected — an unconstrained @@ -42,7 +43,7 @@ def __post_init__(self) -> None: def parse(cls, text: str) -> "Version": """Parse ``6.7.1`` or ``v6.7.1`` into a Version.""" body = text.removeprefix("v") - if not re.fullmatch(r"\d+(?:\.\d+)*", body): + if not re.fullmatch(_VERSION_BODY, body): raise ValueError(f"invalid version: {text!r}") return cls(tuple(int(part) for part in body.split("."))) @@ -94,6 +95,8 @@ def overlaps(self, other: "Version | VersionRange") -> bool: ) def __str__(self) -> str: + if self.lower is None and self.upper is None: + return "any version" if self.lower is not None and self.lower == self.upper: return f"v{self.lower}" lower = f"v{self.lower}" if self.lower is not None else "" diff --git a/tests/regressions/test_sample_regression.py b/tests/regressions/test_sample_regression.py index 9505dad..4178a19 100644 --- a/tests/regressions/test_sample_regression.py +++ b/tests/regressions/test_sample_regression.py @@ -22,19 +22,20 @@ from formal_lib.issue_parser import IssueSpecOutputParser from formal_lib.specs import SPECS from formal_lib.specs.base import IssueRegexSpec -from formal_lib.version import VERSION_RANGE_PATTERN, VersionRange, as_range +from formal_lib.version import VERSION_RANGE_PATTERN, VersionRange SAMPLES_DIR = Path(__file__).parent / "samples" -ORPHANED: list[str] = [] -"""Version-constrained samples whose range overlaps no spec of their backend — -silently dropping them would shrink the suite, so a test asserts this is empty.""" +def discover_samples() -> tuple[list, list[str]]: + """Discover .log/.json pairs, pairing each with the specs it applies to. - -def discover_samples() -> list[tuple[str, IssueRegexSpec, Path, Path]]: - """Discover .log/.json pairs and pair each with the specs it applies to.""" + Also returns the orphaned samples: version-constrained samples whose range + overlaps no spec of their backend — silently dropping them would shrink the + suite, so a test asserts the list is empty. + """ cases = [] + orphaned: list[str] = [] for backend_dir in sorted(SAMPLES_DIR.iterdir()): specs = SPECS.get(backend_dir.name) if not backend_dir.is_dir() or not specs: @@ -55,22 +56,21 @@ def discover_samples() -> list[tuple[str, IssueRegexSpec, Path, Path]]: matched = [ spec for spec in specs - if constraint is None - or any(as_range(v).overlaps(constraint) for v in spec.versions) + if constraint is None or spec.supports(constraint) ] if not matched: - ORPHANED.append(f"{backend_dir.name}/{relative}") + orphaned.append(f"{backend_dir.name}/{relative}") continue + sample_id = f"{backend_dir.name}/{relative.with_suffix('')}" for spec in matched: - sample_id = f"{backend_dir.name}/{relative.with_suffix('')}" + spec_id = sample_id if len(matched) > 1: - versions = ",".join(str(v) for v in spec.versions) - sample_id += f"@{versions}" - cases.append((sample_id, spec, log_file, json_file)) - return cases + spec_id += "@" + ",".join(str(v) for v in spec.versions) + cases.append(pytest.param(spec, log_file, json_file, id=spec_id)) + return cases, orphaned -SAMPLES = discover_samples() +SAMPLES, ORPHANED = discover_samples() @pytest.mark.regression @@ -80,11 +80,7 @@ def test_no_orphaned_samples() -> None: @pytest.mark.regression -@pytest.mark.parametrize( - "spec, log_file, json_file", - [case[1:] for case in SAMPLES], - ids=[case[0] for case in SAMPLES], -) +@pytest.mark.parametrize("spec, log_file, json_file", SAMPLES) def test_sample_output_matches_expected( spec: IssueRegexSpec, log_file: Path, json_file: Path ) -> None: diff --git a/tests/test_version.py b/tests/test_version.py index 6314013..3682808 100644 --- a/tests/test_version.py +++ b/tests/test_version.py @@ -93,6 +93,13 @@ def test_as_range() -> None: assert as_range(r) is r +def test_range_str() -> None: + assert str(VersionRange.parse("v1-v2")) == "v1-v2" + assert str(VersionRange.parse("v6.7.1")) == "v6.7.1" + assert str(VersionRange.parse("-v3")) == "-v3" + assert str(VersionRange()) == "any version" + + # --- spec conflict checker --- _NO_TRACE = StackTraceRegexSpec( @@ -114,6 +121,13 @@ def _spec(*versions: Version | VersionRange) -> IssueRegexSpec: return spec +def test_spec_supports() -> None: + spec = _spec(Version.parse("2"), VersionRange.parse("v5-v6")) + assert spec.supports(Version.parse("2")) + assert spec.supports(VersionRange.parse("v6-v9")) + assert not spec.supports(VersionRange.parse("v3-v4.9")) + + def test_disjoint_specs_do_not_conflict() -> None: specs = { "tool": [