Advertisement

Nonuniform Alias Analysis of Recursive Data Structures and Arrays

  • Arnaud Venet
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2477)

Abstract

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.

Keywords

Null Pointer Abstract Interpretation Abstract Domain Abstract Semantic Program Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    L.O. Andersen. Program Analysis and Specialization for the C Programming Language. PhD thesis, DIKU, University of Copenhagen, 1994.Google Scholar
  2. 2.
    F. Bourdoncle. Efficient chaotic iteration strategies with widenings. In Proc. of the International Conference on Formal Methods in Programming and their Applications, volume 735 of LNCS, pages 128–141, 1993.CrossRefGoogle Scholar
  3. 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. 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. 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. 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. 7.
    P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511–547, August 1992.Google Scholar
  8. 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. 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. 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. 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. 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
  13. 13.
    P. Granger. Static analysis of arithmetical congruences. International Journal of Computer Mathematics, 30:165–190, 1989.CrossRefzbMATHGoogle Scholar
  14. 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
  15. 15.
    M. Hind and A. Pioli. Evaluating the effectiveness of pointer alias analyses. Science of Computer Programming, 39(1):31–55, 2001.zbMATHCrossRefGoogle Scholar
  16. 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. 17.
    M. Karr. Affine relationships among variables of a program. Acta Informatica, pages 133–151, 1976.Google Scholar
  18. 18.
    F. Masdupuy. Using abstract interpretation to detect array data dependencies. In Proceedings of the International Symposium on Supercomputing, 1991.Google Scholar
  19. 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. 20.
    PolySpace Technologies. http://www.polyspace.com.
  21. 21.
    Shmuel Sagiv, Thomas W. Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. TOPLAS, 20(1):1–50, 1998.CrossRefGoogle Scholar
  22. 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. 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
  24. 24.
    A. Venet. Automatic analysis of pointer aliasing for untyped programs. Science of Computer Programming, 35(2):223–248, 1999.zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Arnaud Venet
    • 1
  1. 1.LIX, École PolytechniquePalaiseauFrance

Personalised recommendations