# 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.