audit(0064/cutover): record shipped drop machinery + retire dead desugar arm
Cycle-close tidy for the #55 cutover (its audit drift-resolution). Architect drift review found the design ledger out of step with the codegen that the cutover shipped, plus two debt items; regression green (733 passed / 0 failed across the workspace). design/contracts/0008-memory-model.md — the Codegen contract described the drop-emission *gates* but not the drop machinery the cutover landed. Added three subsections recording the present state (honesty rule): - Per-monomorph drop fns for polymorphic ADTs (crates/ailang-codegen/ src/dropmono.rs: collect_drop_monos / DropAdtMeta, the suffix scheme, value-field-skip on the substituted field type). Ratified by alloc_rc_value_type_field_is_not_rc_dec_dropped. - String-literal rep promotion at owned drop sites (StrRep::Static→Heap on a Str literal flowing into an Own slot the callee drops; gated strictly on Own). Ratified by own_str_literal_arg_is_dropped_exactly_once. - Same-constructor arm grouping in match desugar (build_chain / build_ctor_group bind ctor fields once). Ratified by lit_pat_ctor_tail_drop_single_drop + lit_pat_nil_scrutinee_single_drop. crates/ailang-core/src/desugar.rs — build_chain routes every Ctor-head arm (including a length-1 run) through build_ctor_group, so desugar_one_arm's Pattern::Ctor arm was unreachable dead code duplicating the bind-once lowering. Replaced it with unreachable! naming the invariant, and corrected two stale doc comments (the module-header step 4 and the desugar_one_arm doc still described it as handling ctor arms, and mislabeled the Lit lowering as Term::Match — it is Term::If). Full workspace stayed green, confirming the arm was dead. crates/ailang-check/src/linearity.rs — renamed test implicit_fn_is_exempt → own_param_consumed_once_is_clean. Post-0062 there is no Implicit and no exemption; the test pins the ordinary single-Own-consume clean path. Did the desugar + linearity edits inline rather than via an agent: I had already loaded build_chain/build_ctor_group/desugar_one_arm to prove the arm dead, and a sub-agent would have redone the same reading.
This commit is contained in:
@@ -1897,10 +1897,12 @@ mod tests {
|
|||||||
);
|
);
|
||||||
}
|
}
|
||||||
|
|
||||||
/// All-Implicit fn → check is skipped, no diagnostics, even if the
|
/// A single `Own` param consumed exactly once (the body returns it)
|
||||||
/// body would trigger a use-after-consume under explicit modes.
|
/// is clean — no `over-strict-mode`, no use-after-consume. (Pre-0062
|
||||||
|
/// this was the `Implicit`-exemption case; post-cutover there is no
|
||||||
|
/// `Implicit`, so it pins the ordinary single-consume path.)
|
||||||
#[test]
|
#[test]
|
||||||
fn implicit_fn_is_exempt() {
|
fn own_param_consumed_once_is_clean() {
|
||||||
let m = Module {
|
let m = Module {
|
||||||
schema: ailang_core::SCHEMA.into(),
|
schema: ailang_core::SCHEMA.into(),
|
||||||
name: "t".into(),
|
name: "t".into(),
|
||||||
|
|||||||
@@ -37,17 +37,21 @@
|
|||||||
//! arms returned a non-Unit type to carry a synthetic `_` arm
|
//! arms returned a non-Unit type to carry a synthetic `_` arm
|
||||||
//! dominating the terminator. The polymorphic `__unreachable__`
|
//! dominating the terminator. The polymorphic `__unreachable__`
|
||||||
//! removes that workaround.
|
//! removes that workaround.
|
||||||
//! 4. Each arm is lowered via `desugar_one_arm`:
|
//! 4. `build_chain` lowers the arms head-first:
|
||||||
//! - `Pattern::Wild` → arm body (catch-all; later arms are dropped).
|
//! - A maximal run of consecutive arms sharing the head arm's outer
|
||||||
//! - `Pattern::Var { name }` → `Let { name = scrutinee_var; body }`.
|
//! ctor + arity is lowered together via `build_ctor_group`: lift
|
||||||
//! - `Pattern::Lit { lit }` → `Term::If { cond = (== s_var lit),
|
//! each ctor field to a fresh var, emit ONE `Term::Match` over the
|
||||||
//! then = arm.body, else_ = fall_k }` (Iter 16c). After this
|
//! flat ctor pattern (binding the fields once) plus a wildcard
|
||||||
|
//! fall-through, and thread the bound vars through every arm's
|
||||||
|
//! sub-patterns via `wrap_sub`. Binding once keeps the ctor's
|
||||||
|
//! owned children under a single match scope (no re-match, no
|
||||||
|
//! re-drop).
|
||||||
|
//! - A non-ctor head (Wild/Var/Lit) is lowered via `desugar_one_arm`:
|
||||||
|
//! `Pattern::Wild` → arm body (catch-all; later arms are dropped);
|
||||||
|
//! `Pattern::Var { name }` → `Let { name = scrutinee_var; body }`;
|
||||||
|
//! `Pattern::Lit { lit }` → `Term::If { cond = (== s_var lit),
|
||||||
|
//! then = arm.body, else_ = fall_k }` (Iter 16c). After the Lit
|
||||||
//! rewrite, no `Pattern::Lit` reaches typecheck or codegen.
|
//! rewrite, no `Pattern::Lit` reaches typecheck or codegen.
|
||||||
//! - `Pattern::Ctor { ctor, fields }`: lift each field to a fresh
|
|
||||||
//! var, build a flat outer pattern, walk fields right-to-left
|
|
||||||
//! wrapping inner sub-patterns via `wrap_sub`. Emit a
|
|
||||||
//! `Term::Match` with two arms: the flat ctor and a wildcard
|
|
||||||
//! fall-through into the rest of the chain.
|
|
||||||
//!
|
//!
|
||||||
//! `wrap_sub(fv, sub, body, fall_k)` recurses on `sub`:
|
//! `wrap_sub(fv, sub, body, fall_k)` recurses on `sub`:
|
||||||
//! - `Var(n)` → `Let(n, Var(fv), body)`.
|
//! - `Var(n)` → `Let(n, Var(fv), body)`.
|
||||||
@@ -1259,10 +1263,11 @@ impl Desugarer {
|
|||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
/// Lowers one arm into a term. Wild/Var arms drop the chain (the
|
/// Lowers one non-constructor arm into a term. Wild/Var arms drop
|
||||||
/// arm matches everything); Lit and Ctor arms emit a `Term::Match`
|
/// the chain (the arm matches everything); a Lit arm emits a
|
||||||
/// with the desugared head pattern as the first arm and a
|
/// `Term::If` discriminating on `(== s_var lit)` with `fall_k` as
|
||||||
/// wildcard fall-through to `fall_k`.
|
/// the else-branch. Ctor-head arms never reach here — `build_chain`
|
||||||
|
/// routes them through `build_ctor_group` (bind-once lowering).
|
||||||
fn desugar_one_arm(&mut self, s_var: &Term, arm: &Arm, fall_k: Term) -> Term {
|
fn desugar_one_arm(&mut self, s_var: &Term, arm: &Arm, fall_k: Term) -> Term {
|
||||||
match &arm.pat {
|
match &arm.pat {
|
||||||
Pattern::Wild => arm.body.clone(),
|
Pattern::Wild => arm.body.clone(),
|
||||||
@@ -1282,37 +1287,14 @@ impl Desugarer {
|
|||||||
else_: Box::new(fall_k),
|
else_: Box::new(fall_k),
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
Pattern::Ctor { ctor, fields } => {
|
// `build_chain` routes every Ctor-head arm — including a
|
||||||
// Lift each field to a fresh var; build the flat outer
|
// length-1 run — through `build_ctor_group`, whose bind-once
|
||||||
// pattern, then walk right-to-left wrapping each inner
|
// lowering is the live path. `desugar_one_arm` therefore only
|
||||||
// sub-pattern via `wrap_sub` so the deepest field is
|
// ever sees Wild/Var/Lit heads.
|
||||||
// matched first inside-out.
|
Pattern::Ctor { .. } => unreachable!(
|
||||||
let fresh_vars: Vec<String> = fields.iter().map(|_| self.fresh()).collect();
|
"build_chain routes Ctor-head arms through build_ctor_group; \
|
||||||
let flat_fields: Vec<Pattern> = fresh_vars
|
desugar_one_arm sees only Wild/Var/Lit"
|
||||||
.iter()
|
),
|
||||||
.map(|n| Pattern::Var { name: n.clone() })
|
|
||||||
.collect();
|
|
||||||
let mut inner = arm.body.clone();
|
|
||||||
for (sub, fv) in fields.iter().zip(fresh_vars.iter()).rev() {
|
|
||||||
inner = self.wrap_sub(fv, sub, inner, &fall_k);
|
|
||||||
}
|
|
||||||
Term::Match {
|
|
||||||
scrutinee: Box::new(s_var.clone()),
|
|
||||||
arms: vec![
|
|
||||||
Arm {
|
|
||||||
pat: Pattern::Ctor {
|
|
||||||
ctor: ctor.clone(),
|
|
||||||
fields: flat_fields,
|
|
||||||
},
|
|
||||||
body: inner,
|
|
||||||
},
|
|
||||||
Arm {
|
|
||||||
pat: Pattern::Wild,
|
|
||||||
body: fall_k,
|
|
||||||
},
|
|
||||||
],
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|||||||
@@ -324,6 +324,73 @@ returns that are not `Type::Con` (e.g. unresolved type vars on
|
|||||||
a polymorphic call's pre-monomorphisation site; the
|
a polymorphic call's pre-monomorphisation site; the
|
||||||
monomorphised copies resolve to concrete drop fns).
|
monomorphised copies resolve to concrete drop fns).
|
||||||
|
|
||||||
|
#### Per-monomorph drop fns for polymorphic ADTs
|
||||||
|
|
||||||
|
A polymorphic ADT (`Box a`, `Pair a b`) has no single correct
|
||||||
|
drop fn: a ctor field typed at a type-var lowers to `ptr` and is
|
||||||
|
`rc_dec`'d, but at a value-type instantiation (`Box Int`) that
|
||||||
|
field is an inline `i64`, so dec'ing it dereferences a scalar.
|
||||||
|
Codegen therefore emits **one drop fn per (polymorphic-ADT,
|
||||||
|
concrete instantiation)** and makes the dec-vs-skip decision on
|
||||||
|
the *substituted* field type: a value-type field
|
||||||
|
(`Int`/`Bool`/`Float`/`Unit`) is skipped (inline scalar, no RC);
|
||||||
|
a heap field is dec'd through its own per-monomorph drop symbol
|
||||||
|
so the cascade composes.
|
||||||
|
|
||||||
|
The workspace-global collection lives in
|
||||||
|
`crates/ailang-codegen/src/dropmono.rs` (`collect_drop_monos`,
|
||||||
|
`DropAdtMeta`), built once before the per-module codegen loop and
|
||||||
|
shared by reference with every `Emitter`. Symbol naming:
|
||||||
|
|
||||||
|
- A concrete-monomorphic ADT (declared `vars` empty: `IntList`,
|
||||||
|
`Ordering`) keeps its un-suffixed `drop_<m>_<T>` /
|
||||||
|
`partial_drop_<m>_<T>` symbol byte-for-byte (the `ir_snapshot`
|
||||||
|
goldens pin these).
|
||||||
|
- A polymorphic ADT instantiation gets a mono suffix mangled
|
||||||
|
exactly as `ailang_check::mono::mono_symbol_n` mangles fn
|
||||||
|
symbols (`drop_<m>_Pair__Int_Int`; compound args hash-route to
|
||||||
|
stay bounded).
|
||||||
|
- Intrinsic-storage types (`RawBuf`) are polymorphic but use the
|
||||||
|
flat intrinsic drop path and are NOT suffixed (their drop is
|
||||||
|
element-type independent; the golden pins `drop_<m>_RawBuf`).
|
||||||
|
|
||||||
|
A drop fn and its call sites consult the same `DropAdtMeta`
|
||||||
|
(emission + manglers in `drop.rs`, call-site manglers in
|
||||||
|
`match_lower.rs`), so they always agree on the symbol — a
|
||||||
|
mismatch would be a link error. Ratified by
|
||||||
|
`alloc_rc_value_type_field_is_not_rc_dec_dropped` in
|
||||||
|
`crates/ail/tests/drop_value_field_no_segfault_pin.rs`.
|
||||||
|
|
||||||
|
#### String-literal rep promotion at owned drop sites
|
||||||
|
|
||||||
|
A `Str` literal carries a `StrRep`: `Static` (header-less rodata
|
||||||
|
constant) or `Heap` (rc-headered owned slab). An `Own`-mode drop
|
||||||
|
path emits `ailang_rc_dec` on the value; dec'ing a
|
||||||
|
`StrRep::Static` reads `payload - 8` (the length field) as a fake
|
||||||
|
refcount and `free()`s a static address — a segfault. Codegen
|
||||||
|
therefore promotes a `Str` literal that flows into an `Own` slot
|
||||||
|
the callee will drop from `Static` to `Heap` (codegen then emits
|
||||||
|
`ailang_str_clone` → refcount 1, and the single dec is sound).
|
||||||
|
The promotion is gated **strictly on `Own`**: a `Borrow` slot
|
||||||
|
fires no `rc_dec`, so a borrow-position literal stays
|
||||||
|
`StrRep::Static` (no spurious clone).
|
||||||
|
`crates/ailang-check/src/lower_to_mir.rs` applies this at four
|
||||||
|
sites — the `Term::App` owned-arg site (`is_str_ty` + `Own`) and
|
||||||
|
the loop-carried seed/tail/recur sites of a `Str`-returning loop
|
||||||
|
body. Ratified by `own_str_literal_arg_is_dropped_exactly_once`
|
||||||
|
in `crates/ail/tests/e2e.rs`.
|
||||||
|
|
||||||
|
#### Same-constructor arm grouping in match desugar
|
||||||
|
|
||||||
|
`crates/ailang-core/src/desugar.rs` groups consecutive match
|
||||||
|
arms that share a head constructor (`build_chain` /
|
||||||
|
`build_ctor_group`) into a single match over that constructor's
|
||||||
|
fields, binding the fields once. This keeps a literal sub-pattern
|
||||||
|
(`(Cons (pat-lit K) _)`) from re-matching — and re-dropping — the
|
||||||
|
same owned scrutinee tail across the literal-discriminating arms.
|
||||||
|
Ratified by `lit_pat_ctor_tail_drop_single_drop` and
|
||||||
|
`lit_pat_nil_scrutinee_single_drop` in `crates/ail/tests/e2e.rs`.
|
||||||
|
|
||||||
#### Arg-position policy for compound AST nodes
|
#### Arg-position policy for compound AST nodes
|
||||||
|
|
||||||
The uniqueness and linearity passes walk arguments of compound
|
The uniqueness and linearity passes walk arguments of compound
|
||||||
|
|||||||
Reference in New Issue
Block a user