Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430

Classification

• Type: bounded research / semantic-pipeline integrity spike
• Priority: P2 / backlog; no production implementation by default
• Area: Roslyn lowering → OwnIR → CFG/ICFG and call frontier → existing ownership state/diagnostics
• Prior art: soot-oss/SootUp (Jimple IR, multiple Views, call-graph scope, interprocedural IFDS/IDE via Heros, typestate example, Qilin pointer analysis)
• Default decision: do not adopt SootUp/Heros, port Jimple, replace OwnIR, or introduce a general-purpose typestate engine
• Related Own.NET: Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (WALA: alias/call-context precision), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation harness), Research: semantic subgroup analysis for Own.NET diagnostic quality (bounded pilot) #427 (semantic subgroup scoring), Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (opaque method effects), Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394 (trusted external summaries), Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (canonical call facts), 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 / trace)

Motivation

S5 ended in STOP-SOUNDNESS and did not demonstrate better practical yield than C01 on the evaluated real programs. More solver sophistication is not the next default move. First, determine whether the existing ownership conclusions are based on faithfully represented C# semantics.

SootUp provides useful design prior art, not a .NET-ready analyzer:

• Its pipeline separates frontend → Jimple IR → (interprocedural) CFG/call graph → analyses.
• Its CallGraphScope can deliberately stop expanding library/excluded methods. Crucially, the edge into an excluded method can remain while outgoing edges disappear. ExcludedCallsCollectingCallGraphScope records methods excluded from expansion, making that boundary inspectable.
• Its executable Heros/IDE typestate example explicitly distinguishes facts (tracked values) from automaton states, maps parameters/results across calls, and documents how call/return flow and joins can silently produce wrong answers if modeled incorrectly.
• The typestate example's ICFG switches exceptional flow off. A successful sample therefore cannot be assumed to establish correct C# try/finally, exceptions, disposal, or async semantics.
• Qilin's Java points-to machinery is not a drop-in C# alias engine; alias refinement already has a separate owner in Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429.

Research question: Are there independently reviewable Own.NET false negatives, false positives, or unjustified “safe/no finding” conclusions caused by lost/misrepresented frontend or interprocedural facts (rather than solver precision or external models)? Can we expose those losses and prevent them from silently turning into a stronger conclusion, without a new analysis architecture?

Scope boundaries / overlap

This issue owns pipeline fidelity and visibility of analysis boundaries, not:

