An important step toward adoption of formal methods in software development is support for mainstream programming languages. Unfortunately, these languages are often rather complex and come with substantial standard libraries. However, by choosing a suitable intermediate language, most of the complexity can be delegated to existing execution-oriented (as opposed to verification-oriented) compiler frontends and standard library implementations. In this paper, we describe how support for C++ exceptions can take advantage of the same principle. Our work is based on DiVM, an LLVM-derived, verification-friendly intermediate language.
Our implementation consists of 2 parts: an implementation of the
libunwindplatform API which is linked to the program under test and consists of 9 C functions. The other part is a preprocessor for LLVM bitcode which prepares exception-related metadata and replaces associated special-purpose LLVM instructions.
References
- DiVM: Model Checking with LLVM and Graph Memory, currently unpublished, but a preliminary full text is available
Source Code
The benchmarks included in the paper were obtained with 4 different variants of DIVINE. Source code for each of those variants, in the form of a tarball and a darcs repository is available for download:
- no exception support (the C++ compiler is executed with
-fno-exceptions): [darcs] [tar] - exceptions implemented inside the VM, using special hypercalls (the DIVINE 3 method): [darcs] [tar]
- stub exceptions – exceptions are replaced with a function which indicates an error: [darcs] [tar]
- the DIVINE 4 approach, described in the paper: [darcs] [tar]
Additionally, the source code for re-usable components involved in exception support as implemented in DIVINE 4 (and as described in the paper) are provided here: the LLVM transformation and the DiVM unwinder.
Benchmarks
Additional benchmark results will be published here as they become available.