Using sysi · from source to a checked executable

A tour

One small sysp program, taken all the way down: proved by sysp, lowered to sysi, compiled to RISC-V, linked, and checked twice on the way. Every output on this page is what the tools printed when the docs were last built, not a transcript typed by hand.

1. 1the program
2. 2sysp check
3. 3sysi lower
4. 4sysi asm
5. 5sysi c
6. 6sysi refine
7. 7clang, ld.lld
8. 8sysi validate
9. 9a wrong lowering

1. The program

The example is docs/site/examples/sum.sysp. It has two functions. sum adds up the bytes of a buffer; its contract says the buffer holds at most a million bytes and the result is not negative, and its loop carries an invariant that bounds the running total. run is a driver: it makes a buffer of four bytes, 10, 20, 30 and 40, calls sum, frees the buffer, and returns 0 if the total is 100 and 1 otherwise. The start routine of the test programs calls run and reports its result (step 7).

2. sysp proves it

sysi compiles only programs sysp has verified, so the first step is sysp's own. sysp check turns every place the program could go wrong into an obligation and has z3 prove each: the additions do not overflow, (get xs i) and (put xs i ...) are in bounds, the as conversions fit, each loop invariant holds on entry and is kept, and sum's result is not negative.

These proofs are what lets the lowering be plain. Because sysp proved that (+ s ...) cannot overflow, sysi can add with an ordinary 64-bit add; because it proved the index is in bounds, the load needs no bounds check. sysi lower runs the same check first and refuses a program that does not pass it.

3. sysi lower: the IR

sysi lower turns the checked program into a sysi module: one func per sysp function, made of blocks of instructions on 64-bit words. Below, the sysp source is on the left and its sysi on the right. Point at a line on either side (or tap it) to see which lines it corresponds to; or step through the main points.

Four things to see in sum:

• Parameters are words. sysp's xs is a (ref (buf u8)); in sysi a buffer is two words, the address of its first byte and its length. So sum has two parameters, (params v1 v2). The sig line keeps sysp's signature, from which the word count follows by the ABI (From sysp to sysi).
• Each value is defined once. v3, v4, ... are values, not variables: each is assigned by exactly one instruction. sysp's var s is assigned on every round of the loop, so it is not one sysi value but many.
• The loop head has parameters. b1 is the loop head, and (v5 v6) are its parameters: the values of s and i each time control arrives there. The entry jumps there with (jmp b1 v3 v4), both 0; the body jumps back with (jmp b1 v10 v12), the new total and the next index. Block parameters do the job that phi nodes do in other IRs (The IR).
• The cut is a hint. The cut line at the top of b1 is not an instruction. It records where the loop is in the source, which sysi value holds each sysp variable there ((s v5) (i v6)), and the loop's invariants as sysp wrote them. The first invariant, (<= 0 i (len xs)), is the one sysp adds itself when it turns a for into a while. sysi refine uses the cut to check the loop (step 6); a wrong hint can only make that check fail.

In run, buf-new becomes a call to the platform's sysp_alloc (with the size raised to at least one element: v3 = eq v1 v2 is 1 only when the size is 0), free a call to sysp_free, and the if at the end two blocks that jump to b6 with the value of their arm: b6's parameter v22 is the if's value.

4. sysi asm: RISC-V assembly

sysi asm compiles the same module to RV64 assembly. It allocates registers by live ranges and writes one label per sysi block, named function.block, so the assembly reads alongside the sysi. Here is sum:

Point at a block on either side to see its counterpart.

The buffer's two words stay in a0 and a1, where the RISC-V calling convention puts them: the allocator prefers the register a value arrives in. The loop's two constants are built straight into the head's parameters (li), and the new values in the body are made in the parameters' registers, so the jump back needs no moves. The comparison v7 exists only for the branch, so it is the branch: bge leaves the loop when i reaches the length. The return moves s into a0. Along with the assembly, the backend makes a map of where every value lives at the start of each block; sysi validate makes it again in step 8 and checks the machine code against it. RV64 and C has the details.

5. sysi c: the comparison backend

