3 ms·
There is a third category of memory and other software safety mechanisms: model checking. While it does involve compiling software to a different target -- typi
by nanolith 1y ago
There is a third category of memory and other software safety mechanisms: model checking. While it does involve compiling software to a different target -- typically an SMT solver -- it is not a compile-time mechanism like in Rust.
Kani is a model checker for Rust, and CBMC is a model checker for C. I'm not aware of one (yet!) for Zig, but it would not be difficult to build a port. Both Kani and CBMC compile down to goto-c, which is then converted to formulas in an SMT solver.
- DrNosferatu 1y agoAny good primers on SMT solvers?
- nanolith 1y agoStart with this. https://smt.st/SAT_SMT_by_example.pdf https://smt.st/SAT_SMT_by_example.pdf The algorithms behind SAT / SMT are actually pretty straight-forward. One of these days, I'll get around to publishing an article to demystify them.
- dnautics 1y agoThere isn't a real one yet, but to scratch an itch I tried to build one for Zig. It's not complete nor do I have plans to complete it. https://github.com/ityonemo/clr https://github.com/ityonemo/clr If zig locks down the AIR (intermediate representation at the function level) it would be ideal for running model checking of various sorts. Just by looking at AIR I found it possible to: - identify stack pointer leakage - basic borrow checking - detect memory leaks - assign units to variables and track when units are incompatible