research-article

Speeding up Static Analysis with the Split Operator

Authors:

Vincenzo Arceri,

Greta Dolcetti,

Enea ZaffanellaAuthors Info & Claims

SOAP 2023: Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis

Pages 14 - 19

https://doi.org/10.1145/3589250.3596141

Published: 06 June 2023 Publication History

Abstract

In the context of static analysis based on Abstract Interpretation, we propose a new abstract operator modeling the split of control flow paths: the goal of the operator is to enable a more efficient analysis when using abstract domains that are computationally expensive, having no effect on precision. Focusing on the case of conditional branches guarded by numeric linear constraints, we provide a preliminary experimental evaluation showing that, by using the split operator, we can achieve significant efficiency improvements for a static analysis based on the domain of convex polyhedra. We also briefly discuss the applicability of this new operator to different, possibly non-numeric abstract domains.

References

[1]

Vincenzo Arceri, Isabella Mastroeni, and Sunyi Xu. 2020. Static Analysis for ECMAScript String Manipulation Programs. Appl. Sci., 10 (2020), 3525. https://doi.org/10.3390/app10103525

[2]

Roberto Bagnara, Katy Louise Dobson, Patricia M. Hill, Matthew Mundell, and Enea Zaffanella. 2006. Grids: A Domain for Analyzing the Distribution of Numerical Values. In Logic-Based Program Synthesis and Transformation, 16th International Symposium, LOPSTR 2006, Venice, Italy, July 12-14, 2006, Revised Selected Papers, Germán Puebla (Ed.) (Lecture Notes in Computer Science, Vol. 4407). Springer, 219–235. https://doi.org/10.1007/978-3-540-71410-1_16

[3]

Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. 2007. Widening operators for powerset domains. Int. J. Softw. Tools Technol. Transf., 9, 3-4 (2007), 413–414. https://doi.org/10.1007/s10009-007-0029-y

Digital Library

[4]

Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella. 2008. The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program., 72, 1-2 (2008), 3–21. https://doi.org/10.1016/j.scico.2007.08.001

Digital Library

[5]

Anna Becchi and Enea Zaffanella. 2018. A Direct Encoding for NNC Polyhedra. In Computer Aided Verification - 30th International Conference, CAV 2018, Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, Hana Chockler and Georg Weissenbacher (Eds.) (Lecture Notes in Computer Science, Vol. 10981). Springer, 230–248. https://doi.org/10.1007/978-3-319-96145-3_13

[6]

Anna Becchi and Enea Zaffanella. 2018. An Efficient Abstract Domain for Not Necessarily Closed Polyhedra. In Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, Andreas Podelski (Ed.) (Lecture Notes in Computer Science, Vol. 11002). Springer, 146–165. https://doi.org/10.1007/978-3-319-99725-4_11

[7]

Anna Becchi and Enea Zaffanella. 2019. Revisiting Polyhedral Analysis for Hybrid Systems. In Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, Bor-Yuh Evan Chang (Ed.) (Lecture Notes in Computer Science, Vol. 11822). Springer, 183–202. https://doi.org/10.1007/978-3-030-32304-2_10

Digital Library

[8]

Anna Becchi and Enea Zaffanella. 2020. PPLite: Zero-overhead encoding of NNC polyhedra. Inf. Comput., 275 (2020), 104620. https://doi.org/10.1016/j.ic.2020.104620

[9]

Guillaume Brat, Jorge A. Navas, Nija Shi, and Arnaud Venet. 2014. IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In Software Engineering and Formal Methods - 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings (Lecture Notes in Computer Science, Vol. 8702). Springer, 271–277. https://doi.org/10.1007/978-3-319-10431-7_20

[10]

Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977, Robert M. Graham, Michael A. Harrison, and Ravi Sethi (Eds.). ACM, 238–252. https://doi.org/10.1145/512950.512973

Digital Library

[11]

Patrick Cousot and Nicolas Halbwachs. 1978. Automatic Discovery of Linear Restraints Among Variables of a Program. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, January 1978, Alfred V. Aho, Stephen N. Zilles, and Thomas G. Szymanski (Eds.). ACM Press, 84–96. https://doi.org/10.1145/512760.512770

Digital Library

[12]

Pietro Ferrara, Luca Negrini, Vincenzo Arceri, and Agostino Cortesi. 2021. Static analysis for dummies: experiencing LiSA. In SOAP@PLDI 2021: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, Virtual Event, Canada, 22 June, 2021, Lisa Nguyen Quang Do and Caterina Urban (Eds.). ACM, 1–6. https://doi.org/10.1145/3460946.3464316

Digital Library

[13]

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, and Peter J. Stuckey. 2021. Disjunctive Interval Analysis. In Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science, Vol. 12913). Springer, 144–165. https://doi.org/10.1007/978-3-030-88806-0_7

Digital Library

[14]

Arie Gurfinkel and Sagar Chaki. 2010. Boxes: A Symbolic Abstract Domain of Boxes. In Static Analysis - 17th International Symposium, SAS 2010, Perpignan, France, September 14-16, 2010. Proceedings, Radhia Cousot and Matthieu Martel (Eds.) (Lecture Notes in Computer Science, Vol. 6337). Springer, 287–303. https://doi.org/10.1007/978-3-642-15769-1_18

[15]

Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I, Daniel Kroening and Corina S. Pasareanu (Eds.) (Lecture Notes in Computer Science, Vol. 9206). Springer, 343–361. https://doi.org/10.1007/978-3-319-21690-4_20

[16]

Arie Gurfinkel and Jorge A. Navas. 2021. Abstract Interpretation of LLVM with a Region-Based Memory Model. In Software Verification - 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18-19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18-19, 2021, Revised Selected Papers, Roderick Bloem, Rayna Dimitrova, Chuchu Fan, and Natasha Sharygina (Eds.) (Lecture Notes in Computer Science, Vol. 13124). Springer, 122–144. https://doi.org/10.1007/978-3-030-95561-8_8

