diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index bf7b23e..cd8c158 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -27,7 +27,11 @@ //! binder. //! //! Position propagation: -//! - `Term::App.callee` — Consume (the value is called once). +//! - `Term::App.callee` — Borrow (applying a function value reads it; +//! the value stays live for further applications and is dropped at +//! scope close). A global fn-ref callee is untracked, so this is a +//! no-op there; a tracked function-typed binder is not consumed by +//! application. //! - `Term::App.args[i]` — Borrow if the callee is a `Var` whose //! resolved type is a `Type::Fn` with `param_modes[i] == Borrow`; //! otherwise Consume (Own / Implicit / unknown all default to @@ -163,6 +167,13 @@ fn is_heap_type(t: &Type) -> bool { } } +/// `true` iff `t` is an unboxed value type (`Int`/`Bool`/`Float`/`Unit`). +/// The `Str`-excluding counterpart of `is_heap_type`'s primitive check — +/// see `ailang_core::primitives::is_value_type`. +fn type_is_value(t: &Type) -> bool { + matches!(t, Type::Con { name, .. } if ailang_core::primitives::is_value_type(name)) +} + /// Position in which a [`Term::Var`] is being used. See module-level /// docs for the propagation rules. #[derive(Copy, Clone, Debug, PartialEq, Eq)] @@ -189,6 +200,12 @@ struct BinderState { /// the borrow ends. Consume while `> 0` triggers /// `consume-while-borrowed`. borrow_count: u32, + /// `true` if this binder has an unboxed value type + /// (`Int`/`Bool`/`Float`/`Unit`). A value type has no refcount and + /// is never consumed, so `use_var` skips all consume bookkeeping + /// for it. Invariant per binder; set at the introduction site + /// (param / pattern / lam) where the type is locally available. + is_value: bool, } /// top-level entry. Walks every fn in `m` and emits @@ -352,19 +369,22 @@ fn check_fn( globals, diags, def_name: &f.name, + ctors, binders: HashMap::new(), }; // Install fn parameters as binders, with initial `borrow_count = 1` // for `Borrow` params (the caller's outer borrow stays live for the - // body's whole duration) and `0` for `Own` params. - for (name, mode) in f.params.iter().zip(param_modes.iter()) { + // body's whole duration) and `0` for `Own` params. A value-type + // param starts `is_value = true` and is exempt from consume-tracking. + for (i, (name, mode)) in f.params.iter().zip(param_modes.iter()).enumerate() { let initial = BinderState { consumed: false, borrow_count: match mode { ParamMode::Borrow => 1, ParamMode::Own | ParamMode::Implicit => 0, }, + is_value: param_tys.get(i).map(type_is_value).unwrap_or(false), }; checker.binders.insert(name.clone(), initial); } @@ -414,6 +434,11 @@ struct Checker<'a> { /// Name of the fn currently being checked (becomes /// [`Diagnostic::def`]). def_name: &'a str, + /// ctor name → field types. Used to type pattern binders so a + /// value-typed sub-binder (`Cons(h, t)` with `h: Int`) is exempted + /// from consume-tracking. Mirrors the `ctors` map built in + /// `check_module_with_visible`. + ctors: &'a HashMap>, /// Live binder state, keyed by name. Modified in place; lexical /// scoping is restored by [`Checker::with_binder`]. binders: HashMap, @@ -428,9 +453,16 @@ impl<'a> Checker<'a> { Term::Lit { .. } => {} Term::Var { name } => self.use_var(name, pos), Term::App { callee, args, .. } => { - // The callee itself is consumed (it's "the function value"); - // for var-callees this is typically a global fn ref. - self.walk(callee, Position::Consume); + // Applying a function value READS it (a borrow): the value + // stays live for further applications and is dropped at + // scope close like any other binder. For a global fn-ref + // callee this is a no-op (globals are untracked, so + // `use_var` returns early either way); for a tracked + // function-typed binder (a HOF param) it stops application + // from consuming the binder. The `consumed` check still + // runs in Borrow position, so applying an already-consumed + // function value still fires use-after-consume. + self.walk(callee, Position::Borrow); // Determine arg modes from the callee's resolved type. let arg_modes = self.callee_arg_modes(callee, args.len()); @@ -538,17 +570,22 @@ impl<'a> Checker<'a> { self.walk(a, Position::Borrow); } } - Term::Lam { params, body, .. } => { + Term::Lam { params, param_tys, body, .. } => { // Lam captures cross the linearity boundary: any free // var of the body is implicitly consumed by closure // construction (we don't yet model captured-borrow // discipline; that is 18c.3 territory). For 18c.2 we // walk the body with the lam's own params as fresh - // binders. + // binders; a value-typed lam param is exempt from + // consume-tracking. let mut saved_for_params: HashMap> = HashMap::new(); - for p in params { + for (i, p) in params.iter().enumerate() { saved_for_params.insert(p.clone(), self.binders.remove(p)); - self.binders.insert(p.clone(), BinderState::default()); + let st = BinderState { + is_value: param_tys.get(i).map(type_is_value).unwrap_or(false), + ..BinderState::default() + }; + self.binders.insert(p.clone(), st); } self.walk(body, Position::Consume); for p in params { @@ -637,10 +674,16 @@ impl<'a> Checker<'a> { /// borrow vs. consume, which is 18c.3 work). fn walk_arm(&mut self, arm: &Arm, pos: Position) { 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)); - self.binders.insert(n.clone(), BinderState::default()); + let st = BinderState { + is_value: value_names.contains(n), + ..BinderState::default() + }; + self.binders.insert(n.clone(), st); } self.walk(&arm.body, pos); for n in &names { @@ -681,6 +724,11 @@ impl<'a> Checker<'a> { // sibling args, and for the per-fn-param initial value. } Position::Consume => { + // A value type has no refcount and is never consumed; + // multi-use in any position is legal. + if state.is_value { + return; + } if state.borrow_count > 0 { self.diags .push(make_consume_while_borrowed(self.def_name, name)); @@ -774,6 +822,36 @@ fn collect_pattern_binders(p: &Pattern) -> Vec { } } +/// Collect the names of pattern binders that have an unboxed value +/// type, by walking the pattern alongside the ctor field types. +/// Mirrors `pattern_has_consumed_heap_binder_at`'s descent: a +/// `Pattern::Var` directly under a ctor field of value type is added; +/// a top-level `Pattern::Var` (whole-scrutinee binder, `declared_ty == +/// None`) is conservatively treated as heap and never added. +fn collect_value_pattern_binders( + pat: &Pattern, + declared_ty: Option<&Type>, + ctors: &HashMap>, + out: &mut Vec, +) { + match pat { + Pattern::Wild | Pattern::Lit { .. } => {} + Pattern::Var { name } => { + if let Some(t) = declared_ty { + if type_is_value(t) { + out.push(name.clone()); + } + } + } + Pattern::Ctor { ctor, fields } => { + let field_tys: &[Type] = ctors.get(ctor).map(|v| v.as_slice()).unwrap_or(&[]); + for (i, f) in fields.iter().enumerate() { + collect_value_pattern_binders(f, field_tys.get(i), ctors, out); + } + } + } +} + /// Conservative merge of two branch states: a binder is consumed in /// the merged state iff it was consumed in either branch; borrow_count /// becomes the max of the two. Names present only in one map are @@ -783,6 +861,9 @@ fn merge_states(into: &mut HashMap, other: &HashMap Int))`, + /// returning Int. Used to exercise HOF application linearity. + fn fn_with_fn_param(name: &str, mode: ParamMode, body: Term) -> Def { + Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![Type::Fn { + params: vec![Type::int()], + param_modes: vec![ParamMode::Own], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Own, + effects: vec![], + }], + param_modes: vec![mode], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["p0".into()], + body, + suppress: vec![], + doc: None, + export: None, + }) + } + + /// Applying a function param more than once is a borrow each time, + /// not a consume: `(app p0 (app p0 0))` must NOT fire + /// use-after-consume. (Today the App callee is walked Consume, so + /// the first application consumes `p0` and the second fires + /// use-after-consume — this test is RED until Fix 2.) + #[test] + fn own_fn_param_applied_twice_is_clean() { + let body = Term::App { + callee: Box::new(Term::Var { name: "p0".into() }), + args: vec![Term::App { + callee: Box::new(Term::Var { name: "p0".into() }), + args: vec![Term::Lit { lit: Literal::Int { value: 0 } }], + tail: false, + }], + tail: false, + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + kernel: false, + imports: vec![], + defs: vec![fn_with_fn_param("f", ParamMode::Own, body)], + }; + let diags = check_module(&m); + assert!( + !diags.iter().any(|d| d.code == "use-after-consume"), + "applying a function param is a borrow, not a consume; got {diags:?}" + ); + } + + /// A fn with one `(own (con Int))` value-type param `p0`, returning + /// Int. Used to exercise the value-type exemption. + fn fn_with_int_own(name: &str, body: Term) -> Def { + Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![Type::Con { name: "Int".into(), args: vec![] }], + param_modes: vec![ParamMode::Own], + ret: Box::new(Type::int()), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["p0".into()], + body, + suppress: vec![], + doc: None, + export: None, + }) + } + + /// A value-type param read in two consume positions + /// (`(seq p0 p0)`) must NOT fire use-after-consume: an `Int` has no + /// refcount and is never consumed. RED until Fix 1. + #[test] + fn value_param_multi_read_is_clean() { + let body = Term::Seq { + lhs: Box::new(Term::Var { name: "p0".into() }), + rhs: Box::new(Term::Var { name: "p0".into() }), + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + kernel: false, + imports: vec![], + defs: vec![fn_with_int_own("f", body)], + }; + let diags = check_module(&m); + assert!( + !diags.iter().any(|d| d.code == "use-after-consume"), + "a value-type param is never consumed; multi-read is legal; got {diags:?}" + ); + } + + /// Type-gating guard: a HEAP param (`List`) consumed twice in a ctor + /// (`(term-ctor Pair Pair p0 p0)`) MUST still fire use-after-consume + /// after the fix — the exemption is value-type-only, not blanket. + /// (Green today and after the fix; a regression guard, not RED-first.) + #[test] + fn heap_param_multi_consume_still_errors() { + let body = Term::Ctor { + type_name: "Pair".into(), + ctor: "Pair".into(), + args: vec![ + Term::Var { name: "p0".into() }, + Term::Var { name: "p0".into() }, + ], + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + kernel: false, + imports: vec![], + defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)], + }; + let diags = check_module(&m); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "a heap param consumed twice must still error; got {diags:?}" + ); + } + + /// A borrow function param applied AND passed (the recursive-HOF + /// shape `map_int`) must be clean: application is a borrow, and the + /// param starts borrowed, so neither use-after-consume nor + /// consume-while-borrowed should fire. Covered by Fix 2 (App + /// borrow); this asserts the borrow-param variant. RED until Fix 2. + #[test] + fn borrow_fn_param_applied_is_clean() { + let body = Term::App { + callee: Box::new(Term::Var { name: "p0".into() }), + args: vec![Term::Lit { lit: Literal::Int { value: 0 } }], + tail: false, + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + kernel: false, + imports: vec![], + defs: vec![fn_with_fn_param("f", ParamMode::Borrow, body)], + }; + let diags = check_module(&m); + assert!( + !diags.iter().any(|d| { + d.code == "use-after-consume" || d.code == "consume-while-borrowed" + }), + "applying a borrow function param is a clean read; got {diags:?}" + ); + } + /// All-Implicit fn → check is skipped, no diagnostics, even if the /// body would trigger a use-after-consume under explicit modes. #[test] diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 9b08eb5..71d2590 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -719,6 +719,39 @@ fn borrow_own_demo_is_linearity_clean() { ); } +/// #56 Fix 1+2: under universal activation the linearity analysis must +/// not false-fire on value-type params or on applied function params. +/// These three fixtures use explicit-mode signatures (so the analysis +/// is active today) and were RED before the hardening (docs/specs/0063). +#[test] +fn harden_ownership_false_positives_are_clean() { + for name in ["fp_value", "fp_hof", "fp_map"] { + let entry = examples_dir().join(format!("{name}.ail")); + let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}")); + let diags = check_workspace(&ws); + let lin: Vec<&ailang_check::Diagnostic> = diags + .iter() + .filter(|d| d.code == "use-after-consume" || d.code == "consume-while-borrowed") + .collect(); + assert!(lin.is_empty(), "{name} must be linearity-clean; got: {lin:#?}"); + } +} + +/// #56 type-gating: the exemption is value-type-only. A heap param +/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST +/// still fire use-after-consume — proving the fix did not blanket-silence +/// genuine multi-consume. +#[test] +fn harden_ownership_heap_double_consume_still_errors() { + let entry = examples_dir().join("real_consume.ail"); + let ws = load_workspace(&entry).expect("load real_consume"); + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "real_consume.dup must still fire use-after-consume; got: {diags:#?}" + ); +} + /// RED for fieldtest finding B1 (docs/specs/0058): reading a /// `borrow (RawBuf a)` *parameter* through a borrow-receiver op /// (`RawBuf.get` / `RawBuf.size`) must check clean. Both ops are diff --git a/crates/ailang-core/src/primitives.rs b/crates/ailang-core/src/primitives.rs index 1f00aad..bf1f4bd 100644 --- a/crates/ailang-core/src/primitives.rs +++ b/crates/ailang-core/src/primitives.rs @@ -17,6 +17,18 @@ pub fn is_primitive_name(name: &str) -> bool { matches!(name, "Int" | "Bool" | "Str" | "Unit" | "Float") } +/// Returns `true` iff `name` is an **unboxed value type** — no RC, no +/// heap slab, copied by value. This is the `Str`-excluding subset of +/// [`is_primitive_name`]: `Str` is a primitive zero-arity ctor but is +/// heap-allocated (`ptr`, RC-`dec`'d — codegen `drop.rs:490-492` lowers +/// only `Int`/`Bool`/`Float`/`Unit` to non-`ptr`). Used by the +/// linearity analysis to exempt value-type binders from +/// consume-tracking: a value type is never consumed, so multi-use is +/// always legal. +pub fn is_value_type(name: &str) -> bool { + matches!(name, "Int" | "Bool" | "Float" | "Unit") +} + /// Returns the static-lifetime surface name iff `name` is a /// primitive. Used by the mono pass to embed the human-readable /// form in monomorphised symbol names; the static lifetime is what @@ -60,4 +72,24 @@ mod tests { "Float surface name must be \"Float\"" ); } + + /// `is_value_type` is the unboxed/no-RC subset of the primitives: + /// it agrees with `is_primitive_name` on every name EXCEPT `Str`, + /// which is a primitive zero-arity ctor but is heap-allocated + /// (`ptr`, RC'd) — see drop.rs:490-492. + #[test] + fn value_type_is_primitive_minus_str() { + for name in ["Int", "Bool", "Float", "Unit"] { + assert!(is_value_type(name), "{name} must be a value type"); + assert!(is_primitive_name(name), "{name} must be a primitive"); + } + // The sole divergence: Str is a primitive but NOT a value type. + assert!(!is_value_type("Str"), "Str is heap-allocated, not a value type"); + assert!(is_primitive_name("Str"), "Str is still a primitive zero-arity ctor"); + // Non-primitives are neither. + for name in ["List", "Foo", ""] { + assert!(!is_value_type(name)); + assert!(!is_primitive_name(name)); + } + } } diff --git a/examples/fp_hof.ail b/examples/fp_hof.ail new file mode 100644 index 0000000..c75bafc --- /dev/null +++ b/examples/fp_hof.ail @@ -0,0 +1,12 @@ +(module fp_hof + (fn apply_thrice + (doc "apply a function param three times") + (type (fn-type + (params (own (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con Int))) + (ret (own (con Int))))) + (params f x) + (body (app f (app f (app f x))))) + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body (app print (app apply_thrice (lam (params (typed y (con Int))) (ret (con Int)) (body (app + y 1))) 0))))) diff --git a/examples/fp_map.ail b/examples/fp_map.ail new file mode 100644 index 0000000..c2a0b6f --- /dev/null +++ b/examples/fp_map.ail @@ -0,0 +1,14 @@ +(module fp_map + (data IntList + (doc "boxed list") + (ctor Nil) + (ctor Cons (con Int) (con IntList))) + (fn map_int + (doc "recursive HOF: f applied AND passed to the recursive call") + (type (fn-type + (params (borrow (fn-type (params (own (con Int))) (ret (own (con Int))))) (own (con IntList))) + (ret (own (con IntList))))) + (params f xs) + (body (match xs + (case (pat-ctor Nil) (term-ctor IntList Nil)) + (case (pat-ctor Cons h t) (term-ctor IntList Cons (app f h) (app map_int f t))))))) diff --git a/examples/fp_value.ail b/examples/fp_value.ail new file mode 100644 index 0000000..fbd0c10 --- /dev/null +++ b/examples/fp_value.ail @@ -0,0 +1,10 @@ +(module fp_value + (fn sum_explicit + (doc "value-type param read multiple times") + (type (fn-type (params (own (con Int))) (ret (own (con Int))))) + (params n) + (body (if (app eq n 0) 0 (app + n (app sum_explicit (app - n 1)))))) + (fn main + (type (fn-type (params) (ret (own (con Unit))) (effects IO))) + (params) + (body (app print (app sum_explicit 10))))) diff --git a/examples/real_consume.ail b/examples/real_consume.ail new file mode 100644 index 0000000..6679c83 --- /dev/null +++ b/examples/real_consume.ail @@ -0,0 +1,12 @@ +(module real_consume + (data Box + (doc "heap cell") + (ctor Box (con Int))) + (data Pair + (doc "two boxes") + (ctor Pair (con Box) (con Box))) + (fn dup + (doc "MUST STAY an error: a heap param consumed twice without clone") + (type (fn-type (params (own (con Box))) (ret (own (con Pair))))) + (params b) + (body (term-ctor Pair Pair b b))))