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 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.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Gonthier, Georges (ed.); Norrish, Michael (ed.): Certified programs and proofs. Third international conference, CPP 2013, Melbourne, VIC, Australia, December 11--13, 2013. Proceedings (2013)
- Huang, Daniel; Morrisett, Greg: Formalizing the SAFECode type system (2013)
- Conway, Christopher L.; Dams, Dennis; Namjoshi, Kedar S.; Barrett, Clark: Pointer analysis, conditional soundness, and proving the absence of errors (2008)
- Nita, Marius; Grossman, Dan; Chambers, Craig: A theory of platform-dependent low-level software (2008)
Further publications can be found at: http://safecode.cs.illinois.edu/pubs.html