diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index c2c48f7..e769782 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -629,11 +629,28 @@ impl<'a> Checker<'a> { Term::Match { scrutinee, arms } => { // Scrutinee is read (Borrow), not moved. self.walk(scrutinee, Position::Borrow); + // Determine whether the scrutinee is a borrowed binder: + // a bare `Var` resolving (through `let`-aliases) to a + // tracked binder whose `borrow_count > 0`. A heap-typed + // sub-binder extracted from a borrowed scrutinee aliases + // the caller-owned interior, so it must inherit the + // borrow (mirroring the `Borrow`-param seeding in + // `check_fn`). Any non-`Var` scrutinee is owned/fresh. + let scrutinee_borrowed = match scrutinee.as_ref() { + Term::Var { name } => { + let root = self.resolve_alias(name); + self.binders + .get(&root) + .map(|s| s.borrow_count > 0) + .unwrap_or(false) + } + _ => false, + }; let saved = self.binders.clone(); let mut acc: Option> = None; for arm in arms { self.binders = saved.clone(); - self.walk_arm(arm, pos); + self.walk_arm(arm, pos, scrutinee_borrowed); match acc.as_mut() { None => acc = Some(self.binders.clone()), Some(m) => merge_states(m, &self.binders), @@ -770,15 +787,23 @@ impl<'a> Checker<'a> { /// are linearity-fresh in 18c.2; we do not yet track ownership /// transfer from the scrutinee (that requires modelling pattern /// borrow vs. consume, which is 18c.3 work). - fn walk_arm(&mut self, arm: &Arm, pos: Position) { + fn walk_arm(&mut self, arm: &Arm, pos: Position, scrutinee_borrowed: bool) { let names = collect_pattern_binders(&arm.pat); let mut value_names: Vec = Vec::new(); collect_value_pattern_binders(&arm.pat, None, self.ctors, &mut value_names); let mut saved: HashMap> = HashMap::new(); for n in &names { saved.insert(n.clone(), self.binders.remove(n)); + let is_value = value_names.contains(n); let st = BinderState { - is_value: value_names.contains(n), + is_value, + // A heap-typed sub-binder of a borrowed scrutinee aliases + // the caller-owned interior; seed `borrow_count = 1` so + // consuming it fires `consume-while-borrowed`, mirroring + // the `Borrow`-param seeding in `check_fn`. Value-typed + // sub-binders (e.g. `Int h`) are copied out — no heap + // alias — so they stay freely consumable at `0`. + borrow_count: if scrutinee_borrowed && !is_value { 1 } else { 0 }, ..BinderState::default() }; self.binders.insert(n.clone(), st); @@ -2239,6 +2264,152 @@ mod tests { ); } + /// helper: a fn `sink : (own IntList) -> Int` whose only role is + /// to give an `(own)` arg slot for a consume. Its body matches and + /// moves out the heap-typed tail (`match ys { Cons(_, t) => sink(t), + /// Nil => 0 }`) so the sink genuinely consumes its `(own)` param — + /// no spurious `over-strict-mode` warning on `sink` itself to + /// confound the test. + fn fn_sink_own_intlist(name: &str) -> Def { + let body = Term::Match { + scrutinee: Box::new(Term::Var { name: "ys".into() }), + arms: vec![ + Arm { + pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] }, + body: Term::Lit { lit: Literal::Int { value: 0 } }, + }, + Arm { + pat: Pattern::Ctor { + ctor: "Cons".into(), + fields: vec![ + Pattern::Wild, + Pattern::Var { name: "rest".into() }, + ], + }, + body: Term::App { + callee: Box::new(Term::Var { name: name.to_string() }), + args: vec![Term::Var { name: "rest".into() }], + tail: false, + }, + }, + ], + }; + Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![Type::Con { name: "IntList".into(), args: vec![] }], + param_modes: vec![ParamMode::Own], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Own, + effects: vec![], + }, + params: vec!["ys".into()], + body, + suppress: vec![], + doc: None, + export: None, + }) + } + + /// helper: a fn whose single param is `(borrow IntList)` and whose + /// body is `body`. The borrow param starts the walk with + /// `borrow_count = 1`, so any in-body consume of `xs` — or of a + /// heap sub-binder extracted from `xs` — must fire + /// `consume-while-borrowed`. + fn fn_borrow_intlist(name: &str, body: Term) -> Def { + Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![Type::Con { name: "IntList".into(), args: vec![] }], + param_modes: vec![ParamMode::Borrow], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Own, + effects: vec![], + }, + params: vec!["xs".into()], + body, + suppress: vec![], + doc: None, + export: None, + }) + } + + /// SOUNDNESS PROPERTY (#58): a heap-typed pattern sub-binder + /// extracted from a `(borrow)`-mode match scrutinee inherits the + /// scrutinee's borrowed status, so consuming it must fire + /// `consume-while-borrowed`. + /// + /// `leak : (borrow IntList)` matches `xs` and, in the `Cons(h, t)` + /// arm, passes the heap-typed tail `t` to `sink`, an + /// `(own IntList)` sink. `t` aliases the interior of the + /// caller-owned, only-borrowed `xs`; moving it into an `(own)` + /// param double-frees at runtime (SIGSEGV). The linearity pass + /// already rejects consuming the *whole* borrowed param (sibling + /// fixture `cut55_2d`), but here the sub-binder `t` is seeded as a + /// fresh `BinderState` with `borrow_count = 0`, so the consume goes + /// unflagged. + /// + /// RED today: `check_module` returns no `consume-while-borrowed` + /// diagnostic. The primitive sub-binder `h` (`Int`) is correctly + /// exempt (copied out, no heap alias); the bug is specific to the + /// heap-typed `t`. + #[test] + fn consume_heap_sub_binder_of_borrow_scrutinee_is_rejected() { + // leak body: (match xs + // ((pat-ctor Nil) 0) + // ((pat-ctor Cons (pat-var h) (pat-var t)) (app sink t))) + let body = Term::Match { + scrutinee: Box::new(Term::Var { name: "xs".into() }), + arms: vec![ + Arm { + pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] }, + body: Term::Lit { lit: Literal::Int { value: 0 } }, + }, + Arm { + pat: Pattern::Ctor { + ctor: "Cons".into(), + fields: vec![ + Pattern::Var { name: "h".into() }, + Pattern::Var { name: "t".into() }, + ], + }, + body: Term::App { + callee: Box::new(Term::Var { name: "sink".into() }), + args: vec![Term::Var { name: "t".into() }], + tail: false, + }, + }, + ], + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + kernel: false, + imports: vec![], + defs: vec![ + intlist_typedef(), + fn_sink_own_intlist("sink"), + fn_borrow_intlist("leak", body), + ], + }; + let diags = check_module(&m); + let cwb: Vec<_> = diags + .iter() + .filter(|d| d.code == "consume-while-borrowed" && d.def.as_deref() == Some("leak")) + .collect(); + assert_eq!( + cwb.len(), + 1, + "consuming the heap-typed tail `t` of a borrowed scrutinee must fire \ + consume-while-borrowed (it aliases caller-owned heap → double-free); got {diags:?}" + ); + assert_eq!( + cwb[0].ctx, + serde_json::json!({ "binder": "t" }), + "the diagnostic must name the consumed sub-binder `t`; got {diags:?}" + ); + } + /// RED (over-strict-mode FP on ctor-rebuild): a `State(Float, /// Int)` ADT def. Both fields are primitive — the lint's /// `pattern_has_consumed_heap_binder` filters them out — yet a