explain-checks: the record writer moves to src/lib/explain.zc, embedded and compiled only in that mode; the genome keeps the call sites and a hook

4 files changed, 76 insertions, 54 deletions

diff --git a/src/compiler/analyzer.zc b/src/compiler/analyzer.zc
index 1822fe5..c2ea867 100644
--- a/src/compiler/analyzer.zc
+++ b/src/compiler/analyzer.zc
@@ -772,72 +772,29 @@ int xc_reason(int ix, int arr) {
 	}
 	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 ])
+// and, as the end, the token just read (its ]). src/lib/explain.zc writes it.
 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;
+	int o1, o2, d = 0, k = loopbase, f;
+	if (!xc_on || dry || cmode || incdepth > 0 || !xc_src || chbase != xc_src || !xc_hook) 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);
+	f = xc_hook; f(xc_src, kind, why, place & 0xFFFFFF, o1, tpline, o2, d, xc_fn, xc_file);
 	return 0;
 }
-// is argument 1 --explain-checks? the file name for the records is argument 2
+// is argument 1 --explain-checks? the file name for the records is argument 2.
+// then src/lib/explain.zc is compiled, and its note becomes the hook.
 int xc_init() {
-	int n = rt.syscall(rt.SYS_ARGC, 0, 0, 0), k; word b;
+	int n = rt.syscall(rt.SYS_ARGC, 0, 0, 0), k, s, f; 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);
+	inc_compile(bstr_text(explain_source()), "tinyvm:explain.zc", 0);
+	s = lookup(intern("explain.note")); if (s >= 0) xc_hook = sval[s];
+	s = lookup(intern("explain.version")); if (s >= 0) { f = sval[s]; f(); }
 	return 0;
 }
 // is the constant index xcval known to be inside the allocation f? the same
diff --git a/src/compiler/base.zc b/src/compiler/base.zc
index f2bfeca..b326c80 100644
--- a/src/compiler/base.zc
+++ b/src/compiler/base.zc
@@ -331,7 +331,7 @@ 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 = "<eval>"; char* xc_file = "<eval>";
+int xc_on; word xc_src; char* xc_fn = "<eval>"; char* xc_file = "<eval>"; int xc_hook;
 // 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
diff --git a/src/compiler/check.zc b/src/compiler/check.zc
index 945b800..fb79439 100644
--- a/src/compiler/check.zc
+++ b/src/compiler/check.zc
@@ -112,5 +112,8 @@ int hl_end() {
 // `include std;` and `include icon;` need no file at run time.
 embed "src/lib/std.zc" as bstr std_embedded;
 embed "src/lib/icon.zc" as bstr icon_embedded;
+// the --explain-checks writer, compiled only in that mode
+embed "src/lib/explain.zc" as bstr explain_embedded;
 bstr std_source() { return std_embedded; }
 bstr icon_source() { return icon_embedded; }
+bstr explain_source() { return explain_embedded; }
diff --git a/src/lib/explain.zc b/src/lib/explain.zc
new file mode 100644
index 0000000..aef529b
--- /dev/null
+++ b/src/lib/explain.zc
@@ -0,0 +1,62 @@
+namespace explain;
+include rt;
+// writes the records of zy --explain-checks (format version 1, docs/SPEC.md
+// 4.15.4). the compiler embeds this file and compiles it only in that mode;
+// its analysis calls note once for every bounds check it keeps. no top-level
+// unbounded here: it would carry over into the unit being explained.
+const int NOT_LOOP = 1, NOT_INVARIANT = 2, NOT_LEN = 3, SIZE = 4, PACKED = 5, HOISTED = 6, MAYFREE = 7;
+word src;
+// one character of the unit's source
+int byte(int k) { return (src[k >> 2] >> ((k & 3) * 8)) & 255; }
+// the column (from 1) of the source offset o
+int col(int o) {
+	int k = o;
+	while (k > 0 && byte(k - 1) != 10) k--;
+	return o - k + 1;
+}
+// a json string
+int 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 field(char* name) { rt.put_c(44); str(name); rt.put_c(58); return 0; }
+// the first line
+int version() { rt.put_s("{\"version\":1}"); rt.put_c(10); return 0; }
+// one kept check: kind 0 index, 1 pointer; o1 and o2 the source offsets of its [ and ]
+int note(word unit, int kind, int why, int line, int o1, int end_line, int o2, int depth, char* fn, char* file) {
+	src = unit;
+	rt.put_s("{\"file\":"); str(file);
+	field("line"); rt.put_n(line);
+	field("col"); rt.put_n(col(o1));
+	field("end_line"); rt.put_n(end_line);
+	field("end_col"); rt.put_n(col(o2));
+	field("fn"); str(fn);
+	field("kind"); if (kind) str("pointer"); else str("index");
+	field("loop_depth"); rt.put_n(depth);
+	field("reason");
+	if (why == NOT_LOOP) str("index-not-loop-variable");
+	else if (why == NOT_INVARIANT) str("bound-not-invariant");
+	else if (why == NOT_LEN) str("index-not-len-derived");
+	else if (why == SIZE) str("size-unknown");
+	else if (why == PACKED) str("packed-elements");
+	else if (why == MAYFREE) str("pointer-may-be-freed");
+	else str("hoisted-to-loop-entry");
+	field("fix");
+	if (why == NOT_LOOP) 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 == NOT_INVARIANT) 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 == NOT_LEN) str("bound the loop with len() of the array, or with a constant no larger than its length");
+	else if (why == SIZE) 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 == PACKED) str("packed elements are checked by the runtime on every access");
+	else if (why == MAYFREE) str("the loop body calls something that might free or resize the block; move the call out of the loop");
+	else 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;
+}