A Simulator for LLVM Bitcode
This work provides a domain-specific tool for developers and researchers working with LLVM bitcode, offering incremental improvements in simulation and debugging capabilities.
The authors tackled the problem of simulating and debugging LLVM bitcode programs by introducing an interactive simulator with features like precise thread scheduling, reverse stepping, and compatibility with an existing model checker, resulting in a tool that enables detailed analysis and visualization of program execution.
In this paper, we introduce an interactive simulator for programs in the form of LLVM bitcode. The main features of the simulator include precise control over thread scheduling, automatic checkpoints and reverse stepping, support for source-level information about functions and variables in C and C++ programs and structured heap visualisation. Additionally, the simulator is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker.