Lifting Numerical Abstract Domains to Heap-manipulating Programs
2013
The abstract interpretation literature is rich with numerical abstract domains that allow to infer numerical properties on scalar program variables. Unfortunately, lifting this domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. Our approach allows us to prove the soundness of the combined analysis based on the soundness hypotheses of the existing analyses, and it also facilitates the modular implementation of the analysis. We have prototyped this approach using the \SOOT framework for pointer analyses and the PPL library as numerical domains. Our experiments on the DaCapo benchmark suite show that the combined analysis discovers significantly more numerical invariants than traditional numerical domains with modest time overhead.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
20
References
0
Citations
NaN
KQI