Eliminating stack overflow by abstract interpretation

John Regehr Alastair Reid Kirk Webb
regehr@cs.utah.edu    reid@cs.utah.edu    kwebb@cs.utah.edu   

University of Utah, School of Computing
50 South Central Campus Drive, Room 3190
Salt Lake City, Utah 84112-9205
http://www.cs.utah.edu/flux/

Abstract

An important correctness criterion for software running on embedded microcontrollers is stack safety: a guarantee that the call stack does not overflow. We address two aspects of the problem of creating stack-safe embedded software that also makes efficient use of memory: statically bounding worst-case stack depth, and automatically reducing stack memory requirements. Our first contribution is a method for statically guaranteeing stack safety by performing whole-program analysis, using an approach based on context-sensitive abstract interpretation of machine code. Abstract interpretation permits our analysis to accurately model when interrupts are enabled and disabled, which is essential for accurately bounding the stack depth of typical embedded systems. We have implemented a stack analysis tool that targets 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 a few seconds on the largest programs that we tested. The second contribution of this paper is a novel framework for automatically reducing stack memory requirements. We show that goal-directed global function inlining can be used to reduce the stack memory requirements of component-based embedded software, on average, to 40% of the requirement of a system compiled without inlining, and to 68% of the requirement of a system compiled with aggressive whole-program inlining that is not directed towards reducing stack usage.

In Proceedings of the Third International Conference on Embedded Software (EMSOFT 2003), pages 306-322, Philadelphia, PA, October 15-17 2003.

This paper is © Springer-Verlag 2003.

For more information see the Stacktool web page.


John Regehr <regehr@cs.utah.edu>