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.
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.
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?
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.
> 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.
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.
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.
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.
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.
The trouble with warnings is every compiler has a different set of warnings. It balkanizes the language. Many D features are the result of cherry picking warnings from various compilers and making them standard features.
Not really, as C has had even more diverse implementations per-standardization. I would say the situation is now, much less diverse under the rule of GCC and Clang. (Yeah MSVC also exists.)
Every switch that changes the language semantics creates a separate language. If you have n such switches, your compiler is supporting n x n languages. I've also had troubles writing portable C code with all warnings enabled as different compilers contradicted each other on what was acceptable.
I tried pretty hard to make D a warning-less language, but still some crept in grump grump.
Have fun with this one:
for (int i = 0; i < end; ++i);
foo(i);
One of the best programmers I know came up to me with this loop and told me my C compiler was broken because the loop was only executed once. I pointed at the ; and you can guess the rest.
I added a warning for that in the C compiler, and for D simply disallowed it. I've noticed that some C compilers have since added a warning for that as well. The C folks should just make it illegal.
I've also fixed printf in D so that:
char* p;
printf("%d\n", p);
gives an error message, and the right format to use for `p`. It was a little thing, but it sure found a lot of incorrect formats in my code.
> I've also fixed printf in D so that [...] gives an error message
Just last week I had the case that the C compiler complained, I should use %lld for long long, but the printf implementation shipped with the compiler doesn't support that. Thus, using %ld, even if undefined behaviour was the correct action. I wouldn't like my language making up more work for me for no reason.
Then anyone reading your code will know the empty loop was intentional. BTW, many C compilers warn about the ; on a for loop.
Have you ever discovered this bug:
if (condition);
doThis();
It's a hard one to see in a code review. Yes, that's also disallowed in D.
> I should use %lld for long long, but the printf implementation shipped with the compiler doesn't support that.
Weird that your compiler would support long long, but with a broken Standard library. I don't see that as a feature. You can always cast the argument to long, and at least you won't get undefined behavior.
C compilers without arguments start in 'trust me and shut up mode'. Seems to be sensible to me, because the 'I don't care about correctness' typically coincides with writing throwaway code, while you surely have the time to add compiler arguments when you set up the build system for an actual project.
Making something a valid program that shouldn't be. Thus, potentially creating/hiding bugs. I also explicitly invoke UB on all the code paths I do not want to be valid.
I've had the pleasure of spending many hours hunting down an uninitialized variable, as its value would change anytime I got close to it. BTW, if you really, really, want an uninitialized variable:
I don't think preventing the bug is what's being objected to. Rather that the proposed solution replaces one buggy program with another. If people are inadvertently forgetting to initialize things then you should simply halt compilation when you detect that.
To be clear I think D default initializing is better than C leaving uninitialized. I just don't think it's optimal since the issue isn't one of convenience but rather bug prevention.
I can't possibly be the first - several other comments here are saying the same thing including the one I was trying to clarify with you.
I don't dislike it per se. I think it's an improvement over not having it but I also think that it's sub-optimal in many scenarios when compared to simply failing the build. Since it's a tradeoff to prevent bugs at the expense of language brevity I don't think it should be surprising that not everyone agrees about it.
My personal preference is the "void" that D has for uninitialized in addition to empty braces or something similarly terse for default initialization.
Slight tangent but somehow C++ ended up with the worst of all possible worlds. Some types uninitialized by default, other types default initialized, terse initialization syntax variants that look highly similar but do different things, and much of it context dependent.
D is consistent in that structs also default initialize:
struct S { int a; float f; }
S s;
For C, having an error when the initializer is omitted is better than nothing. However, that is not part of the C Standard, and you'll be relying on having a C compiler with that extension. Otherwise there is undefined behavior. To do it right means it needs to be standardized.
In general, symbolic execution will consider all code paths. If it can't (or doesn't want to) prove that the condition is always true or false it will check that the code is correct in two cases: (1) true branch taken, (2) false branch taken.
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.
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.
Are you implying that Fil-C has this sort of reaction to people confused about why it does certain things in the name of safety, or are you saying Fil-C is just sprinkling magic fairy dust on C and declaring it safe?
> just analyze all possible branches and seek convergence.
This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings?
For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships?
Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations.
Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.
There will always be valid programs that are nonetheless rejected by some verifier (Rice's theorem). That is, programs that have really nothing wrong but nonetheless are rejected as invalid
In those cases you generally try to rewrite it in another way
Isn’t this a very restrictive way to write? Hard for me to imagine as never wrote with such annotations so no idea how viable it is for a large codebase to have this constraint.
Sure, but you want restrictions. You can't get an annotation that magically eliminates (de)allocation errors. It comes at a cost. The advantage of this particular proposal is its simplicity, I think. Otherwise, you'd have to get into contracts with complex expressions and then you'll have to prove those expression hold, and before you know it, your program is filled with proof statements. At least, that's my (limited) experience in SPARK, where you even can't have pointers.
As long as the verifier can be satisfied by wrapping the different results in a common type you should be fine. There has to be some way to appease it in that scenario as otherwise even trivial programs wouldn't be able to pass.
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.
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.
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.
For a company codebase maybe not but for solo projects yeah it can be, what exact options do you enable in clang tidy? Have they changed since the last version you used and now you need to change the config? Do you run cpp-check?
This version of Qt has leaks on exit so you need to ignore them when running asan/valgrind etc...
I agree it's not that hard and should be standard, same regarding enabling all warnings that are reasonable and enable warnings as errors.
> 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.
Show HN: Xr0 – Vanilla C Made Safe with Annotations (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, 2024-03-28, 41 comments)
Xr0: C but Safe (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, 2024-05-05, 4 comments)
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.
And they got stuck with the bounds checker and loops.
But other such checkers are far more advanced, with a better contract syntax.
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.
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.
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.
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.
Not really, as C has had even more diverse implementations per-standardization. I would say the situation is now, much less diverse under the rule of GCC and Clang. (Yeah MSVC also exists.)
I tried pretty hard to make D a warning-less language, but still some crept in grump grump.
Have fun with this one:
One of the best programmers I know came up to me with this loop and told me my C compiler was broken because the loop was only executed once. I pointed at the ; and you can guess the rest.I added a warning for that in the C compiler, and for D simply disallowed it. I've noticed that some C compilers have since added a warning for that as well. The C folks should just make it illegal.
I've also fixed printf in D so that:
gives an error message, and the right format to use for `p`. It was a little thing, but it sure found a lot of incorrect formats in my code.I often have code, which looks like this:
I wouldn't be happy about your policy.> I've also fixed printf in D so that [...] gives an error message
Just last week I had the case that the C compiler complained, I should use %lld for long long, but the printf implementation shipped with the compiler doesn't support that. Thus, using %ld, even if undefined behaviour was the correct action. I wouldn't like my language making up more work for me for no reason.
Have you ever discovered this bug:
It's a hard one to see in a code review. Yes, that's also disallowed in D.> I should use %lld for long long, but the printf implementation shipped with the compiler doesn't support that.
Weird that your compiler would support long long, but with a broken Standard library. I don't see that as a feature. You can always cast the argument to long, and at least you won't get undefined behavior.
Could do that I just don't like the look. :-)
> Have you ever discovered this bug:
Actually no, because the coding style I use either puts it on a single line or with braces. I never indent just a single line.
So:
or: > Weird that your compiler would support long long, but with a broken Standard library.Yeah, for your information it was GCC combined with newlib for arm-none-eabi shipped with Debian/MS Windows.
Those are not what I was mentioning. It was the use of ; immediately following for(). No loop body.
> Have you ever discovered this bug: [...]
Why? What does it cost you?
To be clear I think D default initializing is better than C leaving uninitialized. I just don't think it's optimal since the issue isn't one of convenience but rather bug prevention.
I don't dislike it per se. I think it's an improvement over not having it but I also think that it's sub-optimal in many scenarios when compared to simply failing the build. Since it's a tradeoff to prevent bugs at the expense of language brevity I don't think it should be surprising that not everyone agrees about it.
My personal preference is the "void" that D has for uninitialized in addition to empty braces or something similarly terse for default initialization.
Slight tangent but somehow C++ ended up with the worst of all possible worlds. Some types uninitialized by default, other types default initialized, terse initialization syntax variants that look highly similar but do different things, and much of it context dependent.
if (turing_machine_halts(tm)) return malloc(1); else return NULL;
How is this handled?
This is "valid" C, but I wholly support checking tools that reject it.
This sounds like a very simple form of abstract interpretation, how do you handle the issues it generally brings?
For example if after one branch you don't converge, but after two you do, do you accept that? What if this requires remembering the relationship between variables? How do you represent these relationships?
Historically this has been a tradeoff between representing the state space with high or perfect precision, which however can require an exponential amount of memory/calculations, or approximate them with an abstract domain, which however tend to lose precision after performing certain operations.
Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.
you should refactor so that it's representable.
> Add dynamically sized values (e.g. arrays) and loops/recursion and now you also need to simulate a possibly unbounded number of iterations.
regions are hard. You kinda have to reject regions that are not uniform. loops you can find a fixpoint for.
In those cases you generally try to rewrite it in another way
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?
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.
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.
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.
This version of Qt has leaks on exit so you need to ignore them when running asan/valgrind etc...
I agree it's not that hard and should be standard, same regarding enabling all warnings that are reasonable and enable warnings as errors.
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.