[LLVMdev] Checked arithmetic
regehr at cs.utah.edu
Thu Mar 27 11:10:33 PDT 2008
> 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
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
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.
More information about the llvm-dev