The Vision

The ambition of the Xr0 project is to make it possible to work in C, i.e. vanilla C with no changes to the executed code, while being certain of the safety of one’s code.

We think there are two basic safety issues in C, though undefined behaviour is an extremely multifaceted issue:

• Memory leaks. It is possible for all references to an allocated (i.e. on the heap) region of memory to go out of scope, without the region being deallocated.

• Undefined behaviour (UB): It is possible, with the best available compilers, to write down syntactically valid code whose behaviour is undefined according to the C standard, and be unaware. The most glaring example of this is undefined memory accesses: it is possible to attempt to access memory that is uninitialised, deallocated (use-after-frees and double frees), or nonexistent (NULL-dereferences). Also under UB are arithmetic overflows/underflows, division by zero errors and similar cases.

When Xr0 is complete, it will reject all undefined behaviour, as well as render memory leaks impossible.

The Roadmap

The latest version of Xr0 is already able to eliminate use-after-frees, double frees, null pointer dereferences, the use of uninitialised memory and memory leaks from a limited subset of C89. Beneath is a non-committal¹ listing of the milestones we intend to hit, to the best of our current knowledge:

0. Buffer overflow and underflow protection. Expected in the next 1–3 months.

1. Formalise error handling.

2. Loop verification that’s good enough for most programs.

3. Support for calloc and realloc.

4. Recursion verification that’s good enough for most programs.

5. Support for most of C89 syntax. The possibly-envisioned exclusion here is goto.

6. Complete annotations for Standard library (libx).

7. Release Xr0 1.0.0.

If you’re interested in understanding why we think these problems are solvable, the best way to grasp our approach is to dive into the tutorial.