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

1 files changed, 15 insertions, 6 deletions

diff --git a/src/compiler/expr.zc b/src/compiler/expr.zc
index 8768658..0af01d4 100644
--- a/src/compiler/expr.zc
+++ b/src/compiler/expr.zc
@@ -1365,7 +1365,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);
@@ -1427,6 +1427,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);
@@ -1436,7 +1437,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) {
@@ -1479,6 +1480,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);
@@ -1493,7 +1495,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); }
@@ -1503,6 +1505,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));
@@ -1699,7 +1702,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);
@@ -1711,6 +1714,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);
@@ -1742,7 +1746,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) {
@@ -1780,8 +1785,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;