Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 3/2022

01.04.2022 | General

DivSIM , an interactive simulator for LLVM bitcode

verfasst von: Petr Ročkai, Jiří Barnat

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 3/2022

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

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.
Vorheriger Artikel Temporal-logic query checking over finite data streams

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren
Fußnoten
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.
 
Literatur
1.
2.
Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL, pp. 97–105. ACM (2003)
3.
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.
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.
Basu, S., Saha, D., Smolka, S.A.: Getting to the root of the problem: focus statements for the analysis of counter-examples (2012)
6.
Behrmann, G., David, A., Larsen, K.G.: A tutorial on uppaal. In: SFM (2004)
7.
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.
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.
Groce, A., Kroening, D., Lerda, F.: Understanding counterexamples with explain. In: Computer Aided Verification, LNCS, pp. 453–456. Springer (2004)
10.
11.
Kleiman, R., Brayshaw, M., Eisenstadt, M., Eisenstadt, M.: Tales of debugging from the front lines (1993)
12.
13.
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.
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.
Lee, K.: Using LLDB, pp. 415–434. Apress, Berkeley, CA (2013). ISBN 978-1-4302-5051-7
16.
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.
Magee, J.: Behavioral analysis of software architectures using LTSA. In: ICSE (1999)
18.
Nethercote, N., Seward, J.: Valgrind: a framework for heavyweight dynamic binary instrumentation. In: PLDI (2007)
19.
Ročkai, P., Barnat, J.: A simulator for llvm bitcode. In: Formal Methods for Industrial Critical Systems, pp. 127–142. Springer, Cham (2019)
20.
21.
22.
Stallman, R., Pesch, R., Shebs, S.: Debugging with gdb (2010)
23.
24.
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.
Visser, W., Groce, A.: What went wrong: Explaining counterexamples. In: SPIN, LNCS, pp. 121–135. Springer (2002)
Metadaten
Titel
DivSIM , an interactive simulator for LLVM bitcode
verfasst von
Petr Ročkai
Jiří Barnat
Publikationsdatum
01.04.2022
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 3/2022
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-022-00659-x

Weitere Artikel der Ausgabe 3/2022

International Journal on Software Tools for Technology Transfer 3/2022 Zur Ausgabe

Introduction

Formal methods and tools for industrial critical systems

General

Envelopes and waves: safe multivehicle collision avoidance for horizontal non-deterministic turns

General

Formal verification of OIL component specifications using mCRL2

General

DFT modeling approach for operational risk assessment of railway infrastructure

General

Formal modeling and verification for amplification timing anomalies in the superscalar TriCore architecture

General

Verifiable strategy synthesis for multiple autonomous agents: a scalable approach

Premium Partner

    Bildnachweise