Vellvm: Verifying the LLVM | Hacker News Reader

Vellvm: Verifying the LLVM

cis.upenn.edu

84 pointslelf7 comments

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.

> 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

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.

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

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/ [2] https://cakeml.org/

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.

> 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.

Reply on news.ycombinator.com