Abstract
It is well known that the use of points-to information can substantially improve the accuracy of a static program analysis. Commonly used algorithms for computing points-to information are known to be sound only for memory-safe programs. Thus, it appears problematic to utilize points-to information to verify the memory safety property without giving up soundness. We show that a sound combination is possible, even if the points-to information is computed separately and only conditionally sound. This result is based on a refined statement of the soundness conditions of points-to analyses and a general mechanism for composing conditionally sound analyses.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Adams, S., Ball, T., Das, M., Lerner, S., Rajamani, S.K., Seigle, M., Weimer, W.: Speeding up dataflow analysis using flow-insensitive pointer analysis. In: Static Analysis Symposium, Madrid, Spain, pp. 230–246 (September 2002)
Aho, A.V., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1988)
Andersen, L.O.: Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen (May 1994)
Bruns, G., Chandra, S.: Searching for points-to analysis. In: Foundations of Software Engineering, Charleston, South Carolina, pp. 61–70 (November 2002)
Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C.: Points-to analysis, conditional soundness, and proving the absence of errors. Technical Report TR2008-910, New York University, Dept. of Computer Science (2008)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, Los Angeles, California, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, San Antonio, Texas, pp. 269–282 (1979)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The ASTRÉE analyzer. In: European Symposium on Programming, Edinburgh, Scotland, pp. 21–30 (April 2005)
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: Combination of abstractions in the ASTRÉE static analyzer. In: Asian Computing Science Conference (ASIAN), Tokyo, Japan (December 2006)
Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Principles of Programming Languages, Tucson, Arizona (January 1978)
Dams, D., Namjoshi, K.S.: Orion: Building blocks for program analyzers. In: Formal Methods for Components and Objects, Amsterdam, The Netherlands (November 2005)
Das, M.: Unification-based pointer analysis with directional assignments. In: Programming Language Design and Implementation, Vancouver, British Columbia, pp. 35–46 (2000)
Dhurjati, D., Kowshik, S., Adve, V.: SAFECode: enforcing alias analysis for weakly typed languages. In: Programming Language Design and Implementation, Ottawa, Canada, pp. 144–157 (June 2006)
Dor, N.: Automatic Verification of Program Cleanness. PhD thesis, Tel Aviv University (December 2003)
Dor, N., Rodeh, M., Sagiv, M.: CSSV: towards a realistic tool for statically detecting all buffer overflows in C. In: Programming Language Design and Implementation, San Diego, California, pp. 155–167 (July 2003)
Emami, M., Ghiya, R., Hendren, L.J.: Context-sensitive interprocedural points-to analysis in the presence of function pointers. In: Programming Language Design and Implementation, pp. 242–256 (June 1994)
Foster, J.S., Fähndrich, M., Aiken, A.: Flow-insensitive points-to analysis with term and set constraints. Technical Report UCB/CSD-97-964, University of California, Berkeley (August 1997)
Ghiya, R., Lavery, D.M., Sehr, D.C.: On the importance of points-to analysis and other memory disambiguation methods for C programs. In: Programming Language Design and Implementation, Snowbird, Utah, pp. 47–58 (June 2001)
Gulwani, S., Tiwari, A.: Combining abstract interpreters. In: Programming Language Design and Implementation, Ottawa, Canada (June 2006)
Heintze, N., Tardieu, O.: Demand-driven pointer analysis. In: Programming Language Design and Implementation, Snowbird, Utah, pp. 24–34 (June 2001)
Hind, M.: Pointer analysis: Haven’t we solved this problem yet? In: Program Analysis for Software Tools and Engineering, Snowbird, Utah (June 2001)
ISO Standard - Programming Languages - C, ISO/IEC 9899:1999 (December 1999)
Lattner, C.: Macroscopic Data Structure Analysis and Optimization. PhD thesis, University of Illinois at Urbana-Champaign (May 2005)
Lerner, S., Grove, D., Chambers, C.: Composing dataflow analyses and transformations. In: Principles of Programming Languages, Portland, Oregon, pp. 270–282 (2002)
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: Languages, Compilers, and Tools for Embedded Systems, Ottawa, Canada (2006)
Necula, G.C., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy code. In: Principles of Programming Languages, Portland, Oregon, pp. 128–139 (January 2002)
Steensgaard, B.: Points-to analysis in almost linear time. In: Principles of Programming Languages, St. Petersburg Beach, Florida, pp. 32–41 (January 1996)
Wilson, R.P., Lam, M.S.: Efficient context-sensitive pointer analysis for C programs. In: Programming Language Design and Implementation, San Diego, California, pp. 1–12 (June 1995)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Conway, C.L., Dams, D., Namjoshi, K.S., Barrett, C. (2008). Pointer Analysis, Conditional Soundness, and Proving the Absence of Errors. In: Alpuente, M., Vidal, G. (eds) Static Analysis. SAS 2008. Lecture Notes in Computer Science, vol 5079. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69166-2_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-69166-2_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69163-1
Online ISBN: 978-3-540-69166-2
eBook Packages: Computer ScienceComputer Science (R0)