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

4 files changed, 112 insertions, 42 deletions

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