article

Deriving abstract transfer functions for analyzing embedded software

Authors:

Usit DuongsaaAuthors Info & Claims

ACM SIGPLAN Notices, Volume 41, Issue 7

Pages 34 - 43

https://doi.org/10.1145/1159974.1134657

Published: 14 June 2006 Publication History

Abstract

This paper addresses the problem of creating abstract transfer functions supporting dataflow analyses. Writing these functions by hand is problematic: transfer functions are difficult to understand, difficult to make precise, and difficult to debug. Bugs in transfer functions are particularly serious since they defeat the soundness of any program analysis running on top of them. Furthermore, implementing transfer functions by hand is wasteful because the resulting code is often difficult to reuse in new analyzers and to analyze new languages. We have developed algorithms and tools for deriving transfer functions for the bitwise and unsigned interval abstract domains. The interval domain is standard; in the bitwise domain, values are vectors of three-valued bits. For both domains, important challenges are to derive transfer functions that are sound in the presence of integer overflow, and to derive precise transfer functions for operations whose semantics are a mismatch for the domain (i.e., bit-vector operations in the interval domain and arithmetic operations in the bitwise domain). We can derive transfer functions, and execute them, in time linear in the bitwidth of the operands. These functions are maximally precise in most cases. Our generated transfer functions are parameterized by a bitwidth and are independent of the language being analyzed, and also of the language in which the analyzer is written. Currently, we generate interval and bitwise transfer functions in C and OCaml for analyzing C source code, ARM object code, and AVR object code. We evaluate our derived functions by using them in an interprocedural dataflow analyzer.

References

[1]

Atmel Corp. Atmel AVR 8-bit RISC family. http://www.atmel.com/products/avr.]]

[2]

Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proc. of the 4th Symp. on Principles of Programming Languages (POPL), pages 238--252, Los Angeles, CA, January 1977.]]

Digital Library

[3]

Bruno De Bus, Bjorn De Sutter, Ludo Van Put, Dominique Chanet, and Koen De Bosschere. Link-time optimization of ARM binaries. In Proc. of the 2004 Conf. on Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 211--220, Washington, DC, June 2004.]]

Digital Library

[4]

Jakob Engblom, Andreas Ermedahl, Mikael Nolin, Jan Gustafsson, and Hans Hansson. Worst-case execution-time analysis for embedded real-time systems. Journal of Software Tool and Transfer Technology (STTT), 4(4):437--455, August 2003.]]

[5]

Randall J. Fisher and Henry G. Dietz. Compiling for SIMD within a register. In Proc. of the 11th Intl. Workshop on Languages and Compilers for Parallel Computing, pages 290--304, Chapel Hill, NC, 1998.]]

Digital Library

[6]

Anthony Fox. Formal specification and verification of ARM6. In Proc. of the 16th Intl. Conf. on Theorem Proving in Higher Order Logics (TPHOLs), pages 25--40, Rome, Italy, September 2003.]]

[7]

John K. Gough and Herbert Klaeren. Eliminating range checks using static single assignment form. In Proc. of the 19th Australian Computer Science Conf., Melbourne, Australia, January 1996.]]

[8]

ARM Ltd. ARM7 32-bit RISC Family. http://www.arm.com/products/CPUs/families/ARM7Family.html.]]

[9]

Thomas Lundqvist and Per Stenström. An integrated path and timing analysis method based on cycle-level symbolic execution. Journal of Real-Time Systems, 17(2/3):183--207, November 1999.]]

Digital Library

[10]

George C. Necula, Scott McPeak, S. P. Rahul, and Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In Proc. of the Intl. Conf. on Compiler Construction (CC), pages 213--228, Grenoble, France, April 2002.]]

Digital Library

[11]

Norman Ramsey and Jack W. Davidson. Machine descriptions to build tools for embedded systems. In Proc. of the 1998 Workshop on Languages, Compilers, and Tools for Embedded Systems (LCTES), pages 176--192, Montreal, Canada, June 1998.]]

Digital Library

[12]

Rahul Razdan and Michael D. Smith. A high-performance microarchitecture with hardware-programmable functional units. In Proc. of the 27th Intl. Symp. on Microarchitecture (MICRO), pages 172--180, San Jose, CA, November 1994.]]

Digital Library

[13]

John Regehr and Alastair Reid. Hoist: A system for automatically deriving static analyzers for embedded systems. In Proc. of the 11th Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), October 2004.]]

Digital Library

[14]

John Regehr, Alastair Reid, and Kirk Webb. Eliminating stack overflow by abstract interpretation. In Proc. of the 3rd Intl. Conf. on Embedded Software (EMSOFT), pages 306--322, Philadelphia, PA, October 2003.]]

[15]

Thomas Reps, Alexey Loginov, and Mooly Sagiv. Semantic minimization of 3-valued propositional formulae. In Proc. of the 17th IEEE Symp. on Logic in Computer Science (LICS 2002), Copenhagen, Denmark, July 2002.]]

Digital Library

[16]

Erika Rice, Sorin Lerner, and Craig Chambers. Automatically inferring sound dataflow functions from dataflow fact schemas. In Proc. of the 4th Intl. Workshop on Compiler Optimization Meets Compiler Verification, Edinburgh, UK, April 2005.]]

