Space consumption analysis by abstract interpretation: Inference of recursive functions

• First space analysis for a functional language with regions.
• We use abstract interpretation on the infinite domain of multivariate monotonic functions.
• Our bounds go beyond multivariate polynomials.
• We have formally proved the correctness of all the results and implemented all the algorithms.

We present an abstract interpretation-based static analysis for inferring heap and stack memory consumption in a functional language. The language, called Safe, is eager and first-order, and its memory management system is based on heap regions instead of the more conventional approach of having a garbage collector. This paper begins by presenting Safe features by means of intuitive examples, and then defines its formal semantics, including the memory consumption of particular program executions. It continues by giving the abstract interpretation rules for non-recursive function definitions, and then how the memory consumption of recursive ones is approximated.An interesting property of our analysis is that, under certain reasonable conditions, the inferred bounds are reductive, which means that by iterating the analysis using as input the prior inferred bound, we can get tighter and tighter bounds, all of them correct. In some cases, even the exact bound is obtained. However, and due to lack of space, reductivity is not presented in this paper. The complete development can however be found in a technical report available at the authors' site.The paper includes a related work discussion, and small examples. Bigger case studies are presented in the fore-mentioned technical report.