From a6e52065bb7eaee3bbef5a1c3f879c616e3d24bc Mon Sep 17 00:00:00 2001 From: zinc Date: Thu, 15 Oct 2026 05:25:58 +0330 Subject: prover: do not restore length facts after a call-loop Restoring undirtied lafacts when the body might free was wrong: push can grow an array without dirtying its name, so a[99] after push warned against a stale length 0. Keep the old lafact_keep rule; reorder explain_prover so the constant/affine cases run before the touch() loops. --- src/compiler/analyzer.zc | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'src/compiler') diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc index bf7dd9f..8ceaf09 100644 --- a/src/compiler/analyzer.zc +++ b/src/compiler/analyzer.zc @@ -703,15 +703,15 @@ word lafact_save() { while (i < nloc) { b[2 + i - lbase] = lafact[i]; i++; } return b; } -// after a loop: the locals its body left alone get back the allocation facts -// the loop forgot. a body that might free (r[55]) still restores facts for -// undirtied locals: a call that did not take the local cannot have freed it, -// and proofs inside a later loop re-check r[55] for that loop. without this, -// one touch() earlier in the function would permanently drop every length fact. +// after a loop that frees nothing: the locals its body left alone get back the +// allocation facts the loop forgot. a body with a call (r[55]) does not restore: +// push/pop can change a growable length without "dirtying" the name, and a free +// through an alias is possible; restoring would warn on a[99] after push with a +// stale length 0. int lafact_keep(word r, word b) { int i; - if (!b || dry || r[0]) return 0; + if (!b || dry || r[0] || r[55]) return 0; i = b[0]; while (i < b[1] && i < nloc) { if (b[2 + i - b[0]] && !lafact[i] && !ldirty(r, lname[i]) && lclean(i)) lafact[i] = b[2 + i - b[0]]; i++; } return 0; -- cgit v1.2.3