diff --git a/CLAUDE.md b/CLAUDE.md index d3396c0..dd92cf1 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -32,9 +32,9 @@ hatch build 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. Specs also define a `success` pattern to determine verification outcome from the output text (with `negate_success` for backends where absence of failure indicates success). 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`). 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 `success` pattern determines the `successful` flag, the block pattern finds issue boundaries, then field patterns extract structured data from each block. Traces are parsed via a nested block→entry→fields hierarchy. +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. 3. **Runner** (`formal_lib/verifier_runner.py`) — `VerifierRunner` executes a verifier command, feeds output to the parser, and optionally caches results using content-based hashing (zlib.adler32 + pickle). @@ -52,4 +52,4 @@ The library uses a **specification-driven regex parsing** pattern with three lay ## Adding a New Verifier Backend -Create a new `IssueRegexSpec` instance in `formal_lib/specs/`, including a `success` pattern for determining verification outcome. 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`, add it to the `SPECS` dict, and add a CLI flag 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 also registers the `--backend` choice in `__main__.py`). diff --git a/formal_lib/issue_parser.py b/formal_lib/issue_parser.py index 0313bac..b1c48ce 100644 --- a/formal_lib/issue_parser.py +++ b/formal_lib/issue_parser.py @@ -33,23 +33,18 @@ def parse_output( ) -> VerifierOutput: # Strip ANSI escape codes in case the tool emits colored output. output = ANSI_ESCAPE_PATTERN.sub("", output) - - # Determine success from the spec's success pattern. spec = self.regex_spec - if spec.success: - matched = bool(re.search(spec.success, output, re.MULTILINE)) - successful = not matched if spec.negate_success else matched - else: - successful = True - - # Extract all issue blocks from the output - issue_blocks: list[str] = [] - for match in re.finditer(spec.block, output, re.DOTALL | re.MULTILINE): - issue_blocks.append(match.group(0)) - - # Parse each issue block to extract individual issues + + # Extract issue blocks, then parse each into an issue. The verdict's + # data-driven baseline reads issue severities, so issues are parsed first. + issue_blocks: list[str] = [ + match.group(0) + for match in re.finditer(spec.block, output, re.DOTALL | re.MULTILINE) + ] issues: list[Issue] = [self._parse_issue(block) for block in issue_blocks] + successful = self._is_successful(output, issues) + # Collect hints from annotated blocks that failed to match. hints: list[str] = [] if not successful and not issues: @@ -65,6 +60,26 @@ def parse_output( hints=hints, ) + def _is_successful(self, output: str, issues: list[Issue]) -> bool: + """Return whether the run passed: no error-severity issue, and — when the + spec sets them — the ``success`` pattern matched and the ``failure`` pattern + did not. Warning/info issues never flip the verdict. + + The error-issue baseline and the ``failure`` pattern are independent failure + signals, so a failure missed by one is still caught by the other; ``success`` + is a fail-closed positive requirement (its absence fails the run). + """ + spec = self.regex_spec + if any(issue.severity == "error" for issue in issues): + return False + if spec.success is not None and not re.search( + spec.success, output, re.MULTILINE + ): + return False + if spec.failure is not None and re.search(spec.failure, output, re.MULTILINE): + return False + return True + @staticmethod def _get_hint(pattern: str) -> str: return pattern.hint if isinstance(pattern, AnnotatedPattern) else "" diff --git a/formal_lib/specs/base.py b/formal_lib/specs/base.py index d389dd8..739c010 100644 --- a/formal_lib/specs/base.py +++ b/formal_lib/specs/base.py @@ -243,12 +243,18 @@ class IssueRegexSpec: header (e.g. ESBMC's ``Violated property:`` block, clang's diagnostic header). When set, ``Issue`` properties prefer this location over the stack trace's last frame.""" - success: str = "" - """Regex pattern for determining verification success from output text. - Matched with re.MULTILINE against the full output.""" - negate_success: bool = False - """When False, a match means success. When True, a match means failure - (i.e. success is the absence of the pattern).""" + success: str | None = None + """Regex whose match confirms the run PASSED — a positive verdict line such as + ESBMC/CBMC's ``VERIFICATION SUCCESSFUL``. Fail-closed: when set and it does not + match, the run is reported as failed. ``None`` skips this gate. re.MULTILINE.""" + failure: str | None = None + """Regex whose match forces the verdict to FAILED. Use it for verifiers with no + positive success signal, or whose failures don't always surface as issues (e.g. + Kani run without ``--trace``) so the pattern gates those cases. ``None`` skips it. + re.MULTILINE. + + ``success`` and ``failure`` layer on the data-driven baseline; see + :meth:`IssueSpecOutputParser._is_successful` for how the three combine.""" cache_properties: CachePropertiesFn | None = field(default=None) """Optional function to compute cache properties from verify_source args. When None, default properties are used.""" diff --git a/formal_lib/specs/clang.py b/formal_lib/specs/clang.py index b8360ed..4d8dcf1 100644 --- a/formal_lib/specs/clang.py +++ b/formal_lib/specs/clang.py @@ -5,8 +5,9 @@ clang_spec: IssueRegexSpec = IssueRegexSpec( # Detect clang/gcc diagnostics by the "file:line:col: error/warning:" pattern. detect=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):", - success=r":\d+:\s+error:", - negate_success=True, + # No verdict pattern: a clang `error:` diagnostic is extracted as an error-severity + # issue, so the parser's data-driven baseline already fails the run. Warnings are + # issues too, but severity "warning", so they never fail the build. # Each diagnostic is a block: "file:line:col: type: message\n\n" # Match the diagnostic line plus optional following source/indicator lines. block=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):[^\n]*\n(?:[^\n]*\n[^\s:]*[~^ ]*\n?)?", diff --git a/formal_lib/specs/kani.py b/formal_lib/specs/kani.py index 1f8fa87..18dd7f8 100644 --- a/formal_lib/specs/kani.py +++ b/formal_lib/specs/kani.py @@ -32,23 +32,22 @@ def _kani_message(value: str) -> str: cbmc_spec, # Kani prints its own banner above CBMC's; detect on that. detect=r"^Kani Rust Verifier", - # Derive the verdict from the per-check statuses in CBMC's `** Results:` section, - # NOT the top-line `VERIFICATION` verdict. In old format Kani does not post-process - # its assertion-reachability probes, so a *passing* run still prints `VERIFICATION - # FAILED`: each `reachability_check` property "fails" precisely because the assertion - # is reachable (normal). Keying off the real per-check statuses lets Kani keep - # reachability checks enabled — they catch unreachable, vacuously-passing assertions, - # so disabling them would weaken verification — while still reporting correctly. - # - # negate_success: a match means FAILURE. A real failure is either a `** Results:` - # line for a non-`reachability_check` check with status FAILURE, or the native-format - # `VERIFICATION:- FAILED` line (native format has no such Results lines and is already - # correctly post-processed by Kani, so its verdict line is trustworthy). - success=( + # Kani has no positive success line in old format — a *passing* run still prints + # `VERIFICATION FAILED`, because Kani does not post-process its assertion-reachability + # probes there (each `reachability_check` "fails" precisely because the assertion is + # reachable, which is normal). So clear the `success` pattern inherited from cbmc_spec + # and derive the verdict from a `failure` pattern over the per-check statuses instead. + # This lets Kani keep reachability checks enabled — they catch unreachable, + # vacuously-passing assertions, so disabling them would weaken verification. + success=None, + # A match means FAILED: either a `** Results:` line for a non-`reachability_check` + # check with status FAILURE, or the native-format `VERIFICATION:- FAILED` line (native + # format has no such Results lines and is already correctly post-processed by Kani). + # The pattern also gates the no-`--trace` case, where a failure produces no issues. + failure=( r"^\[[^\]]*\.(?!reachability_check\.)[A-Za-z][\w-]*\.\d+\][^\n]*: FAILURE$" r"|^VERIFICATION:- FAILED$" ), - negate_success=True, # Same trace-block boundaries as CBMC, with two Kani adjustments: # * skip the `reachability_check` properties Kani injects (its native format # hides them; they are not real bugs), and diff --git a/formal_lib/specs/pytest.py b/formal_lib/specs/pytest.py index 3a801d2..a48ae19 100644 --- a/formal_lib/specs/pytest.py +++ b/formal_lib/specs/pytest.py @@ -24,8 +24,9 @@ def _pytest_cache_properties( pytest_spec: IssueRegexSpec = IssueRegexSpec( # Detect pytest by its distinctive session header. detect=r"^={5,} test session starts ={5,}$", - success=r"(?:FAILED|ERROR)", - negate_success=True, + # pytest has no reliable positive success line (a summary can mix passed with + # failed/error), so the verdict is the failure pattern plus the error-issue baseline. + failure=r"(?:FAILED|ERROR)", # Match both collection ERROR blocks and test FAILURE blocks # Test failure: "_____ test_name _____" (underscores, space, identifier, space, underscores) # Collection error: "_____ ERROR collecting path _____" diff --git a/tests/regressions/samples/clang/undeclared_error.json b/tests/regressions/samples/clang/undeclared_error.json new file mode 100644 index 0000000..da397d8 --- /dev/null +++ b/tests/regressions/samples/clang/undeclared_error.json @@ -0,0 +1,20 @@ +{ + "successful": false, + "issues": [ + { + "error_type": "error", + "message": "\u2018zzz\u2019 undeclared (first use in this function)", + "stack_trace": [ + { + "trace_index": 0, + "path": "err.c", + "name": null, + "line_idx": 0 + } + ], + "severity": "error", + "error_location": null + } + ], + "duration": 0.0 +} diff --git a/tests/regressions/samples/clang/undeclared_error.log b/tests/regressions/samples/clang/undeclared_error.log new file mode 100644 index 0000000..cd58211 --- /dev/null +++ b/tests/regressions/samples/clang/undeclared_error.log @@ -0,0 +1,5 @@ +err.c: In function ‘main’: +err.c:1:23: error: ‘zzz’ undeclared (first use in this function) + 1 | int main(void){return zzz;} + | ^~~ +err.c:1:23: note: each undeclared identifier is reported only once for each function it appears in diff --git a/tests/regressions/samples/clang/unused_variable_warning.json b/tests/regressions/samples/clang/unused_variable_warning.json new file mode 100644 index 0000000..cd66756 --- /dev/null +++ b/tests/regressions/samples/clang/unused_variable_warning.json @@ -0,0 +1,20 @@ +{ + "successful": true, + "issues": [ + { + "error_type": "warning", + "message": "unused variable \u2018x\u2019 [-Wunused-variable]", + "stack_trace": [ + { + "trace_index": 0, + "path": "warn.c", + "name": null, + "line_idx": 0 + } + ], + "severity": "warning", + "error_location": null + } + ], + "duration": 0.0 +} diff --git a/tests/regressions/samples/clang/unused_variable_warning.log b/tests/regressions/samples/clang/unused_variable_warning.log new file mode 100644 index 0000000..3b76193 --- /dev/null +++ b/tests/regressions/samples/clang/unused_variable_warning.log @@ -0,0 +1,4 @@ +warn.c: In function ‘main’: +warn.c:1:20: warning: unused variable ‘x’ [-Wunused-variable] + 1 | int main(void){int x; return 0;} + | ^ diff --git a/tests/test_specs/test_verdict.py b/tests/test_specs/test_verdict.py new file mode 100644 index 0000000..0e90d31 --- /dev/null +++ b/tests/test_specs/test_verdict.py @@ -0,0 +1,88 @@ +# Author: Yiannis Charalambous + +"""Tests for the verdict logic in IssueSpecOutputParser._is_successful. + +Uses a tiny synthetic spec: a line ``ISSUE `` becomes one issue of that +severity, and ``PASS`` / ``FAIL`` markers drive the ``success`` / ``failure`` patterns. +""" + +from formal_lib import IssueSpecOutputParser +from formal_lib.specs.base import IssueRegexSpec, StackTraceRegexSpec + +# A stack-trace spec whose block never matches, so issues have an empty stack trace. +_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 _verdict(output: str, *, success: str | None = None, failure: str | None = None) -> bool: + spec = IssueRegexSpec( + block=r"^ISSUE \w+$", + error_type=r"^(ISSUE)", + message=r"^ISSUE (\w+)", + severity=r"^ISSUE (\w+)", + stack_trace_spec=_NO_TRACE, + success=success, + failure=failure, + ) + return IssueSpecOutputParser(spec).parse_output(output).successful + + +# --- data-driven baseline (no patterns) --- + +def test_no_patterns_error_issue_fails() -> None: + assert _verdict("ISSUE error") is False + + +def test_no_patterns_warning_issue_passes() -> None: + assert _verdict("ISSUE warning") is True + + +def test_no_patterns_info_issue_passes() -> None: + assert _verdict("ISSUE info") is True + + +def test_no_patterns_no_issue_passes() -> None: + assert _verdict("nothing to see") is True + + +def test_mixed_warning_and_error_fails() -> None: + assert _verdict("ISSUE warning\nISSUE error") is False + + +# --- success pattern: positive confirmation, fail-closed --- + +def test_success_pattern_must_match_to_pass() -> None: + assert _verdict("PASS", success=r"PASS") is True + # No match -> failed, even with no issues (fail-closed on garbage/crash output). + assert _verdict("truncated output", success=r"PASS") is False + + +def test_success_pattern_overridden_by_error_issue() -> None: + """Even if the success line matched, an error issue means not successful.""" + assert _verdict("PASS\nISSUE error", success=r"PASS") is False + + +# --- failure pattern: the gate for no-issue failures --- + +def test_failure_pattern_gates_a_failure_with_no_issues() -> None: + """The key case the data-driven baseline can't see: a failure that produced no + issues (e.g. Kani without --trace) is still caught by the failure pattern.""" + assert _verdict("FAIL", failure=r"FAIL") is False + assert _verdict("all clear", failure=r"FAIL") is True + + +def test_error_issue_catches_a_missed_failure_pattern() -> None: + """The independent gates close the fail-open: if the failure pattern misses but + the failure surfaced as an error issue, the run is still reported as failed.""" + assert _verdict("ISSUE error", failure=r"FAIL") is False + + +# --- both patterns --- + +def test_both_patterns_failure_wins() -> None: + """When a spec sets BOTH patterns (no shipping spec does today, but the API + allows it), the failure gate wins over a matching success line.""" + assert _verdict("PASS", success=r"PASS", failure=r"FAIL") is True + assert _verdict("PASS\nFAIL", success=r"PASS", failure=r"FAIL") is False