Xr0: C but Safe
xr0.dev
xr0.dev
These should be table stakes when talking about "safe" languages (or subsets thereof); I hope these authors have or propose plans for these classes as well!
(I agree with the more general critique here, that any adaptation invasive enough to provide these properties in C might as well be its own programming language.)
Xr0 is not limited to memory-safety, its goal is to eliminate the possibility of writing C code that results in undefined behaviour. A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Think of Xr0 as a wrapper to C that guarantees you don't violate C's safety semantics.
(Other proposals that I’m aware of seek to forbid those parts of the language outright, or add some kind of runtime instrumentation like isoheaps. Neither of these is particularly palatable for pre-existing codebases with deep, undocumented language feature and ABI assumptions!)
Like this idea a lot. Does that mean it could be used to convert C projects in a strangler pattern style?
This obviously covers type safety, but also spatial memory safety, and can be extended to temporal memory safety, and even some concurrency aspects.
This has been proven for fairly large subsets of programming languages and even some full languages (like SML). Unfortunately, it doesn't hold for most mainstream ones, because programming language theory is often ... under-used ... among language designers.
I would add that temporal safety is significantly harder than spatial safety (spatial safety is only hard in C if you do not want to break the ABI), so it is nice that this project is focusing on it.
"Safe" and "safety" are very overloaded English words that come with a lot of baggage, and perhaps it would be prudent to stop using these broad, nonspecific terms for things like programming languages.
"Memory safety" is a coherent, reasonably well-defined concept, and it's fine to talk about something like that. But what does a broadly, generically "safe" programming language even mean?
A program is safe if it remains well-behaved regardless of inputs. A safe language necessarily constructs such programs. It turns out Memory Safety is a necessary part of this.
The reason this is awkward is that it turns out that languages such as Go do not meet this requirement because they exhibit UB under some data races. There are three ways out of this, which are interesting to contemplate
1. No concurrency. Languages which simply don't have concurrency are fine in this respect, e.g. Python, as are (so long as you don't try to have concurrency) older versions of C and even C++ which simply decline to explain how concurrency is even possible - if you're using say POSIX threads from C89 that's a problem because in C89 concurrency doesn't exist so none of your programs have any meaning whatsoever even if they don't race...
2. Rust's trick, mutation XOR multiple references - you can't write a data race in (safe) Rust, so even though the language has concurrency it's fine, you can't trip yourself this way.
3. Java and OCaml's trick, survive despite loss of Sequential Consistency. The proof we have is SC/DRF - using this construction a program is Sequentially Consistent if it is Data Race Free, but if we can survive loss of Sequential Consistency then this proof isn't important. This is enormously difficult, like it's easily the sort of work that could earn you a PhD if you don't have one already. We also still don't know whether it's potentially worth it. For Java the answer was "No" but for OCaml it's too early to say.
Edited to add: Marked that just not having concurrency only avoids data races, it doesn't magically fix all the other problems C and C++ have for example.
(I can't find anything about it in this page)
Avoiding UB in single threaded programs is the easy part. It's harder for a low level language like C, but not too hard.
But avoiding UB in multithreaded programs is very very hard. Many "safe" managed languages have UB when you misuse synchronization mechanisms, like Go.
Some languages Java and OCaml manage to avoid UB when you have data races. They do so by disallowing some compiler optimizations. OCaml is the better one in this regard (see the paper "bounding data races in time and space")
Is there any proposal or rough ideas or musings or anything that might suggest how Xr0 could possibly guarantee data race freedom?
Would it be something like Rust's Send & Sync traits? Or something else entirely?
I don't see why I would ever choose this over Frama-C which basically does the same (and is actually battle-tested). I just don't see a niche:
- No full control over runtime needed: Java, C#, Python, ...
- Full control over runtime and memory safety: Rust
- Full control over runtime, memory safety and provable absence/presence of certain behaviors (i.e. aerospace, nuclear reactors, ...): Frama-C, CBMC, Astree, ...
Where does Xr0 fit in and how does it differ from existing technology? The fact that they don't even mention any of those tools makes me believe that they are either not aware of them or that they are aware and the difference between this and Frama-C is just syntactic. Not a good look either way.
What is significant about Xr0 is how it applies these old ideas. Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
I don't think you're under any obligation, I just think that not discussing prior art is a bad look.
> What is significant about Xr0 is how it applies these old ideas.
I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
> Xr0 is designed for programmers rather than mathematicians, so to us syntax matters a great, great deal.
Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
See [0] where our reliance on Dijkstra is transparent.
> I don't see anything new about the application of these well-known ideas either. Especially nothing that could explain why Xr0 would be widely used, while Frama-C is extremely niche.
Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
> Proving (the correctness of code) is an inherently mathematical task. So if by "mathematician" you mean someone who does mathematics, then all of your users will be mathematicians.
Absolutely true. But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
(Edit: forgot to add link.)
Mentioning that you're vaguely inspired by Dijkstra is not the same as discussing prior art. And it's not like there isn't enough prior art about "safe C" out there [0, 1, 2, 3, 4, 5, 6, 7, 8, 9].
> Begin with the fact that Xr0 is written in C and feels like C. We're building it so that C programmers will be able to use it without explicitly learning about formal verification.
Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
> But what I mean by "mathematician" is a self-conscious mathematician, or at least someone with a background in formal mathematics.
I'm doubtful Xr0 will be useful for someone without a background in formal verification.
To me, the whole project seems like vapourware. It currently works on an extremely limited subset of C. In fact, this subset is so limited that from a computation theory standpoint, the current capabilities of Xr0 are trivial. Supporting while loops (or general recursion) on the other hand is impossible (from a computation theory standpoint).
Even on this small subset of C it took me five minutes to get an out of memory error and a further five minutes to craft a C program with a double free that passes verification [10].
All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
[0]: https://link.springer.com/chapter/10.1007/978-3-642-03359-9_...
[1]: https://link.springer.com/chapter/10.1007/978-3-540-71316-6_...
[2]: https://link.springer.com/chapter/10.1007/978-3-642-33826-7_...
[3]: https://ieeexplore.ieee.org/document/8543387
[4]: https://dl.acm.org/doi/10.1145/2594291.2594296
[5]: https://link.springer.com/chapter/10.1007/978-3-642-32347-8_...
[6]: https://link.springer.com/chapter/10.1007/978-3-642-20398-5_...
[7]: https://dl.acm.org/doi/10.1145/503272.503286
[8]: https://www.sciencedirect.com/science/article/pii/S157106611...
Nice work with the program. However, the only reason it verifies is we haven't yet implemented `||`, so in the parser the phrase `if (x || !y)` is being interpreted as `if (x)` (see [0] for the relevant production). This may seem like another frustrating indiction of how "extremely limited" the subset of C that Xr0 works on is, and indeed it is. But the most important point is there is no logical flaw in Xr0's design here, and no reason whatever that an error of this kind wouldn't be detected. [1] is an equivalent program that shows the logical cogency of our approach (I know it's ugly!).
> I'm doubtful Xr0 will be useful for someone without a background in formal verification.
> Most of the people interested in formally verifying their C code will already know about formal verification and absolutely don't care about whether Xr0 is written in C or not.
We aren't making Xr0 for people (self-consciously) interested in formal verification, but for C programmers interested in safety of the kind that Rust provides. And I can tell you that C programmers prefer their tools in C.
> All this combined with a website that makes great promises about how awesome Xr0 is (or rather going to be) and handwavy explanations about how easy adding the missing features will be that don't hold up to any scrutiny. Dozens of similar projects exist, few of them work at all on non-trivial C programs and all of them require herculean effort (and are thus only used for safety critical software) to correctly annotate C code (often this includes rewriting parts of the code to make the annotations simpler or unnecessary). There is no discussion at all how Xr0 is going to solve the problems that killed these projects.
Fair enough. The proof is in the pudding. Give us a few months. But understand that we have limited resources (this is an open source project and we're working on it part-time). We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
[0]: https://git.sr.ht/~lbnz/xr0/tree/master/item/src/ast/gram.y#...
You should error on constructs you don't yet support. Not doing so makes it very difficult to ascertain how well Xr0 works.
> We could either stop and make long-form arguments with full bibliographies or focus on building Xr0 into what we say it's going to be.
You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
You're right. We should. (We will be adding this as we are able.)
> You didn't do either though. You wrote long-form arguments about how awesome Xr0 is (or going to be) and how groundbreaking the idea of "interface formality" is. If instead you actually produced a working prototype (or even any technical argument why such a prototype is feasible) I'd be way less doubtful.
A 7-point blog post is hardly "long-form" :)
But more to the point, Rust has already achieved this "interface formality", as we state in the second paragraph of this "long-form" piece. That achievement on the part of Rust is indeed groundbreaking. Is it so crazy to claim that this can be replicated for C, without encumbering it with ownership considerations that have no relationship to interface formality?
Fair enough. We have a much more generous definition of "working prototype" than you do. Hopefully one day soon we'll have something that clears yours.
You're not replicating what Rust does, you're replicating what Frama-C does.
Then again, even just replicating what Rust does would be extremely difficult (if not impossible) given the pervasiveness of undefined behavior in C.
> Fair enough. We have a much more generous definition of "working prototype" than you do.
How many useful C programs do you know that require no loops and no binary operators?
Literally on the website. The purpose of the prototype is to show the feasibility of the approach we've taken, not to work on whole programs.
But it doesn't do that. You haven't shown that this approach is able to deal with loops and loops are pretty fundamental to every C program.
Heck, you haven't technically shown that this approach can deal with binary operators. I would love to turn Xr0 into an improptu SAT solver, but without `&&` and `||` that sadly isn't possible right now.
Xr0 is a work in progress, and we'll get there step-by-step.
Contract.Requires(start > 0);
Contract.Ensures(someReturn != null);
CONTRACT_REQUIRE(x == 0 || x == -1);
if(x) {
void* result = malloc(1);
CONTRACT_ENSURE(result != null);
CONTRACT_CALLER(free(result));
return result;
} else {
CONTRACT_ENSURE(result == 0);
return 0;
}
https://docs.rs/contracts/latest/contracts/
Ada has Design by Contract built into the language (not a library):
https://learn.adacore.com/courses/intro-to-ada/chapters/cont...
DbC is awesome because it formalizes what conditions must exist before and after a piece of code runs and defines who (caller vs. callee) is responsible for what parts.
void x() {
int * p;
p = malloc(1);
if(0) {
free(p);
} else {
free(p);
}
}
0v: src/ast/stmt/verify.c:228: stmt_sel_exec: Assertion `!ast_stmt_sel_nest(stmt)' failed.void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(!f) { free(p); } }
And this doesn't, as expected:
void x(int f) { int * p; p = malloc(1); if(f) { free(p); } if(f) { free(p); } }
edit: another assertion failure:
void x(int f) {
int * p;
p = malloc(1);
if(f) {
free(p);
}
f = !f;
if(f) {
free(p);
}
}We've put a fix in for this on a dev branch for now though: https://github.com/xr0-org/xr0/issues/43
void x(int a, int b) {
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
I'd be perfectly happy refactoring that so I could have an 'a or b' test (I'm assuming $something means that x(0, 0) not free-ing is correct in real code because nitpicking an illustrative example would be silly).
Though note that I'm sufficiently bad at tracking things right when writing C that I tend to spend most of my debugging time figuring out what stupid mistake I made to cause the current segfault - so I'm probably more willing than average to write code differently if it helps me avoid that ;)
Incidentally, you will notice that Xr0 rejects the program as is, which is correct (because of the double free). It can, however, accept code like the following:
void
foo(int a, int b)
{
int *p;
p = malloc(1);
if (a) {
if (!b) {
free(p);
}
}
if (b) {
free(p);
}
if (!a) {
if (!b) {
free(p);
}
}
}
[0]: https://github.com/xr0-org/xr0/tree/fix/nested-branching
void x(int a, int b) { if(! (a != b)) abort();
int * p;
p = malloc(1);
if(a) {
free(p);
}
if(b) {
free(p);
}
}
Great stuff anyway!
Edit: is the algorithm documented anyway? And there is any reason why you guys are not implementing it as a clang/GCC plugin and using the new C and C++ annotation syntax?
We haven't documented the algorithm because it's not the unique part of what we're doing. It works in a very simple-minded way, analysing possible states.
The interesting part is the insight that function interfaces are the boundary along which verification should take place. Applying this idea consistently we escape the combinatorial explosion which tends to plague efforts in this area, because every function can be verified by itself. Notably, Dafny recognised this point before us, and the earliest clear statement we can find regarding it is in Dijkstra's "Notes on Structured Programming", in his chapter "On a Program Model". You may find that illuminating read.
I'm no expert on Clang/GCC and the new annotation syntax for C and C++, but from what I've seen it's not general enough for what we're trying to achieve in Xr0. The safety semantics which are expressed in annotations in Xr0 (see [0] for an example) get very detailed.
[0]: https://xr0.dev/learn#initialisation-of-memory-and-the-clump
Re annotations, I meant the attribute syntax. You can have arbitrary custom syntax in it:
void foo(int *p) [[vx0::setup(p = .clump(sizeof(int))), vx0::body(*p = 0)]] {...}Does it always make sense to strictly enforce code that will be optimized/changed during compilation? Or does Xr0 run after compilation/linking?
How to handle things like unions where you want data in a nice mixed-type struct that is used locally and can also be sent as a stream of uint8_t over a wireless connection? Then, the last function that needs to use the memory frees it. Or is that still fine as long as you malloc once somewhere, free once somewhere, and annotate that the memory region will be accessed as more than one dereferenced type?
Much more important: Will the proposed changes be understandable enough for your average CS undergrad to learn in four months of halfway diligent study? (Then again, you might do away with students taking time to debug improper malloc/free and whatever else falls under the scope of Xr0...)
This doesn't need to be perfect though. Just incrementally better than the status quo.
Have you looked at them? Always good to look at prior art, it's not easy what you're trying to do.
Pretty sure I still have the CCured code lying around in a backup somewhere, I downloaded it and played with it long ago. If it's truly not available on the net anywhere, I suppose I can try to dig it up.
Are any of the many "safe versions of C" getting any traction? There have been so many. It's not a technical problem. It's a mindshare problem.
The future in this area may be something that takes in existing C code and uses a LLM to recognize idioms and annotate. Without some automated way to convert legacy code, this isn't going to happen.
(One big problem with converting to Rust is that Rust's data model is so far from C/C++ that you can't really convert much existing code. You have to rethink the design to fit the affine type model. That's hard.)
https://www.youtube.com/watch?v=Gij9UQy_JEQ
https://github.com/pizlonator/llvm-project-deluge/blob/delug...
Right now I'm ~90% through a major rewrite to use GC instead of isoheaps, because then I'll go from rewrite-a-bit (Fil-C previously required malloc calls to be annotated and for some unions to be changed) to rewrite-nothing (malloc will Just Work and so will unions).
I hope there are others also trying various alternatives. It's too soon for most of these things to tell what traction they may or may not get.
https://www.cs.purdue.edu/homes/rompf/papers/xhebraj-ecoop22...
I haven’t looked at what GCC has in a while because I don’t want to get gpl tainted. :-/
True, but that's likely going to be the case as well to convert to any ”safe version of C” as well, because in the general case the safety of a C program is undecidable: to make it safe, you have to restrict it to a subset of behaviors that can be statically proven as safe, and the borrow checker and “Rust's data model” is just that.
So there's no direct translation from a C++ object hierarchy to Rust structs.
The verbosity of the annotations is the most jarring thing at the beginning. However, do you find any of them unclear? Because we're optimising for similarity to C before terseness.
Though if one wants C and safety and a great language you can get there via, Rust -> Wasm -> C (via wasm2c).
It would be cool to see this applied to say, rsync.
If the annotation is basically just a copy of the function body why have any annotation at all?
> So it's not at all clear that we'll run into this.
It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
This is a profound question. Xr0 annotations seem to be copies of the function bodies, but they aren't actually. What they are is a description of the function's safety semantics, the side effects and circumstances under which the function may be relied upon to exhibit well-defined behaviour (under the C Standard).
They only seem to be copies of the bodies because we're dealing with simple examples in the post here and in the tutorial, but we have a much more significant program ready (documenting) that we'll be sharing soon that shows the difference more clearly.
Xr0 is built in explicit reliance upon the powers of programmers to structure code in such a way that the annotations become simpler and simpler as you move up layers of function abstraction. As a simple example, think about what happens when you allocate memory and free it within a function, e.g.
#include <stdlib.h>
void
foo() ~ [ return malloc(1); ]
{
return malloc(1);
}
void
bar()
{
void *p = foo();
free(p);
}
void
baz()
{
bar(); /* completely safe */
}
We call this simplifying phenomenon denouement, and well-designed programs exhibit it very strongly. Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
> It might not be clear to you, but if you want to allow any annotation with the same semantics as the body of the function you will run into this.
Yes, but we don't. Only well-defined behaviour according to the C Standard. This is the goal for Xr0 v1.0.0. After that the sky is the limit.
You're constantly dodging the question. If annotations aren't copies of function bodies (which is really the only sensible choice), you need to deduce whether a function body matches the annotations. "Structural similarity" between C and your annotation syntax won't make this easier. In fact, it is impossible to deduce whether two C functions are semantically equivalent even though C is extremely structurally similar to C (you could even argue that C and C are structurally identical).
> Our belief that programmers can design constructs that tend towards denouement as one moves down the call stack towards `main` is one of the basic reasons we're working on Xr0.
So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
Maybe I don't understand your point. I am not denying that we're deducing that the body matches the annotations. I'm simply saying that for the restricted case of safety semantics alone, this deduction can be done. Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body. If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
> So your main criticisms of Rust will mostly also apply to Xr0: You need to rewrite existing C code to make annotations practical (and at that point you might as well reimplement it in Rust) and Xr0 will limit the constructs you will use in your code, because annotations will be impractical for code that isn't written for "denouement".
Your quote omits the first sentence of the paragraph, which states that "well-designed programs exhibit [denouement] very strongly". Denouement in the sense we're referring to is an absolute theoretical necessity for any safe program, because at some level (of functional abstraction) the safety concerns must be handled, otherwise the program would have a safety vulnerability.
Xr0 definitely limits constructs, but our claim is that the limitation we're imposing is one that reflects the structure of all safe programs. The same cannot be said about Rust's ownership semantics, which limit an enormous number of simple, safe constructs. So the C programs to which one would be adding Xr0 annotations wouldn't need to be rewritten unless a bug has been discovered.
And I'm saying it can't be done, at least not in a fundamentally less tedious and hard way than Frama-C.
> Yes, it is impossible to deduce semantic equivalence of arbitrary functions. The question is whether it is possible to deduce that annotations capture the safety semantics of the body.
It isn't in general.
> If you have a concrete example it would be helpful here – but for the restricted concerns of safety, not for arbitrary constructs.
Safety is not a "restricted concern": You can for every property P easily construct a function that is safe if and only if property P holds. I'll be using Python because this example (which I like) requires arbitrary size integers. You could obviously also implement this in C, you'd just need to implement arbitrary size integers (or use a library that implements them):
def collatz(x):
if x % 2 == 0:
return x // 2
return x * 3 + 1
def cycle(f, x):
tortoise = f(x)
hare = f(f(x))
while tortoise != hare:
tortoise = f(tortoise)
hare = f(f(hare))
return hare
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element]) # this is safe (or is it?)
Another example would be a C program that generates random planar graphs, computes their chromatic numbers and then collects statistics about them in an `int statistics[5]`:
#include <stdio.h>
void main() {
int statistics[5] = {0};
for(int i = 0; i < 1000; i++) {
struct graph g = generate_random_planar_graph();
int chromatic_number = compute_chromatic_number(g);
statistics[chromatic_number] += 1;
}
printf("%i, %i, %i, %i", statistics[1], statistics[2], statistics[3], statistics[4]);
}
However, the main reason why this argument is flawed is it omits the heart of the matter: the annotations. Xr0 empowers programmers to propagate safety semantics. A program that is only safe if the Collatz conjecture holds is (surprise) only safe if the Collatz conjecture holds. So in Xr0 the only requirement we would impose is that this program be augmented with an annotation that communicates that it is only safe if the Collatz conjecture is true.
So the flaw in the reasoning is we haven't claimed that Xr0 can prove arbitrary programs are safe. We've claimed that Xr0 can prove the correspondence between the safety semantics denoted in an annotation and a function body. Above there are no annotations given which would specify "this program is safe only if the Collatz conjecture is true". It shouldn't be hard to prove the correspondence between such an annotation and the program you've written, e.g.:
def main(): ~ [
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element])
]
buffer = [0, 0, 0, 0, 0]
x = int(input())
if x >= 1:
collatz_cycle_element = cycle(collatz, x)
print(buffer[collatz_cycle_element])
That's the main function. It's the function that gets called when the program starts. Where do you want to propagate the "safety-determining factors" to?
If I'm just supposed to read the annotations on the `main` function (and those annotations can basically just be a copy of it's body), then why do I need the annotations at all? I could also read the program to determine whether it's safe.
If the program's safety depends on the semantics of C and how they've been used in a function, it will be possible to deal with all the conditions upon which a program could be unsafe (in the sense of the standard safety vulnerabilities – like those listed here [0]). Doing so would lead to denouement, so that the annotation to the main function would be empty (meaning none of those bugs can occur).
Programs that might be unsafe should not be verifiable.
[0]: https://alexgaynor.net/2020/may/27/science-on-memory-unsafet...
It really isn't. The second example is what a reasonable C programmer would produce if you asked them to collect statistics about the chromatic number of random planar graphs. It also isn't based on any open problem. It's overall a very reasonable C program and a small one at that. It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
I would love to see how you would write this reasonable program in a way that leads to "denouement".
> Programs that might be unsafe should not be verifiable.
Funnily enough, that's exactly what you criticize Rust for. It's not at all clear that writing programs with "denouement" is any less limiting than Rust. In fact, Frama-C (where you also try to write your code in such a way that the annotations become simpler) feels more limiting than Rust.
So will you admit that the first example has been sufficiently addressed? Because I was commenting on the problem involving the Collatz conjecture.
> It's safety also "depends on the semantics of C and how they've been used in a function", specifically on the fact that accessing an array is safe if and only if the index is in bounds. Out of bounds accesses to memory are probably the most common critical vulnerability in C programs, so it is essential that Xr0 prevents them.
True. As you said earlier:
> The safety of this program requires you to prove that `generate_random_planar_graph` always returns a planar graph, that `compute_chromatic_number` correctly identifies the chromatic number and that the chromatic number of every planar graph is less than 5.
This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
In that this specific program is obviously designed to be extremely hard to prove correct? Yeah. In that most real programs will be easier to prove correct automatically? No.
> This can obviously only be proven if we have the bodies of `generate_random_planar_graph` and `compute_chromatic_number`. Please provide these, and then I can attempt to answer. Because our whole point in Xr0 is that safety comes down to formalising interfaces – without interfaces for these functions we cannot investigate the safety of `main`.
What would be the point of that exactly? We both know that those functions would contain loops and as such Xr0 would be completely unable to verify them. We also know that Xr0 isn't actually able to state that `generate_random_planar_graph` generates a planar graph (other than completely repeating the body in the annotations, I guess). We also both know that Xr0 would not be able to deduce that the chromatic number of planar graphs is less than five.
I already provided two examples of programs the safety of which Xr0 will not be able to verify. I think it's your turn to produce a non-trivial C program that Xr0 will be able to handle.
This discussion really isn't all that enlightening, sadly. Xr0 can't currently handle loops and you haven't produced a single technical argument as to why I should expect Xr0 to be able to handle non-trivial loops in the future.
You also haven't produced a single technical argument as to why Xr0 should succeed where Frama-C failed. The argument that Frama-C is more general while Xr0 is specialized on safety is refuted easily as it is easy to come up with C programs the safety of which depends on arbitrary properties (and I would argue that many if not most real world C programs fall into this category).
But some programmers (like myself) love working in C, and do not like Rust's restrictions. For such programmers even if the question was one of re-implementation (which we don't think it is) Rust would remain undesirable.
Presumably it's easier to rewrite part of your app rather than the whole thing.
But I'm all for a safe version of C17 (or C23/24). It's so disappointing that there isn't a standard memory-safe compiler/runtime/ABI. (And while they're at it, the stack should grow up rather than down.)
Perhaps CHERI or similar will catch on someday. Maybe Apple could try implementing memory checking for clang and Apple Silicon.
It looks as though the idea is that you can annotate existing code, which is a lot easier than rewriting.
That's not necessarily true though.
Half decent C code already has a coherent memory management strategy. The problem is that humans can't follow even pretty straight-forward memory management strategies 100% of the time. If you have a function that returns memory the caller is required to free, or accepts a parameter that the function takes ownership of, that can be easily expressed but hard to get right every time.
In fact, functions typically document this... in half-decent C code. So we're really talking about formalizing the expression of memory management documentation that already exists and is already understood.
> And you're not getting as much safety bang for your buck for the effort as you would in a rewrite in actually safe language.
I just can't think of what the rational argument for this could be. A complete deep rewrite -- where the new language requires reorganizing the code at a low level so that a lot of existing logic cannot be reused (as-is, or transformed in certain specific ways) -- is extremely costly. It is on the order of the total cost of writing the software in the first place plus the entire cost already spent maintaining it over time. Some costs -- like the goodwill of users/adpoters -- simply cannot be paid again at the same rate. For large scale software there would be numerous regressions over a long period of time, while at the same time the software stops adding many new features, since all the focus will on the rewrite and bugs related to the rewrite. I will stand corrected if there is more than one or two exceptional cases of large scale software making a successful transition of this sort without paying a massive cost.
But rewriting assumes I learn a new language on top of rewriting.
Safe C provides an incremental migration path from unsafe C to safe C. And you don't need to completely rewrite, but instead address the issues flagged, which will often be a lot less work and risk than an actual rewrite in a new language. (This seems obvious to me, but apparently not?)
Safety annotations is the directions that C++ has been attempting without much success for a while though, so I'm not very optimistic. But I'm always happy to see another attempt.
Would you go into a thread about emacs and say, "Why would anyone use emacs over vi?" And if not, what makes you think you should do that here?
I'm objecting to the disdainful "why would you do it in C?"
https://gcc.gnu.org/onlinedocs/gcc/Preprocessor-Options.html
The syntax?
Obviously that's not "the only problem", else there wouldn't be huge style guides forbidding tons of practices to make programs safe for NASA and other such uses, aimed at the expert C programmers hired there.
Also obviously that is not "a problem irrespective of which language we are talking about", unless half-knowing the language has the same impact and the language have the same footguns, which is nowhere near true for other languages versus C. You can "half know" Java and not ever get a buffer overflow. You can know C quite well and still get all kinds of dangerous bugs into the code.
I have 10+ years experience (and consider myself highly proficient) in C#, but my interaction with expression trees is mere hours where I've only once or twice needed to solve a very specific small problem which I could do with a small tweak to code copied from Stack Overflow.
Rust and C++ lately have been particularly quickly moving targets to keep up with, where C is still pretty much the same as C99. The compilers are better, their warnings are better, sanitizer modes are incredible, but the things you type into your text editor to express your program structure are still pretty much the same thing.
But those are exceptions: I've definitely felt like I've known more than I really did about at least C, C++, Java, Scheme, Python, Go, bash, Javascript, cron, and several assembly variants, and those platforms did little to stop me from learning about my inexperience in difficult, sometimes embarrassing, sometimes expensive ways.
I'm a big fan of more compile time analysis any way it can be done, and whatever can't at runtime. More types, more proofs, more fuzzing, more sanitizers, and also where possible, more restricted execution models than Turing-complete. Any code that can't prove itself correct is a serious liability. I just also like C... it's got many footguns, yes indeed, it's practically constructed out of only footguns, but there are only like 8 of them, and they're all right there waiting for you to get to know them. It's like having a few good sharp knives in your kitchen. You get to know each well, using them one at a time---and if any is missing from the block you pause everything and look around very carefully.
Relatively tiny and with a disproportionate number of footguns.