huntedbytheirs/libvct-spec
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs: add libVCT public specification set (000-015)

Browse Source
This commit is contained in:
huntedbytheirs
2026-09-13 15:56:53 -04:00
parent 591fdf3107
commit 765c91dabc
16 changed files with 3769 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/006-vir.md
+298
View File
@@ -0,0 +1,298 @@
# 006 — VIR
- **Status:** Draft
- **Normative language:** `MUST`, `MUST NOT`, `SHOULD`, `SHOULD NOT`, and `MAY` are to be
interpreted as described in RFC 2119.
## 1. Purpose
VIR (Vox IR) is the low-level instruction IR of libVCT. It is an SSA form over a control-flow
graph. Every optimization above the backends operates on VIR, and both the C backend and the LLVM
backend consume VIR. Lowering produces it (see [005 — Lowering](005-lowering.md)); the VIR
optimizer transforms it (see [007 — VIR Optimizer](007-vir-optimizer.md)).
VIR is internal and is intended to be machine-generated. A textual form exists for tools,
dumps, and round-trip tests, but it is not a supported authoring surface: programs are built
through the HIR builder or as fixtures for tests (see [003 — HIR](003-hir.md),
[012 — Testing](012-testing.md)).
## 2. Scope
This file specifies the VIR SSA/CFG model, the VIR type system, the instruction set, and the
well-formedness invariants every VIR module must satisfy. It does not specify how VIR is produced
(see [005 — Lowering](005-lowering.md)), how it is optimized (see
[007 — VIR Optimizer](007-vir-optimizer.md)), or how it is emitted (see
[008 — C Backend](008-c-backend.md), [009 — LLVM Backend](009-llvm-backend.md)).
## 3. SSA/CFG model
A **VIR module** contains functions. A **function** has a name, a signature, and a non-empty list
of basic blocks; one block is the **entry block**. Every function is either a definition or a
declaration. A declaration has a signature and no blocks.
A **basic block** has a label, unique within its function, and an ordered list of instructions
ending in exactly one **terminator**. The terminator is the last instruction of the block.
An **SSA value** has a type and is defined by exactly one instruction. Values are referenced by
name. Following the LLVM convention, SSA names written `%name` are numbered values; unnumbered
temporaries are assigned deterministic numbers at print time.
The **CFG** is the directed graph whose nodes are blocks and whose edges are taken from
terminators. Edge `b -> c` means c is a **successor** of b and b is a **predecessor** of c. The
entry block has no predecessors.
**Domination.** Block `a` dominates block `b` if every path from the entry block to `b` passes
through `a`. Domination is reflexive; `a` strictly dominates `b` when `a` and `b` differ. An
instruction `d` dominates a use `u` when the block containing `d` dominates the block containing
`u`, or `d` and `u` are in the same block and `d` appears before `u`.
**SSA form.** Every value has exactly one definition, and every use is dominated by its definition.
The only relaxation is the `Phi` instruction, whose operands are conceptually evaluated at the end
of the corresponding predecessor.
**Def-use.** Each use of a value is a `(user-instruction, operand-index)` pair. The def-use graph
is the union of those pairs over all instructions. Passes that rewrite an operand MUST update both
sides of the edge.
## 4. Type system
VIR types are strictly typed. There are no implicit conversions; a conversion is an explicit cast
instruction.
| Type | Meaning |
|---|---|
| `void` | No value. The result of effect-only calls and functions. |
| `iN` | An `N`-bit two's-complement integer, `N >= 1`. `i1` is boolean. |
| `f32`, `f64` | IEEE-754 binary32 and binary64. `f16`, `f80`, `f128` MAY be supported. |
| `ptr<T>` | A pointer to `T`. |
| `[N x T]` | An array of `N` elements of type `T`. |
| `{T1, ..., Tn}` | A struct with the listed field types in order. A packed variant MAY exist. |
| `union {T1, ...}` | A union of the listed member types. |
| `fn(T1, ...) -> R` | A function type: parameter types and return type `R`. A variadic variant MAY exist. |
- **V-1.** `iN` MUST accept any width `N >= 1`; the implementation MUST NOT restrict integers to a
fixed set of power-of-two widths.
- **V-2.** `void` MUST NOT be used as the type of a value. It is valid only as a function result
type and as the result type of a call that produces no value.
- **V-3.** Aggregate types (`[N x T]`, struct, union) are first-class: they MAY be operands and
results of `load`, `store`, `phi`, `select`, and calls.
- **V-4.** Pointer element types are used for typing `load`, `store`, and indexed `gep`. They are
a convenience for the C backend; the LLVM backend emits opaque `ptr` and relies on the
instructions' operand types for correctness (see [009 — LLVM Backend](009-llvm-backend.md)).
## 5. Instruction set
An instruction has an opcode, zero or more operands, an optional result type and value, and
optional flags. The catalog below is normative for opcode meaning; the exact textual spelling is
specified by the dump format and is not an authoring interface.
### 5.1 Terminators
| Opcode | Syntax (conceptual) | Meaning |
|---|---|---|
| `br` | `br %target` | Unconditional edge. |
| `condbr` | `condbr %cond, %iftrue, %iffalse` | Conditional edge on an `i1` value. |
| `switch` | `switch %value, %default [ case ... ]` | Multi-way edge on an integer value. |
| `ret` | `ret void` / `ret %value` | Return from the function. |
| `unreachable` | `unreachable` | Marks a point that cannot be reached at runtime. |
- **V-5.** Every block MUST end in exactly one terminator.
- **V-6.** A `condbr` condition MUST have type `i1`.
- **V-7.** A `switch` value MUST have integer type; each case constant MUST fit that type.
- **V-8.** A `ret` operand MUST match the function's declared return type, and a void function
MUST use `ret void`.
### 5.2 Memory instructions
| Opcode | Syntax (conceptual) | Meaning |
|---|---|---|
| `alloca` | `%p = alloca T [, align A]` | Allocate `T` on the stack; result type is `ptr<T>`. |
| `load` | `%v = load T, ptr<T> %p [, align A] [, volatile]` | Read a `T` from memory. |
| `store` | `store T %v, ptr<T> %p [, align A] [, volatile]` | Write a `T` to memory. |
| `gep` | `%p = gep T, ptr<T> %base, idx...` | Compute a pointer to an indexed element or field. |
| `memcpy` | `call ...` | Copy memory; also allowed as a dedicated opcode. |
| `memset` | `call ...` | Fill memory; also allowed as a dedicated opcode. |
| `memmove` | `call ...` | Overlapping copy; also allowed as a dedicated opcode. |
- **V-9.** A `load` of type `T` MUST take a pointer of type `ptr<T>`; a `store` MUST agree on `T`.
- **V-10.** A `gep` MUST index into aggregates by **field index**, not by byte offset. The first
index traverses the pointer; subsequent indices traverse arrays and struct fields.
- **V-11.** A `volatile` load or store MUST NOT be reordered with respect to any other volatile or
atomic access, and MUST NOT be eliminated even when its result is unused.
### 5.3 Arithmetic and bitwise instructions
| Category | Opcodes |
|---|---|
| Integer binary | `add`, `sub`, `mul`, `udiv`, `sdiv`, `urem`, `srem` |
| Integer bitwise | `and`, `or`, `xor` |
| Shifts | `shl`, `lshr`, `ashr` |
| Floating binary | `fadd`, `fsub`, `fmul`, `fdiv`, `frem` |
| Floating unary | `fneg` |
- **V-12.** Integer arithmetic MAY carry `nsw` (no signed wrap) and `nuw` (no unsigned wrap)
flags. A result on which overflow occurs under an asserted flag is poison; an implementation
that does not model poison MUST NOT emit such a flag unless the overflow is provably impossible.
- **V-13.** Floating-point instructions MAY carry the fast-math flags `nnan`, `ninf`, `nsz`,
`arcp`, `contract`, `afn`, and `reassoc`. A flag MUST only be set when the corresponding trait or
`Config` licenses it. Fast-math flags MUST NOT be applied at optimization levels below `-Ofast`
unless explicitly configured.
- **V-14.** `udiv`/`sdiv`/`urem`/`srem` by zero is undefined behavior. An implementation that
models this MUST NOT fold such a division to an arbitrary value.
### 5.4 Comparison instructions
| Opcode | Predicates |
|---|---|
| `icmp` | `eq`, `ne`, `slt`, `sle`, `sgt`, `sge`, `ult`, `ule`, `ugt`, `uge` |
| `fcmp` | `oeq`, `one`, `olt`, `ole`, `ogt`, `oge`, `ord`, `uno`, `ueq`, `une`, `ult`, `ule`, `ugt`, `uge`, `true`, `false` |
- **V-15.** The result of `icmp` and `fcmp` MUST have type `i1`.
- **V-16.** Integer comparison predicates beginning with `s` are signed; those beginning with `u`
are unsigned.
### 5.5 Conversion instructions
| Opcode | Meaning |
|---|---|
| `trunc` | Narrow an integer. |
| `zext`, `sext` | Widen an integer, zero- or sign-extending. |
| `fptrunc`, `fpext` | Narrow or widen a float. |
| `fptoui`, `fptosi` | Float to integer. |
| `uitofp`, `sitofp` | Integer to float. |
| `ptrtoint`, `inttoptr` | Pointer/integer conversion. |
| `bitcast` | Reinterpret bits; requires equal size and no pointer-to-pointer element change in the C backend. |
- **V-17.** A conversion MUST be explicit. There MUST be no implicit widening, narrowing, or
signedness change anywhere else in the instruction set.
### 5.6 Other instructions
| Opcode | Syntax (conceptual) | Meaning |
|---|---|---|
| `phi` | `%v = phi T [ v1, %b1 ], [ v2, %b2 ], ...` | SSA merge at a join. |
| `select` | `%v = select %cond, %a, %b` | Choose `%a` or `%b` on an `i1`. |
| `call` | `%v = call R @callee(args...) [flags]` | Call a function or intrinsic. |
| `atomicrmw` | `%v = atomicrmw op, ptr<T> %p, %x ordering` | Atomic read-modify-write, result is the old value. |
| `cmpxchg` | `%v = cmpxchg ptr<T> %p, %expected, %new ordering` | Atomic compare-and-exchange. |
| `fence` | `fence ordering` | Memory ordering fence. |
- **V-18.** A `phi` has one operand per predecessor, each a `(value, predecessor-block)` pair. Its
result type MUST equal each operand's type.
- **V-19.** A `select` condition MUST have type `i1`, and its two value operands MUST share a type
that equals the result type.
- **V-20.** A `call` result value MAY be absent when the callee returns `void`. Call-site attributes
(`Inline`, `NoInline`, `TailCall`, `MustTail`, `NoTail`, `ColdCall`, `NoReturn`, and the
memory-effect requests) MUST be carried on the call and read from its trait, not re-derived.
- **V-21.** Non-atomic accesses MUST NOT be reordered across an atomic access or a fence in a way
that violates the ordering the access declares.
### 5.7 Intrinsics
A VIR intrinsic is a well-known callee referenced by a `call` instruction. The v1 intrinsic set is
fixed:
| Intrinsic | Signature | Meaning |
|---|---|---|
| `memcpy` | `(ptr<T>, ptr<T>, iN) -> void` | Copy `N` bytes between non-overlapping regions. |
| `memset` | `(ptr<T>, i8, iN) -> void` | Fill `N` bytes with the given byte value. |
| `memmove` | `(ptr<T>, ptr<T>, iN) -> void` | Copy `N` bytes between possibly overlapping regions. |
| `sqrt` | `(f32) -> f32`, `(f64) -> f64` | IEEE-754 square root. |
| `fabs` | `(f32) -> f32`, `(f64) -> f64` | Absolute value. |
| `ctpop` | `(iN) -> iN` | Count of set bits. |
| `fshl` | `(iN, iN, iN) -> iN` | Funnel shift left. |
| `sadd_sat`, `uadd_sat`, `ssub_sat`, `usub_sat` | `(iN, iN) -> iN` | Saturating add and subtract. |
| `sadd_overflow`, `uadd_overflow`, `ssub_overflow`, `usub_overflow`, `smul_overflow`, `umul_overflow` | `(iN, iN) -> {iN, i1}` | Wrapping result plus an overflow flag. |
`memcpy`, `memset`, and `memmove` MAY also appear as dedicated opcodes (§5.2); the other intrinsics
appear only as calls.
- **V-25.** An intrinsic `call` MUST use the canonical name in the table above and operands that
match its signature. Its result type follows the signature; the overflow intrinsics return the
struct `{iN, i1}`.
- **V-26.** The intrinsic names are reserved. An implementation MUST recognize them as intrinsics
rather than as user-defined callees, and MUST NOT allow a module to redefine them.
## 6. Well-formedness invariants
A VIR module is **well-formed** when it satisfies all of the following. The verifier checks them
after lowering and, in debug builds, after every pass (see [012 — Testing](012-testing.md)).
- **WF-1 (single definition).** Every SSA value is defined exactly once in its function.
- **WF-2 (def dominates use).** Every use is dominated by its definition, with the phi exception:
an operand `(v, P)` of a phi requires `v` to dominate `P`, or to be the phi's own result when `P`
is a loop back-edge predecessor.
- **WF-3 (termination).** Every basic block ends in exactly one terminator, and no terminator
appears before the end of a block.
- **WF-4 (phi arity).** The number of phi operands equals the number of the phi block's
predecessors, and each named predecessor is an actual predecessor.
- **WF-5 (CFG consistency).** For every successor edge `b -> c` from a terminator, `c` lists `b`
as a predecessor. The entry block has no predecessors.
- **WF-6 (operand types).** Every instruction's operands and result conform to §4 and §5.
- **WF-7 (return type).** Every `ret` agrees with the function's declared return type.
- **WF-8 (function isolation).** No instruction references a value defined in another function.
- **WF-9 (declared callees).** Every `call` names a function that is either defined in the module
or declared in it.
- **WF-10 (alloca result).** An `alloca` of `T` produces a `ptr<T>`, and every `load`/`store`
through it agrees on `T`.
- **WF-11 (dead blocks).** A block unreachable from the entry block MAY remain, but it MUST itself
be well-formed.
Verification policy:
- **V-22.** In debug builds, the verifier MUST run after lowering and after every optimization pass.
A violation MUST assert.
- **V-23.** In release builds, verification MUST be available behind a flag (the driver's
`--verify`) and MUST NOT run by default. A violation detected in release MUST raise an
internal-compiler-error diagnostic as specified in [011 — Diagnostics](011-diagnostics.md).
- **V-24.** An implementation MUST NOT "repair" a detected violation silently.
## 7. Textual form
The textual form prints functions, blocks, instructions, and types in a stable order. It exists
for dumps, tooling, and round-trip tests. The round-trip property is
`print(parse(print(m))) == print(m)` (see [012 — Testing](012-testing.md)). The parser is not a
supported frontend: it MAY assume the input was produced by the printer.
## 8. Example
```
define i32 @sum(i32 %n) {
entry:
br %loop.header
loop.header:
%i = phi i32 [ 0, %entry ], [ %i.next, %loop.latch ]
%s = phi i32 [ 0, %entry ], [ %s.next, %loop.latch ]
%cmp = icmp slt i32 %i, %n
condbr %cmp, %loop.body, %loop.exit
loop.body:
%s.mid = add i32 %s, %i
br %loop.latch
loop.latch:
%i.next = add i32 %i, 1
%s.next = add i32 %s.mid, 0
br %loop.header
loop.exit:
ret i32 %s
}
```
The two phis are required because `loop.header` has two predecessors, `entry` and `loop.latch`.
WF-4 requires both phis to carry exactly two operands, and WF-2 requires each operand to dominate
its named predecessor.
## 9. Cross-references
- [000 — Overview](000-overview.md): determinism, non-goals (no hand-authored VIR).
- [001 — Architecture](001-architecture.md): VIR module placement and visibility.
- [002 — Traits](002-traits.md): the only channel by which VIR receives facts.
- [005 — Lowering](005-lowering.md): constructs and validates VIR.
- [007 — VIR Optimizer](007-vir-optimizer.md): transforms VIR under the invariants here.
- [008 — C Backend](008-c-backend.md): out-of-SSA and C emission.
- [009 — LLVM Backend](009-llvm-backend.md): 1:1 VIR to LLVM mapping.
- [011 — Diagnostics](011-diagnostics.md): internal-compiler-error policy.
- [012 — Testing](012-testing.md): verifier, round-trip, and differential tests.