String equality, written as Prolog's ==.

Whether the term t is the atom a.

Whether the list xs has n terms: the arity of a compound.

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 q, as ir.pl writes it: tmp(Q).

The name d when the term t is tmp(D).

As narrow_type/3: the bytes of the narrow integer type a.

As cas_type/1 and cas_bytes/2: the bytes a cascas nanofilCompare-and-exchange, the one atomic read-modify-write term in the IR: cas(T) reads the T at an address and, if it equals Expected, writes New there, as one sequentially consistent step. Every other atomic operation is a loop of it (c_lower:rmw//7). of type t compares and swaps.

As the first answer of access_size_align/3: a load of type x or a store of width x accesses so many bytes at an address that must be so aligned: 8 for a pointer, whose capability is in the auxaux Fil-CAn object's aux allocation, as large as its payload: where Fil-C keeps the lowers of the pointers stored in the object, slot for slot, while their intvals sit in the object's bytes. The aux word in the object header points at it; it is null for an object no pointer was ever stored into, which the collector then scans as a leaf. A pointer store must *ensure* it exists, which may call the runtime; a pointer load reads it. word of its 8-byte slot, the width for a cascas nanofilCompare-and-exchange, the one atomic read-modify-write term in the IR: cas(T) reads the T at an address and, if it equals Expected, writes New there, as one sequentially consistent step. Every other atomic operation is a loop of it (c_lower:rmw//7)., else 1. No x has two answers.

A list of memory effects, as pointer_memory_effects/2 writes it.

pointer_memory_effects(load, Es).

pointer_memory_effects(store, Es).

pointer_memory_effects(local_load, Es).

pointer_memory_effects(local_store, Es).

let(tmp(Q), a, check(0, Size, Rights, Align), [A]): the 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). of an access of size bytes at the address a, whose proof is q.

check_inst for a size and alignment that size_align gave.

let(tmp(Q), a, check_local(X, Off, Size, Rights, Align), []): the check of an access to the local x at the offset off.

let(D, p, raw_load_pointer(0, Es), [tmp(Q)]).

raw_store_pointer(0, V, tmp(Q), Es).

let(D, K, raw_load(T, 0), [tmp(Q)]).

raw_store(W, 0, V, tmp(Q)).

As checked_access/4, a clause for each row of pizlonate.pl's table: when the instruction i is an access, its check, defining tmp(Q), and its raw access, for the fresh name q it is given. None for an instruction that is not an access.

As flight_inst/2: the 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. of the pure pointer operation i, which is add or sub of an offset, a copy of a temporary or a constant, or itop, which has no lowerlower Fil-CThe lower is how Fil-C represents a capability natively: the address of the first byte of the object a pointer may access, kept beside the pointer's intval in a flight pointer. The object header sits just below it: the upper bound at lower−16 and the aux word at lower−8, whose low 48 bits point at the aux allocation and whose top 16 bits hold the object's flags (free, read-only, global, ...). A null lower accesses nothing, and free sets upper to lower, so every access through any lower of a freed object fails. filc_abi:lower_function/5 keeps each live one in a root.. A copy of a symbol calls its getter and stays as it is.

The name d when the term r is result(tmp(D), K).

As cfg.pl's inst_def/2: the names of the temporaries the instruction i defines; a call can define several.

The text of the name n when it could be a proof's name: an atom that begins chk.

As func_temp_names/3, kept to the names a fresh one could be: of the temporaries that the function with the parameters params and the blocks defines, as a parameter, 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. or an instruction's result, those whose name begins chk.

As fresh_name/4: the name chkI for the least I from n on that is not among names, and I + 1. Each name passed over is another of names, so a fuel of their number is enough: when it is spent, every one of them has been passed over.

Whether the instruction i is a loc(File, Line) marker.

A step of checked_insts/11, in filc modemode nanofilA module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2).: the count of fresh names and the instructions so far, last first, with the instruction i after them: an access as its check and raw access (checked_access), a pure pointer operation as its flight (flight_inst), and any other as it is.

As polled_target/4: the target l of a jump from the block at the index from: poll(L) when the block l is at or before it in block order (index), and l as it is when it is later, or is a poll edge already. None for a label no block has.

As polled_jump/4: the jump j that ends the block at the index from, with a poll edge for each target at or before it, so that every cycle of the function polls.

Each block's label with its place in block order, from i on, added to m. None when a term is not a block or two blocks have one label, where list_to_assoc/2 throws.

As pizlonated_blocks/7: the blocks bs, the first at the index i in block order, their loc markers dropped when drop is set, their instructions by inst_step in filc modemode nanofilA module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2). and their jumps by polled_jump. n counts the fresh names, across the blocks.

As pizlonated_item/4 for the function func(Name, Linkage, Ret, Params, Blocks).

As ir.pl's pointer_inst/1: the instruction i makes, stores, passes or calls through a p value, or converts one.

The blocks of the item it when it is a function.

The instructions and the jump of the term b when it is a block.

As ir.pl's pointer_item/1: the item it has class p somewhere, or is an alias, a weak function, or read-only, weak, external or thread-local data, which only filc modemode nanofilA module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2). models.

As ir.pl's module_mode/2: the module of the items is in filc modemode nanofilA module's mode is plain or filc: filc if it uses anything Fil-C-specific (a p, a call to an external function, ...), plain otherwise, read off its contents (ir:module_mode/2). when an item is a pointer_item, or a function calls a symbol that no function of the module defines. A plain module's addresses are not Fil-C pointers.