SAFECode: enforcing alias analysis for weakly typed languages

Static analysis of programs in weakly typed languages such as C and C++ is generally not sound because of possible memory errors due to dangling pointer references, uninitialized pointers, and array bounds overflow. We describe a compilation strategy for standard C programs that guarantees that aggressive interprocedural pointer analysis (or less precise ones), a call graph, and type information for a subset of memory, are never invalidated by any possible memory errors. We formalize our approach as a new type system with the necessary run-time checks in operational semantics and prove the correctness of our approach for a subset of C. Our semantics provide the foundation for other sophisticated static analyses to be applied to C programs with a guarantee of soundness. Our work builds on a previously published transformation called Automatic Pool Allocation to ensure that hard-to-detect memory errors (dangling pointer references and certain array bounds errors) cannot invalidate the ...

• Type: Conference
• Year: 2006
• Where: PLDI
• Authors: Dinakar Dhurjati, Sumant Kowshik, Vikram S. Adve
• Keywords: Memory Errors, PLDI 2006, Possible Memory Errors, Programming Languages, Run-time Checks