3 ms·

It is quite interesting, but it seems to fail with even very simple examples: void x() { int * p; p = malloc(1); if(0) { free(p); } else {

It is quite interesting, but it seems to fail with even very simple examples: 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.

masklinn 3y ago
To be fair if the program never runs it’s 100% safe.
akiarie 3y ago
Good spot. We hadn't enabled `else` last week when we posted, but we've just fixed this [0]. [0] https://github.com/xr0-org/xr0/releases/tag/v0.15.0 https://github.com/xr0-org/xr0/releases/tag/v0.15.0
- gpderetta 3y ago
  Very nice. I was worried that conditionals would confuse it. But this passes: 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); } }
  - akiarie 3y ago
    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 working as a whole. So you'll get more of these asserts if you try using `&&`, ternaries, and so on. We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43 https://github.com/xr0-org/xr0/issues/43
    - 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?
PennRobotics 3y ago
Plus, at -O1 and up, gcc optimizes this away, so the check itself is not well-defined as necessary. 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...)
- gpderetta 3y ago
  the if(0) was just to minimize the test case. if(variable) also fails. This doesn't need to be perfect though. Just incrementally better than the status quo.

masklinn 3y ago

To be fair if the program never runs it’s 100% safe.

akiarie 3y ago

Good spot. We hadn't enabled `else` last week when we posted, but we've just fixed this [0]. [0] https://github.com/xr0-org/xr0/releases/tag/v0.15.0 https://github.com/xr0-org/xr0/releases/tag/v0.15.0

gpderetta 3y ago
Very nice. I was worried that conditionals would confuse it. But this passes: 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); } }
- akiarie 3y ago
  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 working as a whole. So you'll get more of these asserts if you try using `&&`, ternaries, and so on. We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43 https://github.com/xr0-org/xr0/issues/43
  - 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?

PennRobotics 3y ago

Plus, at -O1 and up, gcc optimizes this away, so the check itself is not well-defined as necessary. 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...)

gpderetta 3y ago
the if(0) was just to minimize the test case. if(variable) also fails. This doesn't need to be perfect though. Just incrementally better than the status quo.