3 ms·

Vellvm: Verifying the LLVM

84 points by lelf 12y ago

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 ago
    Yeah, 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.
teddyknox 12y ago
I have little systems programming experience, could someone explain to me what this does?
- l_dopa 12y ago
  It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program. See also Compcert[1] and CakeML[2] for some other recent work in this area. [1] http://compcert.inria.fr/ http://compcert.inria.fr/ [2] https://cakeml.org/ https://cakeml.org/
- exDM69 12y ago
  Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framework (or at least parts of it) work correctly. Proving here means formal verification, not too dissimilar from making a mathematical proof that something holds. Basically the idea is to look at the optimizations that the LLVM compiler performs and verify that the program after the optimization does the same thing as before optimization. It is easy to write compilers that emit fast code, but a lot harder to write compilers that emit fast and correct code.
  - dspillett 12y ago
    > but a lot harder to write compilers that emit fast and correct code. The hard part is being confident you have correct code for all cases even the rare edge cases. Producing something that works for the happy path is easy. Producing something that works correctly for a wide range of input test conditions is more long winded but still not difficult. This sort of work is about mapping the inputs, assumptions, and outputs into a minimal (mathematical) form and using that to prove that for all cases the process correctly maps one to the other - to try prove that there can be no input for which the output is invalid.

84 points by lelf 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 ago
  Yeah, 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.

teddyknox 12y ago

I have little systems programming experience, could someone explain to me what this does?

l_dopa 12y ago
It's a semantics for the intermediate representation used by most of the LLVM optimization passes defined in a theorem prover. With it you can, for example, write your own LLVM pass in Coq's specification language and prove that it can't introduce bugs by changing the meaning of a program. See also Compcert[1] and CakeML[2] for some other recent work in this area. [1] http://compcert.inria.fr/ http://compcert.inria.fr/ [2] https://cakeml.org/ https://cakeml.org/
exDM69 12y ago
Here's a dumbed down explanation. This actually isn't systems programming, this is compiler technology. It is an effort to prove that the LLVM compiler framework (or at least parts of it) work correctly. Proving here means formal verification, not too dissimilar from making a mathematical proof that something holds. Basically the idea is to look at the optimizations that the LLVM compiler performs and verify that the program after the optimization does the same thing as before optimization. It is easy to write compilers that emit fast code, but a lot harder to write compilers that emit fast and correct code.
- dspillett 12y ago
  > but a lot harder to write compilers that emit fast and correct code. The hard part is being confident you have correct code for all cases even the rare edge cases. Producing something that works for the happy path is easy. Producing something that works correctly for a wide range of input test conditions is more long winded but still not difficult. This sort of work is about mapping the inputs, assumptions, and outputs into a minimal (mathematical) form and using that to prove that for all cases the process correctly maps one to the other - to try prove that there can be no input for which the output is invalid.