4 ms·
I love the idea of a prover running to prove that invariants in input IR is the same as the output IR after running a transformation pass. I think adding invar
by andrewchambers 12y ago
I love the idea of a prover running to prove that invariants in input IR is the same as the output IR after running a transformation pass.
I think adding invariant information to the machine specific IR would be a cool way to verify the compiler backends are bug free.
I've often imagined automatically generating an efficient compiler backend via some sort of bruteforce or heuristic then verifying the code it generates via a theorem prover.
- prutschman 12y ago> I've often imagined automatically generating an efficient compiler backend via some sort of bruteforce or heuristic then verifying the code it generates via a theorem prover. Here's one paper that aims to do basically that, at the peephole optimization level: http://cs.stanford.edu/~sbansal/pubs/asplos06.pdf http://cs.stanford.edu/~sbansal/pubs/asplos06.pdf
- andrewchambers 12y agoYeah, I've read that, they operate on straight lines of code. LLVM works on DAG's, but the ideas are more or less the same.