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.

1 files changed, 6 insertions, 6 deletions

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;