Eliminating stack overflow by abstract interpretation

ABSTRACT

An important correctness criterion for software running on embedded microcontrollers is stack safety: a guarantee that the call stack does not overflow. Our first contribution is a method for statically guaranteeing stack safety of interrupt-driven embedded software using an approach based on context-sensitive dataflow analysis of object code. We have implemented a prototype stack analysis tool that targets software for Atmel AVR microcontrollers and tested it on embedded applications compiled from up to 30,000 lines of C. We experimentally validate the accuracy of the tool, which runs in under 10 sec on the largest programs that we tested. The second contribution of this paper is the development of two novel ways to reduce stack memory requirements of embedded software.

REFERENCES

• 1: Alter, D. 2003. Online stack overflow detection on the TMS320C28x DSP. Texas Instruments Application Note SPRA820. http://www-s.ti.com/sc/psheets/spra820/spra820.pdf.
• 2: Atemu. 2004. Atemu: A sensor network emulator/simulator/debugger. Center for Satellite and Hybrid Communication Networks, University of Maryland. http://www.cshcn.umd.edu/research/atemu/.
• 3: Autopilot Project. 2004. http://autopilot.sourceforge.net.
• 4: Andrew Ayers , Richard Schooler , Robert Gottlieb, Aggressive inlining, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.134-145, June 16-18, 1997, Las Vegas, Nevada, United States
• 5: Baker, T. P. 1990. A stack-based resource allocation policy for realtime processes. In Proc. of the 11th IEEE Real-Time Systems Symp. (RTSS), Lake Buena Vista, FL. 191--200.
• 6: Balakrishnan, G. and Reps, T. 2004. Analyzing memory accesses in x86 executables. In Proc. of the Intl. Conf. on Compiler Construction (CC), Barcelona, Spain.
• 7: Barello, L. 2004. The AvrX real time kernel. http://barello.net/avrx.
• 8: Dennis Brylow , Niels Damgaard , Jens Palsberg, Static checking of interrupt-driven software, Proceedings of the 23rd International Conference on Software Engineering, p.47-56, May 12-19, 2001, Toronto, Ontario, Canada
• 9: Chatterjee, K., Ma, D., Majumdar, R., Zhao, T., Henzinger, T. A., and Palsberg, J. 2003. Stack size analysis for interrupt-driven programs. In Proc. of the 10th Static Analysis Symp., San Diego, CA. 109--126.
• 10: 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]
• 11: Saumya Debray , Robert Muth , Matthew Weippert, Alias analysis of executable code, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-24, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268948]
• 12: J. Engblom, Static Properties of Commercial Embedded Real-Time Programs, and Their Implication for Worst-Case Execution Time Analysis, Proceedings of the Fifth IEEE Real-Time Technology and Applications Symposium, p.46, June 02-04, 1999
• 13: Paolo Gai , Giuseppe Lipari , Marco Di Natale, Minimizing Memory Utilization of Real-Time Task Sets in Single and Multi-Processor Systems-on-a-Chip, Proceedings of the 22nd IEEE Real-Time Systems Symposium (RTSS'01), p.73, December 03-06, 2001
• 14: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 15: Heckmann, R. and Ferdinand, C. 2002. Stack usage analysis and software visualization for embedded processors. In Proc. of the Embedded Intelligence Congress, Nuremberg, Germany.
• 16: Jason Hill , Robert Szewczyk , Alec Woo , Seth Hollar , David Culler , Kristofer Pister, System architecture directions for networked sensors, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.93-104, November 2000, Cambridge, Massachusetts, United States
• 17: Rainer Leupers , Peter Marwedel, Function inlining under code size constraints for embedded processors, Proceedings of the 1999 IEEE/ACM international conference on Computer-aided design, p.253-256, November 07-11, 1999, San Jose, California, United States
• 18: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 19: Jens Palsberg , Di Ma, A Typed Interrupt Calculus, Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, p.291-310, September 09-12, 2002
• 20: 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]
• 21: 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
• 22: Reid, A., Flatt, M., Stoller, L., Lepreau, J., and Eide, E. 2000. Knit: Component composition for systems software. In Proc. of the 4th Symp. on Operating Systems Design and Implementation. Springer Verlag, San Diego, CA. 347--360.
• 23: Saksena, M. and Wang, Y. 2000. Scalable real-time system design using preemption thresholds. In Proc. of the 21st IEEE Real-Time Systems Symp. (RTSS), Orlando, FL.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.3 SPECIAL-PURPOSE AND APPLICATION-BASED SYSTEMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
      D.3.4 Processors

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages

General Terms:
Languages, Reliability, Verification

Keywords:
Microcontroller, abstract interpretation, call stack, context sensitive, dataflow analysis, interrupt-driven, sensor network