4 ms·

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
      > [..] another comment sequence void alloc1() //[ .alloc result; ] // it allocates! If the annotation opening block is always `//[` you have intuitive C comments within that line (either another line comment or a /* / section inside that line. Multiline /*/ comments starting on that line wouldn't be allowed but that would be following the established C preprocessor rules and thus won't surprise any user nor editor/syntax-highlighter. That said, I do agree with your concerns around first-class-ness of syntax annexes for language extensions. The main advantage of using some form of hack exploiting comments is that the existing ecosystem (syntax-highligters, code formatters, auto completion, ...) would keep working. But how code auto formatters would work depend on the details. E.g. I didn't try how would popular auto formatters handle the example above.
    - sigsev_251 3y ago
      Then why not use the standard attribute syntax with a custom namespace (for example `[[xr0::alloc(result)]]`)? Compilers ignore attributes they do not implement (They may issue a warning, but one can either turn off that warning, or use macros to conditionally include the attributes).
      - akiarie 3y ago
        We'll think this through. (Honestly, we've been focused on C89 and I heard about C23 attributes today.)

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
    > [..] another comment sequence void alloc1() //[ .alloc result; ] // it allocates! If the annotation opening block is always `//[` you have intuitive C comments within that line (either another line comment or a /* / section inside that line. Multiline /*/ comments starting on that line wouldn't be allowed but that would be following the established C preprocessor rules and thus won't surprise any user nor editor/syntax-highlighter. That said, I do agree with your concerns around first-class-ness of syntax annexes for language extensions. The main advantage of using some form of hack exploiting comments is that the existing ecosystem (syntax-highligters, code formatters, auto completion, ...) would keep working. But how code auto formatters would work depend on the details. E.g. I didn't try how would popular auto formatters handle the example above.
  - sigsev_251 3y ago
    Then why not use the standard attribute syntax with a custom namespace (for example `[[xr0::alloc(result)]]`)? Compilers ignore attributes they do not implement (They may issue a warning, but one can either turn off that warning, or use macros to conditionally include the attributes).
    - akiarie 3y ago
      We'll think this through. (Honestly, we've been focused on C89 and I heard about C23 attributes today.)