Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
replies(8):
> The coercions introduced by conversion rules can however lead to subtle semantic differences
The example they give is this C code:
1 uint8_t x[1] = { 0 };
2 uint8_t *y = x;
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */
1 let x: [u8; 1] = [0; 1];
2 let mut y: Box<[u8]> = Box::new(x);
3 y[0] = 1;
4 assert!(x[0] == 1) /* failure */
For comparison, the scpptool (my project) auto-translation (to a memory safe subset of C++) feature would translate it to something like:
1 mse::lh::TNativeArrayReplacement<uint8_t, 1> x = { 0 };
2 mse::lh::TNativeArrayReplacement<uint8_t, 1>::iterator y = x; // implicit conversion from array to iterator
3 *y = 1;
4 assert(*x == 1); /* SUCCESS */ // dereferencing of array supported for compatibility
2 mse::TAnyRandomAccessIterator<uint8_t> y = x; // implicit conversion from array to iterator
edit: added translation for line 2 in an alternate hypothetical situation.
the translated code may (quietly) not behave correctly.
If the original C program further relies on x, our translation will error out, and will ask the
programmer to fix their source code. This is another area where we adopt a “semi-active” approach
to verification, and declare that some patterns are poor enough, even for C, that they ought to be
touched up before the translation takes place.The point of noting that the example translation quietly does the wrong thing, is that that is the reason that it would have to be ("unconditionally") rejected.
While the paper does suggest that their example translation would be rejected:
> If the original C program further relies on x, our translation will error out
note that precisely determining whether or not the program "further relies on x" statically (at compile/translation-time) is, in general, a "Halting Problem". (I.e. Cannot be reliably done with finite compute resources.) So they would presumably have to be conservative and reject any cases were they cannot prove that the program does not "further rely on x". So it's notable that they choose to use a (provisional) translation that has to be rejected in a significant set of false positive cases.
And at least on initial consideration, it seems to me that an alternative translation could have, for example, used RefCell<>s or whatever and avoided the possibility of "quietly doing the wrong thing". (And thus, depending on your/their requirements, avoid the need for unconditional rejection.) Now, one might be an a situation where they'd want to avoid the run-time overhead and/or potential unreliability of RefCell<>s, but even then it seems to me that their translation choice does not technically avoid either of those things. Their solution allocates on the heap which has at least some theoretical run-time overhead, and could theoretically fail/panic.
Now I'm not concluding here that their choice is not the right one for their undertaking. I'm just suggesting that choosing a (provisional) translation that has to be rejected with significant false positives (because it might quietly do the wrong thing) is at least initially notable. And that there are other solutions out there that demonstrate translation of C to a (high-performance, deterministic) memory-safe language/dialect that don't have the same limitations.