Document Open Access Logo

Cooking String-Integer Conversions with Noodles

Authors Vojtěch Havlena , Lukáš Holík , Ondřej Lengál , Juraj Síč

PDF
Thumbnail PDF

File

LIPIcs.SAT.2024.14.pdf
  • Filesize: 7.23 MB
  • 19 pages

Document Identifiers

Author Details

Vojtěch Havlena
  • Brno University of Technology, Czech Republic
Lukáš Holík
  • Brno University of Technology, Czech Republic
Ondřej Lengál
  • Brno University of Technology, Czech Republic
Juraj Síč
  • Brno University of Technology, Czech Republic

Funding

This work was supported by the Czech Ministry of Education, Youth and Sports ERC.CZ project LL1908, the Czech Science Foundation project 23-07565S, and the FIT BUT internal project FIT-S-23-8151.

Cite AsGet BibTex

Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Cooking String-Integer Conversions with Noodles. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 14:1-14:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.SAT.2024.14

Abstract

We propose a method for efficient handling string constraints with string-integer conversions. It extends the recently introduced stabilization-based procedure for solving string (dis)equations with regular and length constraints. Our approach is to translate the conversions into a linear integer arithmetic formula, together with regular constraints and word equations. We have integrated it into the string solver Z3-Noodler, and our experiments show that it is competitive and on some established benchmarks even several orders of magnitude faster than the state of the art.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • string solving
  • string conversions
  • SMT solving

Metrics

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

Supplementary Materials

