[LLVMdev] Checked arithmetic

[Gabor Greif]

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


Hi John,

some time ago I tried to encode some crucial properties
of LLVM IR in Omega (Tim Sheard's system). It looked
pretty good, but even encoding basic SSA properties as
types (i.e. may only reference an already defined variable)
cause your brain to overheat :-)

Stefan Monnier [1] has also some papers about provably correct
program transformations using an expressive type system.

Cheers,

	Gabor

[1] http://www.iro.umontreal.ca/~monnier/tcm.pdf