Patrick Cousot
Radhia Cousot
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.
Supplemental Material
- M. Barnett, K. Leino, and W. Schulte. The Spec# programming system: An overview. CASSIS'04, LNCS 3362, 49--69. Springer, 2005. Google Scholar
Digital Library
- M. Barnett, B.-Y. Chang, R. DeLine, B. Jacobs, and K. Leino. Boogie: A modular reusable verifier for object-oriented programs. FMCO'05, LNCS 4111, 364--387. Springer, 2006. Google ScholarDigital Library
- M. Barnett, M. Fähndrich, and F. Logozzo. Embedded contract languages. SAC'10. ACM, 2010. Google ScholarDigital Library
- D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. PLDI'07, 300--309. ACM, 2007. Google ScholarDigital Library
- P. Chalin, J. Kinirya, G. Leavens, and E. Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. FMCO'05, LNCS 4111, 77--101. Springer, 2006. Google ScholarDigital Library
- P. Cousot. Verification by abstract interpretation. Verification -- Theory & Practice, LNCS 2772, 243--268. Springer, 2003.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. 4th POPL, 238--252. ACM, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. 6th POPL, 269--282. ACM, 1979. Google ScholarDigital Library
- P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. Combination of abstractions in the Astrée static analyzer. ASIAN, LNCS 4435, 272--300. Springer, 2006. Google ScholarDigital Library
- er(2008)}z3BjornerDeMouraL. de Moura and N. Bjørner. Z3: An efficient SMT solver. phTACAS’08, LNCS 4963, 337--340. Springer, 2008. Google ScholarDigital Library
- D. Dill. Timing assumptions and verification of finite-state concurrent systems. Automatic Verification Methods for Finite State Systems, LNCS 407, 197--212. Springer, 1989. Google ScholarDigital Library
- I. Dillig, T. Dillig, and A. Aiken. Fluid updates: Beyond strong vs. weak updates. ESOP'10, LNCS 6012, 246--266. Springer, 2010. Google ScholarDigital Library
- I. Dillig, T. Dillig, and A. Aiken. Precise reasoning for programs using containers. 37th POPL. ACM, 2011. Google ScholarDigital Library
- M. Fähndrich and F. Logozzo. Static contract checking with abstract interpretation. FoVeOOS'10, LNCS. Springer, 2010.Google Scholar
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. 29th POPL, 191--202. ACM, 2002. Google ScholarDigital Library
- Garmin Int. Garmin device interface specification. Technical report, Garmin Int., Inc., Olathe, 2006. www.garmin.com/support/pdf/iop_spec.pdf.Google Scholar
- D. Gopan, T. Reps, and S. Sagiv. A framework for numeric analysis of array operations. 32nd POPL, 338--350. ACM, 2005. Google ScholarDigital Library
- S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified logical domains. 35th POPL, 235--246. ACM, 2008. Google ScholarDigital Library
- N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. PLDI'2008, 339--348. ACM, 2008. Google ScholarDigital Library
- R. Jhala and K. McMillan. Array abstractions from proofs. CAV'07, LNCS 4590, 193--206. Springer, 2007. Google ScholarDigital Library
- M. Karr. Affine relationships among variables of a program. Acta Inf., 6: 133--151, 1976.Google ScholarDigital Library
- G. Kildall. A unified approach to global program optimization. 1st POPL, 194--206. ACM, 1973. Google ScholarDigital Library
- L. Kovács and A. Voronkov. Finding loop invariants for programs over arrays using a theorem prover. FASE'2009, LNCS 5503, 470--485. Springer, 2009. Google ScholarDigital Library
- V. Laviron and F. Logozzo. Subpolyhedra: A (more) scalable approach to infer linear inequalities. VMCAI, LNCS 5403, 229--244. Springer, 2009. Google ScholarDigital Library
- S.-H. Lee and D.-H. Cho. Packet-scheduling algorithm based on priority of separate buffers for unicast and multicast services. Electronics Letters, 39 (2): 259--260, 2003.Google ScholarCross Ref
- F. Logozzo. Class-level modular analysis for object oriented languages. SAS'03, LNCS 2694, 37--54. Springer, 2003. Google ScholarDigital Library
- F. Logozzo and M. Fähndrich. On the relative completeness of bytecode analysis versus source code analysis. CC'08, LNCS 4959, 197--212. Springer, 2008. Google ScholarDigital Library
- F. Logozzo and M. Fähndrich. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. SAC, 184--188. ACM, 2008. Google ScholarDigital Library
- M. Marron, D. Stefanovic, M. Hermenegildo, and D. Kapur. Heap analysis in the presence of collection libraries. PASTE'07, 31--36. ACM, 2007. Google ScholarDigital Library
- K. L. McMillan. Quantified invariant generation using an interpolating saturation prover. TACAS'08, LNCS 4963, 197--212. Springer, 2008. Google ScholarDigital Library
- B. Meyer. Eiffel: The Language. Prentice Hall, 1991. Google ScholarDigital Library
- A. Miné. The octagon abstract domain. Higher-Order and Symbolic Computation, 19: 31--100, 2006. Google ScholarDigital Library
- V. Pratt. Two easy theories whose combination is hard. Technical report, MIT, 1977. boole.stanford.edu/pub/sefnp.pdf.Google Scholar
- B. Roy. Transitivité et connexité. Comptes-Rendus del'Académie des Sciences de Paris, Sér. A-B, 249: 216--218, 1959.Google Scholar
- M. Seghir, A. Podelski, and T. Wies. Abstraction refinement for quantified array assertions. SAS'09, LNCS 5673, 3--18. Springer, 2009. Google ScholarDigital Library
- R. Shostak. Deciding linear inequalities by computing loop residues. JACM, 28 (4): 769--779, 1981. Google ScholarDigital Library
- H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P. W. O'Hearn. Scalable shape analysis for systems code. CAV'98, LNCS 5123, 385--398. Springer, 2008. Google ScholarDigital Library
Index Terms
- A parametric segmentation functor for fully automatic and scalable array content analysis
Recommendations
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 languagesWe 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 ...
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Reviews
Ramesh S
Precise and scalable static analysis of realistic software is challenging due to several complex features used in software. One of these features, which has been the focus of attention in recent times, is an array. In spite of several proposals for the static analysis of programs with arrays, the scalability of these analysis procedures has been an issue. This paper proposes a solution to this problem. The central contribution of this paper is FunArray, a new abstract domain for arrays. FunArray is actually a functor that can take other abstract domains used for scalar variables and expressions and provide a domain for the arrays. This enables one to choose from the different analysis methods in the scalar variables and expressions, thereby making a tradeoff between precision and speed at the array level. This abstraction is based on a novel and powerful symbolic representation of arrays as a sequence of consecutive nonoverlapping segments. The strength of this representation stems from the fact that it compactly represents the different cases that one needs to consider while abstracting a concrete array, making the analysis scalable. The array abstraction is implemented in Clousot, a tool that can automatically generate invariants of programs involving array variables. Clousot has been used to successfully analyze several libraries in .NET that are beyond the reach of other existing techniques. The authors of this paper are well-known experts in the field. The many examples, as well as the motivating beginning, definitely ease the readability of the paper. The paper is a bit cryptic, though, which is possibly due to size restrictions. An initial reading is likely to pose some difficulties for readers since the presentation contains some unexplained notations, such as "oo" for infinity. Some typographical errors in crucial places further complicate readability. Overall, though, the paper is accessible and useful for researchers working in the area of static analysis. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments