From 459b7661aaa0d65d01be064bd4b9976c4f045a5c Mon Sep 17 00:00:00 2001 From: zinc Date: Wed, 14 Oct 2026 18:22:04 +0330 Subject: bounds: body scan, loop-entry hoisting, pointer proofs from requested size, --explain-checks v1 (non-o3 code) --- docs/SPEC.md | 4 + src/compiler/analyzer.zc | 328 +++++++++++++++++++++++++++++++++ src/compiler/base.zc | 9 + src/compiler/builtins.zc | 3 + src/compiler/decl.zc | 3 +- src/compiler/expr.zc | 33 +++- src/compiler/setup.zc | 2 + src/compiler/stmt.zc | 26 ++- src/core/core.c | 6 +- src/micro/port_linux.c | 2 +- tests/parity.known | 3 + tests/programs/bounds_body.zc | 11 ++ tests/programs/bounds_hoist.zc | 20 ++ tests/programs/bounds_ptr.zc | 18 ++ tests/programs/explain_checks.expected | 8 + tests/programs/explain_checks.zc | 22 +++ tests/test.sh | 5 + 17 files changed, 488 insertions(+), 15 deletions(-) create mode 100644 tests/programs/bounds_body.zc create mode 100644 tests/programs/bounds_hoist.zc create mode 100644 tests/programs/bounds_ptr.zc create mode 100644 tests/programs/explain_checks.expected create mode 100644 tests/programs/explain_checks.zc diff --git a/docs/SPEC.md b/docs/SPEC.md index f422166..4936856 100644 --- a/docs/SPEC.md +++ b/docs/SPEC.md @@ -662,6 +662,10 @@ int y = 7; asm { y @ 1 + y ! } // y is 8 4.15.2 the runtime, the core, the compiler, the language server, `run.zc` and `build.zc` are unbounded; std, icon and actor are checked except where a function reads headers on purpose. +4.15.3 the compiler drops a check it can prove, and never changes when a check that can fail faults. a check is dropped for a constant index inside the array or the block; in a loop `for (...; i < b; i++)` whose body leaves `i`, `b` and the array alone (it assigns, increments or takes the address of none of them, and makes no closure), for `a[i]` when `b` is `len(a)`, or a constant no larger than a fixed array's length, or than the requested size of the block a pointer was set from (never a rounded block size). for a pointer the body must also call nothing, since a call might free or resize the block. when `b` is an `int` variable, the check of `a[i]` against `n` elements is hoisted: the loop entry works out once whether `0 <= i` and `b <= n`, and the check runs on each access only when that failed, so a fault still comes at the same access, after the same side effects. + +4.15.4 `zy --explain-checks [file] < source` compiles the unit, does not run it, and prints the checks the compiler kept, from the same analysis that drops the others, as json lines (format version 1). the first line is `{"version":1}`. each further line is one object for one kept check, in source order: `file` (the name given, default ``), `line`, `col` (from 1, of the `[`), `end_line`, `end_col` (just past the `]`), `fn` (the function; `` or `` outside a named one), `kind` (`index` for an array, `pointer` for a pointer), `loop_depth` (enclosing loops), `reason`, `fix` (prose), and optionally `edit` (`{"range":{"line":..,"col":..,"end_line":..,"end_col":..},"text":".."}`), present only for a purely mechanical fix. the reasons: `index-not-loop-variable` (the index is not the variable of an enclosing `for (i = ..; i < b; i++)`), `bound-not-invariant` (the body changes the index, the bound or the array, takes an address or makes a closure), `index-not-len-derived` (the bound is not `len()` of the array or a small enough constant), `size-unknown` (a pointer whose block size the compiler does not know), `pointer-may-be-freed` (the body calls something that might free or resize the block), `packed-elements` (sized-integer elements, always checked by the runtime) and `hoisted-to-loop-entry` (kept, but it runs only when the check at the loop entry failed). checks in included files, in unbounded code and in o3 code (which implies unbounded) are not listed. version 1 is stable: new kinds, reasons and fields may appear, and a consumer ignores a kind, a reason or a field it does not know. + ## 5. declarations at the top level ### 5.1 items diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc index 89713ff..1822fe5 100644 --- a/src/compiler/analyzer.zc +++ b/src/compiler/analyzer.zc @@ -512,6 +512,334 @@ int proven_n(int ix, int n) { } return 0; } +// ---- loop bodies and hoisted checks ---- + +// a loop proof only holds while the body leaves the index, the bound and the +// array alone. the compiler reads the body once, in order, so before it +// compiles one it reads its tokens ahead (as capture_scan does) and notes +// every name the body assigns, increments, decrements or takes the address +// of. the record is r = lpinfo + depth * LPI_W: r[0] is 1 when the scan could +// not see the whole body (the source is stdin, it ran out) or found a closure +// (which can change any captured local), and then every name counts; r[1] +// names follow from r[2], at most 32. the body is read as one statement, the +// way the parser will read it (bs_stmt). +// r[40] the loop's index variable (or -1), r[41] its bound, r[42] the entry +// jump to patch, r[43] how many hoisted checks, r[44..47] their element +// counts, r[48..51] their flag slots, r[52] 1 when checks against the bound +// can be hoisted, r[53] 1 when index and bound are left alone, r[54] 1 when +// the record is in use, r[55] 1 when the body might free or resize a block +// (any pointer, which may alias the one a proof is about): it calls a function, +// uses push, pop, resize, defer, asm, quote or new, or stores to a local that +// can own a block. then the size a pointer proof read can change. r[56] the +// allocation facts of the locals at the loop entry (lafact_save), which the +// loop top forgets. +int body_name(word r, int nm) { + if (r[1] >= 32) { r[0] = 1; return 0; } + r[2 + r[1]] = nm; r[1]++; + return 0; +} +// can a store to the name nm free a block? a store to a pointer, a word or +// an array local can (an owner frees what it held), and so can one to a name +// the loop declares, unless a number type comes right before it (pk2, pv2: the +// token before the name) +int body_mayfree(int nm, int pk2, int pv2) { + int j = findloc(nm); word t; + if (j < 0) return !(pk2 == T_ID && (pv2 == sx_int || pv2 == sx_char || pv2 == sx_bool || pv2 == sx_float)); + t = ltype[j]; + if (!t || t == tword || isptr(t) || t[0] == TY_DYN || tracked(j)) return 1; + return 0; +} +// the scan's view of the token before the current one and the one before that +int bs_pk, bs_pv, bs_pk2, bs_pv2; +// note what the current token says about the body, then read the next one +int bs_adv(word r) { + int j; + if (is_id(s_fn)) { peek(); if (pk_tk == T_OP && (pk_tv == s_lp || pk_tv == s_colon)) r[0] = 1; } + if (tk == T_OP && bs_pk == T_ID && (tv == s_eq || tv == s_inc || tv == s_dec || asgfind(tv) >= 0)) { body_name(r, bs_pv); if (body_mayfree(bs_pv, bs_pk2, bs_pv2)) r[55] = 1; } + if (tk == T_ID && bs_pk == T_OP && (bs_pv == s_inc || bs_pv == s_dec || bs_pv == s_amp)) body_name(r, tv); + if (tk == T_OP && tv == s_lp && bs_pk == T_ID) { j = lookup(bs_pv); if (j < 0 || skind[j] != K_KW) r[55] = 1; } + if (tk == T_ID && (tv == sx_push || tv == sx_pop || tv == sx_resize || tv == sx_defer || tv == sx_asm || tv == sx_quote || tv == sx_new)) r[55] = 1; + bs_pk2 = bs_pk; bs_pv2 = bs_pv; bs_pk = tk; bs_pv = tv; + next(); + return 0; +} +// a bracketed group from the current ( [ or {, through its closer +int bs_group(word r) { + int depth = 0; + while (1) { + if (tk == T_EOF) { r[0] = 1; return 0; } + if (tk == T_OP && (tv == s_lb || tv == s_lp || tv == s_lk)) depth++; + else if (tk == T_OP && (tv == s_rb || tv == s_rp || tv == s_rk)) depth--; + bs_adv(r); + if (depth <= 0) return 0; + } + return 0; +} +// one statement, read the way the parser will: a block, if/else, a loop or +// switch with its body, do/while, or anything else up to its ; at depth 0 +int bs_stmt(word r) { + int depth = 0; + if (tk == T_EOF) { r[0] = 1; return 0; } + if (is_op(s_lb)) return bs_group(r); + if (is_id(sx_if)) { + bs_adv(r); if (is_op(s_lp)) bs_group(r); + bs_stmt(r); + if (is_id(sx_else)) { bs_adv(r); bs_stmt(r); } + return 0; + } + if (is_id(sx_while) || is_id(sx_for) || is_id(sx_switch)) { + bs_adv(r); if (is_op(s_lp)) bs_group(r); + return bs_stmt(r); + } + if (is_id(sx_do)) { + bs_adv(r); bs_stmt(r); + if (is_id(sx_while)) { bs_adv(r); if (is_op(s_lp)) bs_group(r); } + if (is_op(s_semi)) bs_adv(r); + return 0; + } + while (1) { + if (tk == T_EOF) { r[0] = 1; return 0; } + if (tk == T_OP && (tv == s_lb || tv == s_lp || tv == s_lk)) depth++; + else if (tk == T_OP && (tv == s_rb || tv == s_rp || tv == s_rk)) { depth--; if (depth < 0) return 0; } + if (depth == 0 && is_op(s_semi)) { bs_adv(r); return 0; } + bs_adv(r); + } + return 0; +} +int body_scan(word r) { + word old, f; int docs = docs_on, record = grec, sp = panic; + r[0] = 0; r[1] = 0; r[55] = 0; + if (isp < 0 || R_SRC[isp * 32] == 0) { r[0] = 1; return 0; } + src_push(1, capture_dummy, 0, 0); old = R_SRC + (isp - 1) * 32; f = R_SRC + isp * 32; + f[0] = old[0]; f[1] = old[1]; f[2] = old[2]; f[3] = old[3]; f[4] = 0; pq_n = f[14]; + docs_on = 0; grec = 0; dry++; + bs_pk = 0; bs_pv = 0; bs_pk2 = 0; bs_pv2 = 0; + bs_stmt(r); + dry--; src_pop(); docs_on = docs; grec = record; panic = sp; + return 0; +} +// may the loop body behind r change the local named nm? +int ldirty(word r, int nm) { + int k = 0; + if (!r || r[0]) return 1; + while (k < r[1]) { if (r[2 + k] == nm) return 1; k++; } + return 0; +} +// a local nothing outside the function's own code can change: no address +// taken, not captured by a closure +int lclean(int i) { + if (laaddr[i]) return 0; + if (local_cell && local_cell[i]) return 0; + if (local_captured && local_captured[i]) return 0; + return 1; +} +// a fresh record for the loop at depth k, or 0 past the first LPI_N depths +word linfo_new(int k) { + word r; + if (k >= LPI_N) return 0; + if (!lpinfo) lpinfo = chk_resize(0, 0, LPI_N * LPI_W); + r = lpinfo + k * LPI_W; + rt.fill_w(r, 0, LPI_W); + r[54] = 1; + return r; +} +// the record of the live loop at depth k, or 0 +word linfo(int k) { + word r; + if (k >= LPI_N || !lpinfo) return 0; + r = lpinfo + k * LPI_W; + if (!r[54]) return 0; + return r; +} +// for a check of index ix against n elements of the array local arr (-1 for +// a fixed array) inside a loop "for (...; ix < bound; ix++)" whose body leaves +// ix and bound alone: the loop entry works out once whether ix < bound <= n +// can fail (0 <= ix at the entry, bound <= n), and the check runs only when it +// can. a plain early fault would move the fault before the side effects of the +// iterations that come first; the flag keeps the check where it was. emits +// the load of the flag and the jump over the check; returns the hole to patch +// past it, or -1 when the check cannot be hoisted. +int hoist_guard(int ix, int n, int arr) { + int k = lsp, j; word r; + if (ix < 0 || n <= 0) return 0 - 1; + while (k > loopbase) { + k--; + r = linfo(k); + if (!r || r[40] != ix) continue; + if (!r[52]) return 0 - 1; + if (arr >= 0 && (ldirty(r, lname[arr]) || !lclean(arr) || r[55])) return 0 - 1; + j = 0; + while (j < r[43] && r[44 + j] != n) j++; + if (j == r[43]) { + if (j >= 4) return 0 - 1; + r[44 + j] = n; r[48 + j] = fslots; fslots++; r[43]++; + } + laddr(r[48 + j]); op(O_LD); + j = hole(); op(O_JZ); + return j; + } + return 0 - 1; +} +// the loop entry of a loop with hoisted checks: each flag is 1 when ix < 0 or +// bound > n, then on to the test at c0 +int hoist_stub(word r, int c0) { + int k = 0; + setlit(r[42], here); + while (k < r[43]) { + vaddr(r[40]); op(O_LD); lit(r[44 + k]); vaddr(r[41]); op(O_LD); op(O_SUB); op(17); + lit(0); op(O_LT); + laddr(r[48 + k]); op(O_ST); + k++; + } + jmp(c0); + return 0; +} +// i < n for a pointer local arr to a block of n words: a loop test against a +// constant of at most n, in a loop whose body leaves arr alone +int proven_p(int ix, int n, int arr) { + int k = lsp, w; word r; + while (k > loopbase) { + k--; + w = lpfact[k]; + if (w >= 0 && p_iv(w) == ix && p_bd(w) == -1 && 0 - p_ar(w) - 2 <= n) { + r = linfo(k); + return r && !ldirty(r, lname[arr]) && lclean(arr) && !r[55]; + } + } + return 0; +} +// the allocation facts of the function's locals, kept past the loop top that forgets them +word lafact_save() { + word b; int i = lbase; + if (dry || nloc <= lbase) return 0; + b = chk_resize(0, 0, nloc - lbase + 2); b[0] = lbase; b[1] = nloc; + 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 +int lafact_keep(word r, word b) { + int i; + if (!b || dry || r[0] || r[55]) 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; +} +// the allocation fact of the pointer local bl at the entry of the innermost +// loop over ix, or 0 +word entry_fact(int ix, int bl) { + int k = lsp; word r, b; + if (ix < 0 || bl < 0) return 0; + while (k > loopbase) { + k--; + r = linfo(k); + if (!r || r[40] != ix) continue; + b = r[56]; + if (!b || bl < b[0] || bl >= b[1]) return 0; + return b[2 + bl - b[0]]; + } + return 0; +} +// the number of elements behind a pointer local: the requested size of the +// block it was set from, when the analyzer knows it (never a rounded block +// size), for one-word elements; -1 when unknown +int ptr_elems(word f, word et, int bl) { + word base; + if (bl < 0 || !f || f[1] == 2 || f[0] < 0 || tbytes(et) || tsz(et) != 1) return 0 - 1; + if (f[6]) { base = af_base(f); if (base[1] == 0 || base[10] < 0) return 0 - 1; if (f[14] && f[13]) return 0 - 1; } // as af_inrange: a live allocation, from its start + return f[0]; +} + +// ---- --explain-checks ---- + +// zy --explain-checks [file] < source compiles the unit without running it and +// prints, as json lines, every bounds check the compiler kept, from the same +// decisions that drop the others. the first line is {"version":1}; the format +// is in docs/SPEC.md. the reason codes: +const int XC_NOT_LOOP = 1, XC_NOT_INVARIANT = 2, XC_NOT_LEN = 3, XC_SIZE = 4, XC_PACKED = 5, XC_HOISTED = 6, XC_MAYFREE = 7; +// why a check of index ix (a local, or -1) into the array local arr stays +int xc_reason(int ix, int arr) { + int k = lsp; word r; + if (ix < 0) return XC_NOT_LOOP; + while (k > loopbase) { + k--; + r = linfo(k); + if (!r || r[40] != ix) continue; + if (!r[53]) return XC_NOT_INVARIANT; + if (arr >= 0 && (ldirty(r, lname[arr]) || !lclean(arr))) return XC_NOT_INVARIANT; + if (arr >= 0 && r[55]) return XC_MAYFREE; + return XC_NOT_LEN; + } + return XC_NOT_LOOP; +} +// one character of the unit's source +int xc_byte(int k) { return (xc_src[k >> 2] >> ((k & 3) * 8)) & 255; } +// the column (from 1) of the source offset o +int xc_col(int o) { + int k = o; + while (k > 0 && xc_byte(k - 1) != 10) k--; + return o - k + 1; +} +// a json string +int xc_str(char* s) { + int i = 0, ch; + rt.put_c(34); + while (s[i]) { + ch = s[i] & 255; + if (ch == 34 || ch == 92) rt.put_c(92); + if (ch < 32) rt.put_c(32); else rt.put_c(ch); + i++; + } + rt.put_c(34); + return 0; +} +int xc_field(char* name) { rt.put_c(44); xc_str(name); rt.put_c(58); return 0; } +// the record of one kept check: kind 0 index, 1 pointer; the place of its [ +// and, as the end, the token just read (its ]) +int xc_note(int kind, int why, int place) { + int o1, o2, d = 0, k = loopbase; + if (!xc_on || dry || cmode || incdepth > 0 || !xc_src || chbase != xc_src) return 0; + o1 = ((place >> 40) & 0x1FFFFF) - 1; o2 = tpend; + if (o1 < 0 || o2 < o1) return 0; + while (k < lsp) { if (R_LOOP[k * 8] != 0 - 1) d++; k++; } + rt.put_s("{\"file\":"); xc_str(xc_file); + xc_field("line"); rt.put_n(place & 0xFFFFFF); + xc_field("col"); rt.put_n(xc_col(o1)); + xc_field("end_line"); rt.put_n(tpline); + xc_field("end_col"); rt.put_n(xc_col(o2)); + xc_field("fn"); xc_str(xc_fn); + xc_field("kind"); if (kind) xc_str("pointer"); else xc_str("index"); + xc_field("loop_depth"); rt.put_n(d); + xc_field("reason"); + if (why == XC_NOT_LOOP) xc_str("index-not-loop-variable"); + else if (why == XC_NOT_INVARIANT) xc_str("bound-not-invariant"); + else if (why == XC_NOT_LEN) xc_str("index-not-len-derived"); + else if (why == XC_SIZE) xc_str("size-unknown"); + else if (why == XC_PACKED) xc_str("packed-elements"); + else if (why == XC_MAYFREE) xc_str("pointer-may-be-freed"); + else xc_str("hoisted-to-loop-entry"); + xc_field("fix"); + if (why == XC_NOT_LOOP) xc_str("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"); + else if (why == XC_NOT_INVARIANT) xc_str("the loop body changes the index, the bound or the array, takes an address or makes a closure; keep them fixed inside the loop"); + else if (why == XC_NOT_LEN) xc_str("bound the loop with len() of the array, or with a constant no larger than its length"); + else if (why == XC_SIZE) xc_str("the compiler does not know the size of the block; allocate it here with a constant size, or index a fixed array"); + else if (why == XC_PACKED) xc_str("packed elements are checked by the runtime on every access"); + else if (why == XC_MAYFREE) xc_str("the loop body calls something that might free or resize the block; move the call out of the loop"); + else xc_str("checked once when the loop starts, and on every access only if that check fails; nothing to do"); + rt.put_c(125); rt.put_c(10); + return 0; +} +// is argument 1 --explain-checks? the file name for the records is argument 2 +int xc_init() { + int n = rt.syscall(rt.SYS_ARGC, 0, 0, 0), k; word b; + if (n < 2) return 0; + b = chk_resize(0, 0, 32); + if (rt.syscall(rt.SYS_ARG, 1, b, 31) < 0 || !rt.eq_w(b, "--explain-checks")) return 0; + xc_on = 1; + if (n > 2) { k = rt.syscall(rt.SYS_ARG, 2, 0, 0); if (k >= 0) { b = chk_resize(0, 0, k + 1); rt.syscall(rt.SYS_ARG, 2, b, k + 1); xc_file = b; } } + rt.put_s("{\"version\":1}"); rt.put_c(10); + return 0; +} // is the constant index xcval known to be inside the allocation f? the same // facts af_index warns from, so a possible failure is never called definite. int af_inrange(word f) { diff --git a/src/compiler/base.zc b/src/compiler/base.zc index c6abad7..f2bfeca 100644 --- a/src/compiler/base.zc +++ b/src/compiler/base.zc @@ -325,6 +325,15 @@ word[8] o3free; int no3free, o3nreg; word[NL] o3cache_initial; word o3cache = o3 // operator names used by numeric type checks. word[12] numops; int nnumops, s_fixed, s_dlen, s_dcap, s_dnew, s_dat, s_dpush, s_dpop, s_dresize, xconst, xcval; int xlenloc, arrloc, fortest, forstep, ft_iv, ft_bd, ft_ir, ft_ck, ft_nops, fs_ok, xstamp; +// what each live loop's body may change, and its hoisted checks (one 56-word +// record per loop depth, the first 64 depths; see body_scan and hoist_guard) +const int LPI_N = 64, LPI_W = 60; +word lpinfo; // allocated at the first loop +// --explain-checks: on, the unit's source (to turn offsets into columns), its +// file name and the function being compiled +int xc_on; word xc_src; char* xc_fn = ""; char* xc_file = ""; +// names body_scan looks for +int sx_push, sx_pop, sx_resize, sx_defer, sx_asm, sx_quote, sx_new, sx_int, sx_char, sx_bool, sx_float, sx_if, sx_else, sx_while, sx_for, sx_switch, sx_do; // local lower bound / len(array); one proof record per live loop int nfact, factcap = RANGE_FACTS; word[RANGE_FACTS] floc_initial, flo_initial, flen_initial; word floc = floc_initial, flo = flo_initial, flen = flen_initial; int s_len_s, s_at_s, s_slice_s, s_cat_s, s_eq_s, s_lt_s, s_le_s, s_put_bs, s_put_s, s_n_to_s, s_new_s; diff --git a/src/compiler/builtins.zc b/src/compiler/builtins.zc index cbc380e..5efe379 100644 --- a/src/compiler/builtins.zc +++ b/src/compiler/builtins.zc @@ -1197,6 +1197,9 @@ int types_init() { s_new_raw = intern("rt.new_raw"); s_oob = intern("rt.oob"); s_bchk = intern("rt.bchk"); s_bnd = intern("rt.bnd"); + sx_push = intern("push"); sx_pop = intern("pop"); sx_resize = intern("resize"); sx_defer = intern("defer"); sx_asm = intern("asm"); sx_quote = intern("quote"); + sx_new = intern("new"); sx_int = intern("int"); sx_char = intern("char"); sx_bool = intern("bool"); sx_float = intern("float"); + sx_if = intern("if"); sx_else = intern("else"); sx_while = intern("while"); sx_for = intern("for"); sx_switch = intern("switch"); sx_do = intern("do"); s_new_oz = intern("rt.new_oz"); s_ld8 = intern("rt.ld8"); s_st8 = intern("rt.st8"); s_ld16 = intern("rt.ld16"); s_st16 = intern("rt.st16"); s_ld32 = intern("rt.ld32"); s_st32 = intern("rt.st32"); diff --git a/src/compiler/decl.zc b/src/compiler/decl.zc index 87281ad..1c72ba0 100644 --- a/src/compiler/decl.zc +++ b/src/compiler/decl.zc @@ -133,6 +133,7 @@ int prescan(int kind, int obj) { // compile a whole unit from stdin int unit_stdin() { int src = readsrc(); + xc_src = src + 0; // a plain copy of the address, not a second owner module_name = 0; module_imports = 0; prescan(3, src); src_push(3, src, 0, 0); @@ -381,7 +382,7 @@ int fndef(int chk, int rty, int ret, int n) { sflag[s] = sflag[s] | F_DEF; fixall(sfix[s], here); sfix[s] = 0; fn_begin(chk, ret); - lt = lt_begin(sval[s], sname[s], lfl); + lt = lt_begin(sval[s], sname[s], lfl); xc_fn = sname[s]; finsym = s; finfer = !ret; effect_current = effect_record(s); rt.fill_w(effect_current, 0, 50); effect_current[0] = 1; if (!chk || stubgen) effect_current[0] = 2; effect_current[1] = np; i = 0; while (i < np) { if (pt[i] == 2) { effect_current[2 + i] = EF_CONSUME; effect_current[26 + i] = EF_CONSUME; } i++; } diff --git a/src/compiler/expr.zc b/src/compiler/expr.zc index a548f8d..8768658 100644 --- a/src/compiler/expr.zc +++ b/src/compiler/expr.zc @@ -647,6 +647,7 @@ word closure_layout(int closure_index, int count) { // variable in. ctx_push / ctx_pop save and restore the enclosing function's // compiler state around the body. int closure() { + char* xcf; int np = 0; char*[24] pn; word[24] pty; int hop, entry, i, t, envl, ncap, c, result, declared = 0, tags = 0, tag, lt, lfl = tline; word[24] ptags; word expected = closure_expected; closure_expected = 0; reserve_closures(nclo + 1); @@ -679,6 +680,7 @@ int closure() { hop = hole(); op(O_JMP); entry = here; fn_begin(1, 0); fbnd = ctx_bnd(); + xcf = xc_fn; xc_fn = ""; lt = lt_begin(entry, "", lfl); if (declared) fty = declared; prologue(); borrow_prologue(); @@ -700,7 +702,7 @@ int closure() { if (result <= 0 || live) result = tword; if (declared) result = declared; epilogue(); - lt_end(lt, here); + lt_end(lt, here); xc_fn = xcf; nclo--; c = nclo; ncap = clo_n[c]; @@ -1363,7 +1365,7 @@ int ptr_chk(int sz) { // through rt.bchk, which only knows the size of a heap block's first word. int postfix() { return postfix_tail(primary()); } int postfix_tail(int c) { - int b, n, t, et; word ft; word[8] bs; int k, ci, was, al, ix, enh, cz, cj, place, offset, temporary, call_owner, readonly, ub, bl, ic, inr; word storage, storage_mask, call_origins; + int b, n, t, et; word ft; word[8] bs; int k, ci, was, al, ix, enh, cz, cj, place, offset, temporary, call_owner, readonly, ub, bl, ic, inr, hg, pn; word storage, storage_mask, call_origins; while (1) { if (tk == T_ID && tv == s_as) { // e as T: same bits, another type next(); t = ptype(); rval(); if (!xaf || xaf[2] != 5) xaf = 0; vf_coerce(t, 0); @@ -1415,7 +1417,7 @@ int postfix_tail(int c) { op(O_SWAP); lit(2); op(O_ADD); op(O_LD); lit(8); op(15); op(O_SWAP); if (tbytes(et) != 1) { lit(tbytes(et)); op(15); } op(O_ADD); - } else callname(intern("datb")); + } else { callname(intern("datb")); xc_note(0, XC_PACKED, place); } et = tpk(et); } else if (xty[0] == TY_DYN) { // a growable array: bounds-checked, through the runtime et = xty[4]; @@ -1468,7 +1470,7 @@ int postfix_tail(int c) { setlit(k, here); op(O_SWAP); lit(2); op(O_ADD); op(O_LD); op(O_SWAP); mulsz(et); op(O_ADD); - } else callname(s_dat); + } else { callname(s_dat); xc_note(0, xc_reason(ix, al), place); } } else { tcneed(isptr(xty) || xty == tword, "only pointers and arrays can be indexed", xty); et = telem(xty); @@ -1490,9 +1492,26 @@ int postfix_tail(int c) { tcneed(isnum(xty) || xty == tword, "an index has to be a number", xty); expect(s_rk); if (!ub && !inr) { - if (n >= 0) { if (!ic && !(ix >= 0 && proven_n(ix, n))) fixed_chk(n); } - else if (tbytes(et)) ptr_chk(0 - tbytes(et)); - else ptr_chk(tsz(et)); + if (n >= 0) { + if (!ic && !(ix >= 0 && proven_n(ix, n))) { + hg = hoist_guard(ix, n, 0 - 1); + fixed_chk(n); + if (hg >= 0) { setlit(hg, here); xc_note(0, XC_HOISTED, place); } + else xc_note(0, xc_reason(ix, 0 - 1), place); + } + } else { + pn = ptr_elems(storage, et, bl); + if (pn < 0) pn = ptr_elems(entry_fact(ix, bl), et, bl); // the loop top forgot the fact; the body leaves the pointer alone (hoist_guard and proven_p check) + if (pn >= 0 && ix >= 0 && proven_p(ix, pn, bl)) pn = pn; // the loop test proved it + else { + hg = 0 - 1; if (pn >= 0) hg = hoist_guard(ix, pn, bl); + if (tbytes(et)) ptr_chk(0 - tbytes(et)); + else ptr_chk(tsz(et)); + if (hg >= 0) { setlit(hg, here); xc_note(1, XC_HOISTED, place); } + else if (pn < 0) xc_note(1, XC_SIZE, place); + else xc_note(1, xc_reason(ix, bl), place); + } + } } if (tbytes(et)) { // packed: byte address = base * 8 + index * bytes if (tbytes(et) != 1) { lit(tbytes(et)); op(15); } diff --git a/src/compiler/setup.zc b/src/compiler/setup.zc index 26a18e0..ac455db 100644 --- a/src/compiler/setup.zc +++ b/src/compiler/setup.zc @@ -175,7 +175,9 @@ int start() { // a genome that carries the language server runs it instead of compiling stdin s = lookup(intern("lsp.lsp_main")); if (s >= 0 && skind[s] == K_FN && (sflag[s] & F_DEF)) { f = sval[s]; f(); rt.halt(); } + xc_init(); unit_stdin(); + if (xc_on) rt.halt(); // --explain-checks: the records are out; main does not run if (here > ptop) ptop = here; rt.scrub(); // compilation's stale words would keep quarantined blocks alive rt.gc(); diff --git a/src/compiler/stmt.zc b/src/compiler/stmt.zc index a67b931..d23cb52 100644 --- a/src/compiler/stmt.zc +++ b/src/compiler/stmt.zc @@ -246,6 +246,7 @@ int loop_push(int cont, int s0) { f[6] = extop; f[7] = 0; lpfact[lsp] = -1; + if (lsp < LPI_N && lpinfo) lpinfo[lsp * LPI_W + 54] = 0; lsp++; return 0; } @@ -312,7 +313,7 @@ int kw_while() { // if it holds and the bound is len(a) of a fixed array, the body is told that // a[i] is in range (lpfact), and its bounds check disappears. int kw_for() { - int save = nloc, s0, sc = -1, c0, a, b, st, c, inf = 0; word borrow_mark = borrow_slots; + int save = nloc, s0, sc = -1, c0, a, b, st, c, inf = 0, xe = -1, cl = 0; word borrow_mark = borrow_slots; word r = 0; word fs = 0; stmtonly(); next(); expect(s_lp); @@ -321,7 +322,10 @@ int kw_for() { else if (tstart()) localdecl(1); else { if (!is_op(s_semi)) { c = expr(); rval(); op(O_DROP); discard(c); } expect(s_semi); } borrow_cleanup_since(borrow_mark); + if (fbnd) fs = lafact_save(); s0 = snap_push(); + // i < n with a variable n: a jump to the loop entry, where hoisted checks get their flags (see hoist_guard) + if (fbnd && infn && !dry && tk == T_ID) { peekat(1); if (pk_tk == T_ID) { peek(); if (pk_tk == T_OP && pk_tv == s_lt) { xe = hole(); op(O_JMP); } } } c0 = here; ft_iv = -1; ft_ck = -1; fs_ok = 0; fortest = 1; if (!is_op(s_semi)) { @@ -342,15 +346,27 @@ int kw_for() { jmp(c0); setlit(b, here); loop_push(st, s0); - if (ft_iv >= 0 && ft_bd >= 0 && fs_ok && getlo(ft_iv) >= 0 && getln(ft_bd) >= 0) { - lpfact[lsp - 1] = pfact(ft_iv, ft_bd, getln(ft_bd)); - } else if (ft_iv >= 0 && ft_ck >= 0 && fs_ok && getlo(ft_iv) >= 0) { // i < constant: proves a fixed array that long - lpfact[lsp - 1] = pfact(ft_iv, -1, 0 - ft_ck - 2); + // a proof needs a body that leaves the index, the bound and the array alone + r = linfo_new(lsp - 1); + if (r) { body_scan(r); r[40] = 0 - 1; r[41] = 0 - 1; r[42] = xe; r[56] = fs; } + if (r && ft_iv >= 0 && fs_ok) { + r[40] = ft_iv; + cl = !ldirty(r, lname[ft_iv]) && lclean(ft_iv); + if (cl && ft_bd >= 0) cl = !ldirty(r, lname[ft_bd]) && lclean(ft_bd); + r[53] = cl; } + if (cl && ft_bd >= 0 && getlo(ft_iv) >= 0 && getln(ft_bd) >= 0) { + if (!ldirty(r, lname[getln(ft_bd)]) && lclean(getln(ft_bd))) lpfact[lsp - 1] = pfact(ft_iv, ft_bd, getln(ft_bd)); + } else if (cl && ft_ck >= 0 && getlo(ft_iv) >= 0) { // i < constant: proves a fixed array that long + lpfact[lsp - 1] = pfact(ft_iv, -1, 0 - ft_ck - 2); + } else if (cl && xe >= 0 && ft_bd >= 0 && ltype[ft_iv] == tint && ltype[ft_bd] == tint) { r[52] = 1; r[41] = ft_bd; } // i < n: checks against n can be hoisted substmt(); backedge(s0); jmp(st); + if (xe >= 0) { if (r && r[43]) hoist_stub(r, c0); else setlit(xe, c0); } loop_end(a, sc); + if (r) { lafact_keep(r, fs); r[56] = 0; } + if (fs) rt.free(fs); snap_pop(s0); block_close(save); fdepth--; diff --git a/src/core/core.c b/src/core/core.c index e3895ae..e7b1ef6 100644 --- a/src/core/core.c +++ b/src/core/core.c @@ -7159,6 +7159,10 @@ int main(int argc, char **argv) "compiles source from stdin and runs main; input after a backtick is program input.\n" "program arguments are available through std.argv; stdin has the name .\n", stdout); +#endif +#ifndef USE_LSP_GENOME + fputs(" zy --explain-checks [file] < source.zc compiles without running and lists\n" + " the bounds checks it kept as json lines (file names them; default ).\n", stdout); #endif fputs("options:\n --help, -h show this help and exit\n" "environment:\n" @@ -7167,7 +7171,7 @@ int main(int argc, char **argv) " ZYTRACE trace native translation and optimization\n", stdout); return 0; } - if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-') { + if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-' && strcmp(argv[1], "--explain-checks")) { #ifdef USE_LSP_GENOME if (strcmp(argv[1], "--format") && strcmp(argv[1], "--annotate") && strcmp(argv[1], "--types")) { #endif diff --git a/src/micro/port_linux.c b/src/micro/port_linux.c index 9331a0b..6245f4f 100644 --- a/src/micro/port_linux.c +++ b/src/micro/port_linux.c @@ -372,7 +372,7 @@ int main(int argc, char **argv) { " TINYVM_MAX_MEMORY_WORDS maximum vm memory in words\n", stdout); return 0; } - if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-') { + if (argc > 1 && argv[1][0] == '-' && argv[1][1] == '-' && strcmp(argv[1], "--explain-checks")) { /* the compiler reads that one */ fprintf(stderr, "micro: unknown option %s; use --help for usage\n", argv[1]); return 2; } 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":"","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":"","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":"","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":"","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":"","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":"","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":"","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 :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" -- cgit v1.2.3