6 ms·

Xr0 verifier, guarantee the safety of C programs at compile time

114 points by Alifatisk 10mo ago

pkhuong 10mo ago
I don't see any explanation of what niche this targets relative to pre-existing tools like Checked C, CMBC, or Frama C...
aw1621107 10mo ago
Previously: Show HN: Xr0 – Vanilla C Made Safe with Annotations (https://news.ycombinator.com/item?id=37536186 https://news.ycombinator.com/item?id=37536186, 2023-09-16, 13 comments) Xr0 Makes C Safer than Rust (https://news.ycombinator.com/item?id=39858240 https://news.ycombinator.com/item?id=39858240, 2024-03-28, 41 comments) Xr0: C but Safe (https://news.ycombinator.com/item?id=39936291 https://news.ycombinator.com/item?id=39936291, 2024-04-04, 144 comments) Show HN: Xr0 is a Static Debugger for C (https://news.ycombinator.com/item?id=40472051 https://news.ycombinator.com/item?id=40472051, 2024-05-05, 4 comments)
- tialaramex 10mo ago
  Thanks! I thought this felt familiar. 2023 is a long time to still be in this "Initial signs are promising" mode. There are no code commits since March 2025. I've had projects which stalled for a few months or even a year, but generally if I said I'll get to it "soon" and two years later I haven't, that's not getting done. There are two boxes of books I planned to unbox "soon" after discovering that the bookshelves for my new flat were full & so I had nowhere to put them. That was when Obama was still President of the United States of America. Don't expect me to ever get around to unboxing those books, I clearly haven't even missed them.
  - muldvarp 10mo ago
    The initial sign for Xr0 never seemed promising for anyone with experience in formal verification. Neither the code nor the ideas they presented were new. I asked them multiple times to clarify how their project differed from the dozens of already existing options for formal verfication of C programs and never got a concrete answer.
    - tgv 10mo ago
      As I see it: tracking (de)allocation in a very simple, understandable way. Unfortunately, that seems to be all it does. It's a start, certainly if you don't want to/cannot use a more complete system, since they can be quite complex. I'm not following this space professionally, only out of interest a bit, but do you know of a system that is so simple?
      - muldvarp 10mo ago
        Xr0 isn't any simpler than for example Frama-C. In fact one of the simplest (but still useful) systems for statically tracking ownership is Rusts borrow checker, which the authors of Xr0 say is _too_ simple.
  - rurban 10mo ago
    Well, apparently someone rewrote it in rust, which was better than their version. Which they needed some time to process how to continue. And they got stuck with the bounds checker and loops. But other such checkers are far more advanced, with a better contract syntax.
thealistra 10mo ago
What happens if a function allocates not deterministically, like if (turing_machine_halts(tm)) return malloc(1); else return NULL; How is this handled?
- jonhohle 10mo ago
  NULL is a valid return for malloc. Wouldn’t that case already be handled?
- dnautics 10mo ago
  as someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.
  - dwattttt 10mo ago
    Rust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas! This is "valid" C, but I wholly support checking tools that reject it.
    - dnautics 10mo ago
      exactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?
      - dnautics 10mo ago
        i made a quip and realized that's not a bad description of what fil-c does
        throwaway17_17 10mo ago
jokoon 10mo ago
Does it require annotations or can it validate any c code? It's odd that so many people promote rust, yet we don't even use static analysis and validators for c or C++. How about enforcing coding standards automatically first, before switching to a new language?
- RossBencina 10mo ago
  > we don't even use static analysis and validators for c or C++ There is some use, how much I don't know. I guess it should be established best practice by now. Also run test suites with valgrind. Historically many of the C/C++ static analyzers were proprietary. I haven't checked lately but I think Coverity was (is?) free for open source projects.
- haileys 10mo ago
  Not sure what this post has to do with Rust, but people do use static analysis on C and C++. The problem is that C and C++ are so flexible that retrofitting static verification after the fact becomes quite difficult. Rust restricts the shape of program you are able to write so that it's possible to statically guarantee memory safety. > Does it require annotations or can it validate any c code? If you had clicked through you would see that it requires annotations.
- 01HNNWZ0MV43FF 10mo ago
  Today's experts are the novices of 40 years ago, and today's novices will be the experts in 40 years. C and C++ don't require static analysis, and it's difficult to set up, and so most of us slide down the incentive gradient of using C / C++ without any helpers except CMake and gdb. Rust requires it, so the noobies use it, so in 40 years the experts will accept it.
  - ranger_danger 10mo ago
    > it's difficult to set up Is it though? I've only ever had to run "scan-build make" for my projects and it spits out a full folder of HTML pages that details any static analysis issues, and I didn't have to change my build system at all.
WalterBright 10mo ago
From the tutorial: #include <stdio.h> int main() { int i; return i; } the behaviour is undefined because i’s value is indeterminate. D solves that problem by initializing variables with the default initializer (in this case 0) if there is not an explicit initializer. That was in the first version of D because I have spent days tracking down an erratic bug that turned out to be an uninitialized variable.
- WalterBright 10mo ago
  BTW, when D compiles C code, it will default initialize the C variables, too.
- dadoum 10mo ago
  I think that the right thing to do is to error out though. When the behaviour of some code cannot be guaranteed, that code should just be ruled out imo. Manually initializing a variable generally doesn't clutter the code, arguably it's making it clearer.
  - Alifatisk 10mo ago
    Dart does this, you can mark a variable as "late" which tells the compiler that you know for certain the variable will be written too before read. If something reads the variable before it's initialized, then the runtime will error. Maybe even on compile time if it can be caught, I am not certain.
- pseudohadamard 10mo ago
  Pretty much any existing C compiler will also solve that problem by telling you that it's uninitialized.
  - WalterBright 10mo ago
    I tried: int test() { int i; return i; } using clang on my Mac mini, and: clang -c test.c and it compiled without complaint.
Animats 10mo ago
Cute. They've introduced ownership to C. The annotation system is expressing ownership, in a rather clunky way. You have to explicitly declare that functions create or release allocated space. That's ownership tracking. But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem.
- LiamPowell 10mo ago
  > But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem. It's not particularly difficult for the prover. You essentially just need to do a translation from C in to your ATP language of choice, with a bunch of constraints that check undefined behaviour never occurs. Tools such as Frama-C and CBMC have supported this for a long time. The difficult part is for the user as they need to add assertions all over the place to essentially keep the prover on the right track and to break down the program in to manageable sections. You also want a bunch of tooling to make things easier for the user, which is a problem that can be as difficult as you want it to be since there's always going to be one more pattern you can detect and add a custom handler/error message for.
  - Animats 10mo ago
    > It's not particularly difficult for the prover. I know that. Did that decades ago. I wanted to see how they did the annotations and proofs. What can you express? Partially filled arrays are moderately hard. Sparsely initialized arrays need a lot of scaffolding. This is an area where most "safe C" variants have foundered.
- rwmj 10mo ago
  Oddly they didn't even reuse the annotation for this that GCC already has: https://stackoverflow.com/questions/18485447/gcc-attribute-malloc https://stackoverflow.com/questions/18485447/gcc-attribute-m...
- 1718627440 10mo ago
  > Cute. They've introduced ownership to C. Ownership semantics are described in every serious C interface. Linters for checking it have also existed for decades. I find the notion that Rust invented it to be incredible stupid. Rust just has different ownership semantics and makes it an enforced part of the language (arguable a good idea). And yes they of course also do bounds-checking.

114 points by Alifatisk 10mo ago

I don't see any explanation of what niche this targets relative to pre-existing tools like Checked C, CMBC, or Frama C...

aw1621107 10mo ago

Previously: Show HN: Xr0 – Vanilla C Made Safe with Annotations (https://news.ycombinator.com/item?id=37536186 https://news.ycombinator.com/item?id=37536186, 2023-09-16, 13 comments) Xr0 Makes C Safer than Rust (https://news.ycombinator.com/item?id=39858240 https://news.ycombinator.com/item?id=39858240, 2024-03-28, 41 comments) Xr0: C but Safe (https://news.ycombinator.com/item?id=39936291 https://news.ycombinator.com/item?id=39936291, 2024-04-04, 144 comments) Show HN: Xr0 is a Static Debugger for C (https://news.ycombinator.com/item?id=40472051 https://news.ycombinator.com/item?id=40472051, 2024-05-05, 4 comments)

tialaramex 10mo ago
Thanks! I thought this felt familiar. 2023 is a long time to still be in this "Initial signs are promising" mode. There are no code commits since March 2025. I've had projects which stalled for a few months or even a year, but generally if I said I'll get to it "soon" and two years later I haven't, that's not getting done. There are two boxes of books I planned to unbox "soon" after discovering that the bookshelves for my new flat were full & so I had nowhere to put them. That was when Obama was still President of the United States of America. Don't expect me to ever get around to unboxing those books, I clearly haven't even missed them.
- muldvarp 10mo ago
  The initial sign for Xr0 never seemed promising for anyone with experience in formal verification. Neither the code nor the ideas they presented were new. I asked them multiple times to clarify how their project differed from the dozens of already existing options for formal verfication of C programs and never got a concrete answer.
  - tgv 10mo ago
    As I see it: tracking (de)allocation in a very simple, understandable way. Unfortunately, that seems to be all it does. It's a start, certainly if you don't want to/cannot use a more complete system, since they can be quite complex. I'm not following this space professionally, only out of interest a bit, but do you know of a system that is so simple?
    - muldvarp 10mo ago
      Xr0 isn't any simpler than for example Frama-C. In fact one of the simplest (but still useful) systems for statically tracking ownership is Rusts borrow checker, which the authors of Xr0 say is _too_ simple.
- rurban 10mo ago
  Well, apparently someone rewrote it in rust, which was better than their version. Which they needed some time to process how to continue. And they got stuck with the bounds checker and loops. But other such checkers are far more advanced, with a better contract syntax.

thealistra 10mo ago

What happens if a function allocates not deterministically, like if (turing_machine_halts(tm)) return malloc(1); else return NULL; How is this handled?

jonhohle 10mo ago
NULL is a valid return for malloc. Wouldn’t that case already be handled?
dnautics 10mo ago
as someone building an analyzer for zig, if you sent something like this through the system im building, it would get handled by Zig's optional type tagging; but lets say you did "free" (so your result is half freed, half not freed): it would get rejected because both branches produce inconsistent type refinements, you don't have to solve the halting problem, just analyze all possible branches and seek convergence.
- dwattttt 10mo ago
  Rust is the poster child for these complaints, but this is a great example of "the language rejects a valid program". Not all things that can be expressed in C are good ideas! This is "valid" C, but I wholly support checking tools that reject it.
  - dnautics 10mo ago
    exactly! "guaranteeing the safety of C" sir what did you think that meant, sprinkling magic fairy dust to make it work!!?
    - dnautics 10mo ago
      i made a quip and realized that's not a bad description of what fil-c does
      - throwaway17_17 10mo ago

jokoon 10mo ago

Does it require annotations or can it validate any c code? It's odd that so many people promote rust, yet we don't even use static analysis and validators for c or C++. How about enforcing coding standards automatically first, before switching to a new language?

RossBencina 10mo ago
> we don't even use static analysis and validators for c or C++ There is some use, how much I don't know. I guess it should be established best practice by now. Also run test suites with valgrind. Historically many of the C/C++ static analyzers were proprietary. I haven't checked lately but I think Coverity was (is?) free for open source projects.
haileys 10mo ago
Not sure what this post has to do with Rust, but people do use static analysis on C and C++. The problem is that C and C++ are so flexible that retrofitting static verification after the fact becomes quite difficult. Rust restricts the shape of program you are able to write so that it's possible to statically guarantee memory safety. > Does it require annotations or can it validate any c code? If you had clicked through you would see that it requires annotations.
01HNNWZ0MV43FF 10mo ago
Today's experts are the novices of 40 years ago, and today's novices will be the experts in 40 years. C and C++ don't require static analysis, and it's difficult to set up, and so most of us slide down the incentive gradient of using C / C++ without any helpers except CMake and gdb. Rust requires it, so the noobies use it, so in 40 years the experts will accept it.
- ranger_danger 10mo ago
  > it's difficult to set up Is it though? I've only ever had to run "scan-build make" for my projects and it spits out a full folder of HTML pages that details any static analysis issues, and I didn't have to change my build system at all.

WalterBright 10mo ago

From the tutorial: #include <stdio.h> int main() { int i; return i; } the behaviour is undefined because i’s value is indeterminate. D solves that problem by initializing variables with the default initializer (in this case 0) if there is not an explicit initializer. That was in the first version of D because I have spent days tracking down an erratic bug that turned out to be an uninitialized variable.

WalterBright 10mo ago
BTW, when D compiles C code, it will default initialize the C variables, too.
dadoum 10mo ago
I think that the right thing to do is to error out though. When the behaviour of some code cannot be guaranteed, that code should just be ruled out imo. Manually initializing a variable generally doesn't clutter the code, arguably it's making it clearer.
- Alifatisk 10mo ago
  Dart does this, you can mark a variable as "late" which tells the compiler that you know for certain the variable will be written too before read. If something reads the variable before it's initialized, then the runtime will error. Maybe even on compile time if it can be caught, I am not certain.
pseudohadamard 10mo ago
Pretty much any existing C compiler will also solve that problem by telling you that it's uninitialized.
- WalterBright 10mo ago
  I tried: int test() { int i; return i; } using clang on my Mac mini, and: clang -c test.c and it compiled without complaint.

Animats 10mo ago

Cute. They've introduced ownership to C. The annotation system is expressing ownership, in a rather clunky way. You have to explicitly declare that functions create or release allocated space. That's ownership tracking. But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem.

LiamPowell 10mo ago
> But "We currently model all buffers as infinitely-sized. We will be adding out-of-bounds checking soon." That's the hard problem. It's not particularly difficult for the prover. You essentially just need to do a translation from C in to your ATP language of choice, with a bunch of constraints that check undefined behaviour never occurs. Tools such as Frama-C and CBMC have supported this for a long time. The difficult part is for the user as they need to add assertions all over the place to essentially keep the prover on the right track and to break down the program in to manageable sections. You also want a bunch of tooling to make things easier for the user, which is a problem that can be as difficult as you want it to be since there's always going to be one more pattern you can detect and add a custom handler/error message for.
- Animats 10mo ago
  > It's not particularly difficult for the prover. I know that. Did that decades ago. I wanted to see how they did the annotations and proofs. What can you express? Partially filled arrays are moderately hard. Sparsely initialized arrays need a lot of scaffolding. This is an area where most "safe C" variants have foundered.
rwmj 10mo ago
Oddly they didn't even reuse the annotation for this that GCC already has: https://stackoverflow.com/questions/18485447/gcc-attribute-malloc https://stackoverflow.com/questions/18485447/gcc-attribute-m...
1718627440 10mo ago
> Cute. They've introduced ownership to C. Ownership semantics are described in every serious C interface. Linters for checking it have also existed for decades. I find the notion that Rust invented it to be incredible stupid. Rust just has different ownership semantics and makes it an enforced part of the language (arguable a good idea). And yes they of course also do bounds-checking.