4 ms·
My personal experience has shown me that static analysis of this kind does not scale for C, the complexity of showing just the memory safety of even simple prog
by xavxav 4y ago
My personal experience has shown me that static analysis of this kind does not scale for C, the complexity of showing just the memory safety of even simple programs grows astonishingly fast.
Proof overhead for memory safety can frequently be on the order of 5-10 lines of annotation per line of code.
- zozbot234 4y agoThis is exactly why the Rust folks chose the kind of analysis that they did for the borrow checker. It's quite co-extensive with the subset of memory-safety proofs that happen to scale up easily and compositionally to larger programs. That said, it would still be very helpful to have true first-class support for the GhostCell pattern in Rust, so as to be able to prove safety for somewhat more complex designs (including safe doubly-linked lists) albeit contained within a single module.
- pron 4y agoThat greatly depends on how many memory-safe programs you want to prove are memory safe. If it's the same subset of programs that a language like Rust can prove to be memory-safe, the annotation overload need not be higher. If you want to prove that an arbitrary memory-safe C program is memory-safe, then, indeed, you'll likely need many more annotations. Even in those situations, adding more annotations or restructuring the code may be cheaper than a rewrite in another language. Sound static analysis for C is already not uncommon in some important domains.
- uecker 4y agoThanks. This is exactly my point. Instead of Rust, we could use a subset of C with suitable annotations and will not require any more annotations than Rust.
- alkonaut 4y agoYeah, ask yourself, if you see if (!x) return; // statment here do_something(x); Which statements on the line saying "statement here" would invalidate the zero check for x?
- pjmlp 4y agoNow add threading, hardware traps and signals into the mix.