Document Open Access Logo

Low-Level Bi-Abduction

Authors Lukáš Holík , Petr Peringer , Adam Rogalewicz , Veronika Šoková , Tomáš Vojnar , Florian Zuleger

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.19.pdf
  • Filesize: 1.19 MB
  • 30 pages

Document Identifiers

Author Details

Lukáš Holík
  • FIT, Brno University of Technology, Czech Republic
Petr Peringer
  • FIT, Brno University of Technology, Czech Republic
Adam Rogalewicz
  • FIT, Brno University of Technology, Czech Republic
Veronika Šoková
  • FIT, Brno University of Technology, Czech Republic
Tomáš Vojnar
  • FIT, Brno University of Technology, Czech Republic
Florian Zuleger
  • Faculty of Informatics, TU Wien, Austria

Funding

The Czech authors were supported by the project 20-07487S of the Czech Science Foundation, the FIT BUT internal project FIT-S-20-6427, and L. Holík by the ERC.CZ project LL1908.

Cite AsGet BibTex

Lukáš Holík, Petr Peringer, Adam Rogalewicz, Veronika Šoková, Tomáš Vojnar, and Florian Zuleger. Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 19:1-19:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.19

Abstract

The paper proposes a new static analysis designed to handle open programs, i.e., fragments of programs, with dynamic pointer-linked data structures - in particular, various kinds of lists - that employ advanced low-level pointer operations. The goal is to allow such programs be analysed without a need of writing analysis harnesses that would first initialise the structures being handled. The approach builds on a special flavour of separation logic and the approach of bi-abduction. The code of interest is analyzed along the call tree, starting from its leaves, with each function analysed just once without any call context, leading to a set of contracts summarizing the behaviour of the analysed functions. In order to handle the considered programs, methods of abduction existing in the literature are significantly modified and extended in the paper. The proposed approach has been implemented in a tool prototype and successfully evaluated on not large but complex programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Separation logic
  • Theory of computation → Logic and verification
  • Software and its engineering → Formal software verification
Keywords
  • programs with dynamic linked data structures
  • programs with pointers
  • low-level pointer operations
  • static analysis
  • shape analysis
  • separation logic
  • bi-abduction

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

Supplementary Materials

