sysi docs · the checks

The machine code, checked

sysi validate reads the linked executable back, instruction word by instruction word, and checks, block by block, that it does what the block's sysi says. What each instruction does is not written in sysi: it is read from isa.sysr, the specification sysr's core is proven against. So the backend, the assembler and the linker need not be trusted, and the meaning of an instruction is written once, for the core and for this check.

What is checked against what

sysi validate prog.sysp --elf prog.elf lowers the program and runs the RV64 backend again, as sysi asm did, keeping not the text but the allocator's map for each function (finfo): the frame's size, where spills and saved registers are, each value's location (a register, or a spill word), each slot's offset, the values live into each block, and the callee-saved registers saved. The map is the claim; the executable is what is checked against it and against the sysi.

Each instruction, as isa.sysr says

sysi/isa.rkt loads sysr's cores/rv64im/platform.sysr, isa.sysr and custom.sysr with sysr's own checker, and evaluates the typed spec functions on one instruction at a time: exec-spec on a concrete pc, a concrete instruction word and the values of the two source registers it names. This is partial evaluation: whatever the word decides (the opcode, the registers, the immediate) is computed, so the large spec collapses, and what depends on register values becomes a small SMT term. A value is a concrete integer, an SMT term of its width, or a struct of these (the spec's result: the value written, whether it writes, the next pc, a load's or store's address, whether it traps).

Two details keep the terms small. The stack pointer is not a symbol but (spv k), the entry stack pointer plus a known k, so frame addresses stay concrete offsets; its low 4 bits fold to k's, since the convention aligns it to 16. And the low half of a widened product is a narrow product: isa.sysr's mul takes the low 64 bits of a 128-bit product, which z3 would otherwise build as a 128-bit multiplier circuit. isa.sysr leaves the divider out, so division and remainder are taken from the RISC-V manual (by zero gives all ones or the dividend; the least value over −1 overflows to itself).

Division without the divider

The backend divides by a constant without the divider (RV64 and C): by a power of two with a biased arithmetic shift, by another constant d with a multiply-high (mulhsu) by a magic number M, a shift by s, and the sign bit added. z3 cannot show that a 64-bit multiply-high equals a division: asked directly, and asked again in a form without a divider, it ran for 5 minutes each time without an answer. So the proof is split. sysi/divconst.rkt proves, in its header, that the formula equals truncated division for every x whenever M = ⌈2^64+s/d⌉ and e = M·d − 2^64+s satisfies 0 < e ≤ 2^s+1. validate checks that side condition in exact arithmetic for the constant at hand (plan-ok?; a plan that fails it stops validate), and then gives sysi's div by d the formula's term instead of the divider's (div-term, rem-term). What z3 is left to show is that the machine code computes the formula, which it does at once: partial evaluation of isa.sysr's MULHSU gives the same 128-bit product the formula names. The divider is not proven in sysr (isa.sysr leaves it out), and the multiplier is, so these divisions now run on proven hardware.

A remainder after the quotient of the same operands in the same block is taken as x − q·y (the backend computes it so, with a multiply and a subtract). That is RISC-V's remainder for every x and y: the manual defines div and rem so that x = q·y + r holds, division by zero and overflow included.

Reading the executable

sysi/elf.rkt is 48 lines: it checks the file is a 64-bit RISC-V ELF, takes its loadable segments (so it can give the 32-bit word at any address, and where in the file that word lies, which the mutation test uses to corrupt it), and reads the symbol table, local symbols included. The backend labels every block (sum.b1) and keeps the labels in the object file, so the validator finds each block's first instruction by name, and a function's end by its symbol's size.

One block, instruction by instruction

Choose one of sum's blocks. The validator first runs the sysi block once, from fresh symbols for the values live into it, collecting its values and its memory events. Then it runs the machine code from the block's label, one instruction at a time, from a state where those same symbols are in the registers the map names; every other register holds junk. At a branch it forks. Each path ends at another block's label or a return, and z3 must prove its obligations. In the figure, a symbol named like a value (v5) is the fresh symbol for that value's incoming word; D₁ is the doubleword the block's first load reads, which both sides share.

The figure works from the assembly text in run.js and gives each instruction its usual meaning; the validator works from the words in the linked executable and gets each meaning from isa.sysr. The obligations shown are the ones validate.rkt asks for this path; the last run proved them all.

Paths through a block

• The start. At the entry block, the parameters are fresh symbols in a0–a7 (or the stack words past them), ra, gp, tp and the callee-saved registers s0–s11 hold their original values, and sp is (spv 0). At any other block, sp is the entry value minus the frame, each value live into the block is a fresh symbol in its location (register or spill word), the saved registers are in their frame words, and so is ra in a function that calls (in one that does not, ra holds its original value, as gp, tp and the callee-saved registers the function does not save always do); every other register is junk: code that reads one gets a value no obligation can rely on.
• Forks. A branch whose condition the partial evaluation cannot decide forks the path, each side with the condition as an assumption.
• The end. A path ends at another block's label (an empty block shares its label with the next one, so at a path's start only a later block's label ends it), at a return, or at an instruction that traps where sysi says unreachable (unimp).
• Limits. A path may not leave its function, run over 2000 instructions, or a block fork past 256 paths. A mutant that turned a call into a plain jump once ran into the callee and forked at each turn of its loop; these limits came from it.

Memory is not modelled

The backend keeps sysi's order of loads, stores and calls. So the validator does not model memory at all: it matches each machine access with the sysi block's next event, one to one. A load must be at the same address with the same width (and zero-extending, as sysi's loads are); then both sides take the same fresh doubleword and read their bytes from it by isa.sysr's load-value, so the same load is the same term on both sides. A store must have the same address and width, and isa.sysr's store mask and data must put sysi's bytes there. A call must go to sysi's callee with the arguments where the convention puts them; afterwards the caller-saved registers are fresh junk and a0, a1 hold the call's results, the same symbols sysi's side uses. A path that skips an event, or makes one sysi does not, fails.

Accesses to the frame are different: spills, saved registers and outgoing stack arguments are addressed from sp, so their addresses are concrete offsets from the entry stack pointer, and a small frame model indexed by offset tracks them (doublewords only). A store above the function's own incoming stack arguments, into the caller's frame, is rejected. An access into one of sysi's own slots is a sysi access, matched like any other.

At each path's end

One z3 query per path, with every obligation the path collected on the way (each access's address, width and bytes; each call's arguments) and these, at its end:

• the successor is the one sysi takes under the path's condition;
• the successor's parameters, and every value live into it, are where the map says;
• the callee-saved registers s0–s11 that the function does not save are untouched (s0 too, though the backend never uses it), and so are gp and tp; the saved ones' frame words still hold their values, and so does ra's (or ra itself, in a function without calls); sp is the entry value minus the frame;
• at a return: sp back at its entry value, ra the original return address (the jump's target), s0–s11 restored, the results in a0 and a1 (a w32 sign-extended).

If the query is not unsat, the validator asks for each obligation alone to name the first that fails, and reports it with the path's end address.

What is assumed

• The entry stack pointer is 16-byte aligned and the return address 4-byte aligned, as the convention says. (A misaligned access traps in isa.sysr, so the next pc depends on these low bits.)
• sysi's own accesses are aligned and in bounds, which sysp proves; so they never touch the frame's spills, and aligned addresses are facts of the query.
• A callee keeps the convention: the callee-saved registers, sp, and the caller's frame.
• A shift takes its amount's low 6 bits. That is RISC-V's definition, and the same as sysi's for the amounts sysp allows (0 to 63); defined so, both sides' terms agree without that fact.
• Division by a constant: the argument in sysi/divconst.rkt's header (its side condition is checked for each constant). A remainder after its quotient: the RISC-V identity x = q·y + r.
• sysr's checker reads isa.sysr correctly, and z3.

A constant live into a block is its value there, as the backend takes it (function-wide): if the backend gave it a location, the location holds that value, since every jump into the block is checked to leave it there; if it gave it none (it builds the constant where it is moved), there is nothing more to check. And z3, asked many questions in one process with push and pop, sometimes answers "unknown" to one that a fresh z3 decides at once (a product with a constant, in sysk's judge): validate then asks that question once more in a fresh process, with only the symbols it names. Neither changes what is proven.

Does it catch wrong code?

tests/validate-test.rkt builds the features program and sysp's 15 benchmark references (with their driver) through sysi asm, clang and ld.lld, twice each: with registers allocated and with every value on the stack. Both must be accepted. The stack build checked against the register build's map must be rejected. Then it corrupts the features program's executable, one instruction word at a time, every 4th instruction (every one with MUTATE=all), each corruption one bit:

Every mutant the validator accepts must be equivalent: the test runs it on sysr's ISS, and it must print what the original prints and exit the same way. The test's last run (specs/008): 408 mutants, 405 rejected; each of the 3 accepted printed on the ISS what the original prints. With every instruction: 1,527 mutants, 1,506 rejected, the 21 accepted all equivalent and each run on the ISS. (With the backend before specs/008, which made more instructions: 490 and 486 by default, 1,828 and 1,806 with every one.) On sysk's kernel, every 20th instruction, with that earlier backend: 1,900 mutants, 1,883 rejected; the 17 accepted were inspected: a value still in the register it came in, a dead write, snez x against x before a beqz.

The runs

On sysk's kernel and tasks, built through sysi asm and linked as sysk links them (tools/sysk-validate.sh), at the last gate:

And on the docs' example, with -v, which names each block as it is checked (first sum's four, then run's seven):