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.
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.
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?
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.
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.
#include <stdio.h>
int main()
{
int i;
return i;
}
the behaviour is undefined because i’s value is indeterminate.
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.
int test()
{
int i;
return i;
}
clang -c test.c
> clang -Wall test.c
test.c:4:16: warning: variable 'i' is uninitialized when used here [-Wuninitialized]
4 | return i;
| ^
test.c:3:14: note: initialize the variable 'i' to silence this warning
3 | int i;
| ^
| = 0
1 warning generated.
warning C4700: uninitialized local variable 'i' usedBut "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.
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.
pkhuong•1d ago