sysi also has a C backend. It is not on the path to the machine; it exists to compare against. Each sysi function becomes a C function on uint64_t words, with a label per block and a goto per jump, and a wrapper with sysp's own C signature calls it:

The tests build each test program through this C and through the RV64 assembly, run both on sysr's instruction-set simulator, and require the same output (tests/rv64-test.rkt).

6. sysi refine: the lowering, checked

Is the sysi on the right really the sysp on the left? sysi refine answers that for each function, with z3. It cuts each function at its loop heads into regions: from the entry to the first loop head or a return, and from each loop head around the loop and out. In each region it runs the sysp function (as sysp's verifier understands it) and the sysi function side by side on symbolic values, and asks z3 to show that both arrive at the same places under the same conditions with the same values: sysp's s equal to the sysi word the cut names for it, the results equal at the return. With -v it names each function as it checks it:

Two functions, each with one loop, make 4 regions in the summary line: sum from its entry and from b1, and the same for run. The cut is what makes this finite: without it, the check would have to follow the loop around for as many rounds as there might be bytes. The call to sum inside run is matched to sysp's call one to one, with the arguments related; both sides then share the call's result, of which the sysp side knows only what sum's contract promises. The lowering, checked explains the check in full.

7. Linking an executable

Assembly is not yet a program. The test programs, and this example, are linked with two small files from tests/programs: a start routine, rt.S, and a link script, link.ld. The docs build runs these commands (from tools/docs.rkt; tests/rv64-test.rkt uses the same flags):

The start routine sets up a stack, calls run, and reports its result to the test device of QEMU's virt machine at 0x100000: 0x5555 for a pass when run returned 0, and otherwise 0x3333 with the result in the upper half, which the simulator turns into an exit code. It also provides the platform functions sysp's programs call: sysp_alloc is a bump allocator over a zeroed area (16-byte aligned; it panics when the area is used up), sysp_free does nothing, sysp_panic exits with code 99, and sysp_irq_save and sysp_irq_restore clear and restore mstatus.MIE.

The link script puts everything at 0x80000000, where QEMU's virt machine (and sysr's simulator) start, with the start routine's .text.boot section first:

clang assembles and ld.lld links, and neither is trusted: what they produced is checked next.

8. sysi validate: the machine code, checked

sysi validate reads the linked executable back. It lowers and compiles the program again to get the sysi module and the map of where each value lives, finds each block's label in the executable, and decodes the instructions there. For each block it runs the sysi block once and the machine code on every path from the label to the next block, a return or a trap, on symbolic registers, taking the meaning of each instruction from sysr's isa.sysr. z3 must then show that the machine code went to the block sysi goes to, with the right values in the places the map names. With -v it names each block:

The 11 blocks in the summary are sum's four and run's seven; a block with a branch has a path for each way. Memory is not modelled: loads, stores and calls must happen in the same order with the same addresses and values on both sides. The machine code, checked explains it in full.

That is the whole chain: sysp proved the source; refine showed the sysi means the same; validate showed the machine code does what the sysi says. The docs build stops here. The tests go one step further with their programs and run them on sysr's simulator (step 5). The same steps run on the sysk kernel in the gate; its last result: not run here.

9. A wrong lowering, rejected

A check is only worth something if it fails when it should. The docs build takes the lowering of sum, changes one instruction, and runs sysi refine's check on the result, the same way tests/refine-test.rkt does for the instructions of its test program (every third one, or all of them with MUTATE=all). The change made here: add->sub.

The address of xs[i] is now computed as the buffer's address minus i, so the loop reads the wrong bytes. The program still checks as well formed, it still compiles, and for an empty buffer it even gives the right answer. Refine reports:

How to read the report, part by part:

Why there and not elsewhere: the changed instruction is in b2, the loop body, which only the region starting at the loop head runs. Following the body from b1 back to b1, sysp's new s is s plus the byte at index i, while the sysi value passed for s, v10, is v5 plus the byte at address v1 - v6. z3 found a state in which the two differ, so the cut's claim that v5 holds s cannot be kept. The region from the entry is unaffected and passes; only the broken one is reported.