fix(codegen): region Number proof judges loop condition and update writes

changelog.d/11782-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.

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<u32, Vec<Option<&'a Expr>>>,
     candidates: &mut HashSet<u32>,

crates/perry-codegen/src/collectors/ptr_shape_numeric.rs

@@ -418,6 +418,12 @@ pub(crate) struct RegionNumberAssumptions<'a> {
     pub(crate) entry_candidates: &'a HashSet<u32>,
     pub(crate) static_numbers: &'a HashSet<u32>,
     pub(crate) f64_reads: &'a HashSet<usize>,
+    /// 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<u32>,
     shape_numeric_fields: &HashSet<String>,
-    region: Option<&RegionNumberAssumptions<'_>>,
+    region: Option<&RegionNumberAssumptions<'a>>,
 ) -> HashSet<u32> {
     // 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<u32, Vec<Option<&'a Expr>>> = HashMap::new();
     let mut let_bound: HashSet<u32> = 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<Shape> 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<u32> {
+        number_set_with_control(stmts, &[], fresh_read)
+    }
+
+    fn number_set_with_control(
+        stmts: &[Stmt],
+        loop_control: &[&Expr],
+        fresh_read: usize,
+    ) -> HashSet<u32> {
         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");
+    }
 }

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<u32>,
@@ -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<usize>,
     number_local_uses: &HashSet<u32>,
     declared_locals: &HashSet<u32>,
@@ -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,

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<u32> = locals.into_iter().collect();
         if !reads.is_subset(&proof_reads) || !locals.is_subset(&proof_locals) {
             return None;

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();