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 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 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..64c0588 100644 --- a/formal_lib/specs/__init__.py +++ b/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", ] diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index 739c010..17ea7c3 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, 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) diff --git a/formal_lib/specs/conflicts.py b/formal_lib/specs/conflicts.py new file mode 100644 index 0000000..021bfc1 --- /dev/null +++ b/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() diff --git a/formal_lib/version.py b/formal_lib/version.py new file mode 100644 index 0000000..5768988 --- /dev/null +++ b/formal_lib/version.py @@ -0,0 +1,109 @@ +# 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_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 +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(_VERSION_BODY, 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 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 "" + 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/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..4178a19 100644 --- a/tests/regressions/test_sample_regression.py +++ b/tests/regressions/test_sample_regression.py @@ -2,56 +2,94 @@ """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 + 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: +def discover_samples() -> tuple[list, list[str]]: + """Discover .log/.json pairs, pairing 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: 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 spec.supports(constraint) + ] + if not matched: + orphaned.append(f"{backend_dir.name}/{relative}") + continue + sample_id = f"{backend_dir.name}/{relative.with_suffix('')}" + for spec in matched: + spec_id = sample_id + if len(matched) > 1: + 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() -SAMPLE_IDS = [f"{spec}/{log.stem}" for spec, log, _ in SAMPLES] +SAMPLES, ORPHANED = discover_samples() + + +@pytest.mark.regression +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", SAMPLES, ids=SAMPLE_IDS) +@pytest.mark.parametrize("spec, log_file, json_file", 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 diff --git a/tests/test_version.py b/tests/test_version.py new file mode 100644 index 0000000..3682808 --- /dev/null +++ b/tests/test_version.py @@ -0,0 +1,167 @@ +# 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 + + +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( + 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_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": [ + _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) == []