Research: Angie/SMG-inspired abstract object graph and sound ownership-state joins (bounded spike) #449

Classification

• Type: bounded research / architecture and correctness spike
• Priority: P3 / backlog; not a production rewrite
• Area: Roslyn → OwnIR → existing ownership/MOS state → alias/resource identity → joins/fixpoint → evidence
• Prior art: VeriFIT/angie (C++/LLVM static-analysis framework, LGPLv3+), Predator and SMG paper
• Related, not superseded: Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429 (WALA / alias precision), Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (IKOS / abstract-state and fixpoint oracle), Research: Fraunhofer CPG-inspired precision escalation and summary-aware soundness gates (bounded spike) #436 (CPG / precision escalation and soundness gates), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (completeness/evidence), Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 (semantic mutation tests), P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 (first divergence), Heap-effect summaries for external code (BCL / annotations) so calls like logging can be proven harmless inside a protocol region #394/Heap-effect summaries: typed write targets, to admit writes provably unrelated to the protected entity #395/Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425 (external effects/model boundaries), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (OwnIR/ICFG semantic fidelity).

Why investigate?

Angie separates an LLVM frontend/CFG from abstract values and a Symbolic Memory Graph (SMG) domain. Its source includes:

• src/Smg/Graph.hpp: memory objects and points-to / has-value edges, allocation, reading, writing, invalid/free handling;
• src/MemoryGraphAnalysis.hpp: memory transfer operations and MemoryGraphAnalysisState;
• src/Smg/Abstraction.hpp: candidate recognition and folding of two concrete regions into a doubly-linked-list segment (DLS);
• src/IState.hpp: abstract state cloning and predecessor relationships;
• src/StateStorage.hpp: worklist/state storage, but equality and join are unimplemented if (false) placeholders.

Caution: this is old research code, not a ready library or soundness oracle. Its last observed commit in the checked branch was Nov 2022; there are explicit unsupported operations (realloc, memcpy, memmove) and SmgIsCmp itself has a comment warning its pointer equality behavior is unsound. The CMake config targets LLVM 5.0. Do not represent the project as production-ready or adopt its semantics without independent proof.

Own.NET-specific question: would a minimal object/alias identity graph plus rigorously specified ownership-state joins resolve a verified ownership false positive/negative or incomplete evidence case that existing OwnIR/MOS cannot already handle? The opportunity is conceptual separation of value/ref identity, object identity, ownership/typestate, and join, not importing C-style raw-memory semantics.

S5 previously reached STOP-SOUNDNESS; an interesting graph is not evidence of net diagnostic utility.

Boundaries and overlap check (mandatory first)

1. Pin current Own.NET commit, analyzer mode(s), and baseline. Inventory existing resource identity/aliases, field/access-path modeling, MOS transfers, branch merges, loop handling, effect summaries, UNKNOWN/INCOMPLETE propagation and evidence.
2. Cross-check Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429, Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433, Research: Fraunhofer CPG-inspired precision escalation and summary-aware soundness gates (bounded spike) #436 and existing ownership/alias work. If the needed mechanism already exists or the first divergence is missing OwnIR facts/models, close NO-GAP or route to the owner issue. Do not duplicate an alias engine, fixpoint solver, or CPG/evidence graph.
3. Pin Angie commit (e.g. cf85a6abe4c8553b99f9f90b58c22d1c628af7d2) and record exactly which mechanisms are implemented vs TODO. Treat Predator/papers as separate prior art, not features implicitly provided by Angie.

Bounded experiment

Only proceed past inventory if there is one independently adjudicated, reproducible case whose first divergence plausibly involves alias/object identity or branch join.

1. Preregister ~10–20 focused C# positive/negative/adversarial fixtures drawn preferentially from existing regression tests plus at least one real source case if available. Include two aliases to one IDisposable, Dispose through an alias, conditional disposal, repeated dispose, owner transfer through a field/wrapper, distinct objects, using/try-finally, unresolved/opaque callee, loop, and exception edge only where OwnIR faithfully models it.
2. Specify on paper a minimal abstract domain: resource identity, may/must aliases, Alive/Disposed/MaybeDisposed/Unknown (illustrative, not prescribed public states), transfer functions, partial order, join, widening/termination policy if needed, and allocation-site/instance identity limitations. Prove/check the required lattice and monotonicity properties; explain why maybe cannot become must.
3. If justified, implement a test-only or narrowly scoped opt-in reference consuming existing OwnIR facts. No LLVM port, native interop, C++ graph library, new production analyzer architecture or solver by default.
4. Contrast baseline and candidate on correctness, not graph size: adjudicated TP/FP/FN, any false-safe promotion, evidence path feasibility, unknown/incomplete cases, first divergence, runtime, state count and memory. Use Research: semantic mutation testing harness for Own.NET analyzer coverage (bounded pilot) #405 mutation/falsification controls and P-022 diagnostics: normalized AnalysisTrace and first-divergence minimizer for Python↔Rust shadow mode #269 instrumentation where appropriate.
5. Explicitly test worklist exhaustion, unmodeled effects, alias ambiguity and joined branches. A missed path / budget cutoff / unsupported construct must never be interpreted as PROVEN_SAFE.

Acceptance / terminal ruling

• Source-pinned Angie implementation audit with explicit TODO/unsupported/unsound cases.
• Own.NET inventory and non-overlap assessment against Research: WALA-inspired demand-driven alias precision for ownership diagnostics (bounded spike) #429/Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433/Research: Fraunhofer CPG-inspired precision escalation and summary-aware soundness gates (bounded spike) #436.
• One independently confirmed baseline failure or documented NO-GAP.
• Formal description of the minimal graph/domain/join, including may-vs-must, soundness assumptions, exceptions/opaque calls and convergence limits.
• Reproducible bounded comparison with baseline, adversarial mutations and first-divergence evidence, if a prototype is warranted.
• ACCEPT-NARROW-FOLLOWUP only for demonstrated improvement without false-safe regression and acceptable cost; otherwise NO-GAP, NO-BENEFIT, UPSTREAM-FACT-GAP or STOP-SOUNDNESS.

Non-goals

No direct Angie/Predator dependency, no LGPL code copying without license review, no LLVM frontend, no simulation of native malloc/free as C# IDisposable, no wholesale alias/points-to rewrite, no automatic public verdict promotions, no rewriting the existing Python/Rust engines by default.

References

• https://github.com/VeriFIT/angie
• https://github.com/VeriFIT/angie/blob/master/src/Smg/Graph.hpp
• https://github.com/VeriFIT/angie/blob/master/src/Smg/Abstraction.hpp
• https://github.com/VeriFIT/angie/blob/master/src/MemoryGraphAnalysis.hpp
• https://github.com/VeriFIT/angie/blob/master/src/StateStorage.hpp
• https://github.com/VeriFIT/angie/blob/master/src/IState.hpp
• https://github.com/kdudka/predator