A Validated Semantics for LLVM IR

Abstract

Intermediate representation (IR) is a language that is used internally by a compiler to represent programs. Translation to an IR should preserve guarantees from the source language's specification because they enable various optimizations. This naturally makes an IR a language that is rich with high-level information.

In LLVM, the semantics of important high-level features in IR was not rigorously defined. It caused compiler optimizations in LLVM to use different interpretations, and bad interactions between the optimizations resulted in miscompilation bugs that are hard to fix. To solve this problem, the IRs semantics must be defined precisely. Then, optimizations that are incorrect with respect to the chosen semantics must be fixed. Both processes are challenging because LLVM is a large, fastly evolving software.

This thesis proposes (1) formal semantics of LLVM IR that resolves critical problems that we have found in the old IR semantics, making it consistent (2) a translation validation framework for LLVM's optimizations to validate the new semantics. We show that the old semantics of undefined behavior and memory model in the IR cannot explain important optimizations in LLVM. We propose new semantics that solves this problem. Next, we present Alive2, a translation validation framework for LLVM based on the new semantics. Alive2 relies on an automatic theorem prover to validate optimizations without any hints from LLVM. It supports most of integer and float operations, memory operations, function calls, and branches. To make validation practical, resources used by the tool is bounded.

The new formal semantics of undefined behavior has been adopted by LLVM. The `freeze' instruction that is proposed by us is officially added into LLVM 10.0, and the official document is updated to use our semantics. Also, critical problems in the old memory model we have found were shared with compiler developers, and patches have landed in LLVM to fix it. Alive2 has found more than 50 miscompilation bugs in LLVM so far and is used daily by LLVM developers.

중간언어는 컴파일러가 변환 중인 프로그램을 내부적으로 나타내기 위해 사용하는 언어이다. 소스 프로그램을 중간언어로 번역할 때는 소스 언어의 명세로부터 얻을 수 있는 여러 고급 정보들을 잘 보존해야 하는데, 그 이유는 컴파일러 최적화가 이 정보들을 활용할 수 있도록 하기 위해서이다. 따라서 중간언어는 이러한 고급 정보를 표현할 수 있는 문법들을 가지고 있다.

기존의 LLVM은 중간언어로 번역된 프로그램에 표현된 고급 정보들의 의미가 무엇인지를 엄밀하게 정의하고 있지 않았었다. 이것은 고급 정보를 나타내는 구문의 의미를 컴파일러 최적화 마다 서로 다르게 이해하는 결과를 낳았고, 이들 간의 나쁜 상호작용은 여러 컴파일러 버그들의 원인이 되었다. 이 문제를 해결하기 위해서는 먼저 중간언어에 있는 고급 정보의 의미를 먼저 정확하고 엄밀하게 정의해야 한다. 그 다음에는, LLVM 내의 컴파일러 최적화들이 해당 정의를 기준으로 옳은지를 하나하나 엄밀하게 체크해야 한다. 하지만 LLVM은 빠르게 진화하는 방대한 소프트웨어이기 때문에 효과적으로 이 문제를 해결하기가 쉽지 않다.

이 학위 논문에서는 (1) LLVM 컴파일러의 중간언어 의미에 존재하던 치명적인 문제들을 해결하는 새로운 형식 의미를 제안하고 (2) 그에 기반한 컴파일러 최적화 번역 검증 (translation validation) 프레임워크를 소개한다. 우리는 LLVM 컴파일러 중간언어의 정의되지 않은 행동 (undefined behavior) 과 메모리 모델에 심각한 문제가 있음을 보이며, 이것을 해결한 새로운 형식 의미를 제안한다. 둘째로, 우리는 자동 번역 검증 프레임워크 Alive2를 개발하였다. 제안된 번역 검증 프레임워크는 자동 명제 증명기 (SMT solver)를 사용해서 최적화의 옳음성을 수학적으로 엄밀하게 확인하며 컴파일러로부터의 도움이 필요하지 않다.

우리가 제안한 정의되지 않은 행동의 형식 의미는 LLVM 컴파일러에 공식적으로 채택되었다. 본 논문에서 제안한 `freeze' 명령어는 LLVM 10.0에 도입 되었으며, 공식 문서는 우리의 형식 의미를 사용하도록 업데이트 되었다. 또한, 기존의 LLVM 메모리 모델에서 찾은 치명적인 문제들은 컴파일러 개발자들에게 공유되었으며 여러 토론을 야기했고 이 문제를 해결하기 위한 패치가 LLVM 컴파일러에 적용되었다. 우리는 Alive2 를 이용해 수십개의 컴파일러 버그를 찾아낼 수 있었으며, 이 도구는 현재 LLVM 컴파일러 개발자들에 의해 코드 리뷰 과정에서 사용되고 있다.