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 ScholarDigital 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 '11We 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 ...
Comments