A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis

Patrick Cousot 1, 2 Radhia Cousot 1, 2 Francesco Logozzo 3
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : We introduce FunArray, a parametric segmentation abstract domain functor for the fully automatic and scalable analysis of array content properties. The functor enables a natural, painless and efficient lifting of existing abstract domains for scalar variables to the analysis of uniform compound data-structures such as arrays and collections (as well as matrices when instantiating the functor on itself). The analysis automatically and semantically divides arrays into consecutive non-overlapping possibly empty segments. Segments are delimited by sets of bound expressions and abstracted uniformly. All bound expressions appearing in a set are equal in the concrete. FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The bound expressions, the segment abstractions and the reduction operator are the three parameters of the analysis. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray inArrayal to adjust and experiment with the abstractions and the algorithms to obtain the appropriate precision/ratio cost. Then we implemented it into Clousot, an abstract interpretation-based static contract checker for .NET. We empirically validated the precision and the performance of the analysis by running it on the main libraries of .NET and on its own code. We were able to infer thousands of invariants and verify the implementation with a modest overhead (circa 1%). To the best of our knowledge this is the first analysis of this kind applied to such a large code base, and proven to scale.
Type de document :
Communication dans un congrès
ACM Press. Proceedings of the 38$^}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. 2011
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00543874
Contributeur : Patrick Cousot <>
Soumis le : lundi 6 décembre 2010 - 18:01:58
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : samedi 3 décembre 2016 - 01:57:31

Fichier

POPL090-Cousot-Cousot-Logozzo....
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00543874, version 1

Collections

Citation

Patrick Cousot, Radhia Cousot, Francesco Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. ACM Press. Proceedings of the 38$^}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. 2011. 〈inria-00543874〉

Partager

Métriques

Consultations de la notice

191

Téléchargements de fichiers

180