Add version support for verifier specs

.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

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/<spec>/` 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/<backend>/` 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 <spec> --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.

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

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",

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

formal_lib/specs/__init__.py

@@ -20,27 +20,51 @@
 from .kani import kani_spec
 from .pytest import pytest_spec
 
-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 _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 _, spec in SPECS.items():
-        if spec.detect and re.search(spec.detect, output, re.MULTILINE):
+    for specs in SPECS.values():
+        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})")
 
 
+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]
+    if len(specs) == 1:
+        return specs[0]
+    return _first_detected(specs, output) or specs[0]
+
+
 __all__ = [
     "AnnotatedPattern",
     "CachePropertiesFn",
@@ -57,4 +81,5 @@ def detect_spec(output: str) -> IssueRegexSpec:
     "kani_spec",
     "missing_hint",
     "pytest_spec",
+    "resolve_spec",
 ]

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, as_range
+
 
 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
@@ -258,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)

formal_lib/specs/conflicts.py

@@ -0,0 +1,67 @@
+# 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
+
+
+def _versions(spec: IssueRegexSpec) -> str:
+    return ", ".join(str(v) for v in spec.versions)
+
+
+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(first.supports(v) for v in second.versions):
+                conflicts.append(
+                    f"{backend}: spec #{i} [{_versions(first)}] overlaps "
+                    f"spec #{j} [{_versions(second)}]"
+                )
+    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}: {_versions(spec)}")
+
+    conflicts = find_conflicts(SPECS)
+    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()