Antoine Miné
ABSTRACT
We propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract the contents of compound variables in a field-sensitive way, whether these fields contain numeric or pointer values, and use stock numerical abstract domains to find an overapproximation of all possible memory states---with the ability to discover relationships between variables. A main novelty of our approach is the dynamic mapping scheme we use to associate a flat collection of abstract cells of scalar type to the set of accessed memory locations, while taking care of byte-level aliases---i.e., C variables with incompatible types allocated in overlapping memory locations. We do not rely on static type information which can be misleading in C programs as it does not account for all the uses a memory zone may be put to.Our work was incorporated within the Astrée static analyzer that checks for the absence of run-time-errors in embedded, safety-critical, numerical-intensive software. It replaces the former memory domain limited to well-typed, union-free, pointer-cast free data-structures. Early results demonstrate that this abstraction allows analyzing a larger class of C programs, without much cost overhead.
- AT&T and The Santa Cruz Operation Inc. System V application binary interface, 1997.]]Google Scholar
- G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In CC 2004, number 2985 in LNCS, pages 5--23. Springer, 2004.]]Google ScholarCross Ref
- B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. A static analyzer for large safety-critical software. In ACM PLDI'03, volume 548030, pages 196--207. ACM Press, 2003.]] Google ScholarDigital Library
- P. Cousot. Verification by abstract interpretation. In Verification: Theory and Practice: Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday, volume 2772, pages 243--268. Springer, 2003.]]Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM POPL'77, pages 238--252. ACM Press, 1977.]] Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.]]Google ScholarCross Ref
- N. Dor, M. Rodeh, and M. Sagiv. Cleanness checking of string manipulations in C programs via integer analysis. In SAS'01, volume 2126 of LNCS. Springer, 2001.]] Google ScholarDigital Library
- J.-L. Lions et al. ARIANE 5, flight 501 failure, report by the inquiry board, 1996.]]Google Scholar
- J. Feret. Static analysis of digital filters. In ESOP'04, volume 2986 of LNCS. Springer, 2004.]]Google Scholar
- D. Gopan, F. DiMaio, N. Dor, T. Reps, and M. Sagiv. Numeric domains with summarized dimensions. In TACAS 2004, LNCS, pages 512--529. Springer, 2004.]]Google ScholarCross Ref
- P. Granger. Static analysis of arithmetical congruences. In International Journal of Computer Mathematics, volume 30, pages 165--190, 1989.]]Google ScholarCross Ref
- M. Hind. Pointer analysis: Haven't we solved this problem yet? In PASTE'01, pages 54--61. ACM Press, 2001.]] Google ScholarDigital Library
- IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Technical report, ANSI/IEEE Std. 745-1985, 1985.]]Google Scholar
- International Organisation for Standardization. Programming languages -- C. Technical report, ISO/IEC 9899:1999, 1999.]]Google Scholar
- A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310--319. IEEE CS Press, 2001.]] Google ScholarDigital Library
- A. Miné. Relational abstract domains for the detection of floating-point run-time errors. In ESOP'04, volume 2986 of LNCS, pages 3--17. Springer, 2004.]]Google Scholar
- G. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In POPL'02, pages 128--139. ACM Press, 2002.]] Google ScholarDigital Library
- A. Pioli and M. Hind. Combining interprocedural pointer analysis and conditional constant propagation. Technical Report 99-103, IBM, 1999.]]Google Scholar
- R. Rugina and M. Rinard. Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In PLDI'00, pages 182--195. ACM Press, 2000.]] Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24(3), 2002.]] Google ScholarDigital Library
- M. Siff, S. Chandra, T. Ball, K. Kunchithapadam, and T. Reps. Coping with type casts in C. In ESEC/FSE'99, pages 180--198. Springer.]] Google ScholarDigital Library
- B. Steensgaard. Points-to analysis by type inference of programs with structures and unions. In CC'96, volume 1060 of LNCS, pages 136--150. Springer, 1996.]] Google ScholarDigital Library
- A. Venet. A scalable nonuniform pointer analysis for embedded programs. In SAS'04, number 3148 in LNCS, pages 149--164. Springer, 2004.]]Google Scholar
- J. Whaley and M. Lam. An efficient inclusion-based points-to analysis for strictly-typed languages. In SAS'02, volume 2477, pages 180--195. Springer.]] Google ScholarDigital Library
- R. Wilson and M. Lam. Efficient context-sensitive pointer analysis for C programs. In PLDI'95, pages 1--12. ACM Press, 1995.]] Google ScholarDigital Library
- S. Yong and S. Horwitz. Pointer-range analysis. In SAS'04, number 3148 in LNCS, pages 133--148. Springer, 2004.]]Google Scholar
- S. Yong, S. Horwitz, and T. Reps. Pointer analysis for programs with structures and casting. In PLDI'99, pages 91--103. ACM Press, 1999.]] Google ScholarDigital Library
Recommendations
Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
Proceedings of the 2006 LCTES ConferenceWe propose a memory abstraction able to lift existing numerical static analyses to C programs containing union types, pointer casts, and arbitrary pointer arithmetics. Our framework is that of a combined points-to and data-value analysis. We abstract ...
Combining range and inequality information for pointer disambiguation
Pentagons is an abstract domain invented by Logozzo and Fhndrich to validate array accesses in low-level programming languages. This algebraic structure provides a cheap less-than check, which builds a partial order between the integer variables used in ...
Refinement-based context-sensitive points-to analysis for Java
Proceedings of the 2006 PLDI ConferenceWe present a scalable and precise context-sensitive points-to analysis with three key properties: (1) filtering out of unrealizable paths, (2) a context-sensitive heap abstraction, and (3) a context-sensitive call graph. Previous work [21] has shown ...
Comments