Skip to main content
Top
Published in: International Journal on Software Tools for Technology Transfer 3/2022

01-04-2022 | General

DivSIM , an interactive simulator for LLVM bitcode

Authors: Petr Ročkai, Jiří Barnat

Published in: International Journal on Software Tools for Technology Transfer | Issue 3/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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, DivSIM is compatible with DiVM (DIVINE VM) hypercalls, which makes it possible to load, simulate and analyse counterexamples from an existing model checker, and with abstract bitcode generated by LART (LLVM Abstraction and Refinement Tool), making it suitable for direct analysis of abstract and/or symbolic programs and counterexamples.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Footnotes
2
How this is achieved is described in more detail in [20].
 
3
A minor technical complication arises from the fact that the formatting function needs to be invoked in the context in which the abstract value exists. However, since debug nodes already carry a reference to the snapshot (program state) which they describe and DiVM can cheaply continue execution from an arbitrary snapshot, this is not a serious problem.
 
4
There are actually two implementation choices. The evaluation could be handed off to the term domain itself, the same as for formatting abstract values, though in this case it is more complicated, since the model needs to be passed to the evaluation routine. However, since the model checker needs to be able to evaluate the terms anyway to build the SMT query, it seems reasonable to do the evaluation on the DiVM /DivSIM side.
 
5
The behaviour of the program may depend on external factors, such as scheduling choices, user inputs, asynchronous events and so on. In DiVM , these all map to the choose hypercall.
 
6
This is often the case in verification-centric tools, partly because it is a simple implementation strategy that builds on the same primitives as the verification tool itself.
 
7
This description is necessarily incomplete, being much more concise than the real representation of the program’s state. Including additional information improves completeness, but compromises brevity, which is an important strength of this presentation format.
 
8
The typical cause will be an out-of-bound memory access on a stack-allocated variable. In real execution, this is not in itself an error, but will be detected and reported by DiVM , since each local variable is allocated in its own memory object (as discussed in Sect. 3).
 
11
The source code of the graphical user interface is available from supplementary materials page at https://​divine.​fi.​muni.​cz/​2021/​sim/​.
 
12
We speculate that this is the primary reason why interactive simulators (and debuggers in general) are so scarce.
 
13
At the time of this writing, work is in progress to provide simple Python bindings for the C++ API, via Boost.Python. We believe the Python API will make DivSIM more accessible to 3rd-party developers.
 
14
Supported by anecdotal evidence from working with students, both individually and in a validation & verification course.
 
