1. Modular, compositional, and executable formal semantics for LLVM IR
- Author
-
Vadim Zaliva, Calvin Beck, Irene Yoon, Yannick Zakowski, Steve Zdancewic, Ilia Zaichuk, CASH - Compilation and Analysis, Software and Hardware (CASH), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), University of Pennsylvania, and Department of Computer and Information Science [Pennsylvania] (CIS)
- Subjects
Monads ,Verified Compilation ,Correctness ,Semantics (computer science) ,Computer science ,Formal semantics (linguistics) ,0102 computer and information sciences ,02 engineering and technology ,computer.software_genre ,Semantic data model ,01 natural sciences ,Operational semantics ,Software and its engineering ,0202 electrical engineering, electronic engineering, information engineering ,Coq ,Safety, Risk, Reliability and Quality ,Theory of computation ,Denotational semantics ,Bisimulation ,[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] ,Interpretation (logic) ,Programming language ,020207 software engineering ,computer.file_format ,Semantics ,Compilers ,010201 computation theory & mathematics ,Program verification ,LLVM ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Executable ,computer ,Software - Abstract
International audience; This paper presents a novel formal semantics, mechanized in Coq, for a large, sequential subset of the LLVM IR. In contrast to previous approaches, which use relationally-specified operational semantics, this new semantics is based on monadic interpretation of interaction trees, a structure that provides a more compositional approach to defining language semantics while retaining the ability to extract an executable interpreter. Our semantics handles many of the LLVM IR's non-trivial language features and is constructed modularly in terms of event handlers, including those that deal with nondeterminism in the specification. We show how this semantics admits compositional reasoning principles derived from the interaction trees equational theory of weak bisimulation, which we extend here to better deal with nondeterminism, and we use them to prove that the extracted reference interpreter faithfully refines the semantic model. We validate the correctness of the semantics by evaluating it on unit tests and LLVM IR programs generated by HELIX.
- Published
- 2021