[LLVMdev] Current work on type-safety proving?
jules at meridiandigital.co.uk
Tue Sep 5 02:06:48 PDT 2006
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:
>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.
More information about the llvm-dev