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.

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

Structs

BorrowFacts

Input facts extracted from MIR for the Datafrog solver.

SolverResult

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

Functions

analyze

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_facts

Populate borrow facts from a MIR function and its CFG.

solve

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