void x() {
int * p;
p = malloc(1);
if(0) {
free(p);
} else {
free(p);
}
}
0v: src/ast/stmt/verify.c:228: stmt_sel_exec: Assertion `!ast_stmt_sel_nest(stmt)' failed.void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(!f) { free(p); } }
And this doesn't, as expected:
void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(f) { free(p); } }
edit: another assertion failure:
void x(int f) {
int * p;
p = malloc(1);
if(f) {
free(p);
}
f = !f;
if(f) {
free(p);
}
}We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43
void x(int a, int b) {
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
I'd be perfectly happy refactoring that so I could have an 'a or b' test (I'm assuming $something means that x(0, 0) not free-ing is correct in real code because nitpicking an illustrative example would be silly).
Though note that I'm sufficiently bad at tracking things right when writing C that I tend to spend most of my debugging time figuring out what stupid mistake I made to cause the current segfault - so I'm probably more willing than average to write code differently if it helps me avoid that ;)
Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free). It can, however, accept code like the following:
void
foo(int a, int b)
{
int *p;
p = malloc(1);
if (a) {
if (!b) {
free(p);
}
}
if (b) {
free(p);
}
if (!a) {
if (!b) {
free(p);
}
}
}
[0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching
void x(int a, int b) { if(! (a != b)) abort();
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
Great stuff anyway!
Edit: is the algorithm documented anyway? And there is any reason why you guys are not implementing it as a clang/GCC plugin and using the new C and C++ annotation syntax?
We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.
The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.
I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.
[0]: https://xr0.dev/learn#initialisation-of-memory-and-the-clump
Re annotations, I meant the attribute syntax. You can have arbitrary custom syntax in it:
void foo(int *p) [[vx0::setup(p = .clump(sizeof(int))), vx0::body(*p = 0)]] {...}Does it always make sense to strictly enforce code that will be optimized/changed during compilation? Or does Xr0 run after compilation/linking?
How to handle things like unions where you want data in a nice mixed-type struct that is used locally and can also be sent as a stream of uint8_t over a wireless connection? Then, the last function that needs to use the memory frees it. Or is that still fine as long as you malloc once somewhere, free once somewhere, and annotate that the memory region will be accessed as more than one dereferenced type?
Much more important: Will the proposed changes be understandable enough for your average CS undergrad to learn in four months of halfway diligent study? (Then again, you might do away with students taking time to debug improper malloc/free and whatever else falls under the scope of Xr0...)
This doesn't need to be perfect though. Just incrementally better than the status quo.