References

  1. Andrew W. Appel. Program Logics - for Certified Compilers. Cambridge University Press, 2014. Google Scholar
  2. J. Berdine, C. Calcagno, B. Cook, D. Distefano, P.W. O'Hearn, T. Wies, and H. Yang. Shape Analysis for Composite Data Structures. In Proc. of CAV'07, volume 4590 of LNCS. Springer, 2007. Google Scholar
  3. A. Bouajjani, C. Drăgoi, C. Enea, and M. Sighireanu. Accurate Invariant Checking for Programs Manipulating Lists and Arrays with Infinite Data. In Proc. of ATVA'12, volume 7561 of LNCS. Springer, 2012. Google Scholar
  4. C. Calcagno and D. Distefano. Infer: An Automatic Program Verifier for Memory Safety of C Programs. In Proc. of NFM'11, volume 6617 of LNCS. Springer, 2011. Google Scholar
  5. C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Beyond Reachability: Shape Abstraction in the Presence of Pointer Arithmetic. In Proc. of SAS'06, volume 4134 of LNCS. Springer, 2006. Google Scholar
  6. C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional Shape Analysis by Means of Bi-Abduction. In Proc. of POPL'09. ACM, 2009. Google Scholar
  7. C. Calcagno, D. Distefano, P. O'Hearn, and H. Yang. Compositional Shape Analysis by Means of Bi-Abduction. Journal of the ACM, 58(6), 2011. Google Scholar
  8. Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. In LICS, pages 366-378. IEEE Computer Society, 2007. Google Scholar
  9. B.-Y.E. Chang, X. Rival, and G.C. Necula. Shape Analysis with Structural Invariant Checkers. In Proc. of SAS'07, volume 4634 of LNCS. Springer, 2007. Google Scholar
  10. W.-N. Chin, C. David, H.H. Nguyen, and S. Qin. Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic. Science of Computer Programming, 77(9), 2012. Google Scholar
  11. C. Curry, Q. Loc Le, and S. Qin. Bi-Abductive Inference for Shape and Ordering Properties. In Proc. of ICECCS'19. IEEE, 2019. Google Scholar
  12. L.M. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In Proc. of TACAS'08, volume 4963 of LNCS. Springer, 2008. Google Scholar
  13. Stéphane Demri, Étienne Lozes, and Alessio Mansutti. The effects of adding reachability predicates in propositional separation logic. In FoSSaCS, volume 10803 of Lecture Notes in Computer Science, pages 476-493. Springer, 2018. Google Scholar
  14. C. Drăgoi, C. Enea, and M. Sighireanu. Local Shape Analysis for Overlaid Data Structures. In Proc. of SAS'13, volume 7935 of LNCS. Springer, 2013. Google Scholar
  15. K. Dudka, P. Peringer, and T. Vojnar. An Easy to Use Infrastructure for Building Static Analysis Tools. In Proc. of EUROCAST'11, volume 6927 of LNCS. Springer, 2011. Google Scholar
  16. K. Dudka, P. Peringer, and T. Vojnar. Byte-Precise Verification of Low-Level List Manipulation. In Proc. of SAS'13, volume 7935 of LNCS. Springer, 2013. Google Scholar
  17. M. Echenim, R. Iosif, and N. Peltier. Unifying Decidable Entailments in Separation Logic with Inductive Definitions. In Proc. of CADE'21, volume 12699 of LNCS. Springer, 2021. Google Scholar
  18. C. Enea, O. Lengál, M. Sighireanu, and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. In Proc. of APLAS'14, volume 8858 of LNCS. Springer, 2014. Google Scholar
  19. B. Fang and M. Sighireanu. Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators. In Proc. of LOPSTR'16, volume 10184 of LNCS. Springer, 2016. Google Scholar
  20. J. Heinen, T. Noll, and S. Rieger. Juggrnaut: Graph Grammar Abstraction for Unbounded Heap Structures. In Proc. of TSS'09, volume 266 of ENTCS. Elsevier, 2010. Google Scholar
  21. L. Holík, O. Lengál, J. Šimáček, A. Rogalewicz, and T. Vojnar. Fully Automated Shape Analysis Based on Forest Automata. In Proc. of CAV'13, volume 8044 of LNCS. Springer, 2013. Google Scholar
  22. L. Holík, P. Peringer, A. Rogalewicz, V. Šoková, T. Vojnar, and F. Zuleger. Low-Level Bi-Abduction, 2022. URL: http://arxiv.org/abs/2205.02590.
  23. R. Iosif, A. Rogalewicz, and T. Vojnar. Deciding Entailments in Inductive Separation Logic with Tree Automata. In Proc. of ATVA'14, volume 8837 of LNCS. Springer, 2014. Google Scholar
  24. S. Ishtiaq and P.W. O'Hearn. Separation and Information Hiding. In Proc. of POPL'01. ACM, 2001. Google Scholar
  25. J.L. Jensen, M.E. Jørgensen, M.I. Schwartzbach, and N. Klarlund. Automatic Verification of Pointer Programs Using Monadic Second-order Logic. In Proc. of PLDI'97. ACM, 1997. Google Scholar
  26. J. Katelaan and F. Zuleger. Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions. In Proc. of LPAR'11, volume 73 of EPiC Series in Computing. EasyChair, 2020. Google Scholar
  27. Q. Loc Le. Compositional Satisfiability Solving in Separation Logic. In Proc. of VMCAI'21, volume 12597 of LNCS. Springer, 2021. Google Scholar
  28. Q. Loc Le, C. Gherghina, S. Qin, and W.-N. Chin. Shape Analysis via Second-Order Bi-Abduction. In Proc. of CAV'14, volume 8559 of LNCS. Springer, 2014. Google Scholar
  29. P. Maksimovic, S.-É. Ayoun, J.F. Santos, and P. Gardner. Gillian, Part II: Real-World Verification for JavaScript and C. In Proc. of CAV'21, volume 12760 of LNCS. Springer, 2021. Google Scholar
  30. P. Maksimovic, J.F. Santos, S.-É. Ayoun, and P. Gardner. Gillian: A Multi-Language Platform for Unified Symbolic Analysis, 2021. URL: http://arxiv.org/abs/2105.14769.
  31. V. Malik, M. Hruška, P. Schrammel, and T. Vojnar. Template-Based Verification of Heap-Manipulating Programs. In Proc. of FMCAD'18. IEEE, 2018. Google Scholar
  32. Jens Pagel and Florian Zuleger. Strong-separation logic. In ESOP, volume 12648 of Lecture Notes in Computer Science, pages 664-692. Springer, 2021. Google Scholar
  33. J.C. Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In Proc. of LICS'02. IEEE, 2002. Google Scholar
  34. M. Sagiv, T. Reps, and R. Wilhelm. Parametric Shape Analysis via 3-Valued Logic. ACM Transactions on Programming Languages and Systems, 24(3), 2002. Google Scholar
  35. J.F. Santos, P. Maksimovic, S.-É. Ayoun, and P. Gardner. Gillian: Compositional Symbolic Execution for All, 2020. URL: http://arxiv.org/abs/2001.05059.
  36. J.F. Santos, P. Maksimovic, S.-É. Ayoun, and P. Gardner. Gillian, Part I: A Multi-Language Platform for Symbolic Execution. In Proc. of PLDI'20. ACM, 2020. Google Scholar
  37. T. Wies, V. Kuncak, K. Zee, A. Podelski, and M. Rinard. On Verifying Complex Properties using Symbolic Shape Analysis. In Proc. of HAV'07, 2007. Google Scholar
  38. H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P.W. O'Hearn. Scalable Shape Analysis for Systems Code. In Proc. of CAV'08, volume 5123 of LNCS. Springer, 2008. Google Scholar
  39. K. Zee, V. Kuncak, and M.C. Rinard. Full Functional Verification of Linked Data Structures. In Proc. of PLDI'08. ACM, 2008. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact