Abstract
This paper introduces ESBMC v7.3, the latest Efficient SMT-Based Context-Bounded Model Checker version, which now incorporates a new Clang-based C++ front-end. While the previous CPROVER-based front-end served well for handling C++03 programs, it encountered challenges keeping up with the evolving C++ language. As new language and library features were added in each C++ version, the limitations of the old front-end became apparent, leading to difficult-to-maintain code. Consequently, modern C++ programs were challenging to verify. To overcome this obstacle, we redeveloped the front-end, opting for a more robust approach using Clang. The new front-end efficiently traverses the Abstract Syntax Tree (AST) in-memory using Clang APIs and transforms each AST node into ESBMC’s Intermediate Representation. Through extensive experimentation, our results demonstrate that ESBMC v7.3 with the new front-end significantly reduces parse and conversion errors, enabling successful verification of a wide range of C++ programs, thereby outperforming previous ESBMC versions.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Deitel, P.J., Deitel, H.M.: C++ How to Program: Introducing the New C++14 Standard. Prentice Hall (2016)
Cordeiro, L.C., de Lima Filho, E.B., de Bessa, I.V.: Survey on automated symbolic verification and its application for synthesising cyber-physical systems. IET Cyper-Phys. Syst. Theory Appl. 5(1), 1–24 (2020). https://doi.org/10.1049/iet-cps.2018.5006
Miller, M.: Trends and challenges in the vulnerability mitigation landscape. USENIX Association (2019)
Fan, J., Li, Y., Wang, S., Nguyen, T.N.: A C/C++ code vulnerability dataset with code changes and CVE summaries. In: Proceedings of the 17th International Conference on Mining Software Repositories, pp. 508–512 (2020)
Common Vulnerabilities and Exposures database. https://cve.mitre.org/
Common Weakness Enumeration. https://cwe.mitre.org/about/index.html
Quadri, S., Farooq, S.U.: Software testing-goals, principles and limitations. Int. J. Comput. Appl. 6(9), 1 (2010)
Ammann, P., Offutt, J.: Introduction to Software Testing. Cambridge University Press, Cambridge (2016)
Monteiro, F.R., Garcia, M., Cordeiro, L.C., de Lima Filho, E.B.: Bounded model checking of C++ programs based on the Qt cross-platform framework. Softw. Test. Verification Reliab. 27(3), e1632 (2017). https://doi.org/10.1002/stvr.1632
Chong, N., et al.: Code-level model checking in the software development workflow. In: 2020 IEEE/ACM 42nd International Conference on Software Engineering: Software Engineering in Practice (ICSE-SEIP), pp. 11–20. IEEE (2020)
Monteiro, F.R., Gadelha, M.R., Cordeiro, L.C.: Model checking C++ programs. Softw. Test. Verification Reliab. 32(1), e1793 (2022)
Ramalho, M., Freitas, M., Sousa, F., Marques, H., Cordeiro, L., Fischer, B.: SMT-based bounded model checking of C++ programs. In: 2013 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems (ECBS), pp. 147–156. IEEE (2013)
LLVM clang. https://clang.llvm.org/
Lopes, B.C., Auler, R.: Getting Started with LLVM Core Libraries. Packt Publishing Ltd. (2014)
Pandey, M., Sarda, S.: LLVM Cookbook. Packt Publishing Ltd. (2015)
Pereira, P.A., et al.: SMT-based context-bounded model checking for CUDA programs. Concurr. Comput. Pract. Exp. 29(22), e3934 (2017). https://doi.org/10.1002/cpe.3934
Dos Reis, G., García, J.D., Logozzo, F., Fähndrich, M., Lahiri, S.: Simple contracts for C++(R1) (2015)
Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24730-2_15
ESBMC L312–L359. https://github.com/esbmc/esbmc/blob/master/src/cpp/cpp_typecheck_compound_type.cpp
C++03 standard. https://www.iso.org/standard/38110.html
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957–974 (2011)
Cordeiro, L.C., Fischer, B.: Verifying multi-threaded software using SMT-based context-bounded model checking. In: Taylor, R.N., Gall, H.C., Medvidovic, N. (eds.) Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, Waikiki, Honolulu, HI, USA, 21–28 May 2011, pp. 331–340. ACM (2011). https://doi.org/10.1145/1985793.1985839
Prata, S.: C++ Primer Plus. Pearson Education India (2012)
Stroustrup, B.: The C++ Programming Language, 4th edn (2013)
Siek, J., Taha, W.: A semantic analysis of C++ templates. In: Thomas, D. (ed.) ECOOP 2006. LNCS, vol. 4067, pp. 304–327. Springer, Heidelberg (2006). https://doi.org/10.1007/11785477_19
GCC test suite. https://gcc.gnu.org/git/?p=gcc.git;a=blob_plain;f=gcc/testsuite/g%2B%2B.dg/template/friend18.C;hb=649fc72d2
GCC bugzilla bug 10158. https://gcc.gnu.org/bugzilla/show_bug.cgi?id=10158
CBMC 5.88.1. https://github.com/diffblue/cbmc/releases/tag/cbmc-5.88.1
cppcheck. https://cppcheck.sourceforge.io/
Deitel, P.: C++ How To Program, 6th edn. Prentice Hall Press (2007)
CBMC regression test suite. https://github.com/diffblue/cbmc/tree/develop/regression/cbmc-cpp
Python unittest. https://docs.python.org/3/library/unittest.html
ESBMC v7.3 evaluation archive on Zenodo. https://zenodo.org/record/8233714
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Niemetz, A., Preiner, M.: Bitwuzla. In: Enea, C., Lal, A. (eds.) CAV 2023, Part II. LNCS, vol. 13965, pp. 3–17. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-37703-7_1
Brummayer, R., Biere, A.: Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-00768-2_16
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_28
Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49
ESBMC CPP support feature coverage and backlog. https://github.com/esbmc/esbmc/wiki/ESBMC-Cpp-Support
Github: ESBMC issue 940: Umbrella issue for the order of ctors/dtors. https://github.com/esbmc/esbmc/issues/940
Song, K., Gadelha, M.R., Brauße, F., Menezes, R.S., Cordeiro, L.C.: ESBMC v7.3: model checking C++ programs using clang AST. arXiv preprint arXiv:2308.05649 (2023)
Sousa, F.R.M., Cordeiro, L.C., de Lima Filho, E.B.: Bounded model checking of C++ programs based on the Qt framework. In: IEEE 4th Global Conference on Consumer Electronics, GCCE 2015, Osaka, Japan, 27–30 October 2015, pp. 179–180. IEEE (2015). https://doi.org/10.1109/GCCE.2015.7398699
UKRI: Sotereia project. https://soteriaresearch.org/
Beyer, D.: Competition on software verification and witness validation: SV-COMP 2023. In: Sankaranarayanan, S., Sharygina, N. (eds.) TACAS 2023. LNCS, vol. 13994, pp. 495–522. Springer, Cham (2023). https://doi.org/10.1007/978-3-031-30820-8_29
Acknowledgements
The ESBMC development is currently funded by ARM, Intel, EPSRC grants EP/T026995/1, EP/V000497/1, EU H2020 ELEGANT 957286, and Soteria project awarded by the UK Research and Innovation for the Digital Security by Design (DSbD) Programme.
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Song, K., Gadelha, M.R., Brauße, F., Menezes, R.S., Cordeiro, L.C. (2024). ESBMC v7.3: Model Checking C++ Programs Using Clang AST. In: Barbosa, H., Zohar, Y. (eds) Formal Methods: Foundations and Applications. SBMF 2023. Lecture Notes in Computer Science, vol 14414. Springer, Cham. https://doi.org/10.1007/978-3-031-49342-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-031-49342-3_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-49341-6
Online ISBN: 978-3-031-49342-3
eBook Packages: Computer ScienceComputer Science (R0)