ECOOP 2020
Sun 15 - Tue 17 November 2020 Online Conference
co-located with SPLASH 2020
Sun 15 Nov 2020 13:00 - 13:20 at SPLASH-I - S-4 Chair(s): Karim Ali, Eli Tilevich
Mon 16 Nov 2020 01:00 - 01:20 at SPLASH-I - S-4 Chair(s): Elisa Gonzalez Boix, Atsushi Igarashi

LLVM is designed for the compile-time, link-time and run-time optimization of programs written in various programming languages. The language supported by LLVM targeted by modern compilers is LLVM IR. In this paper we define K-LLVM, a reference semantics for LLVM IR. To the best of our knowledge, K-LLVM is the most complete formal LLVM IR semantics to date, including all LLVM IR instructions, intrinsic functions in the LLVM documentation and Standard-C library functions that are necessary to execute many LLVM IR programs. Additionally, K-LLVM formulates an abstract machine that executes all LLVM IR instructions. The machine allows to describe our formal semantics in terms of simulating a conceptual virtual machine that runs LLVM IR programs, including non-deterministic programs. Even though the K-LLVM memory model in this paper is assumed to be a sequentially consistent memory model and does not include all LLVM concurrency memory behaviors, the design of K-LLVM’s data layout allows the K-LLVM abstract machine to execute some LLVM IR programs that previous semantics did not cover, such as the full range of LLVM IR behaviors for the interaction among LLVM IR casting, pointer arithmetic, memory operations and some memory flags (e.g. readonly) of function headers. Additionally, the memory model is modularized in a manner that supports investigating other memory models. To validate K-LLVM, we have implemented it in K [41], which generated an interpreter for LLVM IR. Using this, we ran tests including 1,385 unit test programs and 2,156 concrete LLVM IR programs, and K-LLVM passed all of them.

Sun 15 Nov

Displayed time zone: Central Time (US & Canada) change

13:00 - 14:20
S-4Research Papers at SPLASH-I +12h
Chair(s): Karim Ali University of Alberta, Eli Tilevich Virginia Tech
13:00
20m
Talk
K-LLVM: A Relatively Complete Semantics of LLVM IR
Research Papers
Liyi Li University of Illinois at Urbana-Champaign, Elsa Gunter University of Illinois
Link to publication DOI Media Attached
13:20
20m
Talk
A Type-Directed Operational Semantics for a Calculus with a Merge Operator
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Link to publication DOI Media Attached
13:40
20m
Talk
A big step from finite to infinite computationsSCICO Journal-First
Research Papers
Davide Ancona DIBRIS, University of Genova, Italy, Francesco Dagnino DIBRIS, University of Genova, Italy, Jurriaan Rot Radboud University Nijmegen, Elena Zucca University of Genova
Link to publication DOI Media Attached
14:00
20m
Talk
Static Type Analysis by Abstract Interpretation of Python Programs
Research Papers
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Link to publication DOI Media Attached File Attached

Mon 16 Nov

Displayed time zone: Central Time (US & Canada) change

01:00 - 02:20
S-4Research Papers at SPLASH-I
Chair(s): Elisa Gonzalez Boix Vrije Universiteit Brussel, Belgium, Atsushi Igarashi Kyoto University, Japan
01:00
20m
Talk
K-LLVM: A Relatively Complete Semantics of LLVM IR
Research Papers
Liyi Li University of Illinois at Urbana-Champaign, Elsa Gunter University of Illinois
Link to publication DOI Media Attached
01:20
20m
Talk
A Type-Directed Operational Semantics for a Calculus with a Merge Operator
Research Papers
Xuejing Huang The University of Hong Kong, Bruno C. d. S. Oliveira University of Hong Kong
Link to publication DOI Media Attached
01:40
20m
Talk
A big step from finite to infinite computationsSCICO Journal-First
Research Papers
Davide Ancona DIBRIS, University of Genova, Italy, Francesco Dagnino DIBRIS, University of Genova, Italy, Jurriaan Rot Radboud University Nijmegen, Elena Zucca University of Genova
Link to publication DOI Media Attached
02:00
20m
Talk
Static Type Analysis by Abstract Interpretation of Python Programs
Research Papers
Raphaël Monat Sorbonne Université — LIP6, Abdelraouf Ouadjaout Sorbonne Université, Antoine Miné Sorbonne Université
Link to publication DOI Media Attached File Attached