16 ms·

This is another good spot. Xr0's logical/arithmetic analysis is currently limited because we've been more focused on getting the structures of the language work

• gpderetta 3y ago
  This seems very hard in general to fix: void x(int a, int b) { int * p; p = malloc(1); if(a) { free(p); } if(b) { free(p); } } It is possible that the program always guarantees that a!=b, but it would be hard to prove even with whole program analysis. Are you planning additional annotations or this is just not expected to work?
  • mst 3y ago
    I can't speak for the authors but I think I'd file that one under "and if you write this, ideally a small gnome exits the back of the computer and hits the developer with a mallet." 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 ;)
  • 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 ago
      Ideally 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 ago
        Yes, 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 ago
          Will 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)]] {...}