P-015: structured reachability-slice evidence for diagnostics

docs/proposals/P-015-reachability-evidence.md

@@ -0,0 +1,97 @@
+# P-015 -- Reachability-slice evidence: explain the path, not just the point
+
+Status: **accepted, in progress** (model + SARIF builder landed; OwnIR wiring is the next patch)
+
+## Why
+
+Two academic works were proposed as inputs to Own.NET's design: **ReachHover**
+(a data-flow reachability UI; ICSME '23 + a 72-developer survey) and the
+**Optional Checker** (modular cooperating qualifier checkers via partial
+rely-guarantee; ASE '24). A review of that research landed on a sharper framing
+than the original "Rust-style borrow checker compiling to C#" pitch:
+
+> Optional Checker  -> how to build modular, checkable *contracts*
+> ReachHover        -> how to *explain* multi-file diagnostics
+> Own.NET           -> applies both to C#/WPF resources, lifetimes, XAML, DI
+
+The single most important realisation is that the "fact-based frontends -> one
+core -> explainable diagnostics" architecture the review recommends **already
+exists** in this repo (`ownir.py` facts, one core checker, several analyses).
+So the recommendation collapses to one concrete, high-leverage gap rather than a
+rewrite.
+
+## The gap (precise)
+
+A finding answers *that* something is wrong. The reachability question a
+developer actually asks is *why is this held, and through what?* Today:
+
+- `ownlang/ownir.py` `Finding` already carries `related` and emits SARIF
+  **`relatedLocations`** -- good, unordered secondary anchors (e.g. a DI
+  captive's consuming constructor).
+- But there are **no `codeFlows`** anywhere: the *ordered* retention path
+  (`singleton -> transient -> scoped`) that the DI checker already computes
+  (`CaptiveDependency.path` and friends) is dropped into the message **string**
+  instead of being emitted as a structured slice a SARIF/IDE consumer can walk.
+- The core `Diagnostic` (the `.own` path) had no structured secondary locations
+  at all -- only a primary line + caret, plus textual
+  `[consumed by ... at file:line]` riders.
+
+That ordered slice *is* the ReachHover idea. It is the highest-value, smallest
+change in the whole synthesis: the data is already computed; only the
+presentation is missing.
+
+## What this change adds
+
+1. **`ownlang/evidence.py`** -- a pure, dependency-free transform from an ordered
+   chain of `(file, line, label)` steps to the two SARIF constructs:
+   `related_locations(steps)` -> `relatedLocations`, `code_flow(steps)` ->
+   `codeFlows`, and `di_path_steps(path, loc_by_name, end_label)` which turns a
+   DI dependency path (service names) into ordered steps anchored at each
+   service's registration site. One vocabulary for every producer.
+2. **`ownlang/diagnostics.py`** -- `Diagnostic` gains a structured `evidence`
+   slice (`Evidence(line, label, file, role)`), the typed successor to the
+   textual riders, rendered as `note:` lines in both `render` and
+   `render_pretty`. Additive and backward compatible: an empty slice (the common
+   case) leaves existing output byte-for-byte unchanged.
+
+## The remaining wiring (next patch)
+
+The DI findings in `ownir.py` should pass the ordered slice through:
+
+- add `flow: tuple[tuple[str, int, str], ...] = ()` to `ownir.Finding`;
+- in `_sarif_result`, after the existing `relatedLocations`, splice
+  `result["codeFlows"] = evidence.code_flow(f.flow)` when non-empty;
+- in `_di_findings`, build `loc_by_name = {s.name: (s.file, s.line) ...}` once and
+  pass `flow=evidence.di_path_steps(c.path, loc_by_name, end_label)` per family
+  ("captures scoped service" for DI001, "leaked transient IDisposable" for DI004,
+  etc.).
+
+This is a ~10-line edit, intentionally kept out of this commit because
+`ownir.py` is large and must be edited where it can be run against its test
+suite (`build_sarif` has golden-file tests) rather than rewritten wholesale.
+
+## Staged plan (the review's priorities, mapped to this repo)
+
+- **P0 (this proposal)** -- reachability evidence for existing WPF/Event/Dispose/DI
+  findings: structured `relatedLocations` (done) + `codeFlows` slice (builder
+  done; OwnIR wiring next).
+- **P1** -- resource-protocol contracts as first-class declarations
+  (`resource Subscription { acquire: ev += h; release: ev -= h }`), building on
+  the existing `extern fn` per-parameter effects (`borrow`/`borrow_mut`/`consume`).
+- **P2** -- XAML -> .g.cs -> OwnIR join (`xaml_facts.py` already emits an
+  OwnIR-parallel envelope; the join is where the evidence slice spans XAML, the
+  generated `Connect()`, the code-behind handler and the view-model).
+- **P3** -- ArrayPool/Span borrow-like resource views (storage policies in
+  `buffers.py` already exist).
+- **P4** -- a real borrow/lifetime checker for OwnLang as a separate experimental
+  branch -- explicitly *not* the near-term roadmap.
+
+## Non-goals / honest scope
+
+- Not a "Rust borrow checker compiling to C#". The killer cases are C#/WPF
+  resource and lifetime audit (event leaks, `DispatcherTimer`, `IDisposable`
+  ownership, DI lifetime mismatch, pools), not memory safety.
+- Soundness is stated as: **sound for supported patterns, conservative when
+  facts are missing, runtime-correlated when static proof is insufficient** --
+  not whole-language soundness. The runtime-correlation arm already exists in
+  the audit subtree.

ownlang/diagnostics.py

@@ -1,6 +1,6 @@
 """Diagnostics for OwnLang. One place for every code and its human title.
 
-Numbering scheme (renumbered in this revision — see README changelog):
+Numbering scheme (renumbered in this revision -- see README changelog):
 
   001-013  flow-sensitive ownership & loan/permission violations
   020      unsupported construct (loops / async)
@@ -13,6 +13,14 @@
 different, sharper message than one that holds on only some path through a
 branch. That distinction was the reviewer's strongest point and it falls out
 naturally from the set-of-states lattice.
+
+A diagnostic can also carry an ordered *reachability slice* (``Evidence``): the
+chain of program points that explains *why* it holds -- where a resource was
+acquired, where a borrow escapes, where the missing release should go. This is
+the structured successor to the textual ``[consumed by ... at file:line]``
+riders the DI findings append: same information, but a place a tool can point at
+instead of a string to parse (P-015). See ``ownlang.evidence`` for the SARIF
+projection.
 """
 
 from __future__ import annotations
@@ -71,10 +79,39 @@ class Severity(Enum):
     "OWN040": "call to an undeclared function (unknown calls are forbidden)",
     "OWN041": "call argument mismatch",
     # ---- C# front-end resolution coverage (P-014; advisory) ----
-    "OWN050": "declaring type unresolved — leakage analysis skipped",
+    "OWN050": "declaring type unresolved -- leakage analysis skipped",
 }
 
 
+@dataclass(frozen=True)
+class Evidence:
+    """One secondary, structured location that explains a diagnostic -- a single step
+    in its reachability slice: where the resource was acquired, where a borrow
+    escapes, where the missing release should go, what consumed it. The primary
+    ``Diagnostic.line`` stays the anchor; evidence rides alongside it (rendered as
+    ``note:`` lines here; emitted as SARIF relatedLocations / codeFlows by
+    ``ownlang.evidence``).
+
+    This is the structured successor to the textual ``[consumed by ... at
+    file:line]`` riders: the same information, but a place a tool can point at
+    instead of a string to parse.
+    """
+
+    line: int
+    label: str
+    # the file of this step; None means "same file as the diagnostic's anchor".
+    file: str | None = None
+    # what this step is, for consumers that group/colour evidence: a plain "related"
+    # by default, or a resource-protocol role (acquired/released/escaped/consumed/step).
+    role: str = "related"
+
+    def render(self, anchor_file: str) -> str:
+        """A one-line ``note:`` rendering pointing at this step. ``anchor_file`` is
+        the diagnostic's own file, used when this step shares it (``file is None``)."""
+        where = self.file or anchor_file
+        return f"  note: {self.label} at {where}:{self.line}"
+
+
 @dataclass(frozen=True)
 class Diagnostic:
     code: str
@@ -85,9 +122,15 @@ class Diagnostic:
     # diagnostic is about, so the report attributes it by symbol, not by name.
     subject: str | None = None
     # the resource's human "kind" (e.g. "subscription token"), when the finding
-    # is about a tagged resource. Rendered as a ` [resource: <kind>]` suffix —
+    # is about a tagged resource. Rendered as a ` [resource: <kind>]` suffix --
     # domain-neutral metadata a later profile (e.g. WPF) keys off.
     resource_kind: str | None = None
+    # ordered reachability slice that explains this diagnostic (acquire site, escape
+    # site, missing-release point, consuming call). Empty for a single-point finding.
+    # Rendered as `note:` lines; a SARIF consumer maps it to relatedLocations /
+    # codeFlows via ownlang.evidence. Declared LAST so the positional constructor
+    # contract (code, message, line, severity, subject, resource_kind) is preserved.
+    evidence: tuple[Evidence, ...] = ()
 
     @property
     def title(self) -> str:
@@ -113,17 +156,26 @@ def _caret_col(self, src_line: str) -> int | None:
         stripped = len(src_line) - len(src_line.lstrip())
         return stripped + 1 if src_line.strip() else None
 
+    def _evidence_lines(self, filename: str) -> list[str]:
+        """The `note:` lines for this diagnostic's reachability slice, in order.
+        Empty when the finding carries no evidence (the common case), so the base
+        renderings stay byte-for-byte unchanged."""
+        return [e.render(filename) for e in self.evidence]
+
     def render(self, filename: str = "<input>") -> str:
-        """Plain one-line rendering: `file:line: severity: [code] message`."""
-        return (
+        """Plain rendering: `file:line: severity: [code] message`, followed by one
+        `note:` line per evidence step when present."""
+        head = (
             f"{filename}:{self.line}: {self.severity.value}: "
             f"[{self.code}] {self.message}{self._kind_suffix()}"
         )
+        return "\n".join([head, *self._evidence_lines(filename)])
 
     def render_pretty(self, filename: str, source: str) -> str:
         """A rustc-style rendering: a `file:line:col` header, the offending
-        source line, and a caret under the named identifier. Falls back to the
-        plain header when the line/column cannot be resolved."""
+        source line, a caret under the named identifier, and a `note:` line per
+        evidence step. Falls back to the plain header when the line/column cannot
+        be resolved."""
         lines = source.splitlines()
         src_line = lines[self.line - 1] if 1 <= self.line <= len(lines) else ""
         col = self._caret_col(src_line)
@@ -135,4 +187,5 @@ def render_pretty(self, filename: str, source: str) -> str:
             out.append(f"{gutter}{src_line}")
             if col:
                 out.append(" " * (len(gutter) + col - 1) + "^")
+        out.extend(self._evidence_lines(filename))
         return "\n".join(out)

ownlang/evidence.py

@@ -0,0 +1,112 @@
+"""Reachability-slice evidence -> SARIF (P-015).
+
+A finding is only as useful as the *path* it shows. A bare "OWN014: lifetime
+promotion" or "DI001: captive dependency" tells a developer *that* something is
+wrong; it does not answer the question they actually ask -- *why is this value
+held, and through what?* (the data-flow reachability question ReachHover's study
+found developers ask many times a day). This module turns an ordered chain of
+program points into the two SARIF constructs that answer it:
+
+  * ``relatedLocations`` -- unordered secondary anchors ("acquired here",
+    "missing release here", "consuming constructor") that a consumer (GitHub
+    code scanning, an IDE hover) renders as clickable, labelled links beside
+    the primary location.
+  * ``codeFlows`` -- an *ordered* slice: step 1 -> step 2 -> ... -> the finding.
+    This is the reachability slice: e.g. a DI captive's
+    ``singleton -> transient -> scoped`` retention path, each hop a real source
+    location.
+
+It is deliberately a pure, dependency-free transform over ``(file, line, label)``
+triples so every producer in the core -- the OwnIR DI checker, the flow-sensitive
+ownership checker, a future XAML->.g.cs join -- emits the same shape and any
+consumer reads one vocabulary. Frontends produce facts; this is how the core
+*explains* its verdicts.
+
+The builders return plain SARIF fragments (no Own.NET types), so they compose
+into either ``ownlang.ownir.build_sarif`` (the C# extractor path) or the audit
+aggregator without a dependency either way.
+
+A step is only emitted when it has BOTH a resolvable line AND a non-empty file:
+an empty ``artifactLocation.uri`` makes the whole SARIF log unprocessable for
+GitHub code scanning, so a caller must resolve any "same file as the anchor"
+convention (e.g. ``diagnostics.Evidence(file=None)``) to a concrete path before
+building -- ``ownir.Finding`` already carries concrete paths.
+"""
+
+from __future__ import annotations
+
+from collections.abc import Iterable
+from typing import Any
+
+# one evidence step: a source location plus the human label for what happens there.
+Step = tuple[str, int, str]   # (file, line, label)
+
+
+def _phys(file: str, line: int) -> dict[str, Any]:
+    """A SARIF ``physicalLocation`` for a 1-based line. ``region`` is omitted for a
+    file-level step (line < 1) so the location stays schema-valid rather than
+    carrying a bogus ``startLine``."""
+    loc: dict[str, Any] = {"artifactLocation": {"uri": file.replace("\\", "/")}}
+    if line >= 1:
+        loc["region"] = {"startLine": line}
+    return loc
+
+
+def related_locations(steps: Iterable[Step]) -> list[dict[str, Any]]:
+    """SARIF ``relatedLocations`` from evidence steps -- the unordered secondary
+    anchors. A step is dropped unless it has both a resolvable line and a non-empty
+    file: a related location with nowhere to point is noise, and an empty
+    ``artifactLocation.uri`` makes the SARIF log unprocessable for GitHub."""
+    return [
+        {"physicalLocation": _phys(f, ln), "message": {"text": label}}
+        for (f, ln, label) in steps if ln >= 1 and f
+    ]
+
+
+def code_flow(steps: Iterable[Step]) -> list[dict[str, Any]]:
+    """A SARIF ``codeFlows`` value (a one-element list) from an *ordered* slice of
+    evidence steps -- the reachability path that leads to the finding. A step is
+    dropped unless it has both a resolvable line and a non-empty file (see
+    ``related_locations``). Returns ``[]`` when no step survives, so a caller can
+    splice the result conditionally (``if flow: result["codeFlows"] = flow``)."""
+    locations: list[dict[str, Any]] = [
+        {"location": {"physicalLocation": _phys(f, ln), "message": {"text": label}}}
+        for (f, ln, label) in steps if ln >= 1 and f
+    ]
+    if not locations:
+        return []
+    return [{"threadFlows": [{"locations": locations}]}]
+
+
+def di_path_steps(path: tuple[str, ...],
+                  loc_by_name: dict[str, tuple[str, int]],
+                  end_label: str) -> tuple[Step, ...]:
+    """Turn a DI dependency *path* (service names, captor first, captured last)
+    into ordered evidence steps anchored at each service's registration site.
+
+    ``loc_by_name`` maps a service name to its ``(file, line)`` registration
+    location; a hop whose location is unknown is skipped (the slice stays ordered
+    and truthful -- a partial registration graph yields a partial, not a wrong,
+    path). The first hop is labelled the captor singleton, the last with
+    ``end_label`` (which differs per family: "captures scoped service", "leaked
+    transient IDisposable", ...), the middle hops as pass-through links.
+
+    This is the concrete reachability slice the DI checker already computes (the
+    ``path`` tuple on every captive finding) but today only renders into the
+    message text -- here it becomes a structured ``codeFlows``.
+    """
+    n = len(path)
+    steps: list[Step] = []
+    for i, name in enumerate(path):
+        loc = loc_by_name.get(name)
+        if loc is None:
+            continue
+        f, ln = loc
+        if i == 0:
+            label = f"singleton '{name}' (captor)"
+        elif i == n - 1:
+            label = f"{end_label} '{name}'"
+        else:
+            label = f"via '{name}'"
+        steps.append((f, ln, label))
+    return tuple(steps)