Skip to Main content Skip to Navigation
Conference papers

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 - ENS Paris, 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [34 references]  Display  Hide  Download

https://hal.inria.fr/inria-00543874
Contributor : Patrick Cousot Connect in order to contact the contributor
Submitted on : Monday, December 6, 2010 - 6:01:58 PM
Last modification on : Thursday, March 17, 2022 - 10:08:36 AM
Long-term archiving on: : Saturday, December 3, 2016 - 1:57:31 AM

File

POPL090-Cousot-Cousot-Logozzo....
Files produced by the author(s)

Identifiers

  • 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. Proceedings of the 38$^}$ Annual ACM Symposium on Principles Of Programming Languages (POPL), Jan 2011, Austin, Texas, United States. ⟨inria-00543874⟩

Share

Metrics

Record views

100

Files downloads

376