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

7 files changed, 87 insertions, 0 deletions

diff --git a/tests/parity.known b/tests/parity.known
index 37874f9..39898b2 100644
--- a/tests/parity.known
+++ b/tests/parity.known
@@ -18,3 +18,6 @@ tests/programs/bench_strings.zc # reads the repeat count from stdin; with none,
 tests/programs/bounds_fixed.zc # bounds checks: only the self-hosted compiler checks a fixed array index
 tests/programs/bounds_heap.zc # bounds checks: only the self-hosted compiler checks a pointer into a heap block
 tests/programs/bounds_proof.zc # bounds checks: zc0 emits none, so the variable-bound loop is as short as the unbounded one
+tests/programs/bounds_hoist.zc # bounds checks: zc0 emits none, so the loop past the end runs on
+tests/programs/bounds_body.zc # bounds checks: zc0 emits none, so the moved index reads outside the array
+tests/programs/bounds_ptr.zc # bounds checks: zc0 emits none, so the loop past the block does not fault
diff --git a/tests/programs/bounds_body.zc b/tests/programs/bounds_body.zc
new file mode 100644
index 0000000..ea838ac
--- /dev/null
+++ b/tests/programs/bounds_body.zc
@@ -0,0 +1,11 @@
+namespace;
+include rt;
+
+// a loop proof only holds while the body leaves the index alone: here the body
+// moves i back below 0 once, so t[i] keeps its check and the access faults
+int main() {
+	int[4] t; int s = 0, once = 1;
+	for (int i = 0; i < 4; i++) { s = s + t[i]; if (once) { once = 0; i = -3000; } }
+	rt.put_n(s); rt.put_c(10);
+	return 0;
+}
diff --git a/tests/programs/bounds_hoist.zc b/tests/programs/bounds_hoist.zc
new file mode 100644
index 0000000..d7f5e7f
--- /dev/null
+++ b/tests/programs/bounds_hoist.zc
@@ -0,0 +1,20 @@
+namespace;
+include rt;
+
+// a loop for (i = 0; i < n; i++) with an int bound n the body leaves alone:
+// the check of t[i] against t's length is worked out once at the loop entry
+// (0 <= i and n <= length) and runs on each access only when that failed. so
+// a loop that stays inside skips it, and one that runs past the end still
+// faults at the same access, after the same side effects (the puts before it).
+int[8] t;
+int sweep(int n) { int i, s = 0; for (i = 0; i < n; i++) { t[i] = i; s = s + t[i]; } return s; }
+int from(int lo, int n) { int i, s = 0; for (i = lo; i < n; i++) s = s + t[i]; return s; }
+int main() {
+	rt.put_n(sweep(8)); rt.put_c(10);
+	rt.put_n(sweep(3)); rt.put_c(10);
+	rt.put_n(from(2, 8)); rt.put_c(10);
+	int i, n = 10;
+	for (i = 0; i < n; i++) { rt.put_n(i); rt.put_c(32); t[i] = i; }
+	rt.put_s("not reached\n");
+	return 0;
+}
diff --git a/tests/programs/bounds_ptr.zc b/tests/programs/bounds_ptr.zc
new file mode 100644
index 0000000..3190b03
--- /dev/null
+++ b/tests/programs/bounds_ptr.zc
@@ -0,0 +1,18 @@
+namespace;
+include rt;
+
+// a pointer set from rt.new(n) with a constant n: a loop test i < n drops the
+// check, a variable bound hoists it to the loop entry, and a body that calls
+// something keeps it (the call might free the block). all three agree.
+int main() {
+	int* p = rt.new(16); int i, s = 0, n = 16;
+	for (i = 0; i < 16; i++) p[i] = i;
+	for (i = 0; i < n; i++) s = s + p[i];
+	rt.put_n(s); rt.put_c(10);
+	for (i = 0; i < n; i++) { s = s + p[i]; rt.put_s(""); }
+	rt.put_n(s); rt.put_c(10);
+	n = 1000;
+	for (i = 0; i < n; i++) s = s + p[i];
+	rt.put_s("not reached\n");
+	return 0;
+}
diff --git a/tests/programs/explain_checks.expected b/tests/programs/explain_checks.expected
new file mode 100644
index 0000000..c57652a
--- /dev/null
+++ b/tests/programs/explain_checks.expected
@@ -0,0 +1,8 @@
+{"version":1}
+{"file":"<eval>","line":6,"col":32,"end_line":6,"end_col":35,"fn":"g","kind":"pointer","loop_depth":0,"reason":"size-unknown","fix":"the compiler does not know the size of the block; allocate it here with a constant size, or index a fixed array"}
+{"file":"<eval>","line":12,"col":35,"end_line":12,"end_col":38,"fn":"main","kind":"index","loop_depth":1,"reason":"hoisted-to-loop-entry","fix":"checked once when the loop starts, and on every access only if that check fails; nothing to do"}
+{"file":"<eval>","line":13,"col":37,"end_line":13,"end_col":40,"fn":"main","kind":"index","loop_depth":1,"reason":"bound-not-invariant","fix":"the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"}
+{"file":"<eval>","line":14,"col":11,"end_line":14,"end_col":14,"fn":"main","kind":"index","loop_depth":0,"reason":"index-not-loop-variable","fix":"index with the variable of a loop for (i = 0; i < bound; i++), or mark the code unbounded if the index is known to be in range"}
+{"file":"<eval>","line":15,"col":35,"end_line":15,"end_col":38,"fn":"main","kind":"pointer","loop_depth":1,"reason":"hoisted-to-loop-entry","fix":"checked once when the loop starts, and on every access only if that check fails; nothing to do"}
+{"file":"<eval>","line":16,"col":37,"end_line":16,"end_col":40,"fn":"main","kind":"pointer","loop_depth":1,"reason":"pointer-may-be-freed","fix":"the loop body calls something that might free or resize the block; move the call out of the loop"}
+{"file":"<eval>","line":17,"col":35,"end_line":17,"end_col":38,"fn":"main","kind":"index","loop_depth":1,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"}
diff --git a/tests/programs/explain_checks.zc b/tests/programs/explain_checks.zc
new file mode 100644
index 0000000..d528cd8
--- /dev/null
+++ b/tests/programs/explain_checks.zc
@@ -0,0 +1,22 @@
+namespace;
+include rt;
+
+// zy --explain-checks: one line per check the compiler keeps, with its reason
+int[8] t;
+int g(int* p, int k) { return p[k]; }
+int main() {
+	int i, s = 0, n = 8, k = 3;
+	int* q = rt.new(8);
+	int[?] a = rt.new(int[?], 8);
+	for (i = 0; i < 8; i++) s = s + t[i];
+	for (i = 0; i < n; i++) s = s + t[i];
+	for (i = 0; i < n; i++) { s = s + t[i]; n = n - 0; }
+	s = s + t[k];
+	for (i = 0; i < n; i++) s = s + q[i];
+	for (i = 0; i < n; i++) { s = s + q[i]; rt.put_s(""); }
+	for (i = 0; i < n; i++) s = s + a[i];
+	s = s + g(q, 2);
+	unbounded { s = s + t[k]; }
+	rt.put_n(s); rt.put_c(10);
+	return 0;
+}
diff --git a/tests/test.sh b/tests/test.sh
index 39e5949..1be4557 100755
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -230,6 +230,11 @@ ABC" "$l o3 lifts byte loads and stores"
 	chk "$($vm < tests/programs/bounds_heap.zc 2>&1 | head -4)" $'3\n0\nx\nzy: index 11 out of range (length 11)' "$l a pointer to a heap block is checked against its payload"
 	chk "$($vm < tests/programs/enh_ops.zc | md5sum)" "$(md5sum < tests/programs/enh_ops.expected)" "$l enhancement micro-ops on edge values, with variables and with literals"
 	chk "$($vm < tests/programs/bounds_proof.zc)" $'0\n1\n1' "$l a loop test against a constant drops the fixed-array check; a variable bound keeps it"
+	chk "$($vm < tests/programs/bounds_hoist.zc 2>&1 | head -5)" $'28\n3\n27\n0 1 2 3 4 5 6 7 8 zy: index 8 out of range (length 8)\n  at <stdin>:17 in main' "$l a check against an invariant bound is hoisted to the loop entry and still faults in place"
+	chk "$($vm < tests/programs/bounds_body.zc 2>&1 | head -1)" "zy: index -2999 out of range (length 4)" "$l a body that moves the loop index keeps the check"
+	chk "$($vm < tests/programs/bounds_ptr.zc 2>&1 | head -3 | cut -c1-9)" $'120\n240\nzy: index' "$l a pointer from rt.new(n): proved, hoisted, or kept when the body calls"
+	chk "$($vm --explain-checks < tests/programs/explain_checks.zc | md5sum)" "$(md5sum < tests/programs/explain_checks.expected)" "$l --explain-checks lists the kept checks (format v1)"
+	chk "$($vm --explain-checks a/b.zc < tests/programs/bounds.zc | head -1)" '{"version":1}' "$l --explain-checks starts with the version line"
 	chk "$($vm < tests/programs/zc0unbounded.zc)" "42" "$l unbounded in the unit, a prefix and a statement"
 	local r; r=$(bash tests/runerr.sh "$vm" tests/errors | tail -1)
 	chk "$r" "rejected: $(ls tests/errors/*.zc | wc -l | tr -d ' ') passed, 0 failed" "$l analyzer rejects every bad program"