Lifting Numerical Abstract Domains to Heap-manipulating Programs - Archive ouverte HAL Access content directly
Preprints, Working Papers, ... Year :

Lifting Numerical Abstract Domains to Heap-manipulating Programs

(1, 2) , (3) , (4)
1
2
3
4

Abstract

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.
Fichier principal
Vignette du fichier
nump_main.pdf (522.78 Ko) Télécharger le fichier
Origin : Files produced by the author(s)

Dates and versions

hal-00809826 , version 1 (09-04-2013)
hal-00809826 , version 2 (20-12-2013)
hal-00809826 , version 3 (20-12-2013)

Identifiers

  • HAL Id : hal-00809826 , version 1

Cite

Zhoulai Fu, Thomas Jensen, David Pichardie. Lifting Numerical Abstract Domains to Heap-manipulating Programs. 2013. ⟨hal-00809826v1⟩

Collections

CNRS INRIA IRISA
293 View
448 Download

Share

Gmail Facebook Twitter LinkedIn More