Digital Library

[17]

Julien Henry, David Monniaux, and Matthieu Moy. 2012. PAGAI: A Path Sensitive Static Analyser. In Third Workshop on Tools for Automatic Program Analysis, TAPAS 2012, Deauville, France, September 14, 2012 (Electronic Notes in Theoretical Computer Science, Vol. 289). Elsevier, 15–25. https://doi.org/10.1016/j.entcs.2012.11.003

Digital Library

[18]

Bertrand Jeannet and Antoine Miné. 2009. Apron: A Library of Numerical Abstract Domains for Static Analysis. In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, Ahmed Bouajjani and Oded Maler (Eds.) (Lecture Notes in Computer Science, Vol. 5643). Springer, 661–667. https://doi.org/10.1007/978-3-642-02658-4_52

Digital Library

[19]

Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur. 2020. Memory-Efficient Fixpoint Computation. In Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings, David Pichardie and Mihaela Sighireanu (Eds.) (Lecture Notes in Computer Science, Vol. 12389). Springer, 35–64. https://doi.org/10.1007/978-3-030-65474-0_3

Digital Library

[20]

Raphaël Monat, Abdelraouf Ouadjaout, and Antoine Miné. 2021. A Multilanguage Static Analysis of Python Programs with Native C Extensions. In Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, Cezara Dragoi, Suvam Mukherjee, and Kedar S. Namjoshi (Eds.) (Lecture Notes in Computer Science, Vol. 12913). Springer, 323–345. https://doi.org/10.1007/978-3-030-88806-0_16

Digital Library

[21]

Luca Negrini, Vincenzo Arceri, Pietro Ferrara, and Agostino Cortesi. 2021. Twinning Automata and Regular Expressions for String Static Analysis. In Verification, Model Checking, and Abstract Interpretation - 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17-19, 2021, Proceedings, Fritz Henglein, Sharon Shoham, and Yakir Vizel (Eds.) (Lecture Notes in Computer Science, Vol. 12597). Springer, 267–290. https://doi.org/10.1007/978-3-030-67067-2_13

Digital Library

[22]

Gagandeep Singh, Markus Püschel, and Martin T. Vechev. 2017. Fast polyhedra abstract domain. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, Giuseppe Castagna and Andrew D. Gordon (Eds.). ACM, 46–59. https://doi.org/10.1145/3009837.3009885

Digital Library

Cited By

Arceri VDolcetti GZaffanella E(2024)Speeding up static analysis with the split operatorInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00761-2Online publication date: 27-Aug-2024
https://doi.org/10.1007/s10009-024-00761-2
Olivieri LSpoto F(2024)Software verification challenges in the blockchain ecosystemInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00758-x26:4(431-444)Online publication date: 12-Jul-2024
https://doi.org/10.1007/s10009-024-00758-x
Negrini LArceri VCortesi AFerrara P(2024) Tarsis : An effective automata‐based abstract domain for string analysis Journal of Software: Evolution and Process10.1002/smr.2647Online publication date: 14-Feb-2024
https://doi.org/10.1002/smr.2647

Index Terms

Speeding up Static Analysis with the Split Operator
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Automated static analysis
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Numerical static analysis with Soot
SOAP '13: Proceedings of the 2nd ACM SIGPLAN International Workshop on State Of the Art in Java Program analysis

Numerical static analysis computes an approximation of all the possible values that a numeric variable may assume, in any execution of the program. Many numerical static analyses have been proposed exploiting the theory of abstract interpretation, which ...
Stratified Static Analysis Based on Variable Dependencies

In static analysis by abstract interpretation, one often uses widening operators in order to enforce convergence within finite time to an inductive invariant. Certain widening operators, including the classical one over finite polyhedra, exhibit an ...
Pushdown control-flow analysis for free
POPL '16

Traditional 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SOAP 2023: Proceedings of the 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis

June 2023

70 pages

ISBN:9798400701702

DOI:10.1145/3589250

General Chairs:
Pietro Ferrara
Ca' Foscari University of Venice, Italy
,
Liana Hadarean
AWS, USA

Copyright © 2023 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 the author(s) 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].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 06 June 2023

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SOAP '23

Sponsor:

SIGPLAN

SOAP '23: 12th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis

June 17, 2023

FL, Orlando, USA

Acceptance Rates

Overall Acceptance Rate 11 of 11 submissions, 100%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
125
Total Downloads

Downloads (Last 12 months)69
Downloads (Last 6 weeks)2

Reflects downloads up to 04 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Arceri VDolcetti GZaffanella E(2024)Speeding up static analysis with the split operatorInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00761-2Online publication date: 27-Aug-2024
https://doi.org/10.1007/s10009-024-00761-2
Olivieri LSpoto F(2024)Software verification challenges in the blockchain ecosystemInternational Journal on Software Tools for Technology Transfer10.1007/s10009-024-00758-x26:4(431-444)Online publication date: 12-Jul-2024
https://doi.org/10.1007/s10009-024-00758-x
Negrini LArceri VCortesi AFerrara P(2024) Tarsis : An effective automata‐based abstract domain for string analysis Journal of Software: Evolution and Process10.1002/smr.2647Online publication date: 14-Feb-2024
https://doi.org/10.1002/smr.2647
Arceri VDolcetti GZaffanella E(2023)Unconstrained Variable Oracles for Faster Numeric Static AnalysesStatic Analysis10.1007/978-3-031-44245-2_5(65-83)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1007/978-3-031-44245-2_5

View Options

Get Access

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 Table of Contents