From ac9af439563a6f98cd9f68b1459f98e1aae3f271 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Sat, 3 Oct 2026 05:18:42 +0000 Subject: [PATCH 1/2] fix(codegen): region Number proof judges loop condition and update writes A loop region proves a loop-carried local Number with one preheader entry test and a fixed point over the local's writes. The fixed point walked only the loop body, so a write in the `for` update clause or in the condition (`for (...; i++, s = "a") { o.x = o.x + s; }`) was never judged: with no per-iteration recheck, F added the string's NaN-box bits as a double and stored the result into the pointer-free F64 lane. fadd propagates the payload, so the lane held the live string pointer (o.x printed `a`, node `1aa`), untraced by the collector. RegionNumberAssumptions now carries the region's loop control, and the collector feeds its writes into the same shared write inventory as the body's. A local written there is judged by the same fixed point: a number-producing write keeps the fact, anything else drops the local to the generic route. The planner and the preheader pass the loop's condition and update; a body region has none. --- .../PENDING-region-proof-update-clause.md | 8 ++ .../src/collectors/not_bigint_locals.rs | 2 +- .../src/collectors/ptr_shape_numeric.rs | 82 +++++++++++++++- .../perry-codegen/src/stmt/region_loop/mod.rs | 20 +++- .../src/stmt/region_loop/plan.rs | 14 ++- .../test_gap_region_loop_control_writes.ts | 96 +++++++++++++++++++ 6 files changed, 217 insertions(+), 5 deletions(-) create mode 100644 changelog.d/PENDING-region-proof-update-clause.md create mode 100644 test-files/test_gap_region_loop_control_writes.ts diff --git a/changelog.d/PENDING-region-proof-update-clause.md b/changelog.d/PENDING-region-proof-update-clause.md new file mode 100644 index 0000000000..e977673765 --- /dev/null +++ b/changelog.d/PENDING-region-proof-update-clause.md @@ -0,0 +1,8 @@ +Fixed a miscompile in numeric loop regions: a loop-carried local that the +loop's `for` update clause or condition rewrote (for example +`for (...; i++, s = "a") { o.x = o.x + s; }`) kept its Number proof, because +the proof only judged writes in the loop body and the entry test runs once +before the loop. The region then added the string's bits as a double and +stored the result, a live string pointer, into the pointer-free F64 field +(`o.x` printed `a` instead of `1aa`). The proof now judges the condition's and +update's writes with the body's, so such a local takes the generic route. diff --git a/crates/perry-codegen/src/collectors/not_bigint_locals.rs b/crates/perry-codegen/src/collectors/not_bigint_locals.rs index 1b50defe1e..cdb8ce9811 100644 --- a/crates/perry-codegen/src/collectors/not_bigint_locals.rs +++ b/crates/perry-codegen/src/collectors/not_bigint_locals.rs @@ -392,7 +392,7 @@ pub(super) fn collect_writes<'a>( } } -fn collect_writes_expr<'a>( +pub(super) fn collect_writes_expr<'a>( e: &'a Expr, writes: &mut HashMap>>, candidates: &mut HashSet, diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index 7567e98a7e..63f30b0cb2 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs @@ -418,6 +418,12 @@ pub(crate) struct RegionNumberAssumptions<'a> { pub(crate) entry_candidates: &'a HashSet, pub(crate) static_numbers: &'a HashSet, pub(crate) f64_reads: &'a HashSet, + /// Expressions the region evaluates on every iteration outside its + /// statements: a loop region's condition and update. F observes their + /// writes on the back edge exactly as it observes its own, and the entry + /// tests run once before the loop, so a local they write must be judged + /// by the same fixed point as a body write. + pub(crate) loop_control: &'a [&'a Expr], } /// Locals whose every write is number-producing by construction — above all @@ -486,7 +492,7 @@ pub(crate) fn collect_numeric_by_construction_locals_in_region<'a>( // completely `o`'s shape was proven. Empty for every pre-existing caller. shape_members: &HashSet, shape_numeric_fields: &HashSet, - region: Option<&RegionNumberAssumptions<'_>>, + region: Option<&RegionNumberAssumptions<'a>>, ) -> HashSet { // ONE write walker for both fixpoints (`collect_not_bigint_locals` and // this one) — see its doc for why sharing is load-bearing. `None` = a @@ -495,6 +501,11 @@ pub(crate) fn collect_numeric_by_construction_locals_in_region<'a>( let mut writes: HashMap>> = HashMap::new(); let mut let_bound: HashSet = HashSet::new(); super::super::not_bigint_locals::collect_writes(stmts, &mut writes, &mut let_bound); + // A region's loop control runs between F iterations: every write it + // makes reaches F as surely as a body write does. + for e in region.map_or(&[][..], |r| r.loop_control) { + super::super::not_bigint_locals::collect_writes_expr(e, &mut writes, &mut let_bound); + } // The standalone #8105 consumer does not run the Ptr provenance // walk that normally supplies `const_local_inits`. Reconstruct the same // safe fact from the shared exhaustive write set: one initialized write @@ -1024,6 +1035,14 @@ mod region_number_tests { } fn number_set(stmts: &[Stmt], fresh_read: usize) -> HashSet { + number_set_with_control(stmts, &[], fresh_read) + } + + fn number_set_with_control( + stmts: &[Stmt], + loop_control: &[&Expr], + fresh_read: usize, + ) -> HashSet { let boxed = HashSet::new(); let globals = HashMap::new(); let empty_ids = HashSet::new(); @@ -1035,6 +1054,7 @@ mod region_number_tests { entry_candidates: &entry, static_numbers: &empty_ids, f64_reads: &reads, + loop_control, }; collect_numeric_by_construction_locals_in_region( stmts, @@ -1088,4 +1108,64 @@ mod region_number_tests { assert!(!after.contains(&STALE)); assert!(!after.contains(&ACC), "the stale write must drop ACC"); } + + fn fresh_ptr(stmts: &[Stmt]) -> usize { + match &stmts[0] { + Stmt::Let { init: Some(e), .. } => e as *const Expr as usize, + _ => unreachable!(), + } + } + + /// `for (...; ...; i++, acc = "a") { const n = o.x; acc = acc + n; }`: + /// the update clause runs between F iterations, after the one preheader + /// test of ACC. Its write must be judged like a body write, or F adds + /// a string's bits as a double. + #[test] + fn an_update_clause_write_withdraws_the_loop_carried_number_fact() { + let stmts = vec![let_read(FRESH), add_to_acc(FRESH)]; + let read = fresh_ptr(&stmts); + assert!( + number_set(&stmts, read).contains(&ACC), + "fixture: without loop control ACC is proven, or the check below is vacuous" + ); + let string_write = Expr::LocalSet(ACC, Box::new(Expr::String("a".to_string()))); + let after = number_set_with_control(&stmts, &[&string_write], read); + assert!( + !after.contains(&ACC), + "the update clause's string write must drop ACC" + ); + assert!(after.contains(&FRESH)); + + // A number-producing loop-control write keeps the fact: the fixed + // point judges the write, it does not refuse every written local. + let numeric_write = Expr::LocalSet( + ACC, + Box::new(Expr::Binary { + op: perry_hir::BinaryOp::Add, + left: Box::new(Expr::LocalGet(ACC)), + right: Box::new(Expr::Number(1.0)), + }), + ); + let kept = number_set_with_control(&stmts, &[&numeric_write], read); + assert!(kept.contains(&ACC)); + } + + /// `while ((acc = f()), ...)`: a condition write of an unknown value. + #[test] + fn a_condition_write_withdraws_the_loop_carried_number_fact() { + let stmts = vec![let_read(FRESH), add_to_acc(FRESH)]; + let read = fresh_ptr(&stmts); + let call_write = Expr::LocalSet( + ACC, + Box::new(Expr::Call { + callee: Box::new(Expr::LocalGet(99)), + args: Vec::new(), + type_args: Vec::new(), + byte_offset: 0, + }), + ); + let cond = Expr::Sequence(vec![call_write, Expr::LocalGet(ACC)]); + let after = number_set_with_control(&stmts, &[&cond], read); + assert!(!after.contains(&ACC), "the condition's write must drop ACC"); + } } diff --git a/crates/perry-codegen/src/stmt/region_loop/mod.rs b/crates/perry-codegen/src/stmt/region_loop/mod.rs index 9e2ec9700a..1a926e045c 100644 --- a/crates/perry-codegen/src/stmt/region_loop/mod.rs +++ b/crates/perry-codegen/src/stmt/region_loop/mod.rs @@ -497,9 +497,11 @@ fn begin_with( all = ctx.block().and(I1, &all, &pass); arrs.push(a); } + let loop_control: Vec<&Expr> = cond.into_iter().chain(update).collect(); let (number_locals, entry_tests) = number_facts( ctx, body, + &loop_control, &receivers, &p.bare_reads, &p.number_local_uses, @@ -601,6 +603,7 @@ fn body_region_plan(ctx: &FnCtx<'_>, body: &[Stmt]) -> Option<(usize, Plan)> { fn number_facts( ctx: &FnCtx<'_>, tail: &[Stmt], + loop_control: &[&Expr], receivers: &[Receiver], bare_reads: &[(usize, Recv, String)], number_local_uses: &HashSet, @@ -618,14 +621,25 @@ fn number_facts( }) }) .collect(); - number_facts_from_reads(ctx, tail, &f64_reads, number_local_uses, declared_locals) + number_facts_from_reads( + ctx, + tail, + loop_control, + &f64_reads, + number_local_uses, + declared_locals, + ) } /// The same 5L fixed point is used while planning and while lowering. The /// planner supplies only exact fresh bare reads protected by its proposed R. +/// `loop_control` is a loop region's condition and update: they run between +/// F iterations, after the one preheader test, so their writes are judged +/// with the body's. fn number_facts_from_reads( ctx: &FnCtx<'_>, tail: &[Stmt], + loop_control: &[&Expr], f64_reads: &HashSet, number_local_uses: &HashSet, declared_locals: &HashSet, @@ -651,6 +665,7 @@ fn number_facts_from_reads( entry_candidates: &entry_candidates, static_numbers: ctx.number_by_construction_locals, f64_reads, + loop_control, }; let numeric = crate::collectors::collect_numeric_by_construction_locals_in_region( tail, @@ -1050,9 +1065,12 @@ pub(crate) fn lower_split( let (number_locals, entry_tests) = if valid_slot.is_some() { (planned_number_locals, planned_entry_tests) } else { + // Only a body region gets here: it has no loop control of its own, + // and its tests run at the split on every entry. number_facts( ctx, tail, + &[], &receivers, &bare_reads, &number_local_uses, diff --git a/crates/perry-codegen/src/stmt/region_loop/plan.rs b/crates/perry-codegen/src/stmt/region_loop/plan.rs index 17bb2850a1..9337fc73d7 100644 --- a/crates/perry-codegen/src/stmt/region_loop/plan.rs +++ b/crates/perry-codegen/src/stmt/region_loop/plan.rs @@ -956,9 +956,13 @@ pub(super) fn plan( if proof_reads.is_empty() { return Some(seed); } + let loop_control: Vec<&Expr> = loop_ctl + .map(|(cond, update)| cond.into_iter().chain(update).collect()) + .unwrap_or_default(); let (locals, _) = number_facts_from_reads( ctx, tail, + &loop_control, &proof_reads, &seed.number_local_uses, &seed.declared_locals, @@ -991,8 +995,14 @@ pub(super) fn plan( }) }) .collect(); - let (locals, _) = - number_facts_from_reads(ctx, tail, &reads, &p.number_local_uses, &p.declared_locals); + let (locals, _) = number_facts_from_reads( + ctx, + tail, + &loop_control, + &reads, + &p.number_local_uses, + &p.declared_locals, + ); let locals: HashSet = locals.into_iter().collect(); if !reads.is_subset(&proof_reads) || !locals.is_subset(&proof_locals) { return None; diff --git a/test-files/test_gap_region_loop_control_writes.ts b/test-files/test_gap_region_loop_control_writes.ts new file mode 100644 index 0000000000..272a2116e0 --- /dev/null +++ b/test-files/test_gap_region_loop_control_writes.ts @@ -0,0 +1,96 @@ +// A loop region's Number proof for a loop-carried local must see every write +// the region can observe, not only the body's. The condition and the update +// clause run between iterations, after the one preheader entry test, so a +// local they rewrite to a string or an object must not be added as a double +// (and a pointer must never be stored into a pointer-free F64 lane). +class P { + x: number; + constructor() { + this.x = 0; + } +} + +function classUpdate(o: P, s: any): any { + for (let i = 0; i < 3; i++, s = "a") { + o.x = o.x + s; + } + return o.x; +} + +function literalUpdate(o: { x: number }, s: any): any { + for (let i = 0; i < 3; i++, s = "b") { + o.x = o.x + s; + } + return o.x; +} + +function gen(i: number): any { + return i < 1 ? 5 : "g" + i; +} + +function condFor(o: P, n: number): any { + let s: any = 1; + for (let i = 0; (s = gen(i)), i < n; i++) { + o.x = o.x + s; + } + return o.x; +} + +let k = 0; +function next(): any { + k++; + return k === 1 ? 2 : k < 4 ? "w" + k : null; +} + +function condWhile(o: { x: number }): any { + let s: any = 1; + while ((s = next()) && o.x !== -1) { + o.x = o.x + s; + } + return o.x; +} + +function commaUpdate(o: P, s: any, t: any): any { + for (let i = 0; i < 4; (i++, (s = t), (t = "c"))) { + o.x = o.x + s; + } + return o.x; +} + +function compareUpdate(o: P, s: any): number { + let hits = 0; + for (let i = 0; i < 3; i++, s = "9") { + if (o.x < s) hits++; + o.x = o.x + 1; + } + return hits; +} + +function objUpdate(o: P, s: any): any { + const keep = { tag: "live" }; + for (let i = 0; i < 3; i++, s = keep) { + o.x = o.x + s; + } + return o.x; +} + +function main(): void { + console.log("classUpdate", classUpdate(new P(), 1)); + console.log("literalUpdate", literalUpdate({ x: 0 }, 1)); + console.log("condFor", condFor(new P(), 3)); + k = 0; + console.log("condWhile", condWhile({ x: 0 })); + console.log("commaUpdate", commaUpdate(new P(), 1, 2)); + console.log("compareUpdate", compareUpdate(new P(), 5)); + console.log("objUpdate", objUpdate(new P(), 1)); + const big: P[] = []; + for (let r = 0; r < 200; r++) { + const o = new P(); + classUpdate(o, 1); + big.push(o); + } + let junk: string[] = []; + for (let r = 0; r < 20000; r++) junk.push("j" + r); + console.log("after-gc", big[0].x, big[199].x, junk.length); +} +main(); From 673e19e73913875a954783abdddb53fe3fea4e05 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Sat, 3 Oct 2026 09:45:46 +0200 Subject: [PATCH 2/2] changelog: key the region proof fix to PR 11782 --- ...proof-update-clause.md => 11782-region-proof-update-clause.md} | 0 1 file changed, 0 insertions(+), 0 deletions(-) rename changelog.d/{PENDING-region-proof-update-clause.md => 11782-region-proof-update-clause.md} (100%) diff --git a/changelog.d/PENDING-region-proof-update-clause.md b/changelog.d/11782-region-proof-update-clause.md similarity index 100% rename from changelog.d/PENDING-region-proof-update-clause.md rename to changelog.d/11782-region-proof-update-clause.md