[17]

Mark Stephenson, Jonathan Babb, and Saman Amarasinghe. Bitwidth analysis with application to silicon compilation. In Proc. of the Conf. on Programming Language Design and Implementation (PLDI), pages 108--120, Vancouver, Canada, June 2000.]]

Digital Library

[18]

Ben L. Titzer, Daniel Lee, and Jens Palsberg. Avrora: Scalable sensor network simulation with precise timing. In Proc. of the 4th Intl. Conf. on Information Processing in Sensor Networks (IPSN), Los Angeles, CA, April 2005.]]

Digital Library

[19]

Greta Yorsh, Thomas Reps, and Mooly Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In Proc. of the 10th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Barcelona, Spain, March 2004.]]

Cited By

Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Vishwanathan HShachnai MNarayana SNagarakatte SLee J(2022)Sound, precise, and fast abstract interpretation with tristate numbersProceedings of the 20th IEEE/ACM International Symposium on Code Generation and Optimization10.1109/CGO53902.2022.9741267(254-265)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1109/CGO53902.2022.9741267
Godefroid PTaly A(2012)Automated synthesis of symbolic instruction encodings from I/O samplesACM SIGPLAN Notices10.1145/2345156.225411647:6(441-452)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2345156.2254116
Show More Cited By

Index Terms

Deriving abstract transfer functions for analyzing embedded software
1. Software and its engineering
  1. Software notations and tools
    1. Compilers

Recommendations

Pluggable abstract domains for analyzing embedded software
Proceedings of the 2006 LCTES Conference

Many abstract value domains such as intervals, bitwise, constants, and value-sets have been developed to support dataflow analysis. Different domains offer alternative tradeoffs between analysis speed and precision. Furthermore, some domains are a ...
Pushdown control-flow analysis for free
POPL '16

Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Interval analysis of microcontroller code using abstract interpretation of hardware and software
SCOPES '10: Proceedings of the 13th International Workshop on Software & Compilers for Embedded Systems

Static analysis is often performed on source code where intervals -- possibly the most widely used numeric abstract domain -- have successfully been used as a program abstraction for decades. Binary code on microcontroller platforms, however, is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

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

21
Total Citations
View Citations
310
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Küchler AWenning LWendland F(2023)AbsIntIO: Towards Showing the Absence of Integer Overflows in Binaries using Abstract InterpretationProceedings of the 2023 ACM Asia Conference on Computer and Communications Security10.1145/3579856.3582814(247-258)Online publication date: 10-Jul-2023
https://dl.acm.org/doi/10.1145/3579856.3582814
Vishwanathan HShachnai MNarayana SNagarakatte SLee J(2022)Sound, precise, and fast abstract interpretation with tristate numbersProceedings of the 20th IEEE/ACM International Symposium on Code Generation and Optimization10.1109/CGO53902.2022.9741267(254-265)Online publication date: 2-Apr-2022
https://dl.acm.org/doi/10.1109/CGO53902.2022.9741267
Godefroid PTaly A(2012)Automated synthesis of symbolic instruction encodings from I/O samplesACM SIGPLAN Notices10.1145/2345156.225411647:6(441-452)Online publication date: 11-Jun-2012
https://dl.acm.org/doi/10.1145/2345156.2254116
Yoon YLee WYi K(2023)Inductive Program Synthesis via Iterative Forward-Backward Abstract InterpretationProceedings of the ACM on Programming Languages10.1145/35912887:PLDI(1657-1681)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591288
Vishwanathan HShachnai MNarayana SNagarakatte S(2023)Verifying the Verifier: eBPF Range Analysis VerificationComputer Aided Verification10.1007/978-3-031-37709-9_12(226-251)Online publication date: 17-Jul-2023
https://doi.org/10.1007/978-3-031-37709-9_12
Cheng XZhou MSong XGu MSun J(2021)Automatic Integer Error Repair by Proper-Type InferenceIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2019.291386218:2(918-935)Online publication date: 1-Mar-2021
https://doi.org/10.1109/TDSC.2019.2913862
Heule SSchkufza ESharma RAiken A(2016)Stratified synthesis: automatically learning the x86-64 instruction setACM SIGPLAN Notices10.1145/2980983.290812151:6(237-250)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2980983.2908121
Heule SSchkufza ESharma RAiken AKrintz CBerger E(2016)Stratified synthesis: automatically learning the x86-64 instruction setProceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/2908080.2908121(237-250)Online publication date: 2-Jun-2016
https://dl.acm.org/doi/10.1145/2908080.2908121
Sharma RSchkufza EChurchill BAiken A(2015)Conditionally correct superoptimizationACM SIGPLAN Notices10.1145/2858965.281427850:10(147-162)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2858965.2814278
Sharma RSchkufza EChurchill BAiken AAldrich JEugster P(2015)Conditionally correct superoptimizationProceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications10.1145/2814270.2814278(147-162)Online publication date: 23-Oct-2015
https://dl.acm.org/doi/10.1145/2814270.2814278
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.

Media

Figures

Other

Tables

View Issue’s Table of Contents