[LLVMdev] Checked arithmetic

[John Regehr]

> Don't forget prover. :-)

Say on that note here's something that I want to see: a formal semantics 
for LLVM in for example higher order logic.  This would probably not be 
that difficult.

The problem that this solves is that current verified compiler efforts 
appear to be highly specific to both the language and the target.

Once the semantics exists, you can either prove once and for all the that 
each LLVM->LLVM optimization pass preserves the semantics of the code, or 
else just do translation validation.

Verifying the LLVM->native backends should not be incredibly difficult.

Verifying a real LLVM front end would be a big projet but substantial 
headway is being made on that kind of thing for example by Xavier Leroy's 
group.

I've tried to sell some of the HOL folks on this idea (they have a formal 
semantics for an ARM ISA, for example) but so far no dice.

John Regehr