Symbolic Execution for Memory Consumption Analysis
Chu Duc Jiep, Joxan Jaffar and Rasool Maghareh
Abstract
With the advances in both hardware and software of embedded systems in
the past few years, dynamic memory allocation can now be safely used
in embedded software. As a result, the need to develop methods to
avoid heap overflow errors in safety-critical embedded systems has
increased. Resource analysis of imperative programs with non-regular
loop patterns and signed integers, to support both memory allocation
and deallocation, has long been an open problem. Existing methods can
generate symbolic bounds that are parametric w.r.t. the program
inputs; such bounds, however, are imprecise in the presence of
non-regular loop patterns. In this paper, we present a worst-case
memory consumption analysis, based upon the framework of symbolic
execution. Our as- sumption is that loops (and recursions) of
to-be-analyzed programs are indeed bounded. We then can exhaustively
unroll loops and the memory consumption of each iteration can be
precisely computed and summarized for aggregation. Because of
path-sensitivity, our algorithm generates more precise
bounds. Importantly, we demon- strate that by introducing a new
concept of reuse, symbolic execu- tion scales to a set of realistic
benchmark programs.