• a new alias/points-to algorithm (Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429);
• a new mutation framework (Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405), subgroup dashboard (Research: semantic subgroup analysis for Own.NET diagnostic quality (bounded pilot) #427), or diagnostic evidence schema (Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426);
• wholesale method-effect inference (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);
• new detection families, global call graph, or IFDS/IDE migration.

Reuse existing tests, traces, snapshots, and result states where possible. If a case belongs to another issue, link it with reproduction evidence and do not reimplement its work here.

Bounded investigation

0. Snapshot and preregister

• Pin Own.NET repository commit, extractor/engine mode, commands, OS/runtime and representative fixtures.
• Pin a SootUp tag/commit and the relevant source/docs; verify what features actually run, rather than assuming documentation examples are universal correctness claims.
• Select 8–12 already available, reviewed C# positives/negatives or minimized real-OSS counterexamples; do not create a large new fixture suite without evidence of a gap.
• Register expected source-level behavior and a hypothesis before reading analyzer output. Include at least one definite-positive ownership misuse and its near-negative.

1. Source → OwnIR preservation audit

Trace each chosen case through source/Roslyn, emitted OwnIR, CFG/ICFG or existing call representation, transfer/summary logic, and final output. At minimum consider:

• allocation/resource identity, assignment, receiver and argument bindings, return/escape;
• direct, overloaded, interface/virtual and unresolved calls; first-party vs external bodies;
• branch/phi and reachability, guarded cleanup, using / try/finally / exceptional exits;
• partial type/method bodies and cross-file teardown when relevant;
• heap effects and event subscriptions where represented.

Produce an edge/fact preservation ledger for each case: represented correctly, conservatively summarized, omitted, incorrect, or unsupported, with exact source/OwnIR excerpts. Do not infer an absent fact merely from a missing final diagnostic; locate the first demonstrated divergence. Classify faults as frontend/lowering, call frontier, model/summary, transfer/join, oracle, or unsupported.

2. Analysis frontier / completeness experiment

Use SootUp's excluded-call visibility as a reference for an offline audit, not an instruction to copy its types or schema.

On 2–3 deliberately incomplete cases, determine whether the current Own.NET pipeline can tell apart:

1. a resolved/analyzed first-party call;
2. a known call into a method whose body/edges were not explored;
3. multiple possible virtual/interface targets, with at least one unresolved;
4. unsupported/missing source, timeout/budget, or failure.

Try one controlled omission/truncation that would otherwise hide a known-positive misuse. Record whether it results in incomplete/unknown (or existing equivalent), is honestly reported as an unsupported limitation, or becomes a misleading clean/safe conclusion.

No scope expansion is the same as proof of no effects. If #426 already provides the necessary representation, report its behavior instead of proposing another field.

3. Minimal state-transition cross-check (conditional)

Only if step 1 finds an actionable bug or uncertainty in existing resource-state transfers, model one tiny protocol offline: e.g. Alive → Released, Use(Released), DoubleRelease, with Escaped/Unknown handled explicitly. Compare the current analyzer with a manually reviewed transition table over a direct call, one helper call and one alias/branch case. Inspect call-to-start, return, call-to-return bypass, join, and (where applicable) exceptional edges.

SootUp's IDE typestate example is a checklist for analysis obligations, not a claim that IFDS/IDE improves detection here. Do not port Heros or add new protocol syntax. If an existing Own.NET test covers it and passes, record that and stop.

4. Perturbation controls using #405

Use the existing semantic-mutation/metamorphic harness where available, with 2–4 meaning-preserving transformations (e.g. rename local, extract helper, equivalent conditional rewriting) and 2–4 reviewed bug-inducing changes (e.g. remove valid release, wrong-instance release, reassign alias, skip cleanup on an exceptional path). Keep source-level ground truth distinct from the analyzer's expectations.

For each transformation, determine whether the source semantics, OwnIR facts, diagnostic identity/evidence, and completeness changed in a justified way. Do not build a second mutation runner.

5. Comparison, cost, disposition

• Baseline vs audit/prototype per case: expected behavior, exact first divergence, present diagnostic, FP/FN/unknown, witness quality, method frontier, snapshot/reproduction.
• Any optional local instrumentation must be non-semantic and low-impact; measure wall time and peak memory only if a prototype is actually built. Avoid synthetic aggregate accuracy claims from tiny samples.
• Do not suppress previously confirmed findings, turn unknown into safe, or change production default diagnostics in this issue.
• Conclude STOP / RESEARCH ONLY / FOLLOW-UP CANDIDATE. A follow-up implementation issue needs at least one independently verified, product-relevant failure with a minimal causal fix, negative controls, and measured costs where applicable.

Acceptance

• SootUp feature/reference note pinned to exact source/version, distinguishing Java-specific machinery from transferable audit practices.
• 8–12 reviewed C# cases with reproducible source snapshot, Roslyn/OwnIR evidence and expected outcomes (reuse existing cases whenever possible).
• Per-case preservation ledger and first-divergence classification; explicit no gap observed is valid.
• At least two incomplete-call/control examples assessed, including one deliberate missing-edge/unsupported case; document whether a false “clean” verdict is possible.
• Conditional minimal typestate comparison only if a state-transfer gap is reproduced; otherwise mark not justified.
• Mutation/metamorphic cross-check reuses Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405, or explicitly documents why currently unavailable.
• No new unsupported proof/safety claims and no duplicate evidence/completeness system.
• Final GO/NO-GO-style disposition with reproducible evidence and a narrowly specified follow-up only if justified.

References

• SootUp repository / architecture
• Call-graph scoping and ExcludedCallsCollectingCallGraphScope
• Executable interprocedural IDE typestate example
• SootUp Jimple and frontend overview

Success is a reproducible semantic gap found (or convincingly ruled out) and an honest boundary on what the analyzer knows. An elegant new solver without a validated improvement is a STOP.