Loop Analysis for LLVM IR Translation Validation Framework

Abstract

Bugs in compilers can have severe consequences. Apart from traditional methods like testing, one of the ways of keeping compilers correct that gained traction only in recent years is translation validation, a technique ensuring the semantic correctness of optimizations in compilers. Alive2 is an open-source translation validation framework for LLVM that is currently widely used by LLVM developers. In order to make any static analysis tool usable, the frequency of false alarms must be kept to a minimum. Alive2 was designed to have zero false alarms and has been very successful in this endeavor except in the case of certain loops. Our aim in this thesis is to analyze Alive2's loop algorithms in an attempt to find the cause of these false alarms. This was motivated by personal communication with authors of Alive2 who presented the false alarm issue in loops as one of the more challenging and pressing issues in Alive2. We were successful in pinpointing the cause of false alarms and even providing a fix for the issue. Our solution is now a part of the Alive2 framework. Furthermore, we have identified other potential issues in Alive2 which we discuss in the thesis as well.

Chyby v překladačích programovacích jazyků mohou mít vážné následky. Kromě tradičních metod, jako je testování, je jedním ze způsobů zajištění správnosti překladačů translation validation, technika zajišťující sémantic- kou správnost optimalizací v překladačích, která se prosadila teprve v po- sledních pár letech. Alive2 je open-source translation validation framework pro LLVM, který je v současnosti široce používán vývojáři LLVM. Pro za- jištění použitelnosti statických analyzátorů je potřeba minimalizovat četnost falešných pozitiv. Alive2 je navržen tak, aby neměl žádná falešná pozitiva a byl v tomto ohledu velmi úspěšný až na některé programy se smyčkami. Na- ším cílem v této práci je analyzovat algoritmy Alive2 pracující se smyčkami se záměrem identifikace příčiny falešných pozitiv. Naše práce byla motivo- vána komunikací s autory Alive2, kteří považovali problematiku falešných poplachů ve smyčkách jako jeden z náročnějších a závažnějších problémů v Alive2. Podařilo se nám přesně určit podstatu problému falešných poplachů a dokonce i opravit tento problém. Naše řešení je aktuálně součástí Alive2. Kromě toho jsme v Alive2 identifikovali další potenciální problémy, o kterých v této práci také pojednáváme.