5 files changed, 79 insertions, 0 deletions
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;
+}