Research: Doop/Soufflé-style relational points-to and alias analysis (bounded spike) #458

Classification

• Type: bounded research / declarative points-to, alias and call-graph precision spike
• Priority: P2 research backlog; not a production implementation request
• Area: Roslyn semantic facts → OwnIR → existing Rust ownership/dataflow solver → diagnostics/evidence
• Prior art: PLAST Lab Doop (Java/Android pointer and taint analysis with Datalog rules on Soufflé; not a .NET analysis engine); Doop 101; micro rules
• Related, not superseded: Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (WALA/demand-driven aliasing), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (SootUp/IR/ICFG fidelity), Research: Heros-inspired IFDS/IDE feasibility for interprocedural ownership facts (bounded spike) #434 (Heros/IFDS/IDE), Research: Tai-e-inspired semantic fact assertions and selective precision (bounded spike) #443 (Tai-e semantic fact assertions), Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (IKOS abstract-state soundness)
• Default: research/kill-first. Do not port Doop, add a mandatory JVM/Soufflé dependency, rewrite OwnIR or silently change diagnostics.

Why study Doop?

Doop separates fact extraction from declarative, mutually recursive Datalog inference. Its rules derive VarPointsTo, heap-field relationships and call-graph edges, with multiple precision choices (context-insensitive, call-site/object/type sensitive). P/Taint extends the approach to information flow.

Potential transfer to Own.NET is the architecture and validation discipline, not the Java implementation:

1. Make a small, explicit set of existing OwnIR object/alias/call facts inspectable and semantically testable.
2. Evaluate whether relational closure can expose missed interprocedural aliases / dynamic-dispatch edges or provide an independent reference oracle.
3. Measure whether more precise context separation changes ownership verdicts for the right reason.

Important distinctions: may-points-to is not ownership, escape, Dispose semantics or a path-sensitive lifecycle proof. A sound-looking relational closure can still operate on incomplete or incorrectly lowered inputs. Roslyn and the current Own.NET pipeline remain the authoritative C# frontend/baseline.

Bounded experiment (read-only first)

1. Inventory current capability, with code references: what alias identity / fields / call facts / summaries / context sensitivity already exist in Roslyn→OwnIR→Rust? Check relevant Roslyn analysis utilities only as a candidate baseline; confirm accessibility and semantics rather than assuming a drop-in API.
2. Extract 5–8 compact scenarios (positive and negative controls): direct alias; field store/load; parameter/return; virtual/interface dispatch; owning wrapper vs borrowed resource; transfer; duplicate/disjoint resource; opaque/reflection or missing-call edge. Include Dispose and may-alias cases where behavior differs.
3. Build an isolated relational oracle, if useful, using exported tabular OwnIR facts and a minimal Datalog fragment (plain Soufflé CLI optional). No integration, new production engine or pipeline changes. Note that Doop itself cannot directly analyze C#.
4. Differentially compare against current Own.NET output, manually established expected may-alias/call relations and ownership diagnostics. Classify TP/FP/FN, missing facts, context merges and unsupported semantics. Do not mistake larger may-points-to sets for better precision.
5. Cost/complexity: record fact counts, compile/evaluation time, memory, rule complexity and the risk of incomplete closed-world assumptions. Confirm licensing if any code (rather than an idea) is reused.

Deliverables / decision gate

• Short evidence-backed note with upstream code links and version/date; exact Own.NET implementation references; tabular scenario-by-scenario results.
• Identify one smallest useful slice, if any: e.g. a fact-consistency invariant / reference query, targeted alias refinement, or diagnostic explanation. Prefer reuse of existing abstractions and fixtures.
• Explicit GO / CHANGE / KILL, where GO requires a demonstrated Own.NET false negative, false positive, unsoundness exposure or evidence gap not already addressed by Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Research: Heros-inspired IFDS/IDE feasibility for interprocedural ownership facts (bounded spike) #434/Research: Tai-e-inspired semantic fact assertions and selective precision (bounded spike) #443, plus an acceptably cheap implementation path. Otherwise KILL / archive prior art.

Guardrails

• No promises of soundness from Doop/Soufflé by name; precisely track incomplete call graphs, reflection/DI/externals and library summaries.
• Do not conflate reachability, may-alias, ownership, and proof of absence of resource defects.
• Preserve existing tests, CI, issue priority and production architecture until a separately approved change.