[LLVMdev] Checked arithmetic

[John Regehr]

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

I know a bit about how Michael Norrish dealt with this sort of thing in 
his formal semantics for C.  For example, integer width is modeled as a 
constant, but one with an unspecified value.  Other C level choices such 
as order of evaluation of function arguments are modeled using 
nondeterministic choice.  My understanding is that these are not too 
difficult at the level of the language specification, but that they make 
proofs about portable C code very difficult.

I don't have a sense if the platform leaks in LLVM are bad ones or not.

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

But the same is true about LLVM itself, yes?  Sometimes researchers take 
on large infrastructure-type projects because these are great enablers of 
new research.  This is what tenure is for.  Or did Vikram start this 
project as an assistant professor?  If so, my hat is off :).

John Regehr