Repository navigation
IR semantics
What a Lamina program means. This page is normative: where it and an implementation disagree, one of the two is a bug, and the clause number says which claim is at issue.
It is not a tutorial and not an instruction list. The IR reference gives the syntax; this page gives the behaviour that syntax denotes. The reader it is written for is someone adding a backend or depending on the IR's behaviour from a frontend.
Clauses are numbered A1, M3 and so on. A test may cite one. Where a testcase in the
testcases/ directory already pins a behaviour, the clause names the file.
A backend either implements an operation to the semantics below or refuses the module at compile time with a message naming the operation. Silently computing something else is never conforming. Several operations are implemented on some targets and refused on others; each clause says which, and the lists are facts about the current implementation, not promises.
Four targets can be executed on the machine these clauses were checked on: x86_64 Linux and i686 Linux natively, s390x Linux under qemu, and wasm32 under wasmtime. Everything else is checked by compilation only. A clause marked unverified was read out of the implementation but not run.
V1. A local name is a mutable, function-scoped slot with one immutable type. Reading it reads its most recent assignment on the executed path. A name identifies a slot, never a computed value: a slot's type may be keyed by its name, but constants, aliases, expressions and pointer facts may not.
V2. Assigning a name again is allowed. Assigning it at a different type is a validation error:
duplicate definition of '%x' in '@main': first defined as i64 in block 'entry'
instruction 1, redefined as i32 in block 'entry' instruction 2 (a value may be
reassigned, but not with a different type)
V3. Every reachable read must be definitely assigned. A definition somewhere in the function is not enough: the assignment must reach the read on every path. Verified: a name assigned on one arm of a branch and read after the join is refused with
use of '%x' in block 'c' of '@f' is not assigned on every path to it
V4. There is no phi. A value that joins from several edges is assigned on each
incoming edge, with copy.T where an exact transfer is wanted. Writing phi is a parse
error naming that replacement.
V5. There is no undef, no poison and no freeze. Every operation below either
produces a value, traps, or is refused at compile time. No value defers its meaning to a
later use. The whole tower exists to license transformations Lamina does not perform;
Plan/philosophy.md gives the reasoning.
V6. There are no address spaces and one ptr type.
A1. add, sub and mul wrap modulo 2^B, where B is the width of the type.
This holds at every width and does not depend on whether the type is signed. Verified on
x86_64 and s390x: add.i64 9223372036854775807, 1 is i64::MIN, mul.i8 100, 3 is
44, sub.u8 0, 1 is 255.
A2. Signedness comes from the type and from nowhere else. The types are
i8 i16 i32 i64 i128 and u8 u16 u32 u64 u128, plus bool and ptr. There is no
signed/unsigned variant of an opcode: div.i32 is a signed division and div.u32 is an
unsigned one.
A3. The operations that read signedness are div, rem, shr, the four ordered
comparisons lt le gt ge, and extend. add sub mul and or xor shl and the two
equality comparisons do not: their result bits are the same under either reading.
A4. extend.<source>.<target> widens. The source type decides: a signed source
sign-extends, an unsigned or bool source zero-extends. bool is one bit wide, so
extend.bool.i64 yields 0 or 1. Extending to the same width is a parse error pointing
at bitcast; narrowing is a parse error pointing at trunc.
A5. trunc.<source>.<target> narrows by discarding the high bits.
A6. bitcast.<source>.<target> reinterprets the bits of a value at a type of the
same width and changes nothing about them.
A7. add.ovf.T, sub.ovf.T and mul.ovf.T report whether the matching wrapping
operation overflowed. The result is a single bool, not a pair, and not the arithmetic
result: the value comes from the ordinary add.T next to it. A frontend that wants both
writes both.
A8. The question .ovf answers is read from T. A signed type asks about
two's-complement overflow; an unsigned type asks about carry or borrow.
A9. .ovf applies to add, sub and mul only, and to integer types only.
i128 and u128 are refused, as is any 64-bit type on a target with 32-bit integer
registers: in both cases the value lives in a register pair and no backend reports the
overflow of a pair as a whole.
A10. .ovf is implemented on x86_64 and s390x. Every other backend refuses the
module. This is a conformance level, not a semantic variation: a program using .ovf
does not compile elsewhere rather than computing a different answer. Verified by
compilation on twelve targets. The refusal names the backend doing the refusing and the
backends that implement it, so it agrees with this list:
checked arithmetic ('<op>.ovf') is not supported by the AArch64 backend;
it is implemented for x86_64 and s390x
On a 32-bit target the refusal comes earlier, from the lowering, and cites A9's
register-pair rule instead: add.ovf.i64 on a 32-bit target: the value is held in a register pair and no backend reports the overflow of the pair as a whole. Pinned by
checked_arithmetic.lamina.
A11. A shift count has the same width as the value being shifted. Signedness is
free: shl.i64 %x, %c with %c : u64 is accepted and runs. A count of a different
width is a validation error:
the right operand of '%s = shl.i64 %x, %c' in block 'entry' of '@main' is '%c', which
has type i32, but the instruction states i64
Hint: both operands take the instruction's type, a shift count included; convert '%c'
to i64 first
The same rule covers every operand an instruction states a type for, not shifts alone:
both operands of a binary or compare, the operand of a unary, the two arms of a
select, the stored value of a store, an atomic_store or an atomic_binary, and
the expected and desired values of an atomic_cmpxchg. Those positions get a hint
reading the value an instruction names takes the instruction's type. A vector operand
is the same rule over the lane type and the lane count — a <4 x i32> does not stand
where <2 x i64> is stated, and neither does a scalar — with the hint an operand of a vector operation has the instruction's lane type and lane count.
The one deliberate exception is a vector shift or rotate, whose count may be a
scalar: shl.<2 x i64> %v, %c with %c : i64 is accepted.
A12. At run time the count is masked with width - 1. shl.i8 %x, %c shifts by
%c & 7. This is the rule on every backend, including the narrow widths where the
hardware would mask differently: x86 masks a shift count to 5 or 6 bits, so the compiler
emits an explicit mask for i8 and i16 rather than letting the hardware answer.
Verified on x86_64 and s390x, which agree at every width: with %c equal to 9, 17 or
−1, shl.i8 1, %c gives 2, 2 and −128.
A13. A shift count written as a literal that is out of range is a compile error, not a masked shift:
shl.i8 shifts by 8, which is out of range for a 8-bit operand
Hint: A constant count must lie in 0..8; only a count computed at run time is
masked with 7
A negative literal is refused the same way. Both halves of this are deliberate. A count the compiler can see to be out of range is almost always a bug in the frontend, and refusing it costs nothing; a count only known at run time has to do something, and masking is what every target's hardware does.
A14. The refusal in A13 reaches a literal operand, in the parser. A count that is
constant but computed — %c = add.i8 4, 5 then shl.i8 1, %c — is not refused, and
masks per A12. Verified: that program prints 2 at every optimisation level. The rule is
syntactic, and a frontend must not rely on constant folding to catch an out-of-range
count for it.
A15. shr is one opcode. It is arithmetic on a signed type and logical on an
unsigned one, per A3.
A16. rotl and rotr take the count modulo the width. rotl.i8 1, 9 is
rotl.i8 1, 1. This is why rotates are excluded from A13: for a rotate every count is
meaningful, so an out-of-range literal is not evidence of a mistake. Verified on x86_64
and s390x.
A17. rotl and rotr are implemented on x86_64, i686, aarch64, armv7, Cortex-M,
RISC-V 64, s390x and PowerPC64. loongarch64, mips64, wasm, PTX and AMDGPU refuse
them, as does RISC-V 32 (RISC-V32 backend does not support integer rotates yet).
Verified by compiling a rotate with a run-time count: a rotl.i64 on RISC-V 32 does
compile, because a 64-bit value there is a register pair synthesised by the lowering
rather than a backend rotate, but rotl.i32 is refused. Pinned by
bit_intrinsics.lamina and i128_bit_intrinsics.lamina.
T1. A trap stops execution at the offending instruction. It is a fault, and the program does not continue past it.
T2. The trapping conditions are:
- integer division or remainder by zero, signed or unsigned;
- signed division or remainder of the type's minimum value by
-1; - reaching
unreachable; - dereferencing a null pointer, which is architectural rather than a check the compiler emits.
T3. div.i64 10, 0 and div.i64 -9223372036854775808, -1 both trap. Verified at
every width on x86_64 and s390x, for div and rem, signed and unsigned.
T4. On a target whose divide does not fault, the backend emits the comparison itself and branches to a trapping instruction. The sequences differ:
| target | divide by zero | MIN / -1 |
trap instruction |
|---|---|---|---|
| x86_64 | hardware #DE
|
hardware #DE at 64 bits; explicit check at narrower widths |
ud2, or the fault |
| i686 | hardware #DE
|
ud2 at narrow widths, see T8 |
— |
| aarch64 |
cbnz guard |
cmn/cmp guard |
udf #0 |
| RISC-V |
bnez guard |
bne guards |
.word 0 |
| s390x |
ltgr/brcl guard |
cgr/brcl guards |
j .+2, a branch into the middle of its own encoding |
| PowerPC64 |
td/tdi
|
td after a compare |
td |
| mips64 |
bne guard |
bne guards |
teq $0, $0 |
| loongarch64 |
bnez guard |
bne guards |
break 0 |
| armv7, Cortex-M |
cmp guard |
cmn/cmp guards |
udf #0 |
| wasm | the wasm trap | explicit check | unreachable |
T5. The signal a trap raises is target-defined, and on one target it is not even
uniform across widths. x86_64 raises SIGFPE where the hardware divide faults — every
divide by zero, and MIN / -1 at 64 bits — but the explicit MIN / -1 check at i8,
i16 and i32 reaches T4's ud2 and raises SIGILL. s390x, aarch64, RISC-V,
loongarch64 and ARM raise SIGILL; PowerPC64 raises SIGTRAP; wasm raises a
RuntimeError. Verified: div.i64 10, 0 exits with signal 8 on x86_64 and signal 4
under qemu-s390x, while div.i32 -2147483648, -1 exits with signal 4 on x86_64.
A program must not depend on which signal it gets. The guarantee is that execution
stops there.
T6. A division by zero the compiler can see is not a compile error. div.i64 10, 0 compiles and traps at run time, at --opt-level 0 and at --opt-level 2.
Constant folding declines to fold any trapping case rather than removing it, and
dead-code elimination keeps an instruction that may trap. This is the opposite choice from A13, and deliberately so: a
shift by a bad constant has a defined answer the program probably did not want, while a
division by a constant zero has no answer at all and the trap is the behaviour.
T7. unreachable is a terminator and it traps. It is not undefined behaviour and no
pass may assume the block is dead. Verified on x86_64 and s390x by a program written for
the purpose: it writes a byte, reaches unreachable, and dies with SIGILL after that
output has been written.
Nothing in testcases/ pins the trap. unreachable_terminator.lamina is the only
testcase containing the instruction, and it does not reach it: the unreachable sits in
@abort_path, called from a block guarded by a branch that is never taken, so the
program exits 0 and its expected output is three ordinary lines. What that testcase pins
is the other half of this clause — that no pass deletes a block containing
unreachable. A testcase for the trap itself is still missing.
T8. On i686 a narrow signed division is widened to 32 bits and divided with idivl,
which does not fault on MIN / -1 at that width, so the backend emits the check itself:
cmpl against −1, cmpl against the type's minimum, then ud2. Verified by execution:
div.i8 -128, -1 traps on i686, x86_64 and s390x alike. Until e3133eaa it returned
−128 on i686, which is why T2 names the trap rather than leaving it to the hardware.
T9. 128-bit division and remainder call into builtins/, which do not fault. The
lowering synthesises the trap: it computes a predicate that is zero exactly in the
trapping case and divides by it, for the fault alone.
F1. f32 and f64 are IEEE 754 binary32 and binary64. Arithmetic is the plain
hardware operation. There are no fast-math flags, no reassociation, no contraction and
no fma. There is no f16 and no f128.
F2. Floating-point exception flags and rounding modes are not modelled. Nothing in
the compiler reads or writes MXCSR or FPCR. A program cannot observe them through
the IR.
F3. eq le lt gt ge on floats are ordered: each is false when either operand is
NaN. ne is unordered-true: it is true when either operand is NaN. There is no way
to spell the other four combinations, and no ord/uno predicate. Pinned by
float_nan_comparisons.lamina.
F4. neg.f32/neg.f64 flip the sign bit, including on NaN and on zero.
F5. There are no inf or nan literals. The only ways to obtain one are to compute
it, as div.f64 0.0, 0.0, or to bitcast an integer pattern.
F6. A float literal in an f32 context is rounded once, from the decimal text
straight to f32. It is not parsed as f64 and then narrowed, so there is no double
rounding to go wrong. This is the same single-rounding contract F12 states for
inttofp.
The difference is observable. A decimal placed just above an f32 midpoint but within
half an f64 ulp of it lands exactly on the midpoint when parsed as f64, and
ties-to-even then rounds it down — one bit below the correctly rounded answer:
| decimal | correct f32
|
if routed through f64
|
compiler |
|---|---|---|---|
1.5000000596046448031462006156289135105907917022705078125 |
0x3FC00001 |
0x3FC00000 |
0x3FC00001 |
1.142222225666046170333700615628913510590791702270507812500 |
0x3F923457 |
0x3F923456 |
0x3F923457 |
Verified on both literal paths: an instruction operand (add.f32 <lit>, 0.0) and a
global initialiser (global $g: f32 = <lit>). Both round once, and both agree under the
nightly build.
F7. fptoint.<float>.<int> saturates and never traps. It is defined for every
input, and the definition does not depend on the hardware instruction a backend uses.
- NaN gives 0.
- Otherwise the value is truncated toward zero.
- A signed target clamps to the target type's minimum and maximum.
+infgives the maximum,-infthe minimum. - An unsigned target clamps to 0 and the maximum. Every negative value, including
-0.0,-0.5and-inf, gives 0. -
-0.0gives 0. - The clamp is to the target type, not to a register width:
fptoint.f32.i8 128.0is 127, not 128.
F8. This is where Lamina deliberately differs from libgcc, which leaves NaN and
out-of-range inputs undefined. builtins/README.md states the divergence for the
128-bit routines. It is the same contract inline and in the builtins.
F9. F7 was checked by execution over 336 conversions — every combination of f32
and f64 source with the eight integer targets, across zero, both signed zeros, values
either side of each boundary, both infinities and a NaN — against an independent
saturating oracle. x86_64 and s390x produce byte-identical output and both match the
oracle at every point. Pinned by fptoint_signed.lamina and fptoint_unsigned.lamina.
F10. The conversions are not available everywhere. Verified by compiling a function whose operand is a parameter — a constant operand folds and reaches no backend, so a refusal only shows on a run-time value:
| target | refusal |
|---|---|
| i686 | float-to-int, every result of 32 bits or narrower — i8 i16 i32 u8 u16 u32: i686 float to integer conversion is not implemented: x87 reports an out-of-range or NaN operand as the integer indefinite, not as the saturating result the contract names
|
| RISC-V 32 | float-to-int, every result of 32 bits or narrower: RV32 float to integer conversion is not supported
|
| loongarch64 | the unsigned float-to-int form, and unsigned 64-bit int-to-float |
| Cortex-M |
all floating point, not f64 alone; see below |
| PTX, AMDGPU | nothing reaches the conversion: both stop at GPU code emission: functions must be marked as kernels
|
x86_64, aarch64, RISC-V 64, s390x, armv7, mips64, PowerPC64 and wasm accept all four directions.
Cortex-M refuses f32 as well as f64, and refuses it at the function boundary before
the conversion is reached:
thumbv7m does not implement floating point: `a parameter of @f` on f32
(this backend emits no VFP instructions and no soft-float library calls)
The f64 form gets the same message ending (no Cortex-M FPU is double precision).
There is no floating point on this target at all, single precision included.
The i686 and RISC-V 32 rows are float-to-int only. Both targets accept every
inttofp form whose source can be named on a 32-bit target: i8 i16 i32 u8 u16 u32
convert inline, i64 and u64 route to builtins, and a 128-bit source is refused
earlier by P6's rule rather than by the conversion. Swept over all 32 source/target
combinations on each, there is no int-to-float refusal left on either.
The float-to-int rows are narrower than they look, and the difference matters to a
frontend. fptoint.f64.i32 and fptoint.f32.i32 are refused on both; fptoint.f64.i64
and fptoint.f32.i64 compile on both, and route to __fixdfdi and __fixsfdi
rather than to an instruction. builtins/ provides those helpers. Whether the Lamina
builtin or a host libgcc wins at link on those two targets has not been checked here —
neither target can be linked on the development host — so whether the wide form on i686
and RISC-V 32 satisfies F7 is unverified. Treat it as an open question rather than
as a guarantee.
i686's message is the clearest statement of the rule in the tree for the forms it covers: it refuses rather than emit a sequence that would not satisfy F7.
F11. Unverified. loongarch64 fixes up NaN but relies on ftintrz to saturate at
both ends, where every other backend either clamps explicitly or uses an instruction
documented in-tree as saturating. Whether it satisfies F7 for -inf was not checked:
loongarch64 cannot be executed here.
F12. inttofp.<int>.<float> rounds to nearest, ties to even, in a single
rounding. Signedness comes from the source type.
F13. The hard cases are the ones where converting through f64 first would round
twice: u64 to f32, and any 128-bit source. x86_64 has no unsigned 64-bit convert, so
it halves the value and keeps the lost bit as a sticky bit in bit 0 before converting
once. The 128-bit builtins normalise the magnitude, keep the top 64 bits, and OR
everything below into bit 0, so the single hardware convert sees the sticky bit below
the rounding position.
F14. F12 was checked by execution over 463 values per width — the boundary patterns
that distinguish single from double rounding, plus random 64-bit values — round-tripped
through f32 and f64 and compared against a round-to-nearest-ties-to-even oracle
computed in exact integer arithmetic. x86_64 and s390x agree with the oracle and with
each other at every point. Pinned by inttofp_signed.lamina and
inttofp_unsigned.lamina, whose expected values include u64::MAX rounding up to 2^64
in both formats.
F15. F12 is scoped to sources of at most 64 bits in one respect: a 128-bit source
can overflow. u128::MAX as f32 is +inf, as IEEE requires.
F16. Unverified. RISC-V emits fcvt.{s,d}.{l,lu} with no rounding-mode suffix,
so the conversion uses the dynamic frm rather than a mode fixed in the encoding. Under
the default frm this is F12. A program that changes frm behind the compiler's back is
outside the model.
M1. stackalloc.<type> reserves storage for one value of that type in the current
frame and yields a ptr. The pointer is never null. The storage lives until the
function returns and is never freed earlier. There are no lifetime markers.
M2. stackalloc allocates one slot per instruction, not one per execution. A
stackalloc in a loop body yields the same address on every iteration. There is no
variable-length allocation: the size comes from the static type.
M3. There is no heap operation. heapalloc, heapfree, alloc and dealloc are
parse errors naming call @malloc and call @free as the replacement. Allocation is a
call, and the compiler reasons about none of it. stackalloc stays because frame layout
is the compiler's job and mem2reg and SROA both rewrite it.
M4. stackalloc guarantees 8-byte alignment unless align n is written. It does
not guarantee the natural alignment of the allocated type. Verified, and the two
backends disagree in the observable way: with a one-byte slot allocated before it,
stackalloc.i128 lands 16-byte aligned on x86_64 and 8-byte aligned on s390x. A program
that needs the natural alignment of an over-aligned type must ask for it.
M5. align n on stackalloc must be a power of two, and n > 16 is a compile
error — frames are 16-byte aligned and frame realignment is not implemented.
M6. load.<type> <ptr> and store.<type> <ptr>, <value> access memory of that
type. The pointer must not be null; a null dereference traps.
M7. align n on a load or store is a promise the program makes about the
address, not a hint and not a request. The usual use is to state an alignment lower
than natural, saying the address may be misaligned.
M8. When align is absent, the compiler derives one: the minimum of the type's
natural alignment and what it can prove about the address. It proves alignment forward
through getfieldptr (by the field offset), getelem (by the element size and what it
knows divides the index), pointer copies, and globals (by the declared @align). A
pointer it cannot bound — a parameter, a loaded pointer, a call result — is treated as
sufficiently aligned, which is the assumption C makes of a pointer it is handed. The
derived value is capped at natural alignment, so the derivation can only report what the
access needs, never a stronger claim.
M9. A stated alignment larger than the compiler can prove is trusted unconditionally. Nothing intersects it with the derived value. The only diagnostic is for a value above 128.
M10. An access whose address does not actually meet the alignment in force is undefined. Nothing checks alignment at run time. What happens is target-defined: some targets execute it correctly, some fault.
M11. A backend whose memory instructions fault on an unaligned address refuses a stated alignment below the natural one, rather than misaligning silently:
RISC-V cannot issue a store of i32 at alignment 1 (natural alignment is 4);
its memory instructions fault on an unaligned address (function 'main')
Verified by compilation. RISC-V (32 and 64), loongarch64, armv7, PTX, AMDGPU and
Cortex-M refuse; the last of these in its own words, per M12. x86_64, s390x, aarch64,
PowerPC64 (both byte orders) and i686 accept, correctly: their loads handle unaligned
addresses. mips64 accepts and emits the unaligned forms usw/ulw (assembly only).
wasm accepts and its memory model has no alignment requirement. Pinned by
load_store_alignment.lamina, which round-trips an i32 at align 1 on a byte-offset
address.
M12. Cortex-M refuses a stated sub-natural alignment, by name and with the reason, which is why it appears in M11's refusal list rather than as an exception to it:
thumbv7m takes a UsageFault on an unaligned access whenever CCR.UNALIGN_TRP is set,
and this `store` of i32 declares 1-byte alignment for a 4-byte value
thumbv6m refuses the same access, citing a HardFault rather than CCR.UNALIGN_TRP,
since that core has no unaligned support to enable. Cortex-M cannot be executed here,
but the refusal happens before code generation, so compiling is conclusive.
M13. volatile load and volatile store must happen exactly once, must not be
removed, and must not be reordered with other volatile accesses.
M14. Alignment on a 128-bit load or store is refused, not ignored: the value moves one word at a time, so a stated alignment would not describe the access performed.
M15. The pointer model is addresses as numbers. There are no provenance rules, no
noalias, no restrict and no inbounds.
M16. ptrtoint.<int> <ptr> and inttoptr.<int> <value> convert in both directions
and lower to a plain integer conversion. Masking the low bits of a stack address is an
intended idiom, pinned by stack_align.lamina.
M17. Alias analysis is block-local and assumes only allocation identity: two
accesses that are each provably inside their own distinct frame slot do not alias.
Everything else may alias, including a global against a stack slot, and two distinct
globals against each other. It does not use provenance, and because it treats a
ptrtoint/inttoptr round trip as an unknown address it does not need to.
M18. getelem.<element-type> <ptr>, <index> computes base + index * sizeof(element).
The index is a run-time value. There is no bounds information on the instruction and
an out-of-range index is undefined; the access goes wherever the address lands.
M19. getfieldptr requires a struct layout as its type suffix, because the field
offset depends on it:
getfieldptr needs its struct layout as a suffix, because the field offset depends on it
Hint: Did you mean 'getfieldptr.<struct-type> <ptr>, <index>', e.g.
'getfieldptr.!Pair %p, 1'?
The suffix may be a named type !Pair or an inline struct { a: i8, b: i32 }; both are
accepted. A suffix that does not resolve to a struct is a validation error naming the
type found.
M20. A field index past the end of the struct is a compile error, unlike M18:
getfieldptr in '@main' takes field 5, but its struct has 2 fields
M21. Struct layout is C's. Each field of an ordinary struct is rounded up to its own
alignment; a packed struct places each field at the running sum of the preceding sizes
and has alignment 1. Pinned by packed_struct_layout.lamina, which is cross-checked
against C offsetof and sizeof.
M22. The boundary rule. An aggregate is passed and returned as the address of its storage, so a call site or a return must state the aggregate type:
%sum = call @sum_pair(!Pair %pair)
ret.!Pair %p
That annotation is what separates an aggregate from a plain pointer, which the operand's
own type cannot do. Passing a bare ptr where an aggregate is declared is an error:
argument 1 of call to '@s' in '@main' (block 'entry' instruction 4) must be !P
for parameter '%p', but %q is a plain ptr
Hint: An aggregate argument is the address of its storage, so the call site must
name the type: write '!P %q'
The reverse is also an error. Pinned by aggregate_params.lamina,
aggregate_sret_return.lamina, aggregate_mixed_args.lamina and
aggregate_memory_params.lamina.
M23. An aggregate crossing a boundary must be a non-empty integer aggregate. A float field is refused, and so is an aggregate of zero bytes. The messages name the value and the function:
%p of @s has a float field; only integer aggregates cross a boundary so far
%p of @s is empty; an aggregate crossing a boundary holds at least one byte
The empty case is reachable through [0 x i8]; a struct { } is refused earlier by the
parser.
There is no size limit. A 512-byte aggregate — struct { a: [64 x i64] } — passes
as an argument and comes back as a return on x86_64, and round-trips its contents
correctly. Do not assume a register-return budget: the compiler enforces none.
M24. Aggregates by value are refused by loongarch64, wasm, PTX and AMDGPU, each naming itself:
LoongArch64 does not yet pass aggregates by value, as @s does
Wasm32 does not yet pass aggregates by value, as @s does
PTX does not yet pass aggregates by value, as @s does
AMDGPU does not yet pass aggregates by value, as @s does
Verified by compilation, for both arguments and returns. x86_64, aarch64, s390x, RISC-V 64, RISC-V 32, PowerPC64, mips64, armv7, i686 and Cortex-M accept them.
M25. A vector type never crosses a boundary and never has a memory layout; see
S4.
C1. The operations are atomic_load, atomic_store, the read-modify-writes
atomic_add atomic_sub atomic_and atomic_or atomic_xor atomic_exchange,
atomic_cmpxchg, and fence. Each takes a memory ordering as its last operand.
C2. The orderings are relaxed acquire release acqrel seqcst. Which an operation
accepts:
| operation | relaxed | acquire | release | acqrel | seqcst |
|---|---|---|---|---|---|
atomic_load |
yes | yes | no | no | yes |
atomic_store |
yes | no | yes | no | yes |
| read-modify-write | yes | yes | yes | yes | yes |
atomic_cmpxchg success |
yes | yes | yes | yes | yes |
fence |
yes | yes | yes | yes | yes |
atomic_cmpxchg's failure ordering has no row here. What it accepts depends on
the success ordering alongside it, which a one-dimensional row cannot express, so it is
given as a matrix in C3.
Verified by compilation. The refusals read:
atomic_load cannot use release ordering
Hint: Use relaxed, acquire or seqcst
atomic_store cannot use acquire ordering
Hint: Use relaxed, release or seqcst
Pinned by atomic_orderings.lamina.
C3. atomic_cmpxchg carries two orderings, written success first and failure
second, and two rules govern the pair.
The failure ordering is a load, so release and acqrel are refused as a failure
ordering whatever the success ordering is:
atomic_cmpxchg cannot use release failure ordering with seqcst success ordering
Hint: the failure ordering is a load: use relaxed, acquire or seqcst
The failure ordering may also not be stronger than the success ordering, where
strength is the order the orderings are written in above — relaxed, acquire,
release, acqrel, seqcst:
atomic_cmpxchg cannot use seqcst failure ordering with relaxed success ordering
Hint: the failure ordering may not be stronger than the success ordering
Together the two rules give this matrix. All twenty-five combinations were compiled.
| success \ failure | relaxed | acquire | release | acqrel | seqcst |
|---|---|---|---|---|---|
relaxed |
yes | no | no | no | no |
acquire |
yes | yes | no | no | no |
release |
yes | yes | no | no | no |
acqrel |
yes | yes | no | no | no |
seqcst |
yes | yes | no | no | yes |
The cell worth reading twice is the last column: a seqcst failure ordering is
accepted only with a seqcst success ordering. Both refusals are raised in the parser,
before any backend sees the module. atomic_cmpxchg.lamina uses four accepted pairs —
seqcst, seqcst, acquire, relaxed, acqrel, acquire and acquire, acquire — so it
pins the accept side of this matrix and none of the refusals.
C4. A read-modify-write returns the value that was in memory before the
operation. Verified on x86_64 and s390x: against a cell holding 100, atomic_add.i64 %c, 5, seqcst yields 100 and leaves 105.
C5. atomic_cmpxchg likewise returns the value that was in memory before. The
exchange happened exactly when that value equals the expected one; there is no separate
success flag, and the result is a single value, not a pair. Verified: against a cell
holding 7, a cmpxchg expecting 7 returns 7 and stores; the next one expecting 7
returns 9 and does not.
C6. Atomics take an integer or pointer type. bool and ptr are accepted; f32
and f64 are refused. 128-bit atomics are refused.
C7. Atomics are implemented on x86_64, aarch64, RISC-V, s390x and PowerPC64, at
widths 1, 2, 4 and 8 bytes — RISC-V needs the A extension, and 8 bytes only on RV64.
i686, mips64, loongarch64, armv7, Cortex-M, wasm, PTX and AMDGPU refuse them. An
8-byte atomic on a 32-bit target is refused by the lowering before it reaches a backend.
C8. Nothing in the compiler requires an atomic address to be naturally aligned, and
M11's check does not look at atomics. On an LL/SC target a misaligned ldxr or lr.w
faults. Treat an unaligned atomic as undefined. This is a gap rather than a decision;
see the findings.
I1. Four operations reach the outside world. Each produces a result and the parser requires a name for it, so none of them is spelled as a bare statement:
%r = writebyte <value>
%r = write <ptr>, <size>
%r = readbyte
%r = read <ptr>, <size>
A trailing bare name is the equivalent spelling the parser's own hint gives —
writebyte <value>, <name>, readbyte <name>, write <ptr>, <size>, <name>,
read <ptr>, <size>, <name> — and it takes the name without a %. Omitting the result
altogether is a parse error, one per operation:
writebyte needs a result name on the same line
Hint: Write 'writebyte <value>, <name>'
I3 describes what that result is.
The four are kept, against the rule in Plan/philosophy.md that an operation earns its
place only if the compiler must understand it, because they are raw syscalls with no
formatting policy. They are what makes a target with no libc possible at all.
I2. Output goes to file descriptor 1 and input comes from file descriptor 0. There is no descriptor operand.
I3. The result is a count, or one of two sentinels. It is never an errno.
| operation | success | end of input | failure |
|---|---|---|---|
writebyte |
1 |
— | -2 |
write |
bytes written; 0 for size 0 |
— | -2 |
readbyte |
the byte, 0..=255
|
-1 |
-2 |
read |
bytes read; 0 for size 0 |
-1 |
-2 |
Verified on x86_64 and s390x, which agree: writing to a full device and writing to a
closed descriptor both give -2, and reading at end of input gives -1. Note that
read returns -1 at end of input where the POSIX call returns 0.
I4. A NUL byte read by readbyte is 0, not end of input. The sentinel is keyed on
the count, never on the byte. Pinned by readbyte_nul.lamina.
I5. A short write is possible. Every backend issues exactly one syscall or one
library call and maps the result. Nothing loops, and nothing retries on EINTR. A
program that must write all of a buffer loops itself.
I6. The result has no IR type. It is a machine word, which is 32 bits on a 32-bit
target. A frontend must not assume i64.
I7. How these lower is per target and per operating system, and this is what a freestanding program depends on:
| target | mechanism |
|---|---|
| x86_64 Linux, macOS, FreeBSD | direct syscall |
| i686 Linux | direct int $0x80
|
| aarch64 macOS | direct svc #0
|
| aarch64 Linux | call to libc write/read
|
| s390x, RISC-V, PowerPC64, mips64, loongarch64, armv7, Cortex-M | call to libc write/read
|
| wasm32 WASI |
fd_write/fd_read imports, wrapped to the I3 contract |
| wasm non-WASI | imports named write/read/writebyte/readbyte from the host |
So I1's claim holds unconditionally only where the lowering is a raw syscall. On the
other targets a freestanding build emits a call to a write symbol and fails at link,
not at code generation. There is no diagnostic connecting the two.
I8. A target whose operating system has no implementation refuses at code
generation, naming the operation. Verified: --target aarch64_unknown gives
lamina.writebyte has no implementation for Unknown. Pinned by
output_freestanding.lamina, which writes one syscall per byte with no libc.
P1. Endianness is a per-target property. s390x, ppc64 and mips64 are big-endian.
Everything else, including mips64el and ppc64le, is little-endian.
P2. Nothing in the IR lets a program observe endianness except by reinterpreting
memory: storing at one width and reading back at another, or writing a multi-byte buffer
out. There is no byte-order query and no annotation. bswap is a value operation and
does not observe anything.
P3. Because of P2, a testcase that writes raw multi-byte memory has two expected
outputs. io_types.lamina stores an i32 and writes its four bytes; the runner picks
io_types.expected or io_types.big.expected by the target's byte order. Verified: the
program produces 40 e2 01 00 on x86_64 and 00 01 e2 40 under qemu-s390x.
P4. No target has 128-bit integer registers, so wherever a 128-bit value exists at
all it is two 64-bit words. It does not exist everywhere: see P6 for the 32-bit targets,
which refuse it outright rather than split it into four. In memory the low word comes
first on a little-endian target and the high word first on a big-endian one. Verified:
storing (7 << 64) | 3 and reading the two halves back gives 3, 7 on x86_64 and
7, 3 on s390x.
P5. At a function boundary an i128 is a 16-byte integer aggregate, and each
target then applies its own aggregate rule. The convention is not uniform:
| target |
i128 argument and return |
|---|---|
| x86_64 System V | a pair of consecutive general registers if both remain, otherwise entirely on the stack, never split |
| x86_64 Windows | by reference: a pointer to a caller-owned copy, returned through a hidden pointer |
| aarch64 | a register pair, starting at an even register; the skipped register is not backfilled |
| RISC-V 64, PowerPC64 | the next register pair, with no even-register skip |
| s390x | by reference: any aggregate over 8 bytes travels as a pointer |
| 32-bit targets | refused — four registers, and only pairs are split |
Verified by reading the emitted prologue: on x86_64, aarch64 and RISC-V the callee
receives the two words in a register pair; on s390x it receives a pointer and loads
through it. "Two words at a function boundary" describes x86_64, aarch64, RISC-V and
PowerPC64; it does not describe s390x or Windows. Pinned by i128_abi.lamina and
argument_alignment.rs.
P6. i128 is not a usable value type on a 32-bit machine target at all — not
merely at a boundary. A bare local with no call in sight,
%a = add.i128 1, 2
is refused on i686, riscv32, armv7, thumbv6m and thumbv7m:
`%a = add.i128 1, 2` names a 128-bit integer on a 32-bit target: that takes four
registers, and only pairs are split
stackalloc.i128 is refused the same way, with its own reason:
`%q = stackalloc.i128` names a 128-bit integer on a 32-bit target: the slot itself is
sixteen bytes, but no load or store of it can be legalized, because only register pairs
are split
P5's 32-bit targets | refused row is scoped to the ABI; this clause is the wider rule
it is a consequence of. wasm32 is the exception: it is 32-bit but has no register
pairs to legalize into, so a local i128 compiles and computes correctly there
(verified under wasmtime: an i128 carry out of the low word gives the right high
word). wasm32 still refuses i128 at a boundary, and therefore refuses div/rem
too, since those call a helper that takes one.
On the targets where it exists, add sub mul and or xor shl shr rotl rotr, the unary
operations and the conversions are available for i128. div and rem call __divti3
and its family, and the int/float conversions call __floatti* and __fixti*. These
are satisfied by Lamina's own builtins/, written in Lamina IR and compiled for the
target, ahead of any host archive.
P7. i128 arguments and results of callptr are refused: an indirect call carries
no callee signature to pass a 16-byte aggregate by.
P8. The same machinery splits i64 on a target with 32-bit integer registers, so an
i64 is "the wide type" there and gets the same treatment.
P9. The surface is va_start, va_arg.<type>, va_end and va_copy.
P10. va_list is a per-target property, not one layout. It is what the
architecture's own ABI says, which is the point: a va_list built by Lamina has to be
usable by a C library compiled by someone else.
| target | size / alignment | ABI |
|---|---|---|
| x86_64 | 24 / 8 | System V AMD64 §3.5.7 |
| aarch64 | 32 / 8 | AAPCS64 |
| s390x | 32 / 8 | zSeries ELF ABI supplement: struct { long __gpr, __fpr; void *__overflow_arg_area, *__reg_save_area; }
|
| RISC-V 64, PowerPC64, mips64, loongarch64, wasm64 | 8 / 8 | a plain pointer |
| i686, 32-bit ARM, RISC-V 32, wasm32 | 4 / 4 | a plain pointer |
| arx64, RISC-V 128, nvptx64, amdgcn | undefined | no ABI defines one |
An undefined entry is a statement that the ABI names no layout, not an omission.
Two targets depart from their architecture's row, because the OS defines its own:
Win64 and Darwin AArch64 both make va_list a plain pointer. Lamina reserves the
architecture's size on those targets and keeps the pointer at offset 0, so a va_list
handed to C still reads correctly; the bytes past the pointer are unused.
P11. A target is <arch>_<os> with an optional environment: <arch>_<os>_<env>,
where the environment is gnu, musl, eabi, eabihf, none or lamina. A
sub-architecture may replace the architecture: rv64gc, armv7a-neon, ppc64le-power9,
aarch64v8.2.
P12. none selects no libc and no compiler runtime. The two halves fail at
different times, and a freestanding backend author needs both:
-
A compiler-runtime helper is refused at code generation, by name, before anything is emitted:
`__divti3` is a compiler runtime helper that the `none` environment does not provide; define it in the module, or name an implementation with LAMINA_BUILTINS=__divti3=<symbol>The check is keyed on the environment axis and nothing else:
x86_64_linux,_gnu,_musland_laminaall acceptdiv.i128; only_nonerefuses. Verified on x86_64, aarch64, s390x and RISC-V 64. -
A libc symbol still fails at link, with nothing connecting it back to the instruction that wanted it. See I7: a freestanding s390x build of a
writebyteemitsbrasl %r14, writeand the link fails withundefined reference to 'write', while the same program onx86_64_linux_nonelowers to a syscall and runs.
P13. lamina names Lamina's own C library. It parses on x86_64 and aarch64 and
refuses at link, by name, because that library does not exist yet.
S1. A vector type is written <N x T>. [N x T] with brackets is still an array.
S2. T is one of i8 i16 i32 i64, their unsigned forms, f32 and f64. bool,
ptr, i128 and u128 have no lane form.
S3. N * bits(T) must equal a machine vector register width. The widths the type
system admits are 128 and 256. Anything else is refused:
<2 x i32> in load in '@main' is 64 bits, which is no vector register width
Hint: a vector fills one register; widths are 128, 256 bits, so write
<4 x i32> instead of splitting the value yourself
S4. A vector names a value held in one register and never has a memory layout.
It may appear as an instruction's type suffix and nowhere else: not as a parameter type,
not as a return type, not as a global, not as a struct field, not in stackalloc.
Declare the memory as [N x T] and read it with load.<N x T>.
S5. The operations are the element-wise add sub mul and or xor, the shifts
shl shr with either a scalar count or a same-shape vector count, splat,
extractlane, insertlane, shuffle with a compile-time constant lane mask, and
load/store at a vector type. div, rem, rotl and rotr have no vector form;
the error says to extract the lanes and operate on them as scalars. There are no vector
comparisons, reductions, masks or selects.
S6. 256-bit vectors are refused everywhere. They parse and they type-check; no
backend lowers them. Verified across every target, and on x86_64 at every --cpu-level:
x86_64 V256 is not implemented: the backend emits only 128-bit SSE forms,
at every CPU level
The type system and code generation disagree about what the IR admits; S3 describes the type system and S6 describes what you can compile.
S7. 128-bit vectors lower to real SIMD on x86_64 (SSE2), aarch64 (NEON),
wasm (simd128) and RISC-V with the V extension — rv64gcv_linux, not
riscv64_linux, whose ISA string lacks V:
V extension is required for vectors on rv64imafd
No backend scalarizes. s390x, mips64, loongarch64, PowerPC64, armv7, Cortex-M and
i686 refuse by name. Verified by compilation. Pinned by vector_operations.lamina.
S8. Vector memory access has no alignment requirement. x86_64 uses movdqu for every
load and store through memory, wasm emits align=1, and aarch64 uses a plain ldr q.
The rule is in Plan/philosophy.md: an operation earns a place only if the compiler
must understand it. If it is identical to call @name(...), it is sugar and it goes.
That reasoning is not repeated here.
Nothing disappears without a message naming its replacement. Every removed spelling still parses and errors with what to use instead.
N1. No phi. Assign the name on each incoming edge; see V4.
N2. No print. It embedded formatting policy in the compiler.
Unknown instruction opcode 'print'
Hint: Did you mean 'writebyte <value>' for one byte, 'write <ptr>, <size>' for
raw bytes, or a call to a printf-style @extern for formatted output?
N3. No heapalloc, heapfree, memcpy, memmove, memset, alloc, dealloc or
writeptr. Each lowered to exactly one call, no pass reasoned about any of them, and
none was ever compiler-generated. Each error names the call to write instead. memcpy
can come back as an intrinsic when the optimizer inlines small copies or loop idiom
recognition creates them, and not before.
N4. No @no_red_zone:
@no_red_zone was removed
Hint: Delete it. Nothing replaces it: the x86_64 backend never uses the red zone,
and other targets have none
N5. @optimize_speed, @optimize_size, @debug, @strip and @target_triple are
removed in favour of driver flags, each named in its message.
N6. zext/sext are extend; sitofp/uitofp are inttofp; fptosi/fptoui
are fptoint; fpext/fptrunc are fpcast; getelementptr is getelem; getfield
is getfieldptr.
N7. No undef, poison or freeze; see V5. No address spaces until a GPU backend
needs them. No opaque-pointer migration, because there has only ever been one ptr.
N8. The function annotations that exist are @kernel @inline @export @extern @noreturn @noinline @cold @hot @pure @internal @private @hidden @protected @weak @section @align @naked. Anything else is a parse error listing them.
N9. @extern declares a symbol defined elsewhere. A function carrying it may not
have a body:
@extern function 'f' has a body
Hint: @extern declares a symbol defined elsewhere; drop the body to declare it,
or drop @extern to define it here
lamina · ras · weld · lamina-web