Abstract:

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 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 efficient checks can be used to isolate the run-time partitions. Furthermore, we show that the sound analysis information enables static checking techniques that eliminate many run-time checks. Our approach requires no source code changes, allows memory to be managedexplicitly, and does not use meta-data on pointers or individual tag bits for memory. Using several benchmark s 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 eliminating run-time checks.

Download:

Paper:

• SAFECode: Enforcing Alias Analysis for Weakly Typed Languages (PDF)

BibTeX Entry:

@inproceedings{1133999,
 author = {Dinakar Dhurjati and Sumant Kowshik and Vikram Adve},
 title = {SAFECode: enforcing alias analysis for weakly typed languages},
 booktitle = {PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation},
 year = {2006},
 isbn = {1-59593-320-4},
 pages = {144--157},
 location = {Ottawa, Ontario, Canada},
 doi = {http://doi.acm.org/10.1145/1133981.1133999},
 publisher = {ACM},
 address = {New York, NY, USA},
}