aboutsummaryrefslogtreecommitdiff
path: root/tests/programs
diff options
context:
space:
mode:
authorGravatar zinc <zinc@downsta.ir> 2026-10-14 16:09:07 +0330
committerGravatar zinc <zinc@downsta.ir> 2026-10-14 16:09:07 +0330
commite228e7609929763d5acddb728ba543832fcffc6a (patch)
tree9b4ecc4d46bf38e8d20234d631a6d41543daa211 /tests/programs
parentmerge: memdebug obj_base via size classes (diff)
parentbounds checking: constant loop bound proof works, plain-op fixed-array check,... (diff)
merge bounds checking
Diffstat (limited to 'tests/programs')
-rw-r--r--tests/programs/bounds_fixed.zc17
-rw-r--r--tests/programs/bounds_heap.zc16
-rw-r--r--tests/programs/bounds_hi.zc3
-rw-r--r--tests/programs/boundsrules.zc24
-rw-r--r--tests/programs/o3_bounds.zc3
-rw-r--r--tests/programs/o3call.zc2
-rw-r--r--tests/programs/zc0unbounded.zc16
7 files changed, 78 insertions, 3 deletions
diff --git a/tests/programs/bounds_fixed.zc b/tests/programs/bounds_fixed.zc
new file mode 100644
index 0000000..0b3f476
--- /dev/null
+++ b/tests/programs/bounds_fixed.zc
@@ -0,0 +1,17 @@
+namespace;
+include rt;
+
+// a fixed array T[n] with a variable index is checked against n. a loop whose
+// test is the constant n proves the index and drops the check; a constant
+// index is checked when it is compiled.
+int main() {
+ int[6] t; int i, s = 0, k = 6;
+ for (i = 0; i < 6; i++) t[i] = i * i;
+ for (i = 0; i < 6; i++) s = s + t[i];
+ rt.put_n(s); rt.put_c(10);
+ i = 2; rt.put_n(t[i] + t[5]); rt.put_c(10);
+ i = 0;
+ while (i <= k) { s = t[i]; i++; }
+ rt.put_s("not reached\n");
+ return 0;
+}
diff --git a/tests/programs/bounds_heap.zc b/tests/programs/bounds_heap.zc
new file mode 100644
index 0000000..d0bd318
--- /dev/null
+++ b/tests/programs/bounds_heap.zc
@@ -0,0 +1,16 @@
+namespace;
+include rt;
+
+// a pointer to the start of a live heap block is checked against the block's
+// payload, which a buddy block rounds up: rt.new(4) holds 11 words. a pointer
+// into the middle of a block, or to memory that is not a heap block, is not
+// checked. a char is a word, so a char* counts words.
+int main() {
+ int* p = rt.new(4); int* q; char* c = rt.new(2); int i = 10;
+ p[i] = 3; rt.put_n(p[i]); rt.put_c(10);
+ q = p + 1; i = 10; rt.put_n(q[i - 1] - 3); rt.put_c(10);
+ i = 2; c[i] = 'x'; rt.put_c(c[i]); rt.put_c(10);
+ i = 11;
+ rt.put_n(p[i]); rt.put_c(10);
+ return 0;
+}
diff --git a/tests/programs/bounds_hi.zc b/tests/programs/bounds_hi.zc
index 49639c5..5475764 100644
--- a/tests/programs/bounds_hi.zc
+++ b/tests/programs/bounds_hi.zc
@@ -1,7 +1,8 @@
namespace;
include rt;
-// the index is not the induction variable. i + 1 walks off the end.
+// the index is not the induction variable. i + 1 walks off the end, but o3
+// implies unbounded: nothing checks it, and the write lands in the block's slack
o3 fn main() {
fixed int[?] f = rt.new(fixed int[?], 4);
int n = len(f), i;
diff --git a/tests/programs/boundsrules.zc b/tests/programs/boundsrules.zc
new file mode 100644
index 0000000..1ae6a56
--- /dev/null
+++ b/tests/programs/boundsrules.zc
@@ -0,0 +1,24 @@
+namespace;
+include rt;
+
+// unbounded turns the checks off: as a function prefix (in any order with
+// unchecked), as a block, for one statement. o3 implies it. the last read is
+// checked and stops the program.
+int[8] pad;
+int[4] a;
+
+unbounded int pre(int i) { return a[i] * 0 + 1; }
+unchecked unbounded int both(int i) { return a[i] * 0 + 1; }
+o3 int fast(int i) { return a[i] * 0 + 1; }
+int blk(int i) { int r = 0; unbounded { r = a[i] * 0 + 1; } return r; }
+int one(int i) { int r = 0; unbounded r = a[i] * 0 + 1; return r; }
+int checked(int i) { return a[i]; }
+
+int main() {
+ int i = 5;
+ a[3] = 7;
+ rt.put_n(pre(i) + both(i) + fast(i) + blk(i) + one(i)); rt.put_c(10);
+ rt.put_n(checked(3)); rt.put_c(10);
+ rt.put_n(checked(i)); rt.put_c(10);
+ return 0;
+}
diff --git a/tests/programs/o3_bounds.zc b/tests/programs/o3_bounds.zc
index eaf92eb..cd65548 100644
--- a/tests/programs/o3_bounds.zc
+++ b/tests/programs/o3_bounds.zc
@@ -1,5 +1,6 @@
namespace;
include rt;
-// an index outside a T[?] inside o3 code: caught by the inline check
+// an index outside a T[?] inside o3 code: o3 implies unbounded, so nothing checks it
+// (the write lands in the slack of the buddy block) and the program ends normally
fn main() { int[?] a = rt.new(int[?], 5); o3 { int i = 7; a[i] = 1; } rt.free(d*a); return 0; }
diff --git a/tests/programs/o3call.zc b/tests/programs/o3call.zc
index d2292ad..3ad977b 100644
--- a/tests/programs/o3call.zc
+++ b/tests/programs/o3call.zc
@@ -19,7 +19,7 @@ unchecked o3 int nest(int n) {
if (n == 0) return 0;
return n + nest(n - 1);
}
-unchecked fn main() {
+unchecked unbounded fn main() { // reads p[-1], the type word, on purpose
node* n = leaf(4);
int* p = n;
rt.put_n(p[-1] < 0); rt.put_c(' ');
diff --git a/tests/programs/zc0unbounded.zc b/tests/programs/zc0unbounded.zc
new file mode 100644
index 0000000..67c3ae0
--- /dev/null
+++ b/tests/programs/zc0unbounded.zc
@@ -0,0 +1,16 @@
+namespace;
+include rt;
+
+// unbounded in all three places zc0 accepts it (and ignores): the unit, a
+// function prefix and a statement. both compilers print the same.
+unbounded;
+int[4] a;
+unbounded int get(int i) { return a[i]; }
+int main() {
+ int i = 2, r = 0;
+ a[2] = 40;
+ unbounded r = get(i) + 2;
+ unbounded { r = r + a[i - 2]; }
+ rt.put_n(r); rt.put_c(10);
+ return 0;
+}