[LLVMdev] Current work on type-safety proving?

[Julian Hall]

Thanks for your replies.

This all looks extremely interesting, and I see now what I would need to 
do to go ahead with this.

I would plan on using a subset of C++ with a garbage collector as my 
target language, and would probably exclude existing standard libraries 
(my application would require a specific API be available, but not much 
else), except for those that would compile within such a language subset 
(e.g. C string manipulations, some parts of the C++ STL and boost, etc.).

I'm hoping this will be possible without compiler modifications, but 
fear it might not be.  I don't know if the type information emitted by 
G++ is enough to enable all the checks I'll need.

Vikram Adve wrote:

>Jules,
>
>The link Chris forwarded (safecode.cs.uiuc.edu) describes the most  
>relevant work so far.  But that work aims to make ordinary C and C++  
>programs memory-safe, without using garbage collection or any other  
>automatic memory management scheme, i.e., allowing dangling pointers  
>but ensuring they are harmless.  It also allows any casts that are  
>legal in C.
>
>If you want to enforce strict type safety with GC and without  
>arbitrary casts, you should be able to build on top of SAFECode and  
>provide a garbage collector.  You'd have to define what pointer casts  
>are legal and check for them.  But SAFECode would give you several  
>other checks you need including:
>-- array bounds (just looking for 0-length arrays isn't enough)
>-- uninitialized variables
>-- many stdlib usage checks.
>
>--Vikram
>http://www.cs.uiuc.edu/~vadve
>http://llvm.cs.uiuc.edu/
>
>  
>