diff options
| -rw-r--r-- | TODO.md | 1 | ||||
| -rw-r--r-- | src/compiler/analyzer.zc | 46 | ||||
| -rw-r--r-- | tests/programs/bounds_prover.expected | 4 | ||||
| -rw-r--r-- | tests/programs/explain_prover.expected | 9 | ||||
| -rwxr-xr-x | tests/test.sh | 3 |
5 files changed, 44 insertions, 19 deletions
@@ -153,6 +153,7 @@ and pushed there. - x86-64 direct o3-to-o3 calls merged (`rcall_x64` / `rfinish_x64`, e765c3d). `make check` 214/0; icon regression 14/0; jit_x64 vs interp on o3* 17/17; o3_caller_replace and o3direct ok. post-rcall fib on x86-64 jit (ms/iter min): plain 0.54, o3 0.35 (o3 was 0.92 before direct calls). - trees/sieve baseline on x86-64 jit after rcall, before allocator change (ms/iter min): trees plain new/free 2.88, o3 new/free 4.13, o3 arena 0.09; sieve plain 6.96, o3 checked 0.64, o3 raw 0.61. (older llvm note was plain 9.2 / o3 12.0.) - allocator: o3 now uses `new_k` (size-class free lists) like plain code; `new_k`/`recycle_leaf` skip the o3 arg-fatten path. after: trees plain 2.78, o3 new/free 2.71, o3 arena 0.15. still open: emit the freelist pop/push as native code inside a compiled region (today every `new_k` still leaves via a normal call). +- prover gaps (work/prover): rebase onto main, fix lafact_keep after call-loops and proven_p across enclosing loops; bounds_prover / explain_prover land with test.sh checks. still open from the overnight queue: find_replace hardening and remaining TODO items. ### how the work is organized - start with `ONBOARD.md` (reading order and exact commands), then diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc index 8b52f83..bf7dd9f 100644 --- a/src/compiler/analyzer.zc +++ b/src/compiler/analyzer.zc @@ -703,12 +703,15 @@ word lafact_save() { while (i < nloc) { b[2 + i - lbase] = lafact[i]; i++; } return b; } -// after a loop that frees nothing: the locals its body left alone get back the -// allocation facts the loop forgot +// after a loop: the locals its body left alone get back the allocation facts +// the loop forgot. a body that might free (r[55]) still restores facts for +// undirtied locals: a call that did not take the local cannot have freed it, +// and proofs inside a later loop re-check r[55] for that loop. without this, +// one touch() earlier in the function would permanently drop every length fact. int lafact_keep(word r, word b) { int i; - if (!b || dry || r[0] || r[55]) return 0; + if (!b || dry || r[0]) return 0; i = b[0]; 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; @@ -724,7 +727,10 @@ word entry_fact(int ix, int bl) { while (k > loopbase) { k--; r = linfo(k); - if (!r || ldirty(r, lname[bl]) || !lclean(bl) || r[55]) return 0; + // r[55] is left to proven_p / ptr_still: a call in this loop must keep + // the check, but the size fact at entry is still what --explain-checks + // needs for the "might free" reason rather than "size unknown". + if (!r || ldirty(r, lname[bl]) || !lclean(bl)) return 0; b = r[56]; if (b && bl >= b[0] && bl < b[1]) { f = b[2 + bl - b[0]]; if (f) return f; } } @@ -751,6 +757,19 @@ int pbound(int w) { if (p_ar(w) >= 0) return dyn_len(p_ar(w)); return 0 - 1; } +// 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; +} + // 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 @@ -768,15 +787,16 @@ int proven_n(int ix, int n) { // 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; + 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 0; - r = linfo(k); - return r && !ldirty(r, lname[arr]) && lclean(arr) && !r[55]; + // every enclosing loop, not only this one: touch() in an outer + // body must keep the check even when the index loop itself is clean + return ptr_still(arr); } } return 0; @@ -795,18 +815,6 @@ int local_ub(int i) { } 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; diff --git a/tests/programs/bounds_prover.expected b/tests/programs/bounds_prover.expected new file mode 100644 index 0000000..f5e92fa --- /dev/null +++ b/tests/programs/bounds_prover.expected @@ -0,0 +1,4 @@ +28 +36 +0 1 2 3 4 5 6 zy: index 6 out of range (length 6) + at <stdin>:17 in main diff --git a/tests/programs/explain_prover.expected b/tests/programs/explain_prover.expected new file mode 100644 index 0000000..c43c72d --- /dev/null +++ b/tests/programs/explain_prover.expected @@ -0,0 +1,9 @@ +{"version":1} +{"file":"<eval>","line":18,"col":42,"end_line":18,"end_col":45,"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":22,"col":51,"end_line":22,"end_col":54,"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"} +{"file":"<eval>","line":26,"col":62,"end_line":26,"end_col":65,"fn":"main","kind":"pointer","loop_depth":2,"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":27,"col":71,"end_line":27,"end_col":74,"fn":"main","kind":"pointer","loop_depth":2,"reason":"index-not-len-derived","fix":"bound the loop with len() of the array, or with a constant no larger than its length"} +{"file":"<eval>","line":30,"col":46,"end_line":30,"end_col":49,"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"} +{"file":"<eval>","line":34,"col":81,"end_line":34,"end_col":92,"fn":"main","kind":"index","loop_depth":2,"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":35,"col":70,"end_line":35,"end_col":81,"fn":"main","kind":"index","loop_depth":2,"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":36,"col":59,"end_line":36,"end_col":70,"fn":"main","kind":"index","loop_depth":2,"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"} diff --git a/tests/test.sh b/tests/test.sh index 70e12b9..6992c0d 100755 --- a/tests/test.sh +++ b/tests/test.sh @@ -235,6 +235,9 @@ ABC" "$l o3 lifts byte loads and stores" 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 < tests/programs/bounds_prover.zc 2>&1 | head -5)" $'28\n36\n0 1 2 3 4 5 6 zy: index 6 out of range (length 6)\n at <stdin>:17 in main' "$l loop prover: len, cross-array and affine proofs; a too-long constant bound still faults" + chk "$($vm --explain-checks < tests/programs/explain_prover.zc | md5sum)" "$(md5sum < tests/programs/explain_prover.expected)" "$l --explain-checks for the prover cases (proved lines absent, kept lines present)" + chk "$($vm < tests/programs/explain_prover.zc)" "1204" "$l explain_prover runs and prints its checksum" 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) |