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
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 105
EP - 118
BT - POPL'11 - Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
T2 - 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'11
Y2 - 26 January 2011 through 28 January 2011
ER -