A Simulator for LLVM Bitcode
Petr Ro\v{c}kai, Ji\v{r}\'i Barnat
TL;DR
This paper presents an interactive LLVM bitcode simulator with advanced features like thread control, checkpoints, reverse execution, source-level info, heap visualization, and compatibility with DiVM hypercalls for enhanced program analysis.
Contribution
It introduces a novel simulator that integrates source-level debugging, reverse execution, and compatibility with model checkers, improving program analysis capabilities.
Findings
Supports precise thread scheduling control
Enables reverse stepping and checkpoints
Integrates with DiVM hypercalls for counterexample analysis
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Parallel Computing and Optimization Techniques · Formal Methods in Verification