Xr0

C But Safe

Try

Xr0 is a verifier for C. It eliminates many stubborn instances of undefined behaviour, like use-after-frees, double frees, null pointer dereferences and the use of uninitialised memory.

Xr0 uses C-like annotations to verify code:

void *
alloc() ~ [ return malloc(1); ] /* caller must free */
{
        return malloc(1);
}

More about the annotations

They’re attached to every function that is potentially unsafe and express what its callers need to know to use it safely:

void *
alloc_if(int x) ~ [ if (x) return malloc(1); ] /* caller must free if x != 0 */
{
        if (x) {
                return malloc(1);
        } else {
                return NULL;
        }
}

The really subtle safety bugs creep in through layers of function calls. Xr0 makes this impossible, because everything needed to secure safety is distributed through every function call, so that no subtle mistake can creep in. It “quantum entangles” the safety semantics of every part of the program with every other part. Think of it like a infinitely rich type system that rises to the demands of your program’s structure. You still have to make the code safe; Xr0 just checks your work. Thus Xr0 is magical like the wand, not the magician. The real magic comes from the programmer.

Xr0 is a work in progress and currently verifies a subset of C89. Its most significant limitation is we haven’t yet implemented verification for loops and recursive functions, so these are being bridged by axiomatic annotations. Xr0 1.0.0 will enable programming in C with no undefined behaviour, but for now it’s useful for verifying sections of programs.

Xr0 is written in pure C and is open source. View it on GitHub or SourceHut.

Intrigued?

Read the tutorial and give Xr0 a spin.

If you want to go deeper, engage with our theses, which explain how Xr0 will make C safe, and take a look at our vision and roadmap.

Community

Come and talk to us on the Xr0 Zulip, or via email here and here.

Xr0

C But Safe

Intrigued?

Community

Sponsors