More Web Proxy on the site http://driver.im/

research-article

On inter-procedural analysis of programs with lists and data

Authors:

Ahmed Bouajjani,

Cezara Drăgoi,

Constantin Enea,

Mihaela SighireanuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 46, Issue 6

Pages 578 - 589

https://doi.org/10.1145/1993316.1993566

Published: 04 June 2011 Publication History

Abstract

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program configurations are represented by graphs where nodes represent list segments without sharing. The data in these list segments are characterized by constraints in abstract domains. We consider a domain where constraints are in a universally quantified fragment of the first-order logic over sequences, as well as a domain constraining the multisets of data in sequences.

Our analysis computes the effect of each procedure in a local manner, by considering only the reachable part of the heap from its actual parameters. In order to avoid losses of information, we introduce a mechanism based on unfolding/folding operations allowing to strengthen the analysis in the domain of first-order formulas by the analysis in the multisets domain.

The same mechanism is used for strengthening the sound (but incomplete) entailment operator of the domain of first-order formulas. We have implemented our techniques in a prototype tool and we have shown that our approach is powerful enough for automatic (1) generation of non-trivial procedure summaries, (2) pre/post-condition reasoning, and (3) procedure equivalence checking.

References

[1]

D. Beyer, T.A. Henzinger, R. Majumdar, and A. Rybalchenko. Invariant synthesis for combined theories. In VMCAI, volume 4349 of LNCS, pages 378--394. Springer, 2007.

Digital Library

[2]

A. Bouajjani, C. Drăgoi, C. Enea, A. Rezine, and M. Sighireanu. Invariant synthesis for programs manipulating lists with unbounded data. In CAV, volume 6174 of LNCS, pages 72--88. Springer, 2010.

[3]

C. Calcagno, D. Distefano, P.W. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. In POPL, pages 289--300. ACM, 2009.

Digital Library

[4]

CEA. Frama-C Platform. htp://frama-c.com.

[5]

Celia plugin. http://www.liafa.jussieu.fr/celia.

[6]

B.-Y.E. Chang and X. Rival. Relational inductive shape analysis. In POPL, pages 247--260. ACM, 2008.

Digital Library

[7]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pages 238--252. ACM, 1977.

Digital Library

[8]

P. Cousot and R. Cousot. Static determination of dynamic properties of recursive procedures. In IFIP Conf. on Formal Description of Programming Concepts, pages 237--277. North-Holland Publishing Company, 1977.

[9]

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In POPL, pages 269--282. ACM, 1979.

Digital Library

[10]

P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511--547, 1992.

[11]

A. Deutsch. On determining lifetime and aliasing of dynamically allocated data in higher-order functional specifications. In POPL, pages 157--168. ACM, 1990.

Digital Library

[12]

S. Gulwani, T. Lev-Ami, and S. Sagiv. A combination framework for tracking partition sizes. In POPL, pages 239--251. ACM, 2009.

Digital Library

[13]

S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified logical domains. In POPL, pages 235--246. ACM, 2008.

Digital Library

[14]

A. Gupta, R. Majumdar, and A. Rybalchenko. From tests to proofs. In TACAS, volume 5505 of LNCS, pages 262--276. Springer, 2009.

[15]

N. Halbwachs and M. Péron. Discovering properties about arrays in simple programs. In PLDI, pages 339--348. ACM, 2008.

Digital Library

[16]

B. Jeannet. Fixpoint. http://gforge.inria.fr/.

[17]

B. Jeannet and A. Miné. Apron: A library of numerical abstract domains for static analysis. In CAV, volume 5643 of LNCS, pages 661--667. Springer, 2009.

[18]

R. Jhala and K.L. McMillan. Array abstractions from proofs. In CAV, volume 4590 of LNCS, pages 193--206. Springer, 2007.

Digital Library

[19]

R. Manevich, E. Yahav, G. Ramalingam, and S. Sagiv. Predicate abstraction and canonical abstraction for singly-linked lists. In VMCAI, volume 3385 of LNCS, pages 181--198. Springer, 2005.

[20]

B. McCloskey, T.W. Reps, and S. Sagiv. Statically inferring complex heap, array, and numeric invariants. In SAS, volume 6337 of LNCS, pages 71--99. Springer, 2010.

Digital Library

[21]

V. Perrelle and N. Halbwachs. An analysis of permutations in arrays. In VMCAI, volume 5944 of LNCS, pages 279--294, 2010.

Digital Library

[22]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55--74. IEEE Computer Society, 2002.

Digital Library

[23]

N. Rinetzky, J. Bauer, T.W. Reps, S. Sagiv, and R. Wilhelm. A semantics for procedure local heaps and its abstractions. In POPL, pages 296--309. ACM, 2005.

Digital Library

[24]

N. Rinetzky, S. Sagiv, and E. Yahav. Interprocedural shape analysis for cutpoint-free programs. In SAS, volume 3672 of LNCS, pages 284--302. Springer, 2005.

[25]

X. Rival and B.-Y.E. Chang. Calling context abstraction with shapes. In POPL, pages 173--186. ACM, 2011.

Digital Library

[26]

X. Rival and L. Mauborgne. The trace partitioning abstract domain. ACM Transactions on Programming Languages and Systems, 29, 2007.

