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

1 files changed, 92 insertions, 34 deletions

diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc
index d1f6f3d..5bdb0e3 100644
--- a/src/compiler/analyzer.zc
+++ b/src/compiler/analyzer.zc
@@ -500,18 +500,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
@@ -705,21 +693,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() {
@@ -739,22 +712,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