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

research-article

Open access

Demanded abstract interpretation

Authors:

Bor-Yuh Evan Chang,

Manu SridharanAuthors Info & Claims

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 282 - 295

https://doi.org/10.1145/3453483.3454044

Published: 18 June 2021 Publication History

Abstract

We consider the problem of making expressive static analyzers interactive. Formal static analysis is seeing increasingly widespread adoption as a tool for verification and bug-finding, but even with powerful cloud infrastructure it can take minutes or hours to get batch analysis results after a code change. While existing techniques offer some demand-driven or incremental aspects for certain classes of analysis, the fundamental challenge we tackle is doing both for arbitrary abstract interpreters. Our technique, demanded abstract interpretation, lifts program syntax and analysis state to a dynamically evolving graph structure, in which program edits, client-issued queries, and evaluation of abstract semantics are all treated uniformly. The key difficulty addressed by our approach is the application of general incremental computation techniques to the complex, cyclic dependency structure induced by abstract interpretation of loops with widening operators. We prove that desirable abstract interpretation meta-properties, including soundness and termination, are preserved in our approach, and that demanded analysis results are equal to those computed by a batch abstract interpretation. Experimental results suggest promise for a prototype demanded abstract interpretation framework: by combining incremental and demand-driven techniques, our framework consistently delivers analysis results at interactive speeds, answering 95% of queries within 1.2 seconds.

References

[1]

Martín Abadi, Butler W. Lampson, and Jean-Jacques Lévy. 1996. Analysis and Caching of Dependencies. In International Conference on Functional Programming (ICFP). https://doi.org/10.1145/232627.232638

Digital Library

[2]

Umut A. Acar, Amal Ahmed, and Matthias Blume. 2008. Imperative self-adjusting computation. In Principles of Programming Languages (POPL). https://doi.org/10.1145/1328438.1328476

Digital Library

[3]

Umut A. Acar, Guy E. Blelloch, and Robert Harper. 2002. Adaptive functional programming. In Principles of Programming Languages (POPL). https://doi.org/10.1145/1186634

[4]

Alfred V. Aho, Monica S. Lam, Ravi Sethi, and Jeffrey D. Ullman. 2006. Compilers: Principles, Techniques, and Tools (2nd Edition).

Digital Library

[5]

Steven Arzt and Eric Bodden. 2014. Reviser: efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In International Conference on Software Engineering (ICSE). https://doi.org/10.1145/2568225.2568243

Digital Library

[6]

Wayne A. Babich and Mehdi Jazayeri. 1978. The Method of Attributes for Data Flow Analysis: Part II. Demand analysis. Acta Informatica, https://doi.org/10.1007/BF00264320

Digital Library

[7]

Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. 2005. Smallfoot: Modular Automatic Assertion Checking with Separation Logic. In Formal Methods for Components and Objects (FMCO). https://doi.org/10.1007/11804192_6

Digital Library

[8]

François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and Their Applications. https://doi.org/10.1007/BFb0039704

[9]

Cristiano Calcagno and Dino Distefano. 2011. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods (NFM). https://doi.org/10.1007/978-3-642-20398-5_33

[10]

Bor-Yuh Evan Chang, Xavier Rival, and George C. Necula. 2007. Shape Analysis with Structural Invariant Checkers. In Static Analysis (SAS). https://doi.org/10.1007/978-3-540-74061-2_24

[11]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Principles of Programming Languages (POPL). https://doi.org/10.1145/512950.512973

Digital Library

[12]

Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2005. The ASTREÉ Analyzer. In European Symposium on Programming (ESOP). https://doi.org/10.1007/978-3-540-31987-0_3

Digital Library

[13]

Alan J. Demers, Thomas W. Reps, and Tim Teitelbaum. 1981. Incremental Evaluation for Attribute Grammars with Application to Syntax-Directed Editors. In Principles of Programming Languages (POPL). https://doi.org/10.1145/567532.567544

Digital Library

[14]

Dino Distefano, Manuel Fähndrich, Francesco Logozzo, and Peter W. O’Hearn. 2019. Scaling static analyses at Facebook. Commun. ACM, https://doi.org/10.1145/3338112

Digital Library

[15]

Dino Distefano, Peter W. O’Hearn, and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). https://doi.org/10.1007/11691372_19

Digital Library

[16]

Lisa Nguyen Quang Do, Karim Ali, Benjamin Livshits, Eric Bodden, Justin Smith, and Emerson R. Murphy-Hill. 2017. Just-in-time Static Analysis. In Software Testing and Analysis (ISSTA). https://doi.org/10.1145/3092703.3092705

Digital Library

[17]

Evelyn Duesterwald, Rajiv Gupta, and Mary Lou Soffa. 1995. Demand-Driven Computation of Interprocedural Data Flow. In Principles of Programming Languages (POPL). https://doi.org/10.1145/199448.199461

Digital Library

[18]

