test: a constant loop bound drops the fixed-array bounds check (bounds_proof)

2 files changed, 22 insertions, 0 deletions

diff --git a/tests/programs/bounds_proof.zc b/tests/programs/bounds_proof.zc
new file mode 100644
index 0000000..a678fb3
--- /dev/null
+++ b/tests/programs/bounds_proof.zc
@@ -0,0 +1,21 @@
+namespace;
+include rt;
+
+// a loop test i < K with a constant K proves the index of a fixed array of at
+// least K elements, so the bounds check is dropped: the checked loop compiles
+// to exactly as many words as the unbounded one. a variable bound proves
+// nothing and keeps the check. sizes come from the functions' line blocks.
+int[8] t;
+int konst() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
+unbounded int bare() { int i, s = 0; for (i = 0; i < 8; i++) s = s + t[i]; return s; }
+int vary(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }
+unbounded int vbare(int n) { int i, s = 0; for (i = 0; i < n; i++) s = s + t[i]; return s; }
+
+int size(word f) { word b = rt.line_block_of(f); return b[2] - b[1]; }
+
+int main() {
+	rt.put_n(konst() + bare() + vary(8) + vbare(8)); rt.put_c(10);
+	rt.put_n(size(konst) == size(bare)); rt.put_c(10);
+	rt.put_n(size(vary) > size(vbare)); rt.put_c(10);
+	return 0;
+}
diff --git a/tests/test.sh b/tests/test.sh
index 7a80c3c..1625680 100755
--- a/tests/test.sh
+++ b/tests/test.sh
@@ -227,6 +227,7 @@ ABC" "$l o3 lifts byte loads and stores"
 	chk "$($vm < tests/programs/boundsrules.zc 2>&1 | head -3)" $'5\n7\nzy: index 5 out of range (length 4)' "$l unbounded as prefix, block and statement, o3 implies it; checked code reports"
 	chk "$($vm < tests/programs/bounds_fixed.zc 2>&1 | head -3)" $'55\n29\nzy: index 6 out of range (length 6)' "$l a fixed array with a variable index is checked against its length"
 	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/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/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"