| John Regehr and Alastair Reid |
| regehr@cs.utah.edu reid@cs.utah.edu |
In Proceedings of the Eleventh International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 133-143, Boston, MA, October 9-13 2004.
Embedded software must meet conflicting requirements such as being highly reliable, running on resource-constrained platforms, and being developed rapidly. Static program analysis can help meet all of these goals. People developing analyzers for embedded object code face a difficult problem: writing an abstract version of each instruction in the target architecture(s). This is currently done by hand, resulting in abstract operations that are both buggy and imprecise. We have developed Hoist: a novel system that solves these problems by automatically constructing abstract operations using a microprocessor (or simulator) as its own specification. With almost no input from a human, Hoist generates a collection of C functions that are ready to be linked into an abstract interpreter. We demonstrate that Hoist generates abstract operations that are correct, having been extensively tested, sufficiently fast, and substantially more precise than manually written abstract operations. Hoist is currently limited to eight-bit machines due to costs exponential in the word size of the target architecture. It is essential to be able to analyze software running on these small processors: they are important and ubiquitous, with many embedded and safety-critical systems being based on them.
| John Regehr <regehr@cs.utah.edu> |