wip: prover gaps (inline len bound, cross-array, rt.new depth, fixed new, affine i*n+k); unbuilt and untested

7 files changed, 172 insertions, 43 deletions

diff --git a/docs/SPEC.md b/docs/SPEC.md
index 7f37e33..06ee11c 100644
--- a/docs/SPEC.md
+++ b/docs/SPEC.md
@@ -667,7 +667,7 @@ int y = 7; asm { y @ 1 + y ! }    // y is 8
 
 4.15.2 the runtime, the core, the compiler, the language server, `run.zc` and `build.zc` are unbounded; std, icon and actor are checked except where a function reads headers on purpose.
 
-4.15.3 the compiler drops a check it can prove, and never changes when a check that can fail faults. a check is dropped for a constant index inside the array or the block; in a loop `for (...; i < b; i++)` whose body leaves `i`, `b` and the array alone (it assigns, increments or takes the address of none of them, and makes no closure), for `a[i]` when `b` is `len(a)`, or a constant no larger than a fixed array's length, or than the requested size of the block a pointer was set from (never a rounded block size). for a pointer the body must also call nothing, since a call might free or resize the block. when `b` is an `int` variable, the check of `a[i]` against `n` elements is hoisted: the loop entry works out once whether `0 <= i` and `b <= n`, and the check runs on each access only when that failed, so a fault still comes at the same access, after the same side effects.
+4.15.3 the compiler drops a check it can prove, and never changes when a check that can fail faults. a check is dropped for a constant index inside the array or the block; in a loop `for (...; i < b; i++)` whose body leaves `i`, `b` and the array alone (it assigns, increments or takes the address of none of them, and makes no closure), for `a[i]` when `b` is `len(a)`, or a constant no larger than a fixed array's length, or than the requested size of the block a pointer was set from (never a rounded block size). `b` may be `len(a)` written in the test itself, or the `len()` of another fixed array whose length is a known constant no larger than the one indexed. the length of `new(fixed T[?], n)` with a constant `n` is known like the size of a block. the loops may nest to any depth; every loop between the access and the one the size is known at must leave the array or pointer alone. an index `i * n + k` (sums and products of proved loop indices and constants, none negative) is dropped when its largest value is inside the array or block, as for `i < n`, `k < n` into exactly `n * n` elements; with a variable `n` the check stays. for a pointer the body must also call nothing, since a call might free or resize the block (any call: the block may be one another pointer aliases). when `b` is an `int` variable, the check of `a[i]` against `n` elements is hoisted: the loop entry works out once whether `0 <= i` and `b <= n`, and the check runs on each access only when that failed, so a fault still comes at the same access, after the same side effects.
 
 4.15.4 `zy --explain-checks [file] < source` compiles the unit, does not run it, and prints the checks the compiler kept, from the same analysis that drops the others, as json lines (format version 1). the first line is `{"version":1}`. each further line is one object for one kept check, in source order: `file` (the name given, default `<eval>`), `line`, `col` (from 1, of the `[`), `end_line`, `end_col` (just past the `]`), `fn` (the function; `<closure>` or `<eval>` outside a named one), `kind` (`index` for an array, `pointer` for a pointer), `loop_depth` (enclosing loops), `reason`, `fix` (prose), and optionally `edit` (`{"range":{"line":..,"col":..,"end_line":..,"end_col":..},"text":".."}`), present only for a purely mechanical fix. the reasons: `index-not-loop-variable` (the index is not the variable of an enclosing `for (i = ..; i < b; i++)`), `bound-not-invariant` (the body changes the index, the bound or the array, takes an address or makes a closure), `index-not-len-derived` (the bound is not `len()` of the array or a small enough constant), `size-unknown` (a pointer whose block size the compiler does not know), `pointer-may-be-freed` (the body calls something that might free or resize the block), `packed-elements` (sized-integer elements, always checked by the runtime) and `hoisted-to-loop-entry` (kept, but it runs only when the check at the loop entry failed). checks in included files, in unbounded code and in o3 code (which implies unbounded) are not listed. version 1 is stable: new kinds, reasons and fields may appear, and a consumer ignores a kind, a reason or a field it does not know.
 
diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc
index 666a89d..8b52f83 100644
--- a/src/compiler/analyzer.zc
+++ b/src/compiler/analyzer.zc
@@ -501,18 +501,6 @@ int proven(int a, int ix) {
 	}
 	return 0;
 }
-// i >= 0 and i < n for a fixed array of n elements, proved by a loop test
-// against a constant of at most n and a step of +1 (kw_for records the
-// constant as the array field, minus two, with -1 for the bound local)
-int proven_n(int ix, int n) {
-	int k = lsp, w;
-	while (k > loopbase) {
-		k--;
-		w = lpfact[k];
-		if (w >= 0 && p_iv(w) == ix && p_bd(w) == -1 && 0 - p_ar(w) - 2 <= n) return 1;
-	}
-	return 0;
-}
 // ---- loop bodies and hoisted checks ----
 
 // a loop proof only holds while the body leaves the index, the bound and the
@@ -706,21 +694,6 @@ int hoist_stub(word r, int c0) {
 	jmp(c0);
 	return 0;
 }
-// i < n for a pointer local arr to a block of n words: a loop test against a
-// constant of at most n, in a loop whose body leaves arr alone
-
-int proven_p(int ix, int n, int arr) {
-	int k = lsp, w; word r;
-	while (k > loopbase) {
-		k--;
-		w = lpfact[k];
-		if (w >= 0 && p_iv(w) == ix && p_bd(w) == -1 && 0 - p_ar(w) - 2 <= n) {
-			r = linfo(k);
-			return r && !ldirty(r, lname[arr]) && lclean(arr) && !r[55];
-		}
-	}
-	return 0;
-}
 // the allocation facts of the function's locals, kept past the loop top that forgets them
 
 word lafact_save() {
@@ -740,22 +713,107 @@ int lafact_keep(word r, word b) {
 	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;
 }
-// the allocation fact of the pointer local bl at the entry of the innermost
-// loop over ix, or 0
+// the allocation fact of the local bl saved at the entry of an enclosing loop,
+// at any depth, or 0. every loop from here out to the one that saved it has to
+// leave bl alone and free nothing, so the block is still the one it was. (ix is
+// unused; kept so the callers read the same)
 
 word entry_fact(int ix, int bl) {
-	int k = lsp; word r, b;
-	if (ix < 0 || bl < 0) return 0;
+	int k = lsp; word r, b, f;
+	if (bl < 0) return 0;
 	while (k > loopbase) {
 		k--;
 		r = linfo(k);
-		if (!r || r[40] != ix) continue;
+		if (!r || ldirty(r, lname[bl]) || !lclean(bl) || r[55]) return 0;
 		b = r[56];
-		if (!b || bl < b[0] || bl >= b[1]) return 0;
-		return b[2 + bl - b[0]];
+		if (b && bl >= b[0] && bl < b[1]) { f = b[2 + bl - b[0]]; if (f) return f; }
 	}
 	return 0;
 }
+// the length of the fixed growable array local a when the analyzer knows it
+// is a constant: new(fixed T[?], n) with a constant n. -1 when unknown
+
+int dyn_len(int a) {
+	word f, t;
+	if (a < 0) return 0 - 1;
+	t = ltype[a];
+	if (t[0] != TY_DYN || !t[3] || tbytes(t[4])) return 0 - 1;
+	f = lafact[a];
+	if (!f || f[2] != 3 || f[1] == 2 || f[0] < 0 || f[6]) f = entry_fact(0 - 1, a);
+	if (!f || f[2] != 3 || f[1] == 2 || f[0] < 0 || f[6]) return 0 - 1;
+	return f[0];
+}
+// the constant that the loop proof w keeps its index under, or -1: a test
+// against a constant, or against len() of an array of constant length
+
+int pbound(int w) {
+	if (p_bd(w) == 0 - 1) return 0 - p_ar(w) - 2;
+	if (p_ar(w) >= 0) return dyn_len(p_ar(w));
+	return 0 - 1;
+}
+// i >= 0 and i < n for a fixed array of n elements, proved by a loop test
+// with a step of +1 against a constant of at most n, or len() of an array of
+// at most n elements
+
+int proven_n(int ix, int n) {
+	int k = lsp, w, b;
+	while (k > loopbase) {
+		k--;
+		w = lpfact[k];
+		if (w >= 0 && p_iv(w) == ix) { b = pbound(w); if (b >= 0 && b <= n) return 1; }
+	}
+	return 0;
+}
+// the same for a pointer local arr to a block of n words, or a fixed growable
+// array of n elements, in a loop whose body leaves arr alone and frees nothing
+
+int proven_p(int ix, int n, int arr) {
+	int k = lsp, w, b; word r;
+	while (k > loopbase) {
+		k--;
+		w = lpfact[k];
+		if (w >= 0 && p_iv(w) == ix) {
+			b = pbound(w);
+			if (b < 0 || b > n) return 0;
+			r = linfo(k);
+			return r && !ldirty(r, lname[arr]) && lclean(arr) && !r[55];
+		}
+	}
+	return 0;
+}
+// an exclusive upper bound of the value just compiled, when it is known not
+// to be negative, or -1: a loop index under a proof, a constant, or a sum or
+// product of those (bin keeps it in xub, for the code address xubat)
+
+int local_ub(int i) {
+	int k = lsp, w, b, best = 0 - 1;
+	if (ltype[i] != tint) return 0 - 1;
+	while (k > loopbase) {
+		k--;
+		w = lpfact[k];
+		if (w >= 0 && p_iv(w) == i) { b = pbound(w); if (b >= 0 && (best < 0 || b < best)) best = b; }
+	}
+	return best;
+}
+// every enclosing loop leaves the local arr alone and frees nothing (any call
+// might free a block another pointer aliases)
+
+int ptr_still(int arr) {
+	int k = lsp; word r;
+	while (k > loopbase) {
+		k--;
+		r = linfo(k);
+		if (!r || ldirty(r, lname[arr]) || !lclean(arr) || r[55]) return 0;
+	}
+	return 1;
+}
+int oub() {
+	if (lv && lvk == LV_LOCAL) return local_ub(lvi);
+	if (lv) return 0 - 1;
+	if (xconst && xcval >= 0 && xcval < 0x40000000) return xcval + 1;
+	if (xubat == here) return xub;
+	return 0 - 1;
+}
 // the number of elements behind a pointer local: the requested size of the
 // block it was set from, when the analyzer knows it (never a rounded block
 // size), for one-word elements; -1 when unknown
diff --git a/src/compiler/base.zc b/src/compiler/base.zc
index a8dc19f..dc786b5 100644
--- a/src/compiler/base.zc
+++ b/src/compiler/base.zc
@@ -328,7 +328,8 @@ int o3on, o3nxt, o3one; word[32] o3sl; word[32] o3rg; int no3sl; word[O3_REGIONS
 word[8] o3free; int no3free, o3nreg; word[NL] o3cache_initial; word o3cache = o3cache_initial; int argloc, s_hitems, s_hlen, s_fatten;
 // operator names used by numeric type checks.
 word[12] numops; int nnumops, s_fixed, s_dlen, s_dcap, s_dnew, s_dat, s_dpush, s_dpop, s_dresize, xconst, xcval;
-int xlenloc, arrloc, fortest, forstep, ft_iv, ft_bd, ft_ir, ft_ck, ft_nops, fs_ok, xstamp;
+int xlenloc, arrloc, fortest, forstep, ft_iv, ft_bd, ft_ir, ft_ck, ft_ln, ft_nops, fs_ok, xstamp;
+int xub, xubat = 0 - 1;	// an upper bound of the value just compiled (oub), valid while here == xubat
 // what each live loop's body may change, and its hoisted checks (one 56-word
 // record per loop depth, the first 64 depths; see body_scan and hoist_guard)
 const int LPI_N = 64, LPI_W = 60;
diff --git a/src/compiler/expr.zc b/src/compiler/expr.zc
index 9d7cc2b..7471556 100644
--- a/src/compiler/expr.zc
+++ b/src/compiler/expr.zc
@@ -1380,7 +1380,7 @@ int ptr_chk(int sz) {
 // through rt.bchk, which only knows the size of a heap block's first word.
 int postfix() { return postfix_tail(primary()); }
 int postfix_tail(int c) {
-	int b, n, t, et; word ft; word[8] bs; int k, ci, was, al, ix, enh, cz, cj, place, offset, temporary, call_owner, readonly, ub, bl, ic, inr, hg, pn; word storage, storage_mask, call_origins;
+	int b, n, t, et; word ft; word[8] bs; int k, ci, was, al, ix, enh, cz, cj, place, offset, temporary, call_owner, readonly, ub, bl, ic, inr, hg, pn, iu; word storage, storage_mask, call_origins;
 	while (1) {
 		if (tk == T_ID && tv == s_as) {	// e as T: same bits, another type
 			next(); t = ptype(); rval(); if (!xaf || xaf[2] != 5) xaf = 0; vf_coerce(t, 0);
@@ -1442,6 +1442,7 @@ int postfix_tail(int c) {
 				c = expr();
 				ix = -1;
 				if (lv && lvk == LV_LOCAL) ix = lvi;
+				iu = oub();
 				rval(); plainuse(c);
 				if (xconst) offset = xcval; af_index(storage, place);
 				tcneed(isnum(xty) || xty == tword, "an index has to be a number", xty);
@@ -1451,7 +1452,7 @@ int postfix_tail(int c) {
 				if (ub) {	// unbounded, or o3: just the address
 					if (ci && !mdbg && lookup(s_outside) >= 0) { vaddr(ci); op(O_LD); op(O_SWAP); mulsz(et); op(O_ADD); }
 					else addr_stk(et);
-				} else if (!mdbg && ix >= 0 && al >= 0 && proven(al, ix)) {	// the loop test already compared this index with the length
+				} else if (!mdbg && al >= 0 && ((ix >= 0 && (proven(al, ix) || proven_p(ix, dyn_len(al), al))) || (ix < 0 && iu > 0 && iu <= dyn_len(al) && ptr_still(al)))) {	// the loop test already compared this index with the length, or with a constant no larger than it
 					if (ci) { vaddr(ci); op(O_LD); op(O_SWAP); mulsz(et); op(O_ADD); }
 					else addr_stk(et);
 				} else if (ci && !mdbg && enh && ix >= 0) {
@@ -1494,6 +1495,7 @@ int postfix_tail(int c) {
 				c = expr();
 				ix = -1;
 				if (lv && lvk == LV_LOCAL) ix = lvi;
+				iu = oub();
 				rval(); plainuse(c);
 				ic = xconst;
 				if (xconst) offset = xcval; if (n < 0) af_index(storage, place);
@@ -1508,7 +1510,7 @@ int postfix_tail(int c) {
 				expect(s_rk);
 				if (!ub && !inr) {
 					if (n >= 0) {
-						if (!ic && !(ix >= 0 && proven_n(ix, n))) {
+						if (!ic && !(ix >= 0 && proven_n(ix, n)) && !(ix < 0 && iu > 0 && iu <= n)) {
 							hg = hoist_guard(ix, n, 0 - 1);
 							fixed_chk(n);
 							if (hg >= 0) { setlit(hg, here); xc_note(0, XC_HOISTED, place); }
@@ -1518,6 +1520,7 @@ int postfix_tail(int c) {
 						pn = ptr_elems(storage, et, bl);
 						if (pn < 0) pn = ptr_elems(entry_fact(ix, bl), et, bl);	// the loop top forgot the fact; the body leaves the pointer alone (hoist_guard and proven_p check)
 						if (pn >= 0 && ix >= 0 && proven_p(ix, pn, bl)) pn = pn;	// the loop test proved it
+						else if (pn >= 0 && ix < 0 && iu > 0 && iu <= pn && ptr_still(bl)) pn = pn;	// i * n + k under i < n and k < n, into n * n words
 						else {
 							hg = 0 - 1; if (pn >= 0) hg = hoist_guard(ix, pn, bl);
 							if (tbytes(et)) ptr_chk(0 - tbytes(et));
@@ -1714,7 +1717,7 @@ int if_comparison(int name) {
 	return name == s_eqeq || name == s_ne || name == s_lt || name == s_gt || name == s_le || name == s_ge;
 }
 int bin(int minp) {
-	int c = unary(), b, p, a, j, lt, lb, rb, src, lf, rf, ls, rs, fresh, top = 0, il = -1, opp; word borrowed, rightborrow, left_mask, right_mask, infer_left, infer_right;
+	int c = unary(), b, p, a, j, lt, lb, rb, src, lf, rf, ls, rs, fresh, top = 0, il = -1, opp, lu, ru, xu; word borrowed, rightborrow, left_mask, right_mask, infer_left, infer_right;
 	if (fortest == 1) { fortest = 2; top = 1; ft_nops = 0; }
 	while (tk == T_OP) {
 		b = binfind(tv);
@@ -1726,6 +1729,7 @@ int bin(int minp) {
 		borrowed = xaf; left_mask = effect_mask(c); lf = xfloat; ls = xstr; fresh = 0;
 		il = -1;
 		if (top && lv && lvk == LV_LOCAL) il = lvi;
+		lu = oub(); ru = 0 - 1;
 		infer_left = if_value; infer_right = 0;
 		opp = tpack();
 		next(); rval(); plainuse(c);
@@ -1757,7 +1761,8 @@ int bin(int minp) {
 			c = bin(p + 1); infer_right = if_value; rightborrow = xaf; right_mask = effect_mask(c);
 			rb = -1;
 			if (c >= C_VAR && tracked(c - C_VAR)) rb = lroot(c - C_VAR); else rb = xbor;
-			if (top) { ft_ir = -1; if (lv && lvk == LV_LOCAL) ft_ir = lvi; }
+			if (top) { ft_ir = -1; ft_ln = xlenloc; if (lv && lvk == LV_LOCAL) ft_ir = lvi; }
+			ru = oub();
 			rval(); plainuse(c);
 			if (top) { ft_ck = -1; if (xconst && xcval >= 0) ft_ck = xcval; }
 			if (cmode && bname[b] == s_star && xconst && xcval >= 2 && !(xcval & (xcval - 1)) && !lf) {
@@ -1795,8 +1800,12 @@ int bin(int minp) {
 		if (top) {
 			ft_nops++;
 			if (ft_nops > 1) ft_iv = -1;
-			else if (bname[b] == s_lt && blen[b] > 0 && il >= 0 && (ft_ir >= 0 || ft_ck >= 0) && !lf && !rf && !ls && !rs) { ft_iv = il; ft_bd = ft_ir; }
+			else if (bname[b] == s_lt && blen[b] > 0 && il >= 0 && (ft_ir >= 0 || ft_ck >= 0 || ft_ln >= 0) && !lf && !rf && !ls && !rs) { ft_iv = il; ft_bd = ft_ir; }
 		}
+		xu = 0 - 1;	// i * n + k and the like keep a bound when both sides have one
+		if (blen[b] > 0 && !lf && !rf && lu > 0 && ru > 0) { if (bname[b] == s_star) xu = (lu - 1) * (ru - 1) + 1; else if (bname[b] == s_plus) xu = lu + ru - 1; }
+		if (xu > 0x40000000) xu = 0 - 1;
+		xub = xu; xubat = here;
 		lv = 0; lvk = LV_NONE; c = C_PLAIN; xzero = 0; xconst = 0; xlenloc = -1; xstamp = 0; xaf = 0; xvk = 0;
 		effect_value = 0; if (isptr(xty) || xty == tword) effect_value = left_mask | right_mask;
 		if (fresh) c = C_FRESH;
diff --git a/src/compiler/stmt.zc b/src/compiler/stmt.zc
index 703f2db..007306c 100644
--- a/src/compiler/stmt.zc
+++ b/src/compiler/stmt.zc
@@ -337,7 +337,7 @@ int kw_for() {
 	// i < n with a variable n: a jump to the loop entry, where hoisted checks get their flags (see hoist_guard)
 	if (fbnd && infn && !dry && tk == T_ID) { peekat(1); if (pk_tk == T_ID) { peek(); if (pk_tk == T_OP && pk_tv == s_lt) { xe = hole(); op(O_JMP); } } }
 	c0 = here;
-	ft_iv = -1; ft_ck = -1; fs_ok = 0; fortest = 1;
+	ft_iv = -1; ft_ck = -1; ft_ln = -1; fs_ok = 0; fortest = 1;
 	if (!is_op(s_semi)) {
 		if (tk == T_NUM && tv) { peek(); if (pk_tk == T_OP && pk_tv == s_semi) inf = 1; }
 		c = borrow_condition();
@@ -367,6 +367,8 @@ int kw_for() {
 	}
 	if (cl && ft_bd >= 0 && getlo(ft_iv) >= 0 && getln(ft_bd) >= 0) {
 		if (!ldirty(r, lname[getln(ft_bd)]) && lclean(getln(ft_bd))) lpfact[lsp - 1] = pfact(ft_iv, ft_bd, getln(ft_bd));
+	} else if (cl && ft_bd < 0 && ft_ln >= 0 && getlo(ft_iv) >= 0) {	// i < len(a) written in the test
+		if (!ldirty(r, lname[ft_ln]) && lclean(ft_ln)) lpfact[lsp - 1] = pfact(ft_iv, 0 - 3, ft_ln);
 	} else if (cl && ft_ck >= 0 && getlo(ft_iv) >= 0) {	// i < constant: proves a fixed array that long
 		lpfact[lsp - 1] = pfact(ft_iv, -1, 0 - ft_ck - 2);
 	} else if (cl && xe >= 0 && ft_bd >= 0 && ltype[ft_iv] == tint && ltype[ft_bd] == tint) { r[52] = 1; r[41] = ft_bd; }	// i < n: checks against n can be hoisted
diff --git a/tests/programs/bounds_prover.zc b/tests/programs/bounds_prover.zc
new file mode 100644
index 0000000..1b3e3ca
--- /dev/null
+++ b/tests/programs/bounds_prover.zc
@@ -0,0 +1,19 @@
+namespace;
+include rt;
+
+// the new loop proofs drop checks that cannot fail and keep the ones that can:
+// the last loop runs one past a block of 6 and has to fault there.
+int main() {
+	int i, k, s = 0;
+	fixed int[?] a = rt.new(fixed int[?], 8);
+	fixed int[?] m = rt.new(fixed int[?], 16);
+	fixed int[?] c = rt.new(fixed int[?], 6);
+	for (i = 0; i < len(a); i++) a[i] = i;
+	for (i = 0; i < len(a); i++) s = s + a[i];
+	rt.put_n(s); rt.put_c(10);
+	for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) m[i * 4 + k] = i * k;
+	s = 0; for (i = 0; i < len(m); i++) s = s + m[i];
+	rt.put_n(s); rt.put_c(10);
+	for (i = 0; i < 7; i++) { rt.put_n(i); rt.put_c(32); c[i] = i; }
+	return 0;
+}
diff --git a/tests/programs/explain_prover.zc b/tests/programs/explain_prover.zc
new file mode 100644
index 0000000..14486b5
--- /dev/null
+++ b/tests/programs/explain_prover.zc
@@ -0,0 +1,40 @@
+namespace;
+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.
+int touch() { return 0; }
+int[16] sq;
+int main() {
+	int i, j, k, s = 0, n = 4;
+	fixed int[?] a = rt.new(fixed int[?], 8);
+	fixed int[?] b = rt.new(fixed int[?], 10);
+	fixed int[?] c = rt.new(fixed int[?], 6);
+	fixed int[?] m = rt.new(fixed int[?], 16);
+	fixed int[?] m15 = rt.new(fixed int[?], 15);
+	int* p = rt.new(16);
+	// 1. i < len(a) in the test
+	for (i = 0; i < len(a); i++) a[i] = i;	// proved
+	for (i = 0; i < len(a); i++) { s = s + a[i]; i = i + 0; }	// kept: the body moves i
+	// 2. len(a) bounds another array of known length
+	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
+	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
+	// 5. i * n + k into exactly n * n
+	for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) m[i * 4 + k] = i + k;	// proved
+	for (i = 0; i < 4; i++) for (k = 0; k < 4; k++) s = s + p[i * 4 + k];	// proved
+	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
+	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;
+}