fix: resolve cross-module borrow modes in the uniqueness pass (refs #43)
A2a leg of the owned-RawBuf drop-leak. Prerequisite: regression-free
and independently correct, but does NOT alone close the leak — the
three shadow_rebind RED tests (f7f4c3b) stay RED pending the A2b
shadow-collapse leg, which needs a UniquenessTable contract change and
its own spec.
The leg. The uniqueness pass infer_module runs strictly per module
(called per-Emitter from codegen lib.rs:993 with a single Module). The
module holding `main` registers only its own + builtin signatures in
`globals`; the monomorphised intrinsic signatures (RawBuf_get__Int with
param_modes=[Borrow,Implicit], etc.) live exclusively in the raw_buf
module's separate pass. So a qualified cross-module callee
`raw_buf.RawBuf_get__Int` missed `main`'s globals entirely, returned
vec![], and the walk defaulted every arg to Position::Consume —
mis-counting the borrowed `buf` arg as a consume and inflating the
binder's consume_count, which gates off the scope-close drop. This is a
latent over-conservative default affecting ANY cross-module borrow
callee, not just RawBuf.
The fix (additive, two files). infer_module is kept as a thin wrapper
over a new infer_module_with_cross(m, &cross_module_types) that threads
the workspace-flat module->def->Type table (the same module_def_ail_types
codegen already builds and the A1 emit_call rule already reads). On a
same-module globals miss, callee_arg_modes now falls back to
cross_module_callee_ty: split the callee on the last `.`, resolve
<mod>.<def> positionally against the cross-module table, and read its
Type::Fn.param_modes. Same-module + builtin lookup stays the first
resort; unqualified names and absent entries fall through to the
existing all-consume default unchanged. Modes are matched positionally,
so RawBuf.set's Own first param still counts as a consume (the
new/set-chain binders keep consume_count==1 and are not dropped —
correct, set is in-place, same slab).
Verified: full workspace green except the three intended-RED
shadow_rebind tests; ailang-check and ailang-codegen (incl.
intercepts_bijection_with_intrinsic_markers) green; A1's
raw_buf_owned_drop_balances_rc_stats still green. raw_buf_int.ail still
leaks (live=1) — that is the A2b leg, addressed next.
This commit is contained in:
@@ -107,6 +107,32 @@ pub type UniquenessTable = BTreeMap<(String, String), UniquenessInfo>;
|
||||
/// codegen never runs on such inputs because `ail build` runs
|
||||
/// typecheck first.
|
||||
pub fn infer_module(m: &Module) -> UniquenessTable {
|
||||
infer_module_with_cross(m, &BTreeMap::new())
|
||||
}
|
||||
|
||||
/// Same as [`infer_module`], but with access to the workspace-flat
|
||||
/// cross-module signature table (`module -> def -> Type`, the shape
|
||||
/// codegen builds as `module_def_ail_types`). The per-module pass
|
||||
/// only registers same-module + builtin signatures in `globals`; a
|
||||
/// call to a *cross-module* callee (a qualified `<mod>.<def>` name,
|
||||
/// e.g. the monomorphised intrinsic `raw_buf.RawBuf_get__Int` reached
|
||||
/// from a `main` that lives in a different module) misses the
|
||||
/// per-module `globals` and so previously defaulted every arg to
|
||||
/// `Position::Consume` — mis-counting a `Borrow`-mode arg as a
|
||||
/// consume and inflating the binder's `consume_count`, which gates
|
||||
/// off the scope-close `dec` and leaks the slab. Threading the
|
||||
/// cross-module table lets `callee_arg_modes` resolve the qualified
|
||||
/// name positionally to its registered `Type::Fn.param_modes` and
|
||||
/// walk borrow args as `Position::Borrow`.
|
||||
///
|
||||
/// This generalises to any cross-module borrow callee, not just
|
||||
/// RawBuf — it removes a latent over-conservative consume default.
|
||||
/// The same-module `globals` lookup stays the first resort; the
|
||||
/// cross-module table is consulted only on a miss.
|
||||
pub fn infer_module_with_cross(
|
||||
m: &Module,
|
||||
cross_module_types: &BTreeMap<String, BTreeMap<String, Type>>,
|
||||
) -> UniquenessTable {
|
||||
let mut globals: BTreeMap<String, Type> = BTreeMap::new();
|
||||
// register builtin signatures so the App-arg walker
|
||||
// sees their `param_modes` and walks `Borrow`-mode args as
|
||||
@@ -143,7 +169,7 @@ pub fn infer_module(m: &Module) -> UniquenessTable {
|
||||
let mut table: UniquenessTable = BTreeMap::new();
|
||||
for def in &m.defs {
|
||||
if let Def::Fn(f) = def {
|
||||
infer_fn(f, &globals, &mut table);
|
||||
infer_fn(f, &globals, cross_module_types, &mut table);
|
||||
}
|
||||
}
|
||||
table
|
||||
@@ -158,7 +184,12 @@ fn strip_forall(t: &Type) -> &Type {
|
||||
|
||||
/// Per-fn driver: install the parameters as binders, walk the body,
|
||||
/// snapshot the per-binder consume counts into the side table.
|
||||
fn infer_fn(f: &FnDef, globals: &BTreeMap<String, Type>, out: &mut UniquenessTable) {
|
||||
fn infer_fn(
|
||||
f: &FnDef,
|
||||
globals: &BTreeMap<String, Type>,
|
||||
cross_module_types: &BTreeMap<String, BTreeMap<String, Type>>,
|
||||
out: &mut UniquenessTable,
|
||||
) {
|
||||
let inner = strip_forall(&f.ty);
|
||||
if !matches!(inner, Type::Fn { .. }) {
|
||||
return;
|
||||
@@ -167,6 +198,7 @@ fn infer_fn(f: &FnDef, globals: &BTreeMap<String, Type>, out: &mut UniquenessTab
|
||||
let param_states = {
|
||||
let mut walker = Walker {
|
||||
globals,
|
||||
cross_module_types,
|
||||
binders: BTreeMap::new(),
|
||||
def_name: f.name.clone(),
|
||||
out,
|
||||
@@ -223,6 +255,10 @@ struct BinderState {
|
||||
|
||||
struct Walker<'a> {
|
||||
globals: &'a BTreeMap<String, Type>,
|
||||
/// Workspace-flat `module -> def -> Type` table. Consulted only
|
||||
/// when `globals` (same-module + builtins) misses on a qualified
|
||||
/// cross-module callee. See [`infer_module_with_cross`].
|
||||
cross_module_types: &'a BTreeMap<String, BTreeMap<String, Type>>,
|
||||
binders: BTreeMap<String, BinderState>,
|
||||
def_name: String,
|
||||
out: &'a mut UniquenessTable,
|
||||
@@ -392,9 +428,22 @@ impl<'a> Walker<'a> {
|
||||
Term::Var { name } => name,
|
||||
_ => return vec![],
|
||||
};
|
||||
// First resort: same-module + builtin signatures.
|
||||
let ty = match self.globals.get(name) {
|
||||
Some(t) => t,
|
||||
None => return vec![],
|
||||
// Fallback: a qualified `<mod>.<def>` callee whose
|
||||
// signature lives in a *different* module's defs (e.g. a
|
||||
// monomorphised intrinsic like `raw_buf.RawBuf_get__Int`
|
||||
// reached from a `main` in another module). Split on the
|
||||
// last `.` and resolve positionally against the
|
||||
// workspace-flat cross-module table. Without this the
|
||||
// qualified borrow callee would miss and every arg would
|
||||
// default to `Position::Consume`, mis-counting the borrow
|
||||
// arg and leaking the slab.
|
||||
None => match self.cross_module_callee_ty(name) {
|
||||
Some(t) => t,
|
||||
None => return vec![],
|
||||
},
|
||||
};
|
||||
let inner = strip_forall(ty);
|
||||
match inner {
|
||||
@@ -409,6 +458,17 @@ impl<'a> Walker<'a> {
|
||||
}
|
||||
}
|
||||
|
||||
/// Resolve a qualified `<mod>.<def>` callee name against the
|
||||
/// cross-module signature table. Splits on the last `.` so a def
|
||||
/// name carrying no dot (the monomorphic intrinsic symbols do not)
|
||||
/// resolves cleanly. Returns `None` for unqualified names or names
|
||||
/// whose module/def is absent from the table — the caller then
|
||||
/// falls back to the existing `vec![]` (all-consume) default.
|
||||
fn cross_module_callee_ty(&self, name: &str) -> Option<&'a Type> {
|
||||
let (module, def) = name.rsplit_once('.')?;
|
||||
self.cross_module_types.get(module)?.get(def)
|
||||
}
|
||||
|
||||
fn record_binder(&mut self, name: &str, s: &BinderState) {
|
||||
let info = UniquenessInfo {
|
||||
uniqueness: classify(s.consume_count),
|
||||
|
||||
@@ -38,7 +38,7 @@ use ailang_core::ast::*;
|
||||
use ailang_core::Workspace;
|
||||
use std::collections::{BTreeMap, BTreeSet};
|
||||
|
||||
use ailang_check::uniqueness::{infer_module, UniquenessTable};
|
||||
use ailang_check::uniqueness::{infer_module_with_cross, UniquenessTable};
|
||||
|
||||
mod drop;
|
||||
mod escape;
|
||||
@@ -989,8 +989,14 @@ impl<'a> Emitter<'a> {
|
||||
// build the per-module uniqueness side-table once
|
||||
// per emitter. The inference is pure (no I/O, no global state),
|
||||
// so doing it here is cheap and keeps codegen's input self-
|
||||
// contained.
|
||||
let uniqueness = infer_module(module);
|
||||
// contained. Pass the workspace-flat cross-module signature
|
||||
// table so a qualified cross-module borrow callee (e.g. the
|
||||
// monomorphised intrinsic `raw_buf.RawBuf_get__Int` reached
|
||||
// from a `main` in another module) resolves to its registered
|
||||
// `param_modes` instead of defaulting every arg to Consume —
|
||||
// which otherwise inflates the borrow binder's consume_count
|
||||
// and gates off its scope-close drop.
|
||||
let uniqueness = infer_module_with_cross(module, module_def_ail_types);
|
||||
|
||||
Self {
|
||||
module,
|
||||
|
||||
Reference in New Issue
Block a user