References

  1. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Julian Dolby, Petr Janku, Hsin-Hung Lin, Lukás Holík, and Wei-Cheng Wu. Efficient handling of string-number conversion. In Alastair F. Donaldson and Emina Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 943-957. ACM, 2020. URL: https://doi.org/10.1145/3385412.3386034.
  2. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. Flatten and conquer: a framework for efficient analysis of string constraints. In Albert Cohen and Martin T. Vechev, editors, Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, Barcelona, Spain, June 18-23, 2017, pages 602-617. ACM, 2017. URL: https://doi.org/10.1145/3062341.3062384.
  3. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukás Holík, Ahmed Rezine, and Philipp Rümmer. Trau: SMT solver for string constraints. In Nikolaj S. Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1-5. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8602997.
  4. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In Armin Biere and Roderick Bloem, editors, Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, pages 150-166. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08867-9_10.
  5. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. Norn: An SMT solver for string constraints. In CAV'15, volume 9206 of LNCS, pages 462-469. Springer, 2015. Google Scholar
  6. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bui Phi Diep, Lukás Holík, and Petr Janků. Chain-free string constraints. In Yu-Fang Chen, Chih-Hong Cheng, and Javier Esparza, editors, Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, volume 11781 of Lecture Notes in Computer Science, pages 277-293. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-31784-3_16.
  7. Leonardo Alt, Martin Blicha, Antti E. J. Hyvärinen, and Natasha Sharygina. SolCMC: Solidity compiler’s model checker. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings, Part I, volume 13371 of Lecture Notes in Computer Science, pages 325-338. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-13185-1_16.
  8. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength smt solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 415-442, Cham, 2022. Springer International Publishing. Google Scholar
  9. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.
  10. Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB): Strings. https://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml, 2023.
  11. Murphy Berzish. Z3str4: A Solver for Theories over Strings. PhD thesis, University of Waterloo, Ontario, Canada, 2021. URL: https://hdl.handle.net/10012/17102.
  12. Murphy Berzish, Joel D. Day, Vijay Ganesh, Mitja Kulczynski, Florin Manea, Federico Mora, and Dirk Nowotka. String theories involving regular membership predicates: From practice to theory and back. In Thierry Lecroq and Svetlana Puzynina, editors, Combinatorics on Words, pages 50-64, Cham, 2021. Springer International Publishing. Google Scholar
  13. Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, and Vijay Ganesh. An SMT solver for regular expressions and linear arithmetic over string length. In Alexandra Silva and K. Rustan M. Leino, editors, Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event, July 20-23, 2021, Proceedings, Part II, volume 12760 of Lecture Notes in Computer Science, pages 289-312. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-81688-9_14.
  14. František Blahoudek, Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Word equations in synergy with regular constraints. In Marsha Chechik, Joost-Pieter Katoen, and Martin Leucker, editors, Formal Methods, pages 403-423, Cham, 2023. Springer International Publishing. Google Scholar
  15. Véronique Bruyàre, Georges Hansel, Christian Michaux, and Roger Villemaire. Logic and p-recognizable sets of integers. Bulletin of the Belgian Mathematical Society - Simon Stevin, 1(2):191-238, 1994. URL: https://doi.org/10.36045/bbms/1103408547.
  16. Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. Decision procedures for path feasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang., 3(POPL):49:1-49:30, 2019. URL: https://doi.org/10.1145/3290362.
  17. Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Z3-Noodler: An automata-based string solver. In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 24-33, Cham, 2024. Springer Nature Switzerland. Google Scholar
  18. Yu-Fang Chen, David Chocholatý, Vojtěch Havlena, Lukáš Holík, Ondřej Lengál, and Juraj Síč. Solving string constraints with lengths by stabilization. Proc. ACM Program. Lang., 7(OOPSLA2), October 2023. URL: https://doi.org/10.1145/3622872.
  19. Yu-Fang Chen, Vojtech Havlena, Ondrej Lengál, and Andrea Turrini. A symbolic algorithm for the case-split rule in string constraint solving. In Bruno C. d. S. Oliveira, editor, Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, volume 12470 of Lecture Notes in Computer Science, pages 343-363. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64437-6_18.
  20. Yu-Fang Chen, Vojtěch Havlena, Ondřej Lengál, and Andrea Turrini. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, 201:111673, 2023. URL: https://doi.org/10.1016/j.jss.2023.111673.
  21. Joel D. Day, Thorsten Ehlers, Mitja Kulczynski, Florin Manea, Dirk Nowotka, and Danny Bøgsted Poulsen. On solving word equations using SAT. In Emmanuel Filiot, Raphaël M. Jungers, and Igor Potapov, editors, Reachability Problems - 13th International Conference, RP 2019, Brussels, Belgium, September 11-13, 2019, Proceedings, volume 11674 of Lecture Notes in Computer Science, pages 93-106. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30806-3_8.
  22. Leonardo Mendonça de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS'08, volume 4963 of LNCS, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  23. Vijay Ganesh and Murphy Berzish. Undecidability of a theory of strings, linear arithmetic over length, and string-number conversion, 2016. URL: https://arxiv.org/abs/1605.09442.
  24. Quang Loc Le and Mengda He. A decision procedure for string logic with quadratic equations, regular expressions and length constraints. In Sukyoung Ryu, editor, Programming Languages and Systems, pages 350-372, Cham, 2018. Springer International Publishing. Google Scholar
  25. Liana Hadarean. String solving at Amazon. https://mosca19.github.io/program/index.html, 2019. Presented at MOSCA'19.
  26. G. S. Makanin. The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik, 32(2):147-236, 1977. (in Russian). Google Scholar
  27. Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, and Vijay Ganesh. Z3str4: A multi-armed string solver. In Marieke Huisman, Corina S. Pasareanu, and Naijun Zhan, editors, Formal Methods - 24th International Symposium, FM 2021, Virtual Event, November 20-26, 2021, Proceedings, volume 13047 of Lecture Notes in Computer Science, pages 389-406. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-90870-6_21.
  28. OWASP. Top 10. https://owasp.org/www-project-top-ten/2017/, 2017.
  29. OWASP. Top 10. https://owasp.org/Top10/, 2021.
  30. Andrew Reynolds, Andres Nötzli, Clark Barrett, and Cesare Tinelli. A decision procedure for string to code point conversion. In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 218-237, Cham, 2020. Springer International Publishing. Google Scholar
  31. Andrew Reynolds, Andres Notzlit, Clark Barrett, and Cesare Tinelli. Reductions for strings and regular expressions revisited. In 2020 Formal Methods in Computer Aided Design (FMCAD), pages 225-235, 2020. URL: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6_30.
  32. Philipp Rümmer. A constraint sequent calculus for first-order logic with linear integer arithmetic. In Proceedings, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 5330 of LNCS, pages 274-289. Springer, 2008. Google Scholar
  33. Klaus U. Schulz. Makanin’s algorithm for word equations-two improvements and a generalization. In Klaus U. Schulz, editor, Word Equations and Related Topics, pages 85-150, Berlin, Heidelberg, 1992. Springer Berlin Heidelberg. Google Scholar
  34. Z3-Noodler. Automata-based string solver, 2024. URL: https://github.com/VeriFIT/z3-noodler.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact