Xr0 – Semantic Abstraction for C

Home

Theses

Learn

Try

‘The fact that a language originated in 1973 has required as little change as this one has in thirty years of heavy use is truly remarkable, and without parallels anywhere else in computer science or engineering.’¹

Xr0 is a tool for proving that C programs are safe at compile time. It relies on semantic abstractions, which are programmer annotations that describe the safety properties of code:

/* the [] part tells Xr0 we're using the heap */
void *
alloc1() [ .alloc result; ]
{
	return malloc(1);
}

$ 0v alloc1.x
$ echo silence is golden

/* error: this allocates but has no [] */
void *
leak1()
{
	return malloc(1);
}

$ 0v leak1.x
qed error: actual and alleged states differ

Xr0 is currently focused on dealing with memory leaks, but in time we intend for it to give C programmers the same safety guarantees that most higher-level languages offer.

Xr0 is

• C. Xr0 adds safety guarantees that require user-supplied annotations we call abstractions. Apart from these, the code is vanilla C: Xr0 is not the new C++.

• Built in C from the ground up. Well, with Lex and Yacc.

• Small, and we intend to keep it so. We’re currently at around 4700 LOC, and believe we can achieve self-hosting for the memory-leak checking without overshooting the 5000 mark.²

• In its early infancy. What we have right now is little more than a rough draft that demonstrates the viability of our approach. Xr0 can currently only check for leaks, and that only in very simple cases.

• Open source. View the project on SourceHut or GitHub.

Sounds interesting? Then

• Read the tutorial and give Xr0 a spin. We know the examples are very limited, but are still eager to get early feedback on it. Speaking of which,

• Engage us. We welcome and encourage critical discussion on our approach and even on the current implementation. You can find us on the Xr0 Zulip chat. To maximise the constructiveness of criticism, we would encourage you to

• Take a deeper dive by reading the theses and our vision and roadmap. We want you to understand our philosophy in designing Xr0 so you can understand why we think this is so plausible, and why our timelines are achievable. Finally,

• Support us. If you think what we’re doing is interesting, please star the repo on GitHub.

Our Sponsors

The Xr0 project is greatful for generous support from

Zulip

An open-source modern team chat app designed to keep both live and asynchronous conversations organized.