Breaking Phil's upload server on purpose
Phil's compiler backend emits LLVM for an upload client and server. We run that server on Solana. To find out how much our tests would notice if that code were wrong, we made it wrong, one small change at a time, hundreds of times, and counted how many of the broken versions get caught.
This is called mutation analysis. A broken version that passes every test marks something no test checks.
What gets broken
Each mutant is Phil's module with exactly one change. Changes that leave the module malformed are discarded.
| Kind of change | Mutants | Caught by either suite |
|---|
A runtime that checks what the types promised
Phil's types say that every owner is used exactly once and in order. Those facts are erased before LLVM; the emitted module marks the places with the comment !phil proof/typestate fact erased before LLVM. Our Solana runtime puts them back as checks that run on every call the server makes:
- a received frame is committed or destroyed, exactly once, and never left pending;
- a record is read only after its frame was committed;
- the payload is received once, for exactly the length Begin declared;
- nothing is stored before its digest was validated, and nothing is stored twice;
- a payload is stored or released, never both and never neither;
- "accepted" is sent only after a successful store, and "rejected" only after a failed digest check and a release;
- every call is about the object the protocol says it is about, and the server returns 0.
One broken rule fails the Solana transaction. Phil's real server passes all of them on every path our tests reach. Most mutants do not, which is how they are caught.
The server, step by step
Mutants in each block of UploadServer, and how many our suites catch. The two that survive remove an initialisation whose value is never read by a conforming runtime.
| Block | Mutants | Caught by ours |
|---|
Two suites
Phil's integrated test and ours are built for different jobs. Phil's runs the client and the server together on Phil's reference runtime, through three scenarios, and it is one piece of an assurance case that also rests on machine-checked proofs and on tests of earlier slices. Ours runs only the server, on a different runtime, with many malformed inputs. The step-by-step comparison has gone to Phil's author rather than onto this page.
Reproduce it
git clone https://github.com/abiggerhammer/phil ../phil npm ci npm run mutation -- ../phil # needs clang, llvm-as and OpenSSL headers; about seven minutes
The tool is mutation/mutate.ts. The module it mutates is in giveaway/phil-llvm, as emitted by Phil. This is a community project and is not affiliated with Phil.