From 3a1f529590c7ac8e363351cebf61974ad47f7729 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ralph=20K=C3=BCpper?= Date: Thu, 12 Nov 2026 23:56:49 +0100 Subject: [PATCH] codegen: an Array literal of numbers is numeric storage for the Add proof only while the body only reads its elements and length (PERRY_LITERAL_ARRAY_WRITE_CHECK) --- changelog.d/literal-array-sum-proof.md | 1 + .../perry-codegen/src/collectors/ptr_shape.rs | 4 + .../ptr_shape_group_numeric_tests.rs | 62 ++++++++++++ .../src/collectors/ptr_shape_numeric.rs | 78 +++++++++++++++ .../perry/src/commands/compile/compile_env.rs | 1 + .../test_literal_array_sum_after_store.ts | 96 +++++++++++++++++++ 6 files changed, 242 insertions(+) create mode 100644 changelog.d/literal-array-sum-proof.md create mode 100644 tests/parity/language/array/test_literal_array_sum_after_store.ts diff --git a/changelog.d/literal-array-sum-proof.md b/changelog.d/literal-array-sum-proof.md new file mode 100644 index 00000000000..7f5bc494f99 --- /dev/null +++ b/changelog.d/literal-array-sum-proof.md @@ -0,0 +1 @@ +`t = t + a[i]` over a local bound to an Array literal of numbers (`const a = [1, 2, 3]`) no longer drops the elements after a string: the Add proof (`collectors/ptr_shape_numeric.rs`, `numeric_view_value_or_undefined`) treated the literal as numeric storage whatever the body stored into it later, so the accumulator counted as a Number by construction and the numeric arm of the guarded add `fadd`ed the string it held after `(a as any)[1] = "two"` (`1two` where node prints `1two3`). A literal is now numeric storage only while every use of the local in the body is an element read or a `length` read (`retain_unwritten_literal_arrays`, applied to the stable initializers of the numeric fixpoint and to the `Ptr` walk's const initializers); an element store, a method call, an alias, an argument or a capture voids it. Switch `PERRY_LITERAL_ARRAY_WRITE_CHECK=0` keeps today's lowering. Fixture `tests/parity/language/array/test_literal_array_sum_after_store.ts`. diff --git a/crates/perry-codegen/src/collectors/ptr_shape.rs b/crates/perry-codegen/src/collectors/ptr_shape.rs index bc1c919e766..099d54ff2e1 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape.rs @@ -506,6 +506,10 @@ fn collect_shape_proven_ptr_locals_impl( family_present, .. } = walk; + // An Array literal of numbers is numeric storage only while nothing but + // element and `length` reads use it. + let mut const_local_inits = const_local_inits; + numeric::retain_unwritten_literal_arrays(stmts, &[], &mut const_local_inits); // #7770: locals whose every write is number-producing by construction — // they let a provenance `new C(i, i + 1)` resolve its parameters. let mut numeric_locals = collect_numeric_by_construction_locals( diff --git a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs index 07c8a7a94ad..14fe1a29a45 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_group_numeric_tests.rs @@ -1021,3 +1021,65 @@ fn update_value_resolves_via_not_bigint() { "without the not-BigInt fact the update's value is unproven" ); } + +/// `t = t + a[i]` over `const a = [1, 2, 3]`: the literal is numeric storage +/// while only element and `length` reads use it; one element store (or any +/// other use) voids the accumulator's proof. +#[test] +fn literal_array_sum_loses_its_proof_to_an_element_store() { + let program = |store: bool| { + let mut stmts = vec![ + Stmt::Let { + id: 40, + name: "a".to_string(), + ty: Type::Any, + mutable: false, + init: Some(Expr::Array( + vec![Expr::Integer(1), Expr::Integer(2), Expr::Integer(3)], + None, + )), + }, + Stmt::Let { + id: 41, + name: "t".to_string(), + ty: Type::Any, + mutable: true, + init: Some(Expr::Number(0.0)), + }, + ]; + if store { + stmts.push(Stmt::Expr(Expr::IndexSet { + object: Box::new(Expr::LocalGet(40)), + index: Box::new(Expr::Integer(1)), + value: Box::new(Expr::String("two".to_string())), + byte_offset: 0, + byte_end: 0, + element_offset: 0, + })); + } + stmts.push(counted_loop( + 42, + arr_len(40), + vec![Stmt::Expr(Expr::LocalSet( + 41, + Box::new(Expr::Binary { + op: BinaryOp::Add, + left: Box::new(Expr::LocalGet(41)), + right: Box::new(Expr::IndexGet { + element_offset: 0, + byte_offset: 0, + byte_end: 0, + object: Box::new(Expr::LocalGet(40)), + index: Box::new(Expr::LocalGet(42)), + }), + }), + ))], + )); + stmts + }; + assert!(numeric_locals_of(&program(false)).contains(&41)); + assert!( + !numeric_locals_of(&program(true)).contains(&41), + "a string stored into the literal makes `t + a[i]` a concatenation" + ); +} diff --git a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs index 23c5610f3c2..dd92456b454 100644 --- a/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs +++ b/crates/perry-codegen/src/collectors/ptr_shape_numeric.rs @@ -413,6 +413,79 @@ pub(super) fn prove_group_numeric_fields<'a>( // ── #7770: numeric-by-construction locals ────────────────────────────────── +/// `PERRY_LITERAL_ARRAY_WRITE_CHECK=0` (`off`, `false`) keeps today's main: +/// a local bound to an Array literal of numbers counts as numeric storage +/// whatever the body later stores into it. Read per call; a compile-cache +/// input. +pub(crate) fn literal_array_write_check_enabled() -> bool { + !matches!( + std::env::var("PERRY_LITERAL_ARRAY_WRITE_CHECK").as_deref(), + Ok("0") | Ok("off") | Ok("false") + ) +} + +/// Drop from `inits` every local bound to an Array literal of numbers +/// (`const a = [1, 2, 3]`, the Add rule's `numeric_storage`) that `stmts` use +/// other than to read an element (`a[i]`) or `length`. An element store, a +/// method call, an alias, an argument or a capture can put a non-Number into +/// the Array; then `a[i]` is no Number-or-`undefined` and the accumulator of +/// `t = t + a[i]` is no Number by construction: after +/// `(a as any)[1] = "two"` its numeric arm `fadd`ed the string it held +/// (`1two` where node prints `1two3`). The locals are block-scoped bindings +/// of this body, so its expressions (closure bodies included) are all their +/// uses. +pub(super) fn retain_unwritten_literal_arrays( + stmts: &[Stmt], + extra: &[&Expr], + inits: &mut HashMap>, +) { + if !literal_array_write_check_enabled() { + return; + } + let candidates: HashSet = inits + .iter() + .filter(|(_, init)| { + matches!(init, Some(Expr::Array(elements, _)) + if elements.iter().all(|e| matches!(e, Expr::Integer(_) | Expr::Number(_)))) + }) + .map(|(&id, _)| id) + .collect(); + if candidates.is_empty() { + return; + } + // Every use of a candidate, and the uses that only read it. + let mut uses: HashMap = HashMap::new(); + let mut visit = |e: &Expr| { + let read = match e { + Expr::LocalGet(id) => { + if candidates.contains(id) { + uses.entry(*id).or_default().0 += 1; + } + return; + } + Expr::IndexGet { object, .. } => object, + Expr::PropertyGet { + object, property, .. + } if property == "length" => object, + _ => return, + }; + if let Expr::LocalGet(id) = read.as_ref() { + if candidates.contains(id) { + uses.entry(*id).or_default().1 += 1; + } + } + }; + perry_hir::tdz_check::for_each_stmts_expr(stmts, &mut visit); + for e in extra { + perry_hir::tdz_check::for_each_expr_in(e, &mut visit); + } + for id in candidates { + if uses.get(&id).is_some_and(|&(all, reads)| all != reads) { + inits.remove(&id); + } + } +} + /// Extra leaves and entry candidates for one guarded region's F clone. pub(crate) struct RegionNumberAssumptions<'a> { pub(crate) entry_candidates: &'a HashSet, @@ -524,6 +597,11 @@ pub(crate) fn collect_numeric_by_construction_locals_in_region<'a>( stable_local_inits.entry(id).or_insert(Some(*init)); } } + retain_unwritten_literal_arrays( + stmts, + region.map_or(&[][..], |r| r.loop_control), + &mut stable_local_inits, + ); let empty_members: HashSet = shape_members.clone(); let empty_fields: HashSet = shape_numeric_fields.clone(); let mut numeric: HashSet = let_bound diff --git a/crates/perry/src/commands/compile/compile_env.rs b/crates/perry/src/commands/compile/compile_env.rs index 424c50d0c1e..d4b52d33d59 100644 --- a/crates/perry/src/commands/compile/compile_env.rs +++ b/crates/perry/src/commands/compile/compile_env.rs @@ -199,6 +199,7 @@ pub(super) const COMPILE_ENV_VARS: &[&str] = &[ "PERRY_LINUX_MUSL_SYSROOT", "PERRY_LINUX_SYSROOT", "PERRY_LIST_BIRTH_CAPACITY", + "PERRY_LITERAL_ARRAY_WRITE_CHECK", "PERRY_LITERAL_FOR_OF", "PERRY_LLD_LINK", "PERRY_LLVM_AR", diff --git a/tests/parity/language/array/test_literal_array_sum_after_store.ts b/tests/parity/language/array/test_literal_array_sum_after_store.ts new file mode 100644 index 00000000000..5a5bf525bf9 --- /dev/null +++ b/tests/parity/language/array/test_literal_array_sum_after_store.ts @@ -0,0 +1,96 @@ +// `t = t + a[i]` over a local bound to an Array literal of numbers: the Add proof took the literal as numeric storage +// whatever the body stored into it later, so the accumulator counted as a Number by construction and its numeric arm +// `fadd`ed the string it held after a string element (`1two` where node prints `1two3`). Every use other than an +// element or `length` read now voids the proof. Controls: unwritten literals (numeric sums), typed arrays, a +// numeric store, sums through a helper. +function direct(): any { + const a = [1, 2, 3]; + (a as any)[1] = "two"; + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function pushed(): any { + const a = [1, 2, 3]; + (a as any[]).push("four", 5); + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function aliased(): any { + const a = [4, 5, 6]; + const b: any = a; + b[0] = "x"; + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function writeFirst(arr: any): void { + arr[0] = "w"; +} +function viaCall(): any { + const a = [7, 8, 9]; + writeFirst(a); + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function viaClosure(): any { + const a = [1, 1, 1]; + const set = (k: number) => { + (a as any)[k] = "c"; + }; + set(2); + let t: any = 10; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function filled(): any { + const a = [1, 2, 3]; + (a as any).fill("f", 1, 2); + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function twice(): string { + // The same loop over the same literal before and after a string store. + const a = [1, 2, 3]; + let out = ""; + for (let round = 0; round < 2; round++) { + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + out += String(t) + ";"; + (a as any)[0] = "s"; + } + return out; +} +// Controls. +function untouched(): any { + const a = [1.5, 2.5, 3]; + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function numericStore(): any { + const a = [1, 2, 3]; + a[1] = 20; + let t = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function typed(): any { + const a = new Float64Array([1, 2, 3]); + (a as any)[1] = "5"; + let t: any = 0; + for (let i = 0; i < a.length; i++) t = t + a[i]; + return t; +} +function outOfBounds(): any { + const a = [1, 2]; + let t: any = 0; + for (let i = 0; i <= a.length; i++) t = t + a[i]; + return t; +} +console.log(direct(), pushed(), aliased(), viaCall(), viaClosure(), filled()); +console.log(twice()); +console.log(untouched(), numericStore(), typed(), outOfBounds());