interp.pl
Relational semantics of the IR (ir.pl): the outcome of running a function of a module, as a relation that runs in every direction, so that arguments and outcome can both be partially unknown.
Entry points
| Predicate | Does |
|---|---|
run+Module, +Fn, ?Args, +Fuel, ?Outcome | prepares Module, then runs Fn |
module_prepared+Module, −Prepared | the module's mode, initial memory, and indexes of its functions and blocks |
run_prepared+Prepared, +Fn, ?Args, +Fuel, ?Outcome | runs Fn of a prepared module |
Prepare once to run many times. Args are integers or CLP(Z) variables, one per parameter, in the range of the parameter's class (ptrAddr, Cap for a p parameter).
Outcomes
| Outcome | Means |
|---|---|
retV | returned V (an integer or constrained variable) |
retsX1, X2 | returned a tuple |
ret | returned from a void function |
unreachable | executed unreachable |
ubReason | undefined behaviour: division_by_zero, division_overflow, float_conversion (an invalid float-to-integer conversion), or in plain mode out_of_boundsA, Size, a memory access outside every live allocation |
trapReason | a Fil-C check failed (filc mode only): null_capability, out_of_bounds, misaligned, readonly, not_a_function, argument_size, return_size, invalid_free, double_free |
uncheckedReason | a raw access (checked stage, ir.pl) that its capability does not allow: a check is missing or too weak, which only a broken pass produces. It is neither ub nor a trap, so it refines nothing. |
out_of_fuel | executed Fuel blocks without finishing |
Unknown values
Integer arithmetic and branches are CLP(Z) constraints, so the relation runs in every direction. Known values take a fast path (is/2 and if-then-else), which gives the same answers; only unknown values pay for constraints.
Memory addresses, allocation sizes and capabilities must be known when an access, alloc or indirect call uses them; otherwise the run raises an instantiation error, which is incomplete but never wrong.
Float values are concrete unsigned IEEE bits. Float arithmetic uses ieee.pl's integer-only SSE2 semantics, not CLP(Z) or host floats; unknown float inputs also raise an instantiation error.
Memory
Memory is memBytes, Regions, Next, Aux:
| Part | Is |
|---|---|
| Bytes | an assoc from address to byte |
| Regions | regionBase, End, Kind, Life objects; Kind is stack, heap or global, Life is live or freed |
| Next | the next allocation address; addresses are never reused |
| Aux | in filc mode, the capabilities stored in memory |
A byte nobody wrote is, in plain mode, a fresh variable in 0..255, so reading uninitialized memory gives an unknown value rather than a made-up one; in filc mode it is 0, since Fil-C zeroes allocations.
In plain mode a function's allocations die when it returns, and addresses are never reused, so use after return is an out-of-bounds access. In filc mode allocations outlive their function. External callvoid, globalfree, argp, P invalidates P's heap object: End becomes Base and Life becomes freed. A live zero-sized object also has End = Base, but may be freed once. Bytes and stored lowers stay intact; every alias consults the same region's current bounds. Module-defined functions take precedence over this external adapter.
A capability's Base is stable identity, never recovered from address bits. All exposed capabilities for an object have the same rights (objBase or roBase); snapshot initialization is private until its readonly capability is published. Memory-using injected pointer arguments must obey these invariants and name existing objects.
This is the deterministic explicit-free subset, not a GC simulator: no reclamation, concurrent or signal-handler frees, or rewriting dead lowers to the runtime's free singleton. Unknown external effects and addresses remain outside the oracle's domain. It does not justify check elimination or safepoint motion (docs/lifetime.md).
Run state
The run state is sMem, Fuel; each block costs one unit of Fuel. Inside a function the interpreter carries ctxFns, Globals, Blocks, Ret, Mode, Locals:
| Part | Is |
|---|---|
| Fns | the prepared functions |
| Globals | the address of each global |
| Blocks | the function's blocks by label |
| Ret | its return class |
| Mode | the module mode |
| Locals | this invocation's local names and fresh object identities, bound at local_alloc |
A block is entered fromPred, Pred the label of the block that jumped to it, or at entry.
Variable names
| Name | Is |
|---|---|
| K | a class |
| V | an IR value: tmpN, constN or globalN |
| X | a run-time value: an integer, a constrained variable, or in filc mode ptrAddr, Cap |
| Env | the assoc from temporary to run-time value |
| S | a run state |
| Out | an outcome |
| Res | a partial result: valX, ok, ubWhy, trapWhy or uncheckedWhy |
Env0/Env and S0/S are the state before and after.
Outcome is the result of calling the function Fn of module M on Args and executing at most Fuel blocks. With unknown Args each solution constrains them to the inputs that take one path; see run_prepared/5.
Prepared is M ready to run: its mode, the address of each global, its initial memory, and its functions and their blocks indexed by name and label. The initial memory holds integers only, so runs can share it.
Outcome is the result of calling Fn of the prepared module on Args within Fuel blocks. Args is constrained to the ranges of Fn's parameter classes. Where a branch or a division depends on an unknown value (an argument, or a byte nobody wrote), there is one solution per case, each constraining that value; comparisons are reified instead. When every such value is known the outcome is unique, though the run may leave a choice point, so callers use once/1. Fails when the module defines no Fn. Throws nanofil_error when the run needs what the interpreter does not model (a symbol the module does not define, a temporary read before any assignment), and an instantiation error when an address, allocation size or capability is unknown.
X is an argument of class K. A p argument is ptr(Addr, Cap), or an integer address with no pointer term (main.pl's canonical arguments): a defaulty case that comes from outside this module, so the cut stays. An unknown p argument is ptr(_, _).
calling Fn on Xs in state S0 ends with Out in state S. In plain mode a callee's allocations die when it returns; in filc mode every allocation is a heap object that lives until explicitly freed.
Keep identities, bytes and aux, but end just this invocation's stack lifetimes in the latest state. A trap may precede a declaration; its unbound Base is not authority to select and invalidate another object.
promote_cc_to_heap returns null for an empty argument packet. This is distinct from alloc(0), which creates an ordinary zero-sized object.
R is the value of the integer expression Expr. Concrete fast path: when every operand is known, plain arithmetic and if-then-else give the same answers as the constraints, without propagators or choice points. Unknown operands still get constraints. The ground/1 test reads the instantiation, but both branches state the same relation, so the program stays sound for partially known Expr.
B is 1 if Test holds, else 0 (reified when unknown).
Blocks
Out 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.
Env is Env0 with each phi of Phis bound to its value for the edge from Pred, read in EntryEnv. Phis read the environment as it was on entry, so they all bind at once. An entry block has no phis.
the block's Jump continues the run unless an instruction ended it.
Out is the outcome of Jump, ending block From, and everything after it. When the jnz condition is unknown, both edges are solutions, each constraining it; a known one takes the fast path. A pollcheck on the edge (poll(L)) changes nothing the interpreter models: explicit free calls run, but there are no asynchronous frees.
Instructions
Result is cont(Env, S) when every instruction ran, or stop(Outcome, S) when one ended the run.
Result is the result of the instructions Insts after one whose result is Result0.
Result is cont(Env, S) after Inst, or stop(Outcome, S) when it ends the run.
Only libc free's ordinary signature is modeled. Resolution comes first: an in-module function is handled above; an in-module data symbol is not a function. Other signatures and external calls are explicit gaps, not silently failed relations or guessed libc effects.
P designates a function only when it carries that function's capability at its exact callable address. An unknown address is not proof; an external symbol's kind is unknown to the interpreter, which must not guess that it names a function.
A target check authorizes the call, not its signature. Only a failed target check becomes unchecked in raw_call; ABI and callee traps keep their meaning. The conversions below are shared with unchecked call.
the result of an indirect call to F on Ys, with the call's conversion Conv.
indirect_call_conv(+CalleeRet, +Params, +Res, +Args, +Xs, -Ys, -Conv): a call through a function pointer. When the classes the call site passes and expects give the callee's signature (w and l are the same word), it is a direct call. Otherwise it goes through the callee's generic entry: each argument and result word is 8 bytes with its lower beside it, so a p word read as an integer is its address and an integer read as p has no capability. Too few arguments, or fewer result words than the call site reads, fail the generic entry's size checks. Conv is same, conv(CallerWords, CalleeWords) or trap(Why).
Y is the word X written at class From and read at class To through the generic entry.
A p word read as an integer is its address. An integer held at p (see class_arg/2) is its own address: the defaulty case keeps the if-then-else.
Out is the callee's outcome Out0 as a call site that reads CallerWords reads it. An outcome that does not return passes unchanged.
res_result/5, store_res_result/4 and call_outcome_result/5 relate an operation's Res, or a callee's outcome, to the instruction's Result.
and rets_env(+Res, +Xs, +Env0, -Env): Env is Env0 with the returned word X, or words Xs, bound as the call site's Res reads them.
X is the IR value V read at class K, which takes its low bits(K) bits. value_x_/5 indexes on the value. A symbol the module does not define is ptr(0, ext(Name)) in filc mode; in plain mode (which the validator rejects) the read fails.
Flight's two components are read independently from the old environment. Projecting an address takes its low 64 bits; projecting a lower copies capability identity without inspecting it or its address.
Operations
Res is val(X), ub(Why) or trap(Why). Op is an IR term (ir.pl). Commit before integer dispatch: float bits must never get CLP(Z) arithmetic, even if a caller asks for a different result on backtracking.
as op_res/7, for Op of Kind. Loads and allocs use the memory; the rest is arithmetic.
a check whose access_res/7 is Res0 yields P, proven, or traps.
B is the address A plus the constant Off.
Res is the result of a load of type T at class K. A load reads Size bytes and extends them as T names; load(l) takes them as they are.
load(p) exists in filc mode only. It reads the word and the capability the last store(p, ...) left there, none if there was none.
Execute the supplied pointer-access protocol. Its local state keeps the aux word separate from the resolved lower and primary address; only the completed load publishes a pointer. Aux contains abstract capability identities, not native boxes, so resolution is identity.
The interpreter has no GC, aux allocation or asynchronous frees. Ensure/barrier/reload are therefore abstract identities, not a claim that native helpers cannot exit or fail. The observable writes still execute in list order: lower first, then primary bytes, without another bounds check after ensure-aux. Regions and Next are carried opaquely.
Res is val(U), U the Size bytes at the address in Args, or why there is none.
A is the address of the access value A0 and Res is ok when a Size-byte read there may go ahead. Fil-C checks the capability; plain mode checks the region when it reads.
Res is the result of add or sub (Op) of class K on Xs. Pointer arithmetic keeps the capability.
Res is the result of the arithmetic Op of class K on Xs; add and sub are integer here (additive_res/4). ptoi drops the capability; itop has none.
Res is val of Expr, or ub when the divisor Y is zero. An unknown Y gives both cases as solutions; a known one takes the fast path.
x86 idiv traps on both a zero divisor and the one quotient that overflows, so both are undefined here. Known operands take the fast path; otherwise the three cases are disjoint constraints.
The shift count is taken modulo the class width.
B is 1 when X Cond Y holds at class K, else 0.
S is the two's-complement reading of U at class K.
S is the two's-complement reading of the low bits of U, for a field of modulus M with sign threshold H. The first clause is the fast path for a known U; the cut commits to it, and the second clause states the same relation with constraints.
S is the low bits of X that T names, sign- or zero-extended.
Memory: mem(Bytes, Regions, Next, Aux)
Each region(Base, End, Kind, Life) is shared by every capability with that Base. Only free changes a Fil-C object's bounds, monotonically to empty. Freed regions remain so zero-sized live objects and double frees are distinguishable. No reclamation or address reuse is modeled.
Aux is used in filc mode only: it maps an 8-aligned address to the capability a store(p, ...) left there. An integer store leaves it alone, as Fil-C's aux array does.
the pinned runtime's free_with_checks, object_for_deallocate and free_impl, for objects this interpreter owns. ext(_) has a placeholder address, not a known zero; it stays unsupported. Public run/5 also accepts integer p arguments: these have no capability.
Null is a no-op even with an object's lower. Otherwise kind/address validation precedes the FREE test, as object_for_deallocate precedes free_impl. READONLY alone does not prevent deallocation of a heap object.
capabilities refer to registered identities. An injected unknown base is outside the interpreter domain, not authority for the live object that happens to contain its address.
Res is val(U), U the little-endian value of the Size bytes at A, or ub(...). In plain mode an access outside every live region is undefined. In filc mode the access was checked against its capability already. Mem is Mem0 with any unwritten byte read now made a fresh variable (plain mode).
Mem is Mem0 with X written at Addr as Width, when Res is ok.
Mem is Mem0 after a checked store with result Res.
access_res(+Mem, +A, +Cap, +Size, +Kind, +Align, -Res): Fil-C's access check, Res ok or trap(Why). Cap is none, obj(Base) for a writable object, ro(Base) for read-only data, fn(F) for a function object (zero size, so every access fails the bounds check) or ext(Name) for a symbol defined outside the module, which the interpreter cannot follow. Cap must be known: an unknown capability (an unknown p argument) raises an instantiation error, as an unknown address does. An unregistered Base is outside the interpreter's domain.
the access [A, A+Size) lies inside one live region. A and the regions are integers here, so the if-then-else in the callers is sound. The cut commits to the first such region.
Xs are the bytes at A, A+1, ... in Bytes0; Bytes is Bytes0 with each unwritten byte among them bound. An unwritten byte is unknown in plain mode and zero in filc mode, since Fil-C allocations are zeroed.
Bytes is Bytes0 with the bytes Xs at A, A+1, ...
Base is a new region of Size bytes in Mem. Allocations are aligned (Fil-C's to 16), with Fil-C bounds rounded to 16 as prepare_allocate_object does (zero stays zero). A 16-byte gap separates distinct, never-reused identities.
initial_memory(+Mode, +M, -Globals, -Mem): Mem holds every data definition, each in its own region, with its bytes. Globals maps a name to its address, or in filc mode to a pointer value: data objects are 16-aligned with their size rounded up to 8, as Fil-C's are, and each function gets an address and a fn capability.
Globals and Rs add to Globals0 and Rs0 the address and region of Item placed at the next address from A0 that its alignment allows; a function takes no space.
Bytes (and in filc mode Aux) add the bytes (and capabilities) of Item.
place Item at the next 16-aligned address from A0.
Item written at At0; At is the address after it. Data items are IR terms (ir.pl); the cut commits to the pointer item before the clause for every other item.
Size is Size0 plus Item's size. The cut commits to a string before the clause for any other item of width b (a constant).
Bs are the bytes of the data Item, one per character of a string. The cut commits to a string, as in item_size/3.
Printing
Text is the atom that prints Outcome: its integer return value, or just the kind of a pointer, unknown or tuple result. A returned value is an integer, an unknown (a variable, possibly constrained) or ptr(Addr, Cap): a defaulty term, so ret_text/2 tests it.