Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

Xianzhiyu Li, Kunjian Song, Mikhail R. Gadelha, Franz Brauße, Rafael S. Menezes, Konstantin Korovin, Lucas C. Cordeiro

TL;DR

This work advances ESBMC by integrating a Clang AST-based front-end to enhance verification of modern C++ programs. By upgrading memory management, adding robust support for rvalue references, templates, and exception handling, and updating STL-oriented operational models, ESBMC v7.6 broadens language feature coverage and verification accuracy. Experimental results show improved pass rates and competitive timing across benchmarks relative to v2.1 and v7.3, with Boolector emerging as the fastest SMT solver in this setup. While gains are substantial, remaining limitations in AST coverage and certain C++11 features motivate further development and broader STL integration, aiming toward scalable verification of real-world C++ software.

Abstract

This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as 1) exception handling, 2) extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and 3) new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard.

ESBMC v7.6: Enhanced Model Checking of C++ Programs with Clang AST

TL;DR

This work advances ESBMC by integrating a Clang AST-based front-end to enhance verification of modern C++ programs. By upgrading memory management, adding robust support for rvalue references, templates, and exception handling, and updating STL-oriented operational models, ESBMC v7.6 broadens language feature coverage and verification accuracy. Experimental results show improved pass rates and competitive timing across benchmarks relative to v2.1 and v7.3, with Boolector emerging as the fastest SMT solver in this setup. While gains are substantial, remaining limitations in AST coverage and certain C++11 features motivate further development and broader STL integration, aiming toward scalable verification of real-world C++ software.

Abstract

This paper presents Efficient SMT-Based Context-Bounded Model Checker (ESBMC) v7.6, an extended version based on previous work on ESBMC v7.3 by K. Song et al. The v7.3 introduced a new Clang-based C++ front-end to address the challenges posed by modern C++ programs. Although the new front-end has demonstrated significant potential in previous studies, it remains in the developmental stage and lacks several essential features. ESBMC v7.6 further enhanced this foundation by adding and extending features based on the Clang AST, such as 1) exception handling, 2) extended memory management and memory safety verification, including dangling pointers, duplicate deallocation, memory leaks and rvalue references and 3) new operational models for STL updating the outdated C++ operational models. Our extensive experiments demonstrate that ESBMC v7.6 can handle a significantly broader range of C++ features introduced in recent versions of the C++ standard.
Paper Structure (20 sections, 1 equation, 12 figures, 5 tables, 5 algorithms)

This paper contains 20 sections, 1 equation, 12 figures, 5 tables, 5 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. SMT-based BMC technique
  4. Old C++ front-end in v2.1
  5. Model Checking C++ Programs using Clang AST
  6. Polymorphism
  7. Templates
  8. C++ New and Delete
  9. Rvalue References
  10. Move Semantics
  11. Move Member Functions
  12. Exception Handling
  13. C++ Operational Model
  14. Experimental Evaluation
  15. Objectives and Setup
  16. ...and 5 more sections

Figures (12)

  • Figure 1: ESBMC architecture for C++ verification. The grey block represents the extended Clang-based C++ front-end developed in ESBMC v7.6.
  • Figure 2: Example of C++ classes with virtual functions.
  • Figure 3: Object models for Bird and Penguin classes
  • Figure 4: GOTO conversions of the overriding methods and dynamic dispatch.
  • Figure 5: ESBMC verified the Friend18 example from the GCC test suite. gcctestsuite
  • ...and 7 more figures