Deriving abstract transfer functions for analyzing embedded software

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 , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
• 3: Bruno De Bus , Bjorn De Sutter , Ludo Van Put , Dominique Chanet , Koen De Bosschere, Link-time optimization of ARM binaries, Proceedings of the 2004 ACM SIGPLAN/SIGBED conference on Languages, compilers, and tools for embedded systems, June 11-13, 2004, Washington, DC, USA
• 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 , Henry G. Dietz, Compiling for SIMD Within a Register, Proceedings of the 11th International Workshop on Languages and Compilers for Parallel Computing, p.290-304, August 07-09, 1998
• 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 , Per Stenström, An Integrated Path and Timing Analysis Method based onCycle-Level Symbolic Execution, Real-Time Systems, v.17 n.2-3, p.183-207, Nov. 1999 [doi>10.1023/A:1008138407139]
• 10: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 11: Norman Ramsey , Jack W. Davidson, Machine Descriptions to Build Tools for Embedded Systems, Proceedings of the ACM SIGPLAN Workshop on Languages, Compilers, and Tools for Embedded Systems, p.176-192, June 01, 1998
• 12: Rahul Razdan , Michael D. Smith, A high-performance microarchitecture with hardware-programmable functional units, Proceedings of the 27th annual international symposium on Microarchitecture, p.172-180, November 30-December 02, 1994, San Jose, California, United States [doi>10.1145/192724.192749]
• 13: John Regehr , Alastair Reid, HOIST: a system for automatically deriving static analyzers for embedded systems, Proceedings of the 11th international conference on Architectural support for programming languages and operating systems, October 07-13, 2004, Boston, MA, USA
• 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 W. Reps , Alexey Loginov , Mooly Sagiv, Semantic Minimization of 3-Valued Propositional Formulae, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.40, July 22-25, 2002
• 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 , Saman Amarasinghe, Bidwidth analysis with application to silicon compilation, Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation, p.108-120, June 18-21, 2000, Vancouver, British Columbia, Canada
• 18: Ben L. Titzer , Daniel K. Lee , Jens Palsberg, Avrora: scalable sensor network simulation with precise timing, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 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.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors

General Terms:
Algorithms, Languages, Reliability, Verification

Keywords:
abstract interpretation, embedded software, static analysis, transfer functions