Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429

Classification

• Type: bounded research / algorithmic prior-art spike
• Priority: P2 / backlog; not a request to port WALA or ship a new solver
• Area: OwnIR resource identity / aliasing / call-context precision → ownership diagnostics
• Prior art: wala/WALA (T.J. Watson Libraries for Analysis, primarily Java/Android/JavaScript; no drop-in C#/.NET frontend)
• Related Own.NET: Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (first-party call facts), Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 (opaque library summaries), Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395 (typed heap-write targets), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutants and oracle checks), Research: semantic subgroup analysis for Own.NET diagnostic quality (bounded pilot) #427 (semantic subgroup evaluation), Research: evaluate Tabby-style stateful path pruning for bounded ownership diagnostics #424 (Tabby path-state research), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (evidence/completeness contract), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first-divergence instrumentation)

Problem / motivation

Own.NET should not add another general-purpose analysis engine merely because a mature research framework exists. In particular, S5 exposed a soundness problem and showed no demonstrated marginal utility over C01 on evaluated real applications. Before any alias/points-to infrastructure work, establish that a concrete, confirmed Own.NET false negative or false positive is caused by insufficient resource identity, alias, or call-context precision, as opposed to lost Roslyn facts, a missing method summary, incorrect transfer rules, or an invalid test oracle.

WALA is interesting as design prior art, especially its separation between object abstraction policy, call contexts, and propagation/refinement, plus its demand-driven points-to analysis, IFDS tabulation and program slicing. It does not supply ownership/disposal semantics for .NET, and IFDS/points-to alone cannot prove a resource-lifetime property.

Research question: Can a small, budgeted precision escalation on existing OwnIR facts recover a previously missed, independently verified ownership finding, reject a documented false positive, or materially improve a reproducible witness, compared with the current analyzer, at acceptable runtime/memory cost without any unsupported safety claims?

Source areas worth inspecting (pin WALA commit/tag in report)

• ZeroXInstanceKeys: class-based vs. allocation-site abstraction, selective collapsing of instances.
• DemandRefinementPointsTo: demand-driven queries and refinement policy/budgets.
• TabulationSolver and BoundedTabulationSolver: interprocedural fact propagation and budget behavior.
• Slicer: context-sensitive slices via an SDG, dependent on preliminary pointer analysis.

Do not treat WALA's algorithm, performance or soundness guarantees in its source language as a guarantee for a new C# model.

Bounded plan

0. Gap inventory and pre-registration: stop early if there is nothing real to fix

• Inspect a small set of existing reviewed real-OSS and minimized positive/negative Own.NET cases, including Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405/Research: semantic subgroup analysis for Own.NET diagnostic quality (bounded pilot) #427 oracles where available.
• Find at least one independently verified diagnostic discrepancy plausibly attributable specifically to alias/resource identity or call-context abstraction. Prefer two contrasting failures.
• For each, pin source snapshot, expected source-level semantics, expected finding/site, current observed finding/evidence, and a causal hypothesis.
• Determine whether Roslyn → OwnIR already preserved allocation sites, receiver/argument bindings, reference assignments, heap writes, direct/virtual call targets, and relevant exception edges. Facts absent from OwnIR cannot be reconstructed by a solver. If Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 or Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395 blocks the case, classify it as a representation gap and stop, rather than smuggling a frontend rewrite into this spike.
• Exclude cases that are actually model gaps (Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394/Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425), oracle errors, or unreachable/invalid mutants.

1. Compare minimal precision strategies offline

Using the existing pipeline (no production changes by default), attempt the cheapest applicable distinctions one at a time:

1. Baseline: current Own.NET identity/alias and call-summary behavior.
2. Allocation-site-sensitive abstraction: distinguish resource instances created at different sites, while recording joins/escapes that may merge them.
3. Selective call-context refinement, only if needed: distinguish a bounded number of caller/call-site contexts or resource-specific flows for the problematic query. Account for virtual/unknown dispatch explicitly.

Retain clear identity/alias semantics (must-alias, may-alias, definitely-distinct, unknown) and do not equate no proven alias with proven disjointness. Resource release, borrow, transfer, escape, exceptional paths and field/array aliasing must use appropriate may/must rules.

Implement the prototype only at the smallest seam required to test the hypothesis; compare behavior before considering a general-purpose points-to graph, IFDS/IDE port, or whole-program call graph.

2. Adversarial controls

Create/reuse a small reviewed micro-corpus (roughly 10–16 cases, not a synthetic scoreboard), covering where applicable:

• two instances of the same disposable type and calls sharing a callee;
• definite alias versus separate allocation; reassignment and phi/branch merge;
• receiver vs argument identity; ownership transfer / escape;
• field/array/container aliases and unknown heap effects;
• direct vs virtual/interface calls and unresolved targets;
• guarded Dispose, use-after-dispose, double dispose, missing release;
• exceptional path or try/finally, plus one negative near-neighbor.

Compile C# cases and inspect actual OwnIR lowering. Do not count a generated case as ground truth until independently adjudicated. Preserve individual results, not just a pooled score.

3. Budget, uncertainty, and soundness contract

• Explicitly distinguish witness found, complete bounded negative, unknown due to model/dispatch, incomplete due to limit, and unsupported/failed execution. A timed-out or budget-exhausted search is not evidence of no defect.
• Prototype refinements must not suppress existing confirmed positives or silently turn unknown into safe. Test deliberate budget truncation and incomplete traversal.
• Make any performance claims conditional on measurements: wall time, peak RSS, number of visited states/context variants, and cost of initial graph construction, on pinned fixtures and a small real-OSS subset.
• Check deterministic outcomes and, if relevant, Python/Rust parity without broadening P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269.

4. Compare to baseline; issue a go/no-go

Report per-case baseline vs. refinement: expected outcome, actual outcome, FP/FN, proof/witness status, uncertainty/completeness, time and memory. Separate better explanatory slices from better detection. Confirm each apparently new finding by independent C# semantics/reproduction, not the prototype's own output.

GO for a separate implementation issue only if at least one previously missed/false diagnostic is demonstrably fixed by the tested abstraction, negative controls remain correct, uncertainty stays explicit, and measured cost is justified. Otherwise NO-GO / research only.

Acceptance

• Source-backed design note pinned to WALA version/commit, with exact transferable ideas and .NET limitations.
• Reviewed gap inventory; classify each candidate as identity/alias precision, lost lowering facts, missing model, transfer error, unsupported case, or bad oracle.
• A minimal reproducible baseline-versus-refinement experiment if an eligible real gap exists, or an early NO-GO with evidence if none does.
• Reviewed positive, negative, and adversarial controls, with source/OwnIR snapshots and exact commands.
• Explicit incomplete/unknown outcomes tested under truncation; no new unproven “safe” verdicts.
• Per-case accuracy/witness and resource-cost comparison, without fabricated precision/recall rates from tiny samples.
• Final GO / NO-GO / RESEARCH ONLY verdict and, only on GO, a separate narrowly scoped implementation issue.

Non-goals

No WALA/Java runtime dependency, Roslyn frontend replacement, broad OwnIR redesign, generic IFDS/IDE or concolic engine, unbounded program slicing, wholesale heap graph, new default CI gate, or implicit production diagnostic changes. Do not duplicate #424/#426 evidence/path work or #394/#395 summaries. This is an experiment to establish incremental diagnostic utility, not an infrastructure project looking for justification.

Success means validated improvement on a real ownership problem. A sophisticated solver that still finds nothing new is a STOP.