[LLVMdev] Checked arithmetic

[Pertti Kellomäki]

John Regehr wrote:
> 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.

Except that some aspects of the host platform leak through
to .bc files. This may or may not be a problem.

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

That would be quite nice indeed.

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

You could sell it to me. How much money do you have? ;-)
But seriously, that is something I would very much like to see.
One of the reasons why you have not had success may be that with current
prover technology, formalizing LLVM semantics and carrying out proofs
would be a fairly straightforward exercise, but not a trivial amount
of work. Not a good combination in academic sense.

On the other hand, formalizing LLVM and proving some properties
would make for a very nice open source proof project, which would
be an interesting beast.
-- 
Pertti