As ir.pl writes the temporarytemporary nanofilA temporary is a function-local IR name, tmp(N), holding one word of one class. Parameters, phis and instructions define temporaries; operands read them. Names are ground terms, compared only for equality: no logic variable appears in IR. named d: tmp(D).

As ir.pl writes a value: tmp(N), const(N) or global(S).

As ir.pl writes the rightsrights Fil-CRights are what an access asks of a capability: read or write, where write allows reading too. Every check, renew and raw access names the rights it needs. of an access: read or write.

As ir.pl writes the bound a half checkhalf_check nanofilhalf_check(Bound, Lo, Hi, Rights, Align) of [Q1, P] is exactly a check of [Lo, Hi) at P that natively tests only one bound, upper or lower; the other end is known from Q1's earlier check of the same object, P being at a known distance from Q1's pointer. tests: upper or lower.

As ir.pl writes a narrow integer type: sw, uw, sh, uh, sb or ub.

As ir.pl writes the type of a raw load: l, s, d, x, or a narrow type.

As ir.pl writes a comparison's Cond: eq, ne, the signed and unsigned integer orders sle to ugt, the float orders le lt ge gt, o (ordered) or uo (unordered).

As ir.pl writes one memory effect of a raw pointer load or store: aux_read, lower_resolve, address_read, atomic_read, aux_ensure, lower_barrier, rooted_reload, lower_write, address_write or atomic_write.

As ir.pl writes the Effects of a raw pointer load or store: the list of its effects, in order.

As ir.pl writes the width of a store: b, h, w, l, p, s, d or x.

The atom signed or unsigned. No term of the IR holds it: it is written only in the terms of enc_op that are not ops.

As ir.pl writes a checkcheck Fil-CAn access check: check(Lo, Hi, Rights, Align) of a pointer P traps unless P's capability permits Rights on [P+Lo, P+Hi) with P+Lo Align-aligned, and otherwise yields P as a proof of class a. check_local does the same for a named local, and check_function yields a function proof of class f (ir:op_kind/2, pizlonate:checked_access/4). or one of its reusereuse nanofilReuse is using earlier evidence instead of a new check. --checks=reuse deletes a check whose access an earlier live proof already covers, so the access reads that proof; it works across plain edges and for related pointers at a constant offset (check_reuse:reuse_checks/2, m7.md, round 3). A reuse form is any op that trusts evidence other than a check just before it: renew, renew_hull, half_check, renew_if, check_limit and check_ahead. forms of the name f: f(Lo, Hi, Rights, Align).

As ir.pl writes an Op: an atom such as add or ptoi, or a compound such as cmp(Cond, K), ext(T), alloc(Align), check(Lo, Hi, Rights, Align), check_ahead(Lo, Hi, Rights, Align, AHi), half_check(Bound, Lo, Hi, Rights, Align), span_test(Lo, Hi), limit(Size), check_local(Name, Off, Bytes, Rights, Align), raw_load(T, Off) or raw_load_pointer(Off, Effects).

A float widening is ext(s) or ext(d), naming its source class; a float to an integer is stosi, stoui, dtosi, dtoui, xtosi or xtoui, and an integer to a float swtof, uwtof, sltof or ultof. Those are all the conversions ir.pl has. At any other class ExtF k is written ext(K), and FloatToInt k sg and IntToFloat k sg are written float_to_int(K, Sg) and int_to_float(K, Sg), Sg being signed or unsigned: none of them is an op, and the decoder refuses each.

As ir.pl writes an argument of a flightflight nanofilA flight builds a pointer from two independent sources: flight(D, Op, Args, Lower) computes D's address with copy, add or sub over l values and pointer addresses, and takes its capability from the pointer Lower names, or none (pizlonate:flight_inst/2). Making the pair proves nothing about access; no check, getter, memory access or safepoint happens inside it.: address(V), or the value itself.

As ir.pl writes a flight's Lower: none or lower(V).

As ir.pl writes one result of a call, the temporary d of class k: result(tmp(D), K).

As ir.pl writes a call's Res: void, result(tmp(D), K), or tuple([result(tmp(D1), K1), result(tmp(D2), K2)]).

As ir.pl writes a call's argument, the class first: arg(K, V).

As ir.pl writes a call's arguments: the list of them.