Manuel Fähndrich and Francesco Logozzo. 2010. Static Contract Checking with Abstract Interpretation. In Formal Verification of Object-Oriented Software (FoVeOOS). https://doi.org/10.1007/978-3-642-18070-5_2

[19]

Rodney Farrow. 1986. Automatic generation of fixed-point-finding evaluators for circular, but well-defined, attribute grammars. In Compiler Construction (CC). https://doi.org/10.1145/12276.13320

Digital Library

[20]

John Field and Tim Teitelbaum. 1990. Incremental Reduction in the lambda Calculus. In LISP and Functional Programming. https://doi.org/10.1145/91556.91679

Digital Library

[21]

Matthew A. Hammer, Jana Dunfield, Kyle Headley, Nicholas Labich, Jeffrey S. Foster, Michael W. Hicks, and David Van Horn. 2015. Incremental computation with names. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). https://doi.org/10.1145/2814270.2814305

Digital Library

[22]

Matthew A. Hammer, Yit Phang Khoo, Michael Hicks, and Jeffrey S. Foster. 2014. Adapton: composable, demand-driven incremental computation. In Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/2594291.2594324

Digital Library

[23]

Nevin Heintze and Olivier Tardieu. 2001. Demand-Driven Pointer Analysis. In Programming Language Design and Implementation (PLDI). https://doi.org/10.1145/378795.378802

Digital Library

[24]

Susan Horwitz, Thomas W. Reps, and Shmuel Sagiv. 1995. Demand Interprocedural Dataflow Analysis. In Foundations of Software Engineering (FSE). https://doi.org/10.1145/222124.222146

Digital Library

[25]

Bertrand Jeannet and Antoine Miné. 2009. Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer-Aided Verification (CAV). https://doi.org/10.1007/978-3-642-02658-4_52

Digital Library

[26]

K. Rustan M. Leino and Valentin Wüstholz. 2015. Fine-Grained Caching of Verification Results. In Computer-Aided Verification (CAV). https://doi.org/10.1007/978-3-319-21690-4_22

[27]

Stephen Magill, Aleksandar Nanevski, Edmund Clarke, and Peter Lee. 2006. Inferring invariants in separation logic for imperative list-processing programs. In Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE).

[28]

Eva Magnusson and Görel Hedin. 2007. Circular reference attributed grammars - their evaluation and applications. Sci. Comput. Program., https://doi.org/10.1016/j.scico.2005.06.005

Digital Library

[29]

Antoine Miné. 2006. The octagon abstract domain. High. Order Symb. Comput., https://doi.org/10.1007/s10990-006-8609-1

Digital Library

[30]

William Pugh and Tim Teitelbaum. 1989. Incremental Computation via Function Caching. In Principles of Programming Languages (POPL). https://doi.org/10.1145/75277.75305

Digital Library

[31]

Thomas Reps. 1998. Program analysis via graph reachability. Information and Software Technology, https://doi.org/10.1016/S0950-5849(98)00093-7

[32]

Thomas W. Reps. 1982. Optimal-Time Incremental Semantic Analysis for Syntax-Directed Editors. In Principles of Programming Languages (POPL). https://doi.org/10.1145/582153.582172

Digital Library

[33]

Thomas W. Reps. 1994. Solving Demand Versions of Interprocedural Analysis Problems. In Compiler Construction (CC). https://doi.org/10.1007/3-540-57877-3_26

[34]

John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In Logic in Computer Science (LICS). https://doi.org/10.1109/LICS.2002.1029817

[35]

Barbara G. Ryder. 1983. Incremental Data Flow Analysis. In Principles of Programming Languages (POPL). https://doi.org/10.1145/567067.567084

Digital Library

[36]

Caitlin Sadowski, Edward Aftandilian, Alex Eagle, Liam Miller-Cushon, and Ciera Jaspan. 2018. Lessons from building static analysis tools at Google. Commun. ACM, https://doi.org/10.1145/3188720

Digital Library

[37]

Shmuel Sagiv, Thomas W. Reps, and Susan Horwitz. 1996. Precise Interprocedural Dataflow Analysis with Applications to Constant Propagation. Theor. Comput. Sci., https://doi.org/10.1016/0304-3975(96)00072-2

Digital Library

[38]

Mauricio Santos. 2016. Buckets-JS: A JavaScript Data Structure Library. https://github.com/mauriciosantos/Buckets-JS

[39]

Micha Sharir and Amir Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications.

[40]

Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Principles of Programming Languages (POPL). https://doi.org/10.1145/3093333.3009885

Digital Library

[41]

Emma Söderberg and Görel Hedin. 2012. Incremental Evaluation of Reference Attribute Grammars using Dynamic Dependency Tracking.

[42]

Johannes Späth, Lisa Nguyen Quang Do, Karim Ali, and Eric Bodden. 2016. Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java. In Object-Oriented Programming (ECOOP). https://doi.org/10.4230/DARTS.2.1.12

[43]

Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. 2005. Demand-Driven Points-To Analysis for Java. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). https://doi.org/10.1145/1094811.1094817

Digital Library

[44]

Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021. DAI: Demanded Abstract Interpretation. https://github.com/cuplv/dai

[45]

Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021. Demanded Abstract Interpretation (artifact). https://doi.org/10.5281/zenodo.4663292

Digital Library

[46]

Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. 2021. Demanded Abstract Interpretation (Extended Version). https://doi.org/10.1145/3453483.3454044

[47]

Tamás Szabó, Gábor Bergmann, Sebastian Erdweg, and Markus Voelter. 2018. Incrementalizing lattice-based program analyses in Datalog. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA). https://doi.org/10.1145/3276509

Digital Library

[48]

Tamás Szabó, Sebastian Erdweg, and Markus Voelter. 2016. IncA: a DSL for the definition of incremental program analyses. In Automated Software Engineering (ASE). https://doi.org/10.1145/2970276.2970298

Digital Library

[49]

F. Kenneth Zadeck. 1984. Incremental data flow analysis in a structured program editor. In Compiler Construction (CC). https://doi.org/10.1145/502874.502888

Digital Library

Cited By

Quiring BVan Horn D(2024)Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow AnalysisProceedings of the ACM on Programming Languages10.1145/36746508:ICFP(728-755)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674650
Beyer DKettl MLemberger T(2024)Decomposing Software Verification using Distributed Summary SynthesisProceedings of the ACM on Software Engineering10.1145/36607661:FSE(1307-1329)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660766
Stein BChang BSridharan M(2024)Interactive Abstract Interpretation with Demanded SummarizationACM Transactions on Programming Languages and Systems10.1145/364844146:1(1-40)Online publication date: 29-Mar-2024
https://dl.acm.org/doi/10.1145/3648441
Show More Cited By

Index Terms

Demanded abstract interpretation
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Formal software verification
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Control-flow analysis of function calls and returns by abstract interpretation

Abstract interpretation techniques are used to derive a control-flow analysis for a simple higher-order functional language. The analysis approximates the interprocedural control-flow of both function calls and returns in the presence of first-class ...
Deriving escape analysis by abstract interpretation

Escape analysis of object-oriented languages approximates the set of objects which do not escape from a given context. If we take a method as context, the non-escaping objects can be allocated on its activation stack; if we take a thread, Java ...
A²I: abstract² interpretation

The fundamental idea of Abstract² Interpretation (A²I), also called meta-abstract interpretation, is to apply abstract interpretation to abstract interpretation-based static program analyses. A²I is generally meant to use abstract interpretation to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2021: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2021

1341 pages

ISBN:9781450383912

DOI:10.1145/3453483

General Chair:
Stephen N. Freund
Williams College, USA
,
Program Chair:
Eran Yahav
Technion, Israel

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 June 2021

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

PLDI '21

Sponsor:

SIGPLAN

PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 20 - 25, 2021

Virtual, Canada

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
1,012
Total Downloads

Downloads (Last 12 months)261
Downloads (Last 6 weeks)28

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Quiring BVan Horn D(2024)Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow AnalysisProceedings of the ACM on Programming Languages10.1145/36746508:ICFP(728-755)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674650
Beyer DKettl MLemberger T(2024)Decomposing Software Verification using Distributed Summary SynthesisProceedings of the ACM on Software Engineering10.1145/36607661:FSE(1307-1329)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660766
Stein BChang BSridharan M(2024)Interactive Abstract Interpretation with Demanded SummarizationACM Transactions on Programming Languages and Systems10.1145/364844146:1(1-40)Online publication date: 29-Mar-2024
https://dl.acm.org/doi/10.1145/3648441
Chimdyalwar B(2024)Fast and Precise Interval Analysis on Industry code2024 IEEE 35th International Symposium on Software Reliability Engineering Workshops (ISSREW)10.1109/ISSREW63542.2024.00049(67-72)Online publication date: 28-Oct-2024
https://doi.org/10.1109/ISSREW63542.2024.00049
Tang X(2024)Improved Incremental Verification for Neural NetworksTheoretical Aspects of Software Engineering10.1007/978-3-031-64626-3_23(392-409)Online publication date: 14-Jul-2024
https://doi.org/10.1007/978-3-031-64626-3_23
Ugare SBanerjee DMisailovic SSingh G(2023)Incremental Verification of Neural NetworksProceedings of the ACM on Programming Languages10.1145/35912997:PLDI(1920-1945)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591299
Düsing JHermann BBissyandé TKlein JBird CSarro F(2023)Persisting and Reusing Results of Static Program Analyses on a Large ScaleProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00080(888-900)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00080
Urban C(2023)Static Analysis for Data ScientistsChallenges of Software Verification10.1007/978-981-19-9601-6_5(77-91)Online publication date: 22-Jul-2023
https://doi.org/10.1007/978-981-19-9601-6_5

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Media

Figures

Other

Tables

View Table of Contents