A block is a labelled straight line of a function: phisphi 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., then instructions, then one jump (goto, branch, ret, rets, ret, unreachable). The first block is the entry and has no phis; its label is the name edges use.

• ir.pl: blockLabel, Phis, Insts, Jump; Syntax.v: block with b_label, b_phis, b_insts, b_jump; Semantics.v's find_block.

• A jump target may be pollL, a pollpoll 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). edge. The control-flow graph is cfg:func_cfg/2cfg.plfunc_cfg+Blocks, -CfgdetCfg = cfg(Entry, Rpo, Succs, Preds) is the control-flow graph of Blocks, whose first block is the entry: (func_cfg).

• Entering a block costs one unit of fuelfuel nanofilThe interpreter's bound on executed blocks: each block entered costs one unit, and running out ends the run out_of_fuel, which proves nothing (interp:run/5). (interp:block_outcome/7interp.plblock_outcome+Ctx, +Label, +Pred, +Env₀, +S₀, -Out, -SnondetOut and S are the outcome and final state of running the block Label, entered from Pred (from(L) or entry), and everything after it. Each block costs one unit of fuel., step at Enter), so the model's OutOfFuel comes where the interpreter's does.

The subtlety: labels must be unique (no_dups, checked by valid_func). The successor map keeps the last block of a label while the machine runs the first, so with a duplicate the proofs about dominancedominance nanofilBlock A dominates block B when every path from the entry to B passes through A. The validator decides it with the dominator tree's preorder intervals: each label gets the numbers of its subtree, and A dominates B when B's number lies in A's interval. would speak of a different graph from the one that runs.

Defined in ir.pl's header and Syntax.v.