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