Article

Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics

Author:

Antoine MinéAuthors Info & Claims

LCTES '06: Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems

Pages 54 - 63

https://doi.org/10.1145/1134650.1134659

Published: 14 June 2006 Publication History

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.

References

[1]

AT&T and The Santa Cruz Operation Inc. System V application binary interface, 1997.]]

[2]

G. Balakrishnan and T. Reps. Analyzing memory accesses in x86 executables. In CC 2004, number 2985 in LNCS, pages 5--23. Springer, 2004.]]

[3]

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.]]

Digital Library

[4]

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.]]

[5]

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.]]

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.]]

[7]

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.]]

Digital Library

[8]

J.-L. Lions et al. ARIANE 5, flight 501 failure, report by the inquiry board, 1996.]]

[9]

J. Feret. Static analysis of digital filters. In ESOP'04, volume 2986 of LNCS. Springer, 2004.]]

[10]

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.]]

[11]

P. Granger. Static analysis of arithmetical congruences. In International Journal of Computer Mathematics, volume 30, pages 165--190, 1989.]]

[12]

M. Hind. Pointer analysis: Haven't we solved this problem yet? In PASTE'01, pages 54--61. ACM Press, 2001.]]

Digital Library

[13]

IEEE Computer Society. IEEE standard for binary floating-point arithmetic. Technical report, ANSI/IEEE Std. 745-1985, 1985.]]

[14]

International Organisation for Standardization. Programming languages -- C. Technical report, ISO/IEC 9899:1999, 1999.]]

[15]

A. Miné. The octagon abstract domain. In AST 2001 in WCRE 2001, IEEE, pages 310--319. IEEE CS Press, 2001.]]

Digital Library

[16]

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.]]

[17]

G. Necula, S. McPeak, and W. Weimer. CCured: type-safe retrofitting of legacy code. In POPL'02, pages 128--139. ACM Press, 2002.]]

Digital Library

[18]

A. Pioli and M. Hind. Combining interprocedural pointer analysis and conditional constant propagation. Technical Report 99-103, IBM, 1999.]]

[19]

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.]]

Digital Library

[20]

M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24(3), 2002.]]

Digital Library

[21]

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.]]

Digital Library

[22]

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.]]

Digital Library

[23]

A. Venet. A scalable nonuniform pointer analysis for embedded programs. In SAS'04, number 3148 in LNCS, pages 149--164. Springer, 2004.]]

[24]

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.]]

Digital Library

[25]

R. Wilson and M. Lam. Efficient context-sensitive pointer analysis for C programs. In PLDI'95, pages 1--12. ACM Press, 1995.]]

Digital Library

[26]

S. Yong and S. Horwitz. Pointer-range analysis. In SAS'04, number 3148 in LNCS, pages 133--148. Springer, 2004.]]

[27]

S. Yong, S. Horwitz, and T. Reps. Pointer analysis for programs with structures and casting. In PLDI'99, pages 91--103. ACM Press, 1999.]]

Digital Library

Cited By

Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Ghidini RErhard JSchwarz MSeidl HArceri VPasqua M(2024)C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689994(2-9)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689994
An XJia XDu HXie Y(2024)Structure-Sensitive Pointer Analysis for Multi-structure ObjectsProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3671396(155-164)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3671396
Show More Cited By

Recommendations

Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
Proceedings of the 2006 LCTES Conference

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 ...
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 Conference

We 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LCTES '06: Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems

June 2006

220 pages

ISBN:159593362X

DOI:10.1145/1134650

General Chair:
Mary Jane Irwin
Pennsylvania State University, USA
,
Program Chair:
Koen De Bosschere
Ghent University, Belgium

ACM SIGPLAN Notices Volume 41, Issue 7
Proceedings of the 2006 LCTES Conference
July 2006
208 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/1159974
Issue’s Table of Contents

Copyright © 2006 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 June 2006

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

LCTES06

Sponsor:

LCTES06: Languages, Compilers, and Tools for Embedded Systems 2006

June 14 - 16, 2006

Ontario, Ottawa, Canada

Acceptance Rates

Overall Acceptance Rate 116 of 438 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

80
Total Citations
View Citations
707
Total Downloads

Downloads (Last 12 months)22
Downloads (Last 6 weeks)1

Reflects downloads up to 13 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Simonnet JLemerre MSighireanu M(2024)A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level CodeProceedings of the ACM on Programming Languages10.1145/36897128:OOPSLA2(30-59)Online publication date: 8-Oct-2024
https://dl.acm.org/doi/10.1145/3689712
Ghidini RErhard JSchwarz MSeidl HArceri VPasqua M(2024)C-2PO: A Weakly Relational Pointer Domain: “These Are Not the Memory Cells You Are Looking For”Proceedings of the 10th ACM SIGPLAN International Workshop on Numerical and Symbolic Abstract Domains10.1145/3689609.3689994(2-9)Online publication date: 17-Oct-2024
https://dl.acm.org/doi/10.1145/3689609.3689994
An XJia XDu HXie Y(2024)Structure-Sensitive Pointer Analysis for Multi-structure ObjectsProceedings of the 15th Asia-Pacific Symposium on Internetware10.1145/3671016.3671396(155-164)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1145/3671016.3671396
Flanders MSharma RMichael AGrossman DKohlbrenner DTsafrir DMusuvathi MGupta RAbu-Ghazaleh N(2024)Avoiding Instruction-Centric Microarchitectural Timing Channels Via Binary-Code TransformationsProceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 210.1145/3620665.3640400(120-136)Online publication date: 27-Apr-2024
https://dl.acm.org/doi/10.1145/3620665.3640400
Milanese MMiné A(2024)Under-Approximating Memory AbstractionsStatic Analysis10.1007/978-3-031-74776-2_12(300-326)Online publication date: 20-Oct-2024
https://dl.acm.org/doi/10.1007/978-3-031-74776-2_12
Monat RMilanese MParolini FBoillot JOuadjaout AMiné A(2024)Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution)Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57256-2_26(387-392)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57256-2_26
Seidl HErhard JSchwarz MTilscher S(2024)2-Pointer LogicTaming the Infinities of Concurrency10.1007/978-3-031-56222-8_16(281-307)Online publication date: 20-Mar-2024
https://doi.org/10.1007/978-3-031-56222-8_16
Monat ROuadjaout AMiné A(2023)Mopsa-C: Modular Domains and Relational Abstract Interpretation for C Programs (Competition Contribution)Tools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_37(565-570)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_37
Nicole OLemerre MBardin SRival X(2021)No Crash, No Exploit: Automated Verification of Embedded Kernels2021 IEEE 27th Real-Time and Embedded Technology and Applications Symposium (RTAS)10.1109/RTAS52030.2021.00011(27-39)Online publication date: May-2021
https://doi.org/10.1109/RTAS52030.2021.00011
Monat ROuadjaout AMiné A(2021)A Multilanguage Static Analysis of Python Programs with Native C ExtensionsStatic Analysis10.1007/978-3-030-88806-0_16(323-345)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_16
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten