SAFECode: enforcing alias analysis for weakly typed languages

SAFECode: enforcing alias analysis for weakly typed languages,10.1145/1133981.1133999,Dinakar Dhurjati,Sumant Kowshik,Vikram S. Adve

SAFECode: enforcing alias analysis for weakly typed languages   (Citations: 42)
BibTex | RIS | RefWorks Download
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 mem- ory 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 (dan- gling pointer references and certain array bounds errors) cannot in- validate the call graph, points-to information or type information. The key insight behind our approach is that pool allocation can be used to create a run-time partitioning of memory that matches the compile-time memory partitioning in a points-to graph, and effi- cient checks can be used to isolate the run-time partitions. Further- more, we show that the sound analysis information enables static checking techniques that eliminate many run-time checks. Our ap- proach requires no source code changes, allows memory to be man- aged explicitly, and does not use meta-data on pointers or individual tag bits for memory. Using several benchmarks and system codes, we show experimentally that the run-time overheads are low (less than 10% in nearly all cases and 30% in the worst case we have seen). We also show the effectiveness of static analyses in eliminat- ing run-time checks.
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: