Can't we just make macros to redefine types as some 'safe' type variant system, and #include "safetypes.h" or something? It's ugly, but searching your source code for 'int a[5]' and replacing it with 'INT(a,5)' might be dumb enough to work.
(Who invented array slices? It was a concept that came along much later than one might have expected.)
[1] https://staff.aist.go.jp/y.oiwa/FailSafeC/index-en.html
[2] https://people.cs.rutgers.edu/~sn349/softbound/
The former apparently implements full ANSI C, and the latter apparently has a memory safety proof in Coq.
The group that did [1] also did an ANSI C to Java compiler.
It seems to me that we could really use a safe ABI (x86_64_safe, etc.) for C/C++, and that it should be supported by clang and gcc.
Maybe CHERI will catch on someday...
> This C code is guaranteed to be safe. We had an AI go through it and make it safe.
No, thanks. That sounds more like a problem than a solution.
"We find that typ3c automatically converted 67.9% of pointers in our benchmark programs to checked types, which improves on the 48.4% inferred by unification-style algorithms used in prior work. boun3c was able to infer bounds for 77.3% of pointers that required them."
That's reasonably good. The real goal is to convert all pointers to either run-time checked pointers (slower) or compile-time checked pointers. It's already possible to convert everything to "fat pointers". GCC used to have that as an option. But the goal is to eliminate the need for that for code that's frequently executed. That is, inner loops. It's good to see activity in this area.
The output code is kind of clunky looking, but that could be fixed.
• Microsoft source code annotation language (SAL)
• Cyclone (AT&T research language)
• SCC, the Safe C compiler.
• Ccured
• MemSafe
The breakthrough will come when someone can create an automated system to convert unsafe C into safe something. AI may be far enough along to do that now. Every array in a valid C program has a size, defined by some expression known to the programmer. All you have to do is find that expression and tell the language about it. Most of the time this is easy. Sometimes it's hard. Sometimes it's impossible, in which case the program is probably a buffer overflow waiting to happen.
[1] http://animats.com/papers/languages/safearraysforc43.pdf