A Parametric segmentation functor for fully automatic and scalable array content analysis

Patrick Cousot, Radhia Cousot, Francesco Logozzo

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. 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 symbolic expressions appearing in a bound set are equal in the concrete. The FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The analysis is presented as a general framework parameterized by the choices of bound expressions, segment abstractions and the reduction operator. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray in Arrayal 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 non-trivial 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.

Original languageEnglish (US)
Title of host publicationPOPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
Pages105-118
Number of pages14
DOIs
StatePublished - 2010
Event38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11 - Austin, TX, United States
Duration: Jan 26 2011Jan 28 2011

Other

Other38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
CountryUnited States
CityAustin, TX
Period1/26/111/28/11

Fingerprint

Data structures
Concretes
Costs
Experiments

Keywords

  • Array abstraction
  • Array content analysis
  • Array property inference
  • Interpretation
  • Invariant synthesis
  • Program verification
  • Static analysis

ASJC Scopus subject areas

  • Software

Cite this

Cousot, P., Cousot, R., & Logozzo, F. (2010). A Parametric segmentation functor for fully automatic and scalable array content analysis. In POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 105-118) https://doi.org/10.1145/1926385.1926399

A Parametric segmentation functor for fully automatic and scalable array content analysis. / Cousot, Patrick; Cousot, Radhia; Logozzo, Francesco.

POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 105-118.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Cousot, P, Cousot, R & Logozzo, F 2010, A Parametric segmentation functor for fully automatic and scalable array content analysis. in POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 105-118, 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11, Austin, TX, United States, 1/26/11. https://doi.org/10.1145/1926385.1926399
Cousot P, Cousot R, Logozzo F. A Parametric segmentation functor for fully automatic and scalable array content analysis. In POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. p. 105-118 https://doi.org/10.1145/1926385.1926399
Cousot, Patrick ; Cousot, Radhia ; Logozzo, Francesco. / A Parametric segmentation functor for fully automatic and scalable array content analysis. POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 2010. pp. 105-118
@inproceedings{9325313485424bee99c27d20c196f810,
title = "A Parametric segmentation functor for fully automatic and scalable array content analysis",
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. 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 symbolic expressions appearing in a bound set are equal in the concrete. The FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The analysis is presented as a general framework parameterized by the choices of bound expressions, segment abstractions and the reduction operator. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray in Arrayal 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 non-trivial 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.",
keywords = "Array abstraction, Array content analysis, Array property inference, Interpretation, Invariant synthesis, Program verification, Static analysis",
author = "Patrick Cousot and Radhia Cousot and Francesco Logozzo",
year = "2010",
doi = "10.1145/1926385.1926399",
language = "English (US)",
isbn = "9781450304900",
pages = "105--118",
booktitle = "POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages",

}

TY - GEN

T1 - A Parametric segmentation functor for fully automatic and scalable array content analysis

AU - Cousot, Patrick

AU - Cousot, Radhia

AU - Logozzo, Francesco

PY - 2010

Y1 - 2010

N2 - 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. 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 symbolic expressions appearing in a bound set are equal in the concrete. The FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The analysis is presented as a general framework parameterized by the choices of bound expressions, segment abstractions and the reduction operator. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray in Arrayal 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 non-trivial 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.

AB - 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. 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 symbolic expressions appearing in a bound set are equal in the concrete. The FunArray can be naturally combined via reduced product with any existing analysis for scalar variables. The analysis is presented as a general framework parameterized by the choices of bound expressions, segment abstractions and the reduction operator. Once the functor has been instantiated with fixed parameters, the analysis is fully automatic. We first prototyped FunArray in Arrayal 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 non-trivial 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.

KW - Array abstraction

KW - Array content analysis

KW - Array property inference

KW - Interpretation

KW - Invariant synthesis

KW - Program verification

KW - Static analysis

UR - http://www.scopus.com/inward/record.url?scp=79952016331&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952016331&partnerID=8YFLogxK

U2 - 10.1145/1926385.1926399

DO - 10.1145/1926385.1926399

M3 - Conference contribution

AN - SCOPUS:79952016331

SN - 9781450304900

SP - 105

EP - 118

BT - POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

ER -