2 ms·
This is another good find. We haven't yet implemented the `!=` operator (or most of the binary operators). Incidentally, you will notice that Xr0 rejects the p
by akiarie 3y ago
This is another good find. We haven't yet implemented the `!=` operator (or most of the binary operators).
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);
}
}
}
I say "can" because we only have this working on a development branch [0], and there are still some issues we're resolving on this, hopefully by next week.
[0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching https://github.com/xr0-org/xr0/tree/fix/nested-branching
- gpderetta 3y agoIdeally you would express the precondition that a and b are mutually exclusive like this: void x(int a, int b) { if(! (a != b)) abort(); int * p; p = malloc(1); if(a) { free(p); } if(b) { free(p); } } And the program would be accepted. I'm on my phone and can't verify it though. 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?
- akiarie 3y agoYes, the code example you've given is exactly in the direction we're thinking. (Edit: thought it can't be verified yet.) 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 https://xr0.dev/learn#initialisation-of-memory-and-the-clump
- gpderetta 3y agoWill take a look at your reference. Stroustup and Sutter have tried annotating every function, but their declarative function wasn't expressive enough. Adding arbitrarily expressions might help though. 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)]] {...}