bounds: body scan, loop-entry hoisting, pointer proofs from requested size, --explain-checks v1 (non-o3 code)

1 files changed, 21 insertions, 5 deletions

diff --git a/src/compiler/stmt.zc b/src/compiler/stmt.zc
index a67b931..d23cb52 100644
--- a/src/compiler/stmt.zc
+++ b/src/compiler/stmt.zc
@@ -246,6 +246,7 @@ int loop_push(int cont, int s0) {
 	f[6] = extop;
 	f[7] = 0;
 	lpfact[lsp] = -1;
+	if (lsp < LPI_N && lpinfo) lpinfo[lsp * LPI_W + 54] = 0;
 	lsp++;
 	return 0;
 }
@@ -312,7 +313,7 @@ int kw_while() {
 // if it holds and the bound is len(a) of a fixed array, the body is told that
 // a[i] is in range (lpfact), and its bounds check disappears.
 int kw_for() {
-	int save = nloc, s0, sc = -1, c0, a, b, st, c, inf = 0; word borrow_mark = borrow_slots;
+	int save = nloc, s0, sc = -1, c0, a, b, st, c, inf = 0, xe = -1, cl = 0; word borrow_mark = borrow_slots; word r = 0; word fs = 0;
 	stmtonly();
 	next();
 	expect(s_lp);
@@ -321,7 +322,10 @@ int kw_for() {
 	else if (tstart()) localdecl(1);
 	else { if (!is_op(s_semi)) { c = expr(); rval(); op(O_DROP); discard(c); } expect(s_semi); }
  borrow_cleanup_since(borrow_mark);
+	if (fbnd) fs = lafact_save();
 	s0 = snap_push();
+	// 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;
 	if (!is_op(s_semi)) {
@@ -342,15 +346,27 @@ int kw_for() {
 	jmp(c0);
 	setlit(b, here);
 	loop_push(st, s0);
-	if (ft_iv >= 0 && ft_bd >= 0 && fs_ok && getlo(ft_iv) >= 0 && getln(ft_bd) >= 0) {
-		lpfact[lsp - 1] = pfact(ft_iv, ft_bd, getln(ft_bd));
-	} else if (ft_iv >= 0 && ft_ck >= 0 && fs_ok && getlo(ft_iv) >= 0) {	// i < constant: proves a fixed array that long
-		lpfact[lsp - 1] = pfact(ft_iv, -1, 0 - ft_ck - 2);
+	// a proof needs a body that leaves the index, the bound and the array alone
+	r = linfo_new(lsp - 1);
+	if (r) { body_scan(r); r[40] = 0 - 1; r[41] = 0 - 1; r[42] = xe; r[56] = fs; }
+	if (r && ft_iv >= 0 && fs_ok) {
+		r[40] = ft_iv;
+		cl = !ldirty(r, lname[ft_iv]) && lclean(ft_iv);
+		if (cl && ft_bd >= 0) cl = !ldirty(r, lname[ft_bd]) && lclean(ft_bd);
+		r[53] = cl;
 	}
+	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_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
 	substmt();
 	backedge(s0);
 	jmp(st);
+	if (xe >= 0) { if (r && r[43]) hoist_stub(r, c0); else setlit(xe, c0); }
 	loop_end(a, sc);
+	if (r) { lafact_keep(r, fs); r[56] = 0; }
+	if (fs) rt.free(fs);
 	snap_pop(s0);
 	block_close(save);
 	fdepth--;