article

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

Author:

Antoine MinéAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 7

Pages 54 - 63

https://doi.org/10.1145/1159974.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

Gurfinkel ANavas J(2022)Abstract Interpretation of LLVM with a Region-Based Memory ModelSoftware Verification10.1007/978-3-030-95561-8_8(122-144)Online publication date: 22-Feb-2022
https://doi.org/10.1007/978-3-030-95561-8_8
Delmas DOuadjaout AMiné A(2021)Static Analysis of Endian Portability by Abstract InterpretationStatic Analysis10.1007/978-3-030-88806-0_5(102-123)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_5
Mansur MMariano BChristakis MNavas JWüstholz V(2021)Automatically Tailoring Abstract Interpretation to Custom Usage ScenariosComputer Aided Verification10.1007/978-3-030-81688-9_36(777-800)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_36
Show More Cited By

Index Terms

Recommendations

Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics
LCTES '06: Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems

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 ...
Field-sensitive unreachability and non-cyclicity analysis

Field-sensitive static analyses of object-oriented code use approximations of the computational states where fields are taken into account, for better precision. This article presents a novel and sound definite analysis of Java bytecode that ...
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 ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

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

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

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 June 2006

Published in SIGPLAN Volume 41, Issue 7

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

80
Total Citations
View Citations
711
Total Downloads

Downloads (Last 12 months)26
Downloads (Last 6 weeks)4

Reflects downloads up to 08 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gurfinkel ANavas J(2022)Abstract Interpretation of LLVM with a Region-Based Memory ModelSoftware Verification10.1007/978-3-030-95561-8_8(122-144)Online publication date: 22-Feb-2022
https://doi.org/10.1007/978-3-030-95561-8_8
Delmas DOuadjaout AMiné A(2021)Static Analysis of Endian Portability by Abstract InterpretationStatic Analysis10.1007/978-3-030-88806-0_5(102-123)Online publication date: 13-Oct-2021
https://doi.org/10.1007/978-3-030-88806-0_5
Mansur MMariano BChristakis MNavas JWüstholz V(2021)Automatically Tailoring Abstract Interpretation to Custom Usage ScenariosComputer Aided Verification10.1007/978-3-030-81688-9_36(777-800)Online publication date: 15-Jul-2021
https://doi.org/10.1007/978-3-030-81688-9_36
Ouadjaout AMiné A(2021)A Library Modeling Language for the Static Analysis of C ProgramsStatic Analysis10.1007/978-3-030-65474-0_11(223-247)Online publication date: 13-Jan-2021
https://doi.org/10.1007/978-3-030-65474-0_11
Journault MMiné AMonat ROuadjaout A(2020)Combinations of Reusable Abstract Domains for a Multilingual Static AnalyzerVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-41600-3_1(1-18)Online publication date: 14-Mar-2020
https://doi.org/10.1007/978-3-030-41600-3_1
Lei YSui Y(2019)Fast and Precise Handling of Positive Weight Cycles for Field-Sensitive Pointer AnalysisStatic Analysis10.1007/978-3-030-32304-2_3(27-47)Online publication date: 2-Oct-2019
https://doi.org/10.1007/978-3-030-32304-2_3
Payet ÉSpoto F(2018)Checking Array Bounds by Abstract Interpretation and Symbolic ExpressionsAutomated Reasoning10.1007/978-3-319-94205-6_46(706-722)Online publication date: 30-Jun-2018
https://doi.org/10.1007/978-3-319-94205-6_46
Cuoq PRunarvot LCherepanov A(2017)Detecting Strict Aliasing Violations in the WildVerification, Model Checking, and Abstract Interpretation10.1007/978-3-319-52234-0_2(14-33)Online publication date: 12-Jan-2017
https://doi.org/10.1007/978-3-319-52234-0_2
Blazy SLaporte VPichardie D(2016)An abstract memory functor for verified C static analyzersACM SIGPLAN Notices10.1145/3022670.295193751:9(325-337)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/3022670.2951937
Blazy SLaporte VPichardie DGarrigue JKeller GSumii E(2016)An abstract memory functor for verified C static analyzersProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951937(325-337)Online publication date: 4-Sep-2016
https://dl.acm.org/doi/10.1145/2951913.2951937
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 Issue’s Table of Contents