Replace negate_success with success + failure verdict gates

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

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

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

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<source>\n<indicator>"
     # Match the diagnostic line plus optional following source/indicator lines.
     block=r"^[^\s:]+:\d+:\d+:\s+(?:error|warning):[^\n]*\n(?:[^\n]*\n[^\s:]*[~^ ]*\n?)?",

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

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

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
+}

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

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
+}

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;}
+      |                    ^

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 <severity>`` 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