[LLVMdev] Current work on type-safety proving?

Jules jules at dsf.org.uk
Mon Sep 4 07:04:23 PDT 2006

I was just wondering what existing work has been done on proving
programs type-safe using the LLVM framework?  I've read the paper on
memory-safety for embedded systems, but that's not quite what I'm
looking for, as my application (which involves running untrusted code
within a trusted context) might fail if a pointer to one object became a
pointer to another of the same type.

Looking at the documentation, it seems a trivial check for type-safety
would be simply to ensure that the program didn't use any 'cast'
instructions, only used the memory allocation facilities of a trusted
garbage collector, and didn't contain any zero-length arrays (as these
might be used for unsafe pointer arithmetic).  However I guess that in
the real world, these constraints would be almost impossible to program
to (e.g., my simple C++ test programs suggest that it's impossible to
write any non-trivial C++ program that doesn't generate a 'cast'), so
there must be circumstances that allow such constructs.

Has any work been done on this?  If not, what pointers would you give
for places to start?



More information about the llvm-dev mailing list