6 ms·

Show HN: Xr0 – Vanilla C Made Safe with Annotations

17 points by akiarie 3y ago

Xr0 is a new static analyser that aims to make it possible to write vanilla C and get the same safety guarantees that are available other higher-level languages. We've been working on Xr0 for the past couple of months and are excited to share an early prototype. @betz47 and I are here to answer any questions.

deleted 3y ago
[deleted]
Alifatisk 3y ago
Reminds me of https://github.com/microsoft/checkedc https://github.com/microsoft/checkedc
lifthrasiir 3y ago
I'm glad that I wasn't the only persion pondering the similar thing (referring to the theses), but I'm not sure if the current direction can produce a small enough solution. For example I expected the following to work even with the currently restricted xlib: #include <stdlib.h> foo(int **pp) [ if (@pp) { .alloc *pp; } else { .undefined; } ] { *pp = malloc(4); // or: int *qq = malloc(4); *pp = qq; } It seems that `*pp` doesn't even work in the abstraction. (I originally tried structs, but realized that Xr0 currently doesn't support them.) This is crucial because you can't just do pattern matching against abstractions and axioms, there should be some sort of tactics that massage abstractions so that appropriate axioms can be used if any. Even keeping track of non-variable places (here `*qq`) is not trivial, please consider how to handle the commented code.
- akiarie 3y ago
  Appreciate the thinking and tinkering. Xr0 has a long way ahead of it before we have a fully-consistent, reliable syntax and set of axioms. For one thing, we delayed implementing the dereference operator `*p` because we were focused on getting our basic model to work with loops (which led us to focus on the array-indexing syntax, e.g. `p[0]`). The below works, but I note that quite a few meaningless or incorrect permutations of the abstract work (and shouldn't). #include <stdlib.h> foo(void **pp) [ .alloc pp[0]; ] { void *q; q = malloc(4); pp[0] = q; }
countWSS 3y ago
Seems like it has potential, try to run it for files in some open source projects like curl? Pick something gnarly with lots of string allocs.
- akiarie 3y ago
  Good thinking, but it's a bit early for real use — we'll be focused for the next couple of months on getting it self-hosting.
DamonHD 3y ago
I find it implausible that this can catch all the ways that C programmers actually do mess up (as one for ~40Y). I can make even languages such as Java leak memory even though it shouldn't be possible, nominally, so just knowing that something is returning heap-allocated memory somehow doesn't seem to help much. But I have only skimmed the page, so hopefully I am wrong!
schemescape 3y ago
How does it compare to existing static analysis tools for C? Any unique/new features? Does code using the annotations compile as is?
- akiarie 3y ago
  It's most similar to Frama-C/ACSL in terms of the annotative approach. What's most distinctive about Xr0 is it's built to be reliant on the programmer to structure the code in a way that is amenable to verification of safety. Another unique thing is that the annotation language is C-like and should be easy to pick up for programmers. The code will compile if the annotations are stripped, and we'll have a command to do this soon.
  - NonEUCitizen 3y ago
    Why not make annotations look like comments to Xr0-unaware C compilers? e.g. instead of starting with "[" , make annotations start with "//[" or "/*[" , making your example: void alloc1() //[ .alloc result; ] { return malloc(1); } Then it will be unnecessary to strip annotations.
    - akiarie 3y ago
      This is a really important question for us. I view it as an issue of tradeoffs. The advantage of putting the annotations in comments is C compilers can compile the code right away, which may make it easier for existing projects to adopt it. The disadvantage is that the annotations become second-class citizens, and will never feel native. Placing them in comments also means that they cannot have their own comments unless we introduce another comment sequence for the annotation environment. Again, it means that we can't use the preprocessor, so conditional compilation is impossible. So basically, we're trading some compatibility for nicer, native-like source. For us, "beauty is the first test", and we believe that there's no way for the source to be beautiful if we put the annotations in comments.
      - ithkuil 3y ago

17 points by akiarie 3y ago

deleted 3y ago

[deleted]

Alifatisk 3y ago

Reminds me of https://github.com/microsoft/checkedc https://github.com/microsoft/checkedc

lifthrasiir 3y ago

I'm glad that I wasn't the only persion pondering the similar thing (referring to the theses), but I'm not sure if the current direction can produce a small enough solution. For example I expected the following to work even with the currently restricted xlib: #include <stdlib.h> foo(int **pp) [ if (@pp) { .alloc *pp; } else { .undefined; } ] { *pp = malloc(4); // or: int *qq = malloc(4); *pp = qq; } It seems that `*pp` doesn't even work in the abstraction. (I originally tried structs, but realized that Xr0 currently doesn't support them.) This is crucial because you can't just do pattern matching against abstractions and axioms, there should be some sort of tactics that massage abstractions so that appropriate axioms can be used if any. Even keeping track of non-variable places (here `*qq`) is not trivial, please consider how to handle the commented code.

akiarie 3y ago
Appreciate the thinking and tinkering. Xr0 has a long way ahead of it before we have a fully-consistent, reliable syntax and set of axioms. For one thing, we delayed implementing the dereference operator `*p` because we were focused on getting our basic model to work with loops (which led us to focus on the array-indexing syntax, e.g. `p[0]`). The below works, but I note that quite a few meaningless or incorrect permutations of the abstract work (and shouldn't). #include <stdlib.h> foo(void **pp) [ .alloc pp[0]; ] { void *q; q = malloc(4); pp[0] = q; }

countWSS 3y ago

Seems like it has potential, try to run it for files in some open source projects like curl? Pick something gnarly with lots of string allocs.

akiarie 3y ago
Good thinking, but it's a bit early for real use — we'll be focused for the next couple of months on getting it self-hosting.

DamonHD 3y ago

I find it implausible that this can catch all the ways that C programmers actually do mess up (as one for ~40Y). I can make even languages such as Java leak memory even though it shouldn't be possible, nominally, so just knowing that something is returning heap-allocated memory somehow doesn't seem to help much. But I have only skimmed the page, so hopefully I am wrong!

schemescape 3y ago

How does it compare to existing static analysis tools for C? Any unique/new features? Does code using the annotations compile as is?

akiarie 3y ago
It's most similar to Frama-C/ACSL in terms of the annotative approach. What's most distinctive about Xr0 is it's built to be reliant on the programmer to structure the code in a way that is amenable to verification of safety. Another unique thing is that the annotation language is C-like and should be easy to pick up for programmers. The code will compile if the annotations are stripped, and we'll have a command to do this soon.
- NonEUCitizen 3y ago
  Why not make annotations look like comments to Xr0-unaware C compilers? e.g. instead of starting with "[" , make annotations start with "//[" or "/*[" , making your example: void alloc1() //[ .alloc result; ] { return malloc(1); } Then it will be unnecessary to strip annotations.
  - akiarie 3y ago
    This is a really important question for us. I view it as an issue of tradeoffs. The advantage of putting the annotations in comments is C compilers can compile the code right away, which may make it easier for existing projects to adopt it. The disadvantage is that the annotations become second-class citizens, and will never feel native. Placing them in comments also means that they cannot have their own comments unless we introduce another comment sequence for the annotation environment. Again, it means that we can't use the preprocessor, so conditional compilation is impossible. So basically, we're trading some compatibility for nicer, native-like source. For us, "beauty is the first test", and we believe that there's no way for the source to be beautiful if we put the annotations in comments.
    - ithkuil 3y ago