Literature
2.
go back to reference Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97–105. ACM (2003) Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97–105. ACM (2003)
3.
go back to reference Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: IFM, LNCS. Springer (2004) Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and static driver verifier: technology transfer of formal methods inside microsoft. In: IFM, LNCS. Springer (2004)
4.
go back to reference Barnat, J., Beran, J., Brim, L., Kratochvíla, T., Ročkai, P.: Tool chain to support automated formal verification of avionics Simulink designs. In: FMICS, number 7437 in LNCS, pp. 78–92. Springer (2012) Barnat, J., Beran, J., Brim, L., Kratochvíla, T., Ročkai, P.: Tool chain to support automated formal verification of avionics Simulink designs. In: FMICS, number 7437 in LNCS, pp. 78–92. Springer (2012)
5.
go back to reference Basu, S., Saha, D., Smolka, S.A.: Getting to the root of the problem: focus statements for the analysis of counter-examples (2012) Basu, S., Saha, D., Smolka, S.A.: Getting to the root of the problem: focus statements for the analysis of counter-examples (2012)
6.
go back to reference Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM (2004) Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM (2004)
7.
go back to reference Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX Association (2008) Cadar, C., Dunbar, D., Engler, D.R.: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX Association (2008)
8.
go back to reference Chalupa, M., Jašek, T., Tomovič, L., Hruška, M., Šoková, V., Ayaziová, P., Strejček, J., Vojnar, T.: Symbiotic 7: Integration of predator and more. In: TACAS, pp. 413–417. Springer, Cham (2020). ISBN 978-3-030-45237-7 Chalupa, M., Jašek, T., Tomovič, L., Hruška, M., Šoková, V., Ayaziová, P., Strejček, J., Vojnar, T.: Symbiotic 7: Integration of predator and more. In: TACAS, pp. 413–417. Springer, Cham (2020). ISBN 978-3-030-45237-7
9.
go back to reference Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Computer Aided Verification, LNCS, pp. 453–456. Springer (2004) Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Computer Aided Verification, LNCS, pp. 453–456. Springer (2004)
11.
go back to reference Kleiman, R., Brayshaw, M., Eisenstadt, M., Eisenstadt, M.: Tales of debugging from the front lines (1993) Kleiman, R., Brayshaw, M., Eisenstadt, M., Eisenstadt, M.: Tales of debugging from the front lines (1993)
13.
go back to reference Lauko, H., Ročkai, P., Barnat, J.: Symbolic computation via program transformation. In: Theoretical Aspects of Computing—ICTAC, pp. 313–332. Springer, Cham (2018) Lauko, H., Ročkai, P., Barnat, J.: Symbolic computation via program transformation. In: Theoretical Aspects of Computing—ICTAC, pp. 313–332. Springer, Cham (2018)
14.
go back to reference Lauko, H., Štill, V., Ročkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: TACAS, pp. 204–208. Springer, Cham (2019) Lauko, H., Štill, V., Ročkai, P., Barnat, J.: Extending DIVINE with symbolic verification using SMT. In: TACAS, pp. 204–208. Springer, Cham (2019)
15.
go back to reference Lee, K.: Using LLDB, pp. 415–434. Apress, Berkeley, CA (2013). ISBN 978-1-4302-5051-7 Lee, K.: Using LLDB, pp. 415–434. Apress, Berkeley, CA (2013). ISBN 978-1-4302-5051-7
16.
go back to reference Legay, A., Nowotka, D., Poulsen, D.B., Tranouez, L.-M.: Statistical model checking of llvm code. In: Formal Methods, pp. 542–549. Springer, Cham (2018) Legay, A., Nowotka, D., Poulsen, D.B., Tranouez, L.-M.: Statistical model checking of llvm code. In: Formal Methods, pp. 542–549. Springer, Cham (2018)
17.
go back to reference Magee, J.: Behavioral analysis of software architectures using LTSA. In: ICSE (1999) Magee, J.: Behavioral analysis of software architectures using LTSA. In: ICSE (1999)
18.
go back to reference Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007) Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007)
19.
go back to reference Ročkai, P., Barnat, J.: A simulator for llvm bitcode. In: Formal Methods for Industrial Critical Systems, pp. 127–142. Springer, Cham (2019) Ročkai, P., Barnat, J.: A simulator for llvm bitcode. In: Formal Methods for Industrial Critical Systems, pp. 127–142. Springer, Cham (2019)
22.
go back to reference Stallman, R., Pesch, R., Shebs, S.: Debugging with gdb (2010) Stallman, R., Pesch, R., Shebs, S.: Debugging with gdb (2010)
24.
go back to reference Visan, A.-M., Arya, K.: Gene Cooperman, and Tyler Denniston. URDB: a universal reversible debugger based on decomposing debugging histories. In: PLOS ’11 (2011) Visan, A.-M., Arya, K.: Gene Cooperman, and Tyler Denniston. URDB: a universal reversible debugger based on decomposing debugging histories. In: PLOS ’11 (2011)
25.
go back to reference Visser, W., Groce, A.: What went wrong: Explaining counterexamples. In: SPIN, LNCS, pp. 121–135. Springer (2002) Visser, W., Groce, A.: What went wrong: Explaining counterexamples. In: SPIN, LNCS, pp. 121–135. Springer (2002)
Metadata
Title
DivSIM , an interactive simulator for LLVM bitcode
Authors
Petr Ročkai
Jiří Barnat
Publication date
01-04-2022
Publisher
Springer Berlin Heidelberg
Published in
International Journal on Software Tools for Technology Transfer / Issue 3/2022
Print ISSN: 1433-2779
Electronic ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00659-x

Other articles of this Issue 3/2022

International Journal on Software Tools for Technology Transfer 3/2022 Go to the issue

Premium Partner