The IR
sysi, the language, is small on purpose: one kind of value, a handful of instructions, memory that is only touched by explicit loads and stores, and control flow made of blocks that jump to each other. Each instruction is easy to give a meaning, which is what the two checks need. This page goes through it, piece by piece, with the tour's sum as the running example.
Values: 64-bit words, each defined once
Every sysi value is a 64-bit word, as in an RV64 register. There are no types in the instructions: a sysp i64 is the word read as two's complement; a u8, a bool (1 for true) or a w8 to w32 is its value zero-extended to 64 bits; a buffer is two words; a struct is the address of its bytes. Arithmetic is modulo 264, and the operations that need a sign (lt, le, gt, ge, div, rem, sar) read the words as signed. From sysp to sysi has the full list of what each sysp type becomes.
Values are named v1, v2, ..., and each is defined exactly once in a function: by being one of its parameters, one of a block's parameters, or the result of one instruction. This is static single assignment (SSA). It means a value's name always stands for the same computation, which makes both checks simpler: a value can be given one symbolic meaning and used wherever it appears.
Instructions
There are 23 kinds of instruction: 17 operations on two words, and six more for constants, memory, addresses and calls. The list below is OPS in sysi/ir.rkt; each meaning is from docs/reference.md §2. The last column counts each kind in the tour's module, the lowering of sum.sysp.
| Kinds | Form | Meaning | In the tour |
|---|
Offsets in load and store are constants, and every access is naturally aligned. There is no instruction for a type conversion: sysp's as changes no value, because sysp proved the value fits, and words narrower than 64 bits are kept zero-extended by masking after the operations that could set high bits. There is no instruction that checks anything either: no bounds check, no overflow check, no division-by-zero check. sysp proved those cannot fail.
Terminators
A block is a straight line of instructions ending in exactly one terminator, which says where control goes next:
| Form | Meaning |
|---|
Blocks with parameters
Where two paths meet, a value may have come from either. A loop is the plain case: sum's running total is 0 on the way in and the new total on the way back round. Many IRs (LLVM's among them) handle this with phi nodes, special instructions at the top of a block that pick a value depending on which predecessor control came from. sysi instead gives blocks parameters, like a function's: (block b1 (v5 v6) ...), and every jump to the block passes one word for each, (jmp b1 v10 v12). The parameters are defined on entry to the block, once in the text, and take a new value on every arrival.
Run sum on a buffer and watch. The figure executes the sysi below, as the tour's lowering wrote it, one instruction at a time, on concrete words. The buffer starts at address 0x1000; its bytes are yours to change.
| value | now | defined by | earlier |
|---|
Two things are worth noticing. First, the entry block's jump and the body's jump both pass two words to b1, and the head's code does not care which one it came from: there is nothing to choose, so nothing like a phi node is needed. Second, v5 and v6 are defined once in the text but get a fresh value on every arrival, while v8 to v12 get a fresh value on every round of the body: SSA is about the program text, not about time. The backends turn a jump's arguments into register moves (RV64 and C); the C backend writes them as a block of assignments that reads every argument before writing any parameter, so that (jmp b1 v6 v5) would swap correctly.
Functions
A function has a name, which is its C symbol (sysp's ring-push is ring_push); its source, the sysp function it came from; and its sig, the sysp signature with each parameter's type and mode (own, ref, mut or shared). The params are the words the function receives, and how many there are follows from the signature by the ABI: a buffer is two words, a mut struct one (its address), and so on. Then come its stack slots, if any, and its blocks, the first of which is the entry. Here is the grammar from docs/reference.md §3:
- Slots are a function's stack memory:
(slot S SIZE ALIGN), and(v = addr S)gives the address. The lowering uses them for structs it builds or copies and for scalars whose address is passed on (amutargument). - Cuts are the hints at loop heads:
(cut (at "file:line:col") (vars (NAME v) ...) (invariant "...") ...), written as the first item of the head block. They say which sysi value holds each sysp variable there and carry the loop's invariants. They are not instructions; the backends ignore them andsysi refinereads them (why). - A
(source NAME twin)marks the kernel twin of a function that both kernel and user code reach, namedsysp_kernel_...(twins).
Modules: layouts, data, externs
A module is what one sysi lower produces: every function of the program, and three kinds of declaration they need.
- Layouts,
(layout NAME (size N) (align N) (field NAME TYPE OFFSET) ...): each sysp struct's memory layout, C's (computed bysysi/abi.rkt). The instructions only see offsets; the layouts are there for the ABI, for the checks and for reading the module. - Data,
(data D #"bytes"): read-only bytes, the program's string literals.(v = global D)gives the address. - Externs,
(extern F (sig ...)): functions that are called but not defined in sysi: the program's ownexternfunctions (written in assembly), and the platform's, declared the same way when they are used. The tour's module declares two of them: .
The text form is an s-expression, written one item per line and one instruction per line by write-module and read back by read-module. A module read back from its text is equal to the module written; tests/ir-test.rkt checks that, and tests/bench-test.rkt checks it on each of sysp's benchmark programs.
What sysi check checks
sysi check FILE.sysi runs check-module from sysi/ir.rkt and prints each problem, then ok or the count. sysi lower runs the same check on everything it produces and stops with an internal error if any problem is found, so a lowered module is always well formed. The check is about form, not meaning (that is what sysi refine is for):
ret returns as many as the signature says.load and store with a width of u8 to u64 and a constant offset; slots and data that exist; a terminator at the end of each block.Dominance is computed the classic way: a block's dominators are itself plus those common to all its predecessors, iterated until nothing changes. Try breaking the tour's module and see what the check says. The figure runs the same checks as check-module, ported line for line, with its messages; the first button is the module as lowered.
sum, changed
sysi check
tests/ir-test.rkt holds the check to these rules: a well-formed function has no problems and reads back as itself; a value used but never defined, defined twice, or defined on only one of two paths that meet is reported; jumps, returns and calls with the wrong number of words are reported; and the ABI gives small structs as words and large ones by address.