A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2011

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

Résumé

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.
Fichier principal
Vignette du fichier
POPL090-Cousot-Cousot-Logozzo.pdf (296.11 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00543874 , version 1 (06-12-2010)

Identifiants

  • HAL Id : inria-00543874 , version 1

Citer

Patrick Cousot, Radhia Cousot, Francesco Logozzo. A Parametric Segmentation Functor for Fully Automatic and Scalable Array Content Analysis. Proceedings of the 38$^{\mathrm{th}}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. ⟨inria-00543874⟩
121 Consultations
418 Téléchargements

Partager

Gmail Facebook X LinkedIn More