As ir.pl writes an instruction: let(tmp(D), K, Op, Args), flight(tmp(D), Op, Args, Lower), raw_store(Width, Off, Value, Addr), raw_store_pointer(Off, Value, Addr, Effects), call(Res, Callee, Args), raw_call(Res, Callee, Args), local_alloc(Name, Size) or loc(File, Line).

A RawStore of the width Wp is written raw_store(p, ...), which is not an instruction of the IR (a pointer store is raw_store_pointer) and which the decoder refuses.

As ir.pl writes a jump's target: the label L, or poll(L) for a poll edgepoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1).. A label is any ground term, and one that is itself poll(L) cannot be told from a poll edge to L: To of it is written poll(L), which the decoder reads as Poll of L. The decoder never gives such a To.

As ir.pl writes the jump that ends a block: goto(L), branch(V, L1, L2), ret(V), rets([V1, V2]), ret or unreachable.

As ir.pl writes one pair of a phiphi nanofilA phi phi(tmp(D), K, [Pred-Value]) gives D the value paired with the block control came from. A block's phis run together on entry, each reading its operand as it stood at the end of the predecessor., a predecessor's label and the value for the edge from it: Pred − Value.

As ir.pl writes a phiphi nanofilA phi phi(tmp(D), K, [Pred-Value]) gives D the value paired with the block control came from. A block's phis run together on entry, each reading its operand as it stood at the end of the predecessor.: phi(tmp(D), K, [Pred-Value]).

The decoder dec reads the term t, and the encoder enc writes what it read as t again. Then dec also reads what enc wrote as the same value, since that is t: one statement checks both directions.

The decoder dec reads back each value of xs from the term the encoder enc writes for it.

Every class is read back from eclass's atom for it.

Both rights are read back.

Both bounds are read back.

Every narrow type is read back.

Every load type is read back.

Every condition is read back.

Every effect is read back.

Every width is read back.

Every value is read back.

The two effect lists of a pointer load, and the empty one.

Every op that is an atom, the float conversions among them.

Every op that is a compound, one or two of each.

The conversions ir.pl does not have are refused, each one.

A raw store of a pointer is refused, and a label poll(l) reads back as a poll edge.

let(tmp(chk0), a, check(0, 8, write, 1), [tmp(p)]): a check.

let(tmp(chk0), a, check_local(x, 0, 1, read, 1), []): a check of a named local, which reads no argument.

let(tmp(a), l, raw_load(sb, 0), [tmp(chk3)]): a raw load.

let(tmp(back), p, raw_load_pointer(0, [aux_read, lower_resolve, address_read]), [tmp(chk2)]): a raw pointer load.

let(tmp(c), w, cmp(eq, w), [tmp(k), const(1)]): a comparison.

let(tmp(b), d, ext(s), [tmp(a)]): a float widening.

let(tmp(kl), l, ext(sw), [tmp(k)]): an integer extension.

let(tmp(r), w, dtosi, [tmp(b)]): a float to an integer.

let(tmp(base), p, copy, [global(g)]): a symbol's address.

raw_store(l, 0, const(-2), tmp(chk0)): a raw store.

raw_store_pointer(0, tmp(obj), tmp(chk1), [aux_ensure, lower_barrier, rooted_reload, lower_write, address_write]): a raw pointer store.

flight(tmp(q), add, [address(tmp(p)), const(8)], lower(tmp(p))): a flight with a lower.

flight(tmp(f), copy, [tmp(i)], none): a flight without one.

call(void, global(churn), []): a call with no result.

call(result(tmp(p), p), global(make), [arg(l, tmp(v))]): a call with one result.

call(tuple([result(tmp(c), l), result(tmp(d), l)]), global(two), [arg(l, tmp(a))]): a call with a tuple of results.

raw_call(result(tmp(a), s), tmp(chk0), [arg(s, const(1069547520))]): a call of a proven function.

raw_call(tuple([result(tmp(g), l), result(tmp(h), l)]), tmp(chk2), [arg(l, tmp(x))]): one with a tuple of results.

local_alloc(x, 13): a named local.

loc('basic.c', 12): a source position.

branch(tmp(c), poll(fill), sum): a branch, one edge polling.

goto(poll(loop)): a goto that polls.

goto(end): a plain goto.

ret(const(1)): a return of one value.

rets([tmp(n), tmp(m)]): a return of a tuple.

ret: a return from a void function.

unreachable.

phi(tmp(i), w, [start-const(0), fill-tmp(i1)]): a phi of two edges.