The checks · tested

The checker, tested

sysi refine proves that sysi's code does what a model of sysp says: a symbolic evaluator written from sysp's verifier. If the model were wrong, the proofs would be about the wrong thing. This page shows how the model itself is tested: it runs on values, and what it computes is compared with what the same program does compiled by sysi and run on sysr's simulator.

Why test a checker

A proof of refinement relates two meanings: sysi's (its reference, §1-2) and sysp's as the evaluator in sysi/refine.rkt takes it (sysp-region-eval, the lowering, checked). The second is written by hand, rule by rule, from sysp's verifier. A wrong rule (a - read as an addition, a comparison off by one) would not make refine fail: the lowering and the model could agree with each other and both be wrong. Nothing in the proof can notice that; running the program can.

So the model gets a second use. The chain below is what is compared: the model run on values at one end, the machine code run on sysr's ISS at the other. Agreement on a call says that the model, the lowering and the RV64 backend do the same thing on those inputs.

The model, run on values

sysi/concrete.rkt runs the evaluator itself, not a copy: sysp-region-eval is the function refine calls. A call runs region by region, as refine cuts it: from the function's entry, or a loop head, to the returns and loop heads it reaches. The terms a region builds have no free symbols left but the evaluator's own choices, and the events fix those: a call's result is what running the callee gives (or, for put-byte, a model that writes the byte); at an atomic block's entry, other tasks changed nothing. Exactly one exit must be taken; its values start the next region. Each fact the evaluator assumed on the way (the obligations sysp's verifier proved there, but for a product's range, which the evaluator leaves out) is checked on the values.

Here is the docs' example, its run function run that way (recorded by tools/docs.rkt run). A region is listed as it ends, so sum's regions come before the region of run that called it. At a loop head the values are the variables in scope; i-start and i-end are a for loop's bounds, which the evaluator keeps beside i. Step through it:

Random calls, both ways

sysi difftest FILE.sysp ... takes every function whose parameters are numbers and buffers. For each it draws inputs at random (small integers and the literals the contract names, a buffer's bytes from a short list of 0, 255, digits, letters and the characters a parser looks for, buffers of lengths the contract suggests) and keeps those its requires accept, evaluated on the values. A function whose requires it cannot evaluate (a quantifier over two variables, say) gets no inputs, and is listed. Private functions, and those that can reach an extern other than put-byte, are not tested.

It then writes a sysp driver: per call, a function that builds the inputs, makes the call, and prints the result and every buffer the callee may change (its mut parameters); dt-run calls them all. The driver, with the program, runs two ways: on the model, each call alone (within 20,000 regions, so a call that does not end is that call's failure), and as sysi's RV64 code on sysr's ISS, with the test runtime's start calling dt_run. Every call must print the same, and no assumption may be false. The driver's machine code, as linked, must also pass sysi validate, so each difftest run checks the backend on code no test program contains.

What it has found

On the benchmark's programs, sysk's libraries, arith.sysp, and sysk's kernel and tasks as the gate builds them (make sysk-difftest), every call agreed and every assumption held (counts in specs/007-checker-tested). One assumption was false on the way, and it was in difftest's own driver: it printed a w64 through (as i64 ...), which sysp allows only when the value fits. A bitset function set bit 63, the value no longer fit, and the model reported the cast's assumption false where the ISS printed a negative number. A w64 is now printed as its two 32-bit halves.

It has also found a bug in the backend (specs/008). A branch on a comparison with a constant read the constant from a register whose value had already been replaced; the test programs never compared that way, so the tests did not see it, but difftest's drivers loop to a buffer's length, which is a constant there. Its calls printed differently, and sysi validate on the driver named the block. That is why difftest now validates its driver on every run.

To see whether it would notice a wrong rule, eight rules of the model were broken one at a time, and difftest was run on the benchmark, on sysk's libraries and on tests/programs/arith.sysp. On the first try, four of the eight went unnoticed on the benchmark and the libraries: a remainder computed unsigned, a division by a power of two rounding down, an arithmetic >> on words, and a byte's range one short. On the inputs drawn, those programs never divided a negative number, never shifted a word with its top bit set, and never added bytes up to 255, so a wrong rule there changed nothing they printed. Two changes followed. The input draw now gives a negative integer in about a third of the draws (one in ten before, mostly from −3 to 0), and lets a byte be one of the contract's literals. And arith.sysp was written to reach those corners: every operator on negative operands, division and remainder by powers of two, shifts of words with the top bit set, and byte arithmetic up to 255. With both, each of the eight is noticed by at least one program:

From specs/007 (8 calls a function, seed 1). "differ": calls that printed differently; "false": assumptions of the model found false. When > reads as >=, the driver's own number printing breaks too (its loop never ends), so every call fails.

Running it

sysi difftest takes the program's files and --cases N (calls per function, 8 unless given), --seed N (1 unless given), --only F and -v (every call, with its inputs and what it printed). It needs clang, ld.lld and sysr beside this repository, as validate's tests do. It exits 0 only if no call differs, no assumption is false and nothing failed to run.