A Formal Semantics of the GraalVM Intermediate Representation

Autor:	Webb, Brae J., Utting, Mark, Hayes, Ian J.
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science Computer Science - Programming Languages
Druh dokumentu:	Working Paper
DOI:	10.1007/978-3-030-88885-5_8
Popis:	The optimization phase of a compiler is responsible for transforming an intermediate representation (IR) of a program into a more efficient form. Modern optimizers, such as that used in the GraalVM compiler, use an IR consisting of a sophisticated graph data structure that combines data flow and control flow into the one structure. As part of a wider project on the verification of optimization passes of GraalVM, this paper describes a semantics for its IR within Isabelle/HOL. The semantics consists of a big-step operational semantics for data nodes (which are represented in a graph-based static single assignment (SSA) form) and a small-step operational semantics for handling control flow including heap-based reads and writes, exceptions, and method calls. We have proved a suite of canonicalization optimizations and conditional elimination optimizations with respect to the semantics. Comment: 16 pages, 8 figures, to be published to ATVA 2021
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2107.01815 Zobrazit plný text záznamu View this record from Arxiv