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.

2 files changed, 13 insertions, 11 deletions

diff --git a/tests/programs/explain_prover.expected b/tests/programs/explain_prover.expected
index c43c72d..f6854c7 100644
--- a/tests/programs/explain_prover.expected
+++ b/tests/programs/explain_prover.expected
@@ -1,9 +1,9 @@
 {"version":1}
-{"file":"<eval>","line":18,"col":42,"end_line":18,"end_col":45,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"}
-{"file":"<eval>","line":22,"col":51,"end_line":22,"end_col":54,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
-{"file":"<eval>","line":26,"col":62,"end_line":26,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"}
-{"file":"<eval>","line":27,"col":71,"end_line":27,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
-{"file":"<eval>","line":30,"col":46,"end_line":30,"end_col":49,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
-{"file":"<eval>","line":34,"col":81,"end_line":34,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
-{"file":"<eval>","line":35,"col":70,"end_line":35,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
-{"file":"<eval>","line":36,"col":59,"end_line":36,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":19,"col":42,"end_line":19,"end_col":45,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"}
+{"file":"<eval>","line":23,"col":51,"end_line":23,"end_col":54,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
+{"file":"<eval>","line":29,"col":46,"end_line":29,"end_col":49,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
+{"file":"<eval>","line":33,"col":81,"end_line":33,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":34,"col":70,"end_line":34,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":35,"col":59,"end_line":35,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":37,"col":62,"end_line":37,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"}
+{"file":"<eval>","line":38,"col":71,"end_line":38,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"size-unknown","fix":"the compiler does not know the size of the block; allocate it here with a constant size, or index a fixed array"}
diff --git a/tests/programs/explain_prover.zc b/tests/programs/explain_prover.zc
index 14486b5..088cb1d 100644
--- a/tests/programs/explain_prover.zc
+++ b/tests/programs/explain_prover.zc
@@ -3,6 +3,7 @@ include rt;
 
 // the loop prover, case by case: each "kept" line must stay in zy --explain-checks
 // and each "proved" line must not. run, it prints one checksum.
+// call-loops come last: they clear allocation facts for the rest of the function.
 int touch() { return 0; }
 int[16] sq;
 int main() {
@@ -20,11 +21,9 @@ int main() {
 	for (i = 0; i < len(a); i++) s = s + b[i];	// proved: 8 <= 10
 	for (i = 0; i < len(a); i++) s = s + sq[i];	// proved: 8 <= 16
 	for (i = 0; i < len(a); i++) if (i < 6) s = s + c[i];	// kept: 6 < 8
-	// 3. a pointer of constant size at depth 2 and 3
+	// 3. a pointer of constant size
 	for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) p[j] = j;	// proved
 	for (i = 0; i < 2; i++) for (k = 0; k < 2; k++) for (j = 0; j < 16; j++) s = s + p[j];	// proved
-	for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) { s = s + p[j]; touch(); }	// kept: the body calls
-	for (i = 0; i < 2; i++) { touch(); for (j = 0; j < 16; j++) s = s + p[j]; }	// kept: the outer body calls
 	// 4. new(fixed int[?], n) with a constant n
 	for (i = 0; i < 6; i++) s = s + c[i];	// proved
 	for (i = 0; i < 7; i++) if (i < 6) s = s + c[i];	// kept: 7 > 6
@@ -34,6 +33,9 @@ int main() {
 	for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) if (i * 4 + k < 15) s = s + m15[i * 4 + k];	// kept: 15 < 16
 	for (i = 0; i < 4; i++) for (k = 0; k < 5; k++) if (k < 4) s = s + m[i * 4 + k];	// kept: k < 5
 	for (i = 0; i < n; i++) for (k = 0; k < n; k++) s = s + m[i * n + k];	// kept: n is a variable
+	// 6. a call in the body keeps the check (clears facts afterward)
+	for (i = 0; i < 2; i++) for (j = 0; j < 16; j++) { s = s + p[j]; touch(); }	// kept: the body calls
+	for (i = 0; i < 2; i++) { touch(); for (j = 0; j < 16; j++) s = s + p[j]; }	// kept: the outer body calls
 	rt.put_n(s); rt.put_c(10);
 	rt.free(d*a); rt.free(d*b); rt.free(d*c); rt.free(d*m); rt.free(d*m15); rt.free(p);
 	return 0;