Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

fix(check): GREEN — over-strict-mode recognises ctor-rebuild-from-primitive-fields as a consume

Browse Source 
Drives the RED test from a11cb7c to GREEN. Bug-fix iter
bugfix-over-strict-mode-ctor-rebuild-consume (debug -> implement
mini). Check-only lint-precision fix; zero codegen / runtime / ABI /
schema / DESIGN.md change.

The [over-strict-mode] lint's consume-detection
(any_sub_binder_consumed_for / pattern_has_consumed_heap_binder,
crates/ailang-check/src/linearity.rs) only recognised a consume of an
(own (con T)) param when a heap-typed pattern-binder was moved out of
`match p`. When p was destructured into purely primitive fields fed
into a Term::Ctor rebuilding p's own ctor, that genuine
dismantle+rebuild consume was invisible, so the lint spuriously
advised "(borrow ...) would suffice". An LLM author "fixing" that by
flipping an export own->borrow would silently invert the ABI
ownership contract — why a low-severity advisory FP got a real
RED-first fix.

Fix: a second recognition path in any_sub_binder_consumed_for — a
`match p` arm destructuring binders out of p's ctor that references
any of them (primitive or not) inside a Term::Ctor's args in the arm
body genuinely consumes p. Two pure helpers: ctor_uses_any_binder
(finds a fresh-allocation Term::Ctor reachable in the arm body) +
term_mentions_any_binder (deep free-var scan, so binder flow through
an intervening expr like (+ acc px) is recognised, not only a bare
Var arg). Conservative toward NOT suppressing: a ctor ignoring p's
payload still warns (negative-control verified). Over-strict-only —
by-name-shadowing imprecision is extra-silence, never under-strict
(Known debt in the journal + the fn doc). The two stale doc comments
that mis-attributed this FP to a nested `match` corrected for
doc-honesty (debugger concern #2 — same code region, in-scope).

Boss-verified independently: RED test now GREEN; full
cargo test -p ailang-check 108/0 lib + every binary 0-failed with NO
existing test modified; ail check examples/embed_backtest_step_tick.ail
no longer warns over-strict on st/tick (exit 0);
embed_backtest_step_tick_borrow.ail + M3 embed_backtest_step_record.ail
still clean; embed_tick_e2e + bench posture untouched.

+166/-20 in crates/ailang-check/src/linearity.rs only. Journal +
stats + INDEX line in this commit.
This commit is contained in:
Brummel
2026-05-18 23:50:13 +02:00
parent a11cb7cc9f
commit 208d7095bc
4 changed files with 254 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/linearity.rs
+166 -20
View File
@@ -116,16 +116,28 @@
//! `match xs { Cons(h, t) => h }` returns `h: Int`; without the
//! filter, `h.consume_count == 1` would silence the lint.
//!
//! **Known debt: deeply-nested-match-on-sub-binder.** A pattern like
//! `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`
//! has the inner match's scrutinee `t` (not `p`), so the inner-arm
//! binder `t2`'s consume is not seen when we ask "did any arm-binder
//! of `match p` get consumed?". The outer-arm binder `t` has
//! `consume_count == 0` (matching is Borrow), so the lint will fire
//! even though `(own T)` is genuinely needed because `t2` is
//! consumed. This is recorded in the JOURNAL as a follow-up; for the
//! current corpus it would cost a spurious warning rather than miss
//! a real one.
//! ### Bugfix `over-strict-mode-ctor-rebuild-consume`
//!
//! The heap-typed-sub-binder check above does not see the consume
//! when an arm destructures `p`'s ctor into *primitive* fields and
//! then feeds them into a `Term::Ctor` that rebuilds an allocation —
//! e.g. `match p { State(acc, n) => State(acc, n) }`, or the nested
//! `match st { State(acc, n) => match tick { Tick(px) => State(..) } }`
//! body of `embed_backtest_step_tick`. The rebuild dismantles `p`'s
//! box and re-packages its payload into a fresh allocation; with
//! `(borrow ...)` the scrutinee's box could not be taken apart, so
//! `(own ...)` is genuinely required and the lint must stay silent.
//! `pattern_has_consumed_heap_binder` filters the primitive binders
//! out, so it could not catch this. The fix adds a second
//! recognition path (`collect_pattern_binders` +
//! `ctor_uses_any_binder`):
//! if a destructured binder of the matched arm — primitive or not —
//! is referenced by any `Term::Ctor` in the arm body, the param is
//! consumed. An earlier draft of this note mis-attributed the
//! false-positive to deeply-nested `match`-on-sub-binder; that was a
//! misdiagnosis. The defect is the unrecognised ctor-rebuild
//! consume, independent of match nesting, and it caused a *spurious*
//! warning (over-strict), never a missed one.
use crate::diagnostic::Diagnostic;
use crate::uniqueness::{infer_module as infer_uniqueness, UniquenessTable};
@@ -840,16 +852,24 @@ fn make_use_after_consume_at_reuse_as(def: &str, binder: &str, body: &Term) -> D
/// `match p ...` may sit arbitrarily deep inside `If` / `Let` /
/// `App` / etc.
///
/// **Known limit (recorded as debt in JOURNAL.md):** if an arm's
/// body contains a *nested* match on a sub-binder of `p` (e.g.
/// `match p { Ctor(_, t) => match t { Ctor(_, t2) => consume(t2) } }`),
/// we only check `t.consume_count`, not `t2.consume_count`. The
/// inner match's scrutinee is `t`, not `p`, and our recursion looks
/// for `match-on-pname`, so we miss `t2`. For the current corpus
/// this would mean a *spurious* warning (the lint fires but `(own)`
/// is genuinely needed), not a missed one. The fix is to either
/// chase pattern-binder lineage or to check inner matches whose
/// scrutinee transitively traces back to `p`.
/// **Ctor-rebuild consume (bugfix
/// `over-strict-mode-ctor-rebuild-consume`):** besides a heap-typed
/// sub-binder being moved out, the param is also genuinely consumed
/// when an arm destructures `p`'s ctor and feeds the extracted
/// fields — *including purely primitive ones* — into a `Term::Ctor`
/// that builds a fresh allocation (e.g.
/// `match p { State(acc, n) => State(acc, n) }`, or the nested
/// `match st { State(acc, n) => match tick { Tick(px) => State(..) } }`
/// shape of `embed_backtest_step_tick`). The rebuild dismantles
/// `p`'s box and re-packages its payload, which `(borrow ...)` could
/// not do, so `(own ...)` is required. `pattern_has_consumed_heap_binder`
/// misses this because the destructured fields are primitive; the
/// `collect_pattern_binders` + `ctor_uses_any_binder` pair below
/// recognises it. The earlier draft of this comment mis-attributed
/// the defect
/// to a nested `match` on a sub-binder of `p`; the real mechanism is
/// the unrecognised ctor-rebuild consume, independent of match
/// nesting.
fn any_sub_binder_consumed_for(
t: &Term,
pname: &str,
@@ -865,6 +885,20 @@ fn any_sub_binder_consumed_for(
if pattern_has_consumed_heap_binder(&arm.pat, uniq, def_name, ctors) {
return true;
}
// Ctor-rebuild consume: destructuring `p`'s ctor
// and feeding the extracted fields (incl.
// primitive ones) into a `Term::Ctor` builds a
// fresh allocation out of `p`'s dismantled
// payload. That genuinely consumes the `(own)`
// scrutinee — `(borrow)` could not dismantle it.
// `pattern_has_consumed_heap_binder` misses this
// because the destructured fields are primitive.
let destructured = collect_pattern_binders(&arm.pat);
if !destructured.is_empty()
&& ctor_uses_any_binder(&arm.body, &destructured)
{
return true;
}
// Recurse into the arm body: a deeper
// `match p ...` could also count.
if any_sub_binder_consumed_for(&arm.body, pname, uniq, def_name, ctors) {
@@ -990,6 +1024,118 @@ fn pattern_has_consumed_heap_binder_at(
}
}
/// Bugfix `over-strict-mode-ctor-rebuild-consume`: `true` iff some
/// `Term::Ctor` reachable in `t` builds a fresh allocation whose
/// argument subtrees mention at least one of `binders` (the names
/// the matched arm destructured out of `p`'s ctor). That means the
/// dismantled payload of the `(own)` scrutinee — possibly via an
/// intervening expression such as `(+ acc px)` — flows into a newly
/// allocated ctor, which `(borrow ...)` could not do (a borrowed
/// value's box may not be taken apart and re-packaged). So `(own)`
/// is genuinely required and the lint must stay silent.
///
/// Conservative toward *not* suppressing: the ctor's args must
/// actually reference a destructured binder. A ctor that ignores
/// `p`'s payload (e.g. `match p { _ => Other(42) }`, or
/// `match p { P(x) => Other(42) }`) does **not** trip this and the
/// lint still warns. The binder scan is by name; a destructured
/// primitive binder shadowed and rebound before reaching the ctor
/// is not a corpus shape, and any resulting imprecision is in the
/// over-strict (extra-silence) direction the cause explicitly
/// permits, never under-strict.
fn ctor_uses_any_binder(t: &Term, binders: &[String]) -> bool {
match t {
Term::Ctor { args, .. } => {
// A freshly-built allocation: does its payload draw from
// the destructured binders (at any depth)? Also recurse
// — a ctor may be nested inside another ctor's args.
args.iter().any(|a| term_mentions_any_binder(a, binders))
|| args.iter().any(|a| ctor_uses_any_binder(a, binders))
}
Term::Lit { .. } | Term::Var { .. } => false,
Term::Match { scrutinee, arms } => {
ctor_uses_any_binder(scrutinee, binders)
|| arms.iter().any(|a| ctor_uses_any_binder(&a.body, binders))
}
Term::App { callee, args, .. } => {
ctor_uses_any_binder(callee, binders)
|| args.iter().any(|a| ctor_uses_any_binder(a, binders))
}
Term::Let { value, body, .. } => {
ctor_uses_any_binder(value, binders) || ctor_uses_any_binder(body, binders)
}
Term::LetRec { body, in_term, .. } => {
ctor_uses_any_binder(body, binders) || ctor_uses_any_binder(in_term, binders)
}
Term::If { cond, then, else_ } => {
ctor_uses_any_binder(cond, binders)
|| ctor_uses_any_binder(then, binders)
|| ctor_uses_any_binder(else_, binders)
}
Term::Seq { lhs, rhs } => {
ctor_uses_any_binder(lhs, binders) || ctor_uses_any_binder(rhs, binders)
}
Term::Do { args, .. } => args.iter().any(|a| ctor_uses_any_binder(a, binders)),
Term::Lam { body, .. } => ctor_uses_any_binder(body, binders),
Term::Clone { value } => ctor_uses_any_binder(value, binders),
Term::ReuseAs { source, body } => {
ctor_uses_any_binder(source, binders) || ctor_uses_any_binder(body, binders)
}
Term::Loop { binders: lb, body } => {
lb.iter().any(|b| ctor_uses_any_binder(&b.init, binders))
|| ctor_uses_any_binder(body, binders)
}
Term::Recur { args } => args.iter().any(|a| ctor_uses_any_binder(a, binders)),
}
}
/// Bugfix `over-strict-mode-ctor-rebuild-consume`: deep free-variable
/// scan — does `t` mention any name in `binders` anywhere in its
/// subtree (as a `Var`, possibly under `Clone` / `App` / arithmetic /
/// nested ctor / …)? Used to test whether a `Term::Ctor`'s argument
/// draws, directly or through an intervening expression, from the
/// destructured payload of the matched `(own)` param.
fn term_mentions_any_binder(t: &Term, binders: &[String]) -> bool {
match t {
Term::Var { name } => binders.iter().any(|b| b == name),
Term::Lit { .. } => false,
Term::Ctor { args, .. } | Term::Do { args, .. } | Term::Recur { args } => {
args.iter().any(|a| term_mentions_any_binder(a, binders))
}
Term::App { callee, args, .. } => {
term_mentions_any_binder(callee, binders)
|| args.iter().any(|a| term_mentions_any_binder(a, binders))
}
Term::Match { scrutinee, arms } => {
term_mentions_any_binder(scrutinee, binders)
|| arms.iter().any(|a| term_mentions_any_binder(&a.body, binders))
}
Term::Let { value, body, .. } => {
term_mentions_any_binder(value, binders) || term_mentions_any_binder(body, binders)
}
Term::LetRec { body, in_term, .. } => {
term_mentions_any_binder(body, binders) || term_mentions_any_binder(in_term, binders)
}
Term::If { cond, then, else_ } => {
term_mentions_any_binder(cond, binders)
|| term_mentions_any_binder(then, binders)
|| term_mentions_any_binder(else_, binders)
}
Term::Seq { lhs, rhs } => {
term_mentions_any_binder(lhs, binders) || term_mentions_any_binder(rhs, binders)
}
Term::Lam { body, .. } => term_mentions_any_binder(body, binders),
Term::Clone { value } => term_mentions_any_binder(value, binders),
Term::ReuseAs { source, body } => {
term_mentions_any_binder(source, binders) || term_mentions_any_binder(body, binders)
}
Term::Loop { binders: lb, body } => {
lb.iter().any(|b| term_mentions_any_binder(&b.init, binders))
|| term_mentions_any_binder(body, binders)
}
}
}
/// Iter 19a: a scrutinee "is" `pname` if it's a bare `Var { pname }`
/// or `Clone(Var { pname })`. Anything else (a fresh App result, a
/// let-binder, …) does not put `pname` directly in scrutinee