CPP Support

Supported features:

ESBMC v7 supports the following C++ features:

• Class

• C++ New and Delete: Dangling pointer, Double delete and Mismatched operators

• constructors and destructors

• lvalue reference

• rvalue reference

• Move semantics: Move constructor, Move assignment operator.

• C++ OM fixed: string_view, algorithm, vector, Typeinfo, iterator, string, queue, numeric, set

• Standard lib: <type_traits>

• Improved references and Temporary object

• New Clang node

  • DefaultInit Expr
  • sizeof Expr
  • C++ 11 nullptr_t Expr
  • C++ 17 variable template declarations

• template

  • Umbrella issue: https://github.com/esbmc/esbmc/issues/989 (original estimate 2-3 weeks, logged 2.5 weeks)

• inheritance and polymorphism:

  • single-level polymorhism
  • multi-level polymorhism
  • pure virtual method
  • virtual inheritance (the diamond problem)
  • correct order of ctors/dtors:
    • tracked by the umbrella issue issue 940, affected features are listed below:
      • Virtual destructor
      • Base initialization for the most-derivied class
      • Order of destruction in case of object composition (part-whole relationship)

• (TODO) Exception handling:

  • try-catch, throw

Features WIP:

• Fixing our OMs for STL libraries
  • See guidelines: https://github.com/esbmc/esbmc/wiki/Guidelines-for-Fixing-Operational-Models-(OM)-in-ESBMC
  • OM workload estimate and tracking: https://github.com/esbmc/esbmc/wiki/OM-Workload-Estimate-and-Tracking

Backlog:

Issues are listed from high to low priority in each subsection:

• Feature issues:

  • [] [Order of ctor/dtor - umbrella issue] https://github.com/esbmc/esbmc/issues/940
  • [dangling pointer] https://github.com/esbmc/esbmc/issues/894
  • [zero initialization] https://github.com/esbmc/esbmc/issues/1103
  • [Corner cases]:
    • [] [vtable setup for class template] https://github.com/esbmc/esbmc/issues/1127
    • [unamed union ctor] https://github.com/esbmc/esbmc/issues/1128
    • [] [function as non-type parameter] https://github.com/esbmc/esbmc/issues/1129
  • [formalisation dynamic alloc] https://github.com/esbmc/esbmc/issues/825
  • [new] https://github.com/esbmc/esbmc/issues/924

• OM issues:

  • [OM simplification] https://github.com/esbmc/esbmc/issues/965

Development Tracking:

The new clang-based frontend is under development. We are currently working to pass the benchmark regression/esbmc-cpp/cpp which contains 370 test cases. Please see benchmark stats in each subsection.

The stats are generated by applying the following commands in the benchmark logs from Github workflow “Run a Benchmark”:

To generate stats about error signatures:

egrep "Assertion|ERROR" * -rn | egrep -v "//" | cut -d':' -f3- | sort | uniq -c

To generate stats about passes:

egrep "VERIFICATION FAILED|VERIFICATION SUCCESSFUL" * -rn | rev | cut -d ':' -f 1 | rev | sort | uniq -c

Summary of Pass Rate in Each Test Suite:

The following lines are used to fix the TCs, and added here for future reference: The commands below are for future reference: Fix the include path for Linux CIs:

egrep "\-I ~/libraries" . -rl | xargs sed -i 's/-I \~\/libraries/-I \/__w\/esbmc\/esbmc\/src\/cpp\/library/g'

Add tag for each TC in a test suite:

from pathlib import Path
for path in Path('./').rglob('test.desc'):
    print(path)
    f = open(path,'r')
    lines = f.readlines()[:-1]
    lines.append("<item_10_mode>KNOWNBUG</item_10_mode>" + "\n")
    lines.append("</test-case>")
    f.close()
    f = open(path,'w')
    f.writelines(lines)

Tracking Error Signatures for esbmc-cpp/cpp test suite:

Since we’ve added the support for most of the key features, most, if not all, errors are of the type PARSE ERRORS in our OMs for STL test suites. There’s no need to track parse errors for those test suites. See section Summary of Pass Rate in Each Test Suite for the most up-to-date pass rate.

Build LLVM from source:

Using a debug build of clang greatly helps debugging the clang-based C++ converter in ESBMC. See Rafael’s guide in https://github.com/esbmc/esbmc/wiki/Windows-Build#llvm