5 ms·
Is it feasible to prove the correctness of all existing LLVM passes this way? What about the backends and Clang and Rust frontends?
by devit 11y ago
Is it feasible to prove the correctness of all existing LLVM passes this way?
What about the backends and Clang and Rust frontends?
- nickpsecurity 11y agohttps://news.ycombinator.com/item?id=10604379 https://news.ycombinator.com/item?id=10604379 Work in progress for correctness that's being hit from many, different directions. I don't know of anyone doing the front-ends, though. Not for LLVM, anyway.
- gsnedders 11y agoThe frontends are hard because you need to start with a formal definition of the language, really. Rust doesn't really have anything resembling a spec at the moment. C/C++ you still have the first problem of creating a formalization of the spec before you can verify the front-end.
- kachnuv_ocasek 11y agoC actually has multiple formal semantics. The most recent I'm aware of is Robbert Krebbers' (almost) complete formalizatiom of C11 in the CH2O project.[1] See also his upcoming PhD thesis[2] for more details. [1] http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ [2] http://robbertkrebbers.nl/thesis.html http://robbertkrebbers.nl/thesis.html
- gsnedders 11y agoArguably C doesn't: C is just what the spec says. You can try and formalise what the spec says (as, rightly, many have done), but it's hard to guarantee correctness of that formalisation.