Nonuniform Alias Analysis of Recursive Data Structures and Arrays
In this paper we present an alias analysis which is able to infer position-dependent equality relationships between pointers in recursively defined data structures or arrays. Our work is based on a semantic model of the execution of a program in which every allocated object is identified by a timestamp which represents the state of the program at the instant of the object creation. We provide a simple numerical abstraction of timestamps which is accurate enough to distinguish between elements of arrays or list-like structures. We follow the methodology of Abstract Interpretation to derive a sound approximation of the program semantics from this abstraction. The computability of our analysis is then guaranteed by using an abstract numerical lattice to represent relations between timestamps.
KeywordsNull Pointer Abstract Interpretation Abstract Domain Abstract Semantic Program Semantic
Unable to display preview. Download preview PDF.
- 1.L.O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, 1994.Google Scholar
- 3.M. Burke, P. R. Carini, J.-D. Choi, and M. Hind. Interprocedural pointer alias analysis. Technical report, IBM Research Report, 1997.Google Scholar
- 4.P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303–342. Prentice-Hall, Inc., Englewood Cliffs, 1981.Google Scholar
- 5.P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977.Google Scholar
- 6.P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the Sixth Conference on Principles of Programming Languages POPL’79, pages 269–282. ACM Press, 1979.Google Scholar
- 7.P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511–547, August 1992.Google Scholar
- 8.P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the Fifth Conference on Principles of Programming Languages. ACM Press, 1978.Google Scholar
- 9.A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In POPL 1990, pages 157–168, 1990.Google Scholar
- 10.A. Deutsch. A storeless model of aliasing and its abstraction using finite representations of right-regular equivalence relations. In Proceedings of the 1992 International Conference on Computer Languages, pages 2–13. IEEE Computer Society Press, 1992.Google Scholar
- 11.A. Deutsch. Interprocedural may-alias analysis for pointers: beyond k-limiting. In ACM SIGPLAN’94 Conference on Programming Language Design and Implementation. ACM Press, 1994.Google Scholar
- 12.R. Ghiya and L. J. Hendren. Is it a tree, a dag, or a cyclic graph? a shape analysis for heap-directed pointers in c. In Porceedings of POPL 1996, pages 1–15, 1996.Google Scholar
- 14.P. Granger. Static analysis of linear congruence equalities among variables of a program. In TAPSOFT’91, volume 493. Lecture Notes in Computer Science, 1991.Google Scholar
- 16.H.B.M Jonkers. Abstract storage structures. In De Bakker and Van Vliet, editors, Algorithmic languages, pages 321–343. IFIP, 1981.Google Scholar
- 17.M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133–151, 1976.Google Scholar
- 18.F. Masdupuy. Using abstract interpretation to detect array data dependencies. In Proceedings of the International Symposium on Supercomputing, 1991.Google Scholar
- 19.A. Miné. A new numerical abstract domain based on difference-bound matrices. In PADO II, volume 2053 of LNCS, pages 155–172. Springer-Verlag, May 2001.Google Scholar
- 20.PolySpace Technologies. http://www.polyspace.com.
- 22.B. Steensgaard. Points-to analysis by type inference of programs with structures and unions. In Proceedings of the 1996 International Conference on Compiler Construction, volume 1060 of LNCS, pages 136–150, 1996.Google Scholar
- 23.A. Venet. Abstract cofibered domains: Application to the alias analysis of untyped programs. In Proceedings of the Third International Static Analysis Symposium SAS’96, volume 1145 of Lecture Notes in Computer Science, pages 366–382. Springer-Verlag, 1996.Google Scholar