Digital Library

[27]

S. Sagiv, T.W. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, 24(3):217--298, 2002.

Digital Library

[28]

M. Sharir and A. Pnueli. Two approaches to interprocedural data flow analysis. In Program Flow Analysis: Theory and Applications, pages 189--234. New York University, 1981.

[29]

V. Vafeiadis. Shape-value abstraction for verifying linearizability. In VMCAI, volume 5403 of LNCS, pages 335--348. Springer, 2009.

Cited By

Huihui CHongwei Z(2021)Optimizing demand‐driven null dereference verification via merging branchesExpert Systems10.1111/exsy.1270739:6Online publication date: 27-May-2021
https://doi.org/10.1111/exsy.12707
Illous HLemerre MRival X(2021)A relational shape abstract domainFormal Methods in System Design10.1007/s10703-021-00366-4Online publication date: 24-Apr-2021
https://doi.org/10.1007/s10703-021-00366-4
Fang BSighireanu M(2017)Hierarchical Shape Abstraction for Analysis of Free List Memory AllocatorsLogic-Based Program Synthesis and Transformation10.1007/978-3-319-63139-4_9(151-167)Online publication date: 25-Jul-2017
https://doi.org/10.1007/978-3-319-63139-4_9
Show More Cited By

Index Terms

On inter-procedural analysis of programs with lists and data

Recommendations

On inter-procedural analysis of programs with lists and data
PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation

We address the problem of automatic synthesis of assertions on sequential programs with singly-linked lists containing data over infinite domains such as integers or reals. Our approach is based on an accurate abstract inter-procedural analysis. Program ...
Interprocedural pointer alias analysis

We present practical approximation methods for computing and representing interprocedural aliases for a program written in a language that includes pointers, reference parameters, and recursion. We present the following contributions: (1) a framework ...
Precise and efficient integration of interprocedural alias information into data-flow analysis

Data-flow analysis is a basis for program optimization and parallelizing transformations. The mechanism of passing reference parameters at call sites generates interprocedural aliases which complicate this analysis. Solutions have been developed for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 46, Issue 6

PLDI '11

June 2011

652 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/1993316

Issue’s Table of Contents

PLDI '11: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2011
668 pages
ISBN:9781450306638
DOI:10.1145/1993498
General Chair:
Mary Hall
University of Utah
,
Program Chair:
David Padua
University of Illinois at Urbana-Champaign

Copyright © 2011 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 June 2011

Published in SIGPLAN Volume 46, Issue 6

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

29
Total Citations
View Citations
409
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)1

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Huihui CHongwei Z(2021)Optimizing demand‐driven null dereference verification via merging branchesExpert Systems10.1111/exsy.1270739:6Online publication date: 27-May-2021
https://doi.org/10.1111/exsy.12707
Illous HLemerre MRival X(2021)A relational shape abstract domainFormal Methods in System Design10.1007/s10703-021-00366-4Online publication date: 24-Apr-2021
https://doi.org/10.1007/s10703-021-00366-4
Fang BSighireanu M(2017)Hierarchical Shape Abstraction for Analysis of Free List Memory AllocatorsLogic-Based Program Synthesis and Transformation10.1007/978-3-319-63139-4_9(151-167)Online publication date: 25-Jul-2017
https://doi.org/10.1007/978-3-319-63139-4_9
Kirchner FKosmatov NPrevosto VSignoles JYakobowski B(2015)Frama-C: A software analysis perspectiveFormal Aspects of Computing10.1007/s00165-014-0326-727:3(573-609)Online publication date: 9-Jan-2015
https://doi.org/10.1007/s00165-014-0326-7
Drăgoi CGupta AHenzinger T(2013)Automatic Linearizability Proofs of Concurrent Objects with Cooperating UpdatesComputer Aided Verification10.1007/978-3-642-39799-8_11(174-190)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39799-8_11
Garg PMadhusudan PParlato G(2013)Quantified Data Automata on Skinny Trees: An Abstract Domain for ListsStatic Analysis10.1007/978-3-642-38856-9_11(172-193)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38856-9_11
Drăgoi CEnea CSighireanu M(2013)Local Shape Analysis for Overlaid Data StructuresStatic Analysis10.1007/978-3-642-38856-9_10(150-171)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38856-9_10
Bouajjani ADrăgoi CEnea CSighireanu M(2012)Accurate invariant checking for programs manipulating lists and arrays with infinite dataProceedings of the 10th international conference on Automated Technology for Verification and Analysis10.1007/978-3-642-33386-6_14(167-182)Online publication date: 3-Oct-2012
https://dl.acm.org/doi/10.1007/978-3-642-33386-6_14
Giet JRidoux FRival X(2023)A Product of Shape and Sequence AbstractionsStatic Analysis10.1007/978-3-031-44245-2_15(310-342)Online publication date: 24-Oct-2023
https://doi.org/10.1007/978-3-031-44245-2_15
Illous HLemerre MRival X(2021)A relational shape abstract domainFormal Methods in System Design10.1007/s10703-021-00366-4Online publication date: 24-Apr-2021
https://doi.org/10.1007/s10703-021-00366-4
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents