Module solver 

Datafrog-based NLL borrow solver.

Implements Non-Lexical Lifetimes using Datafrog’s monotone fixed-point engine. This is the core of Shape’s borrow checking — it determines which borrows are alive at each program point and detects conflicts.

Single source of truth: This solver produces BorrowAnalysis, which is consumed by the compiler, LSP, and diagnostic engine. No consumer re-derives results.

The Datafrog pattern

Datafrog is a lightweight Datalog engine that computes fixed points over monotone relations. The pattern used here is:

1. Define input relations — static facts extracted from MIR that never change during iteration (e.g. cfg_edge, invalidates).
2. Define derived variables — monotonically-growing sets computed by Datafrog’s iteration engine (e.g. loan_live_at).
3. Seed the derived variable with initial facts (each loan is live at its issuance point).
4. Express rules as from_leapjoin calls inside a while iteration.changed() loop. Each rule joins a derived variable against input relations and produces new tuples. Datafrog deduplicates and tracks whether any new tuples were added (the changed() check).
5. Convergence: Because all relations are sets of tuples and rules only add (never remove), the iteration terminates when no new tuples are produced — the monotone fixed point.
6. Post-processing: After convergence, the derived relation is .complete()-d into a frozen Relation and scanned for error conditions.

Input relations (populated from MIR)

• loan_issued_at(Loan, Point) — a borrow was created
• cfg_edge(Point, Point) — control flow between points
• invalidates(Point, Loan) — an action invalidates a loan
• use_of_loan(Loan, Point) — a loan is used (the ref is read/used)

Derived relations (Datafrog fixpoint)

• loan_live_at(Loan, Point) — a loan is still active
• error(Point, Loan, Loan) — two conflicting loans are simultaneously active

Additional analyses

• Post-solve relaxation: solve() skips ReferenceStoredIn* errors when the container slot’s EscapeStatus is Local (never escapes).
• Interprocedural summaries: extract_borrow_summary() derives per-function conflict pairs for call-site alias checking.
• Task-boundary sendability: Detects closures with mutable captures crossing detached task boundaries (B0014).

Structs

BorrowFacts

Input facts extracted from MIR for the Datafrog solver.

SolverResult

Raw solver output (before combining with liveness for full BorrowAnalysis).

Functions

analyze

extract_borrow_summary

Run the complete borrow analysis pipeline for a MIR function. This is the main entry point — produces the single BorrowAnalysis consumed by compiler, LSP, and diagnostics. Extract a borrow summary for a function — describes which parameters are borrowed and which parameter pairs must not alias at call sites.

extract_facts

Populate borrow facts from a MIR function and its CFG.

solve

Run the Datafrog solver to compute loan liveness and detect errors.

Type Aliases

CalleeSummaries

Callee return-reference summaries, keyed by function name.