Combining Range and Inequality Information for Pointer Disambiguation

Autor: Maalej, Maroua, Paisante, Vitor, Quintão Pereira, Fernando Magno, Gonnord, Laure
Přispěvatelé: Optimisation des ressources : modèles, algorithmes et ordonnancement (ROMA), 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), Université de Lyon, Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Laboratório de Linguagens de Programação (LLP), Universidade Federal de Minas Gerais, Université Claude Bernard Lyon 1 (UCBL), This work was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon,within the program 'Investissements d'Avenir' (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR)., ENS Lyon, CNRS, INRIA, Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon)-Centre National de la Recherche Scientifique (CNRS)-Université de Lyon-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-École normale supérieure - Lyon (ENS Lyon), École normale supérieure - Lyon (ENS 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 - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL)
Jazyk: angličtina
Rok vydání: 2016
Předmět:
Zdroj: [Research Report] RR-9076, ENS Lyon; CNRS; INRIA. 2016
Popis: Pentagons is an abstract domain invented by Logozzo and Fähndrich to validate arrayaccesses in low-level programming languages. This algebraic structure provides a cheap “less-thancheck”, which builds a partial order between the integer variables used in a program. In this paper,we show how we have used the ideas available in Pentagons to design and implement a novel aliasanalysis. This new algorithm lets us disambiguate pointers with offsets, so common in C-stylepointer arithmetics, in a precise and efficient way. Together with this new abstract domain wedescribe several implementation decisions that lets us produce a practical pointer disambiguationalgorithm on top of the LLVM compiler. Our alias analysis is able to handle programs as large asSPEC’s gcc in a few minutes. Furthermore, we have been able to improve the percentage of pairsof pointers disambiguated, when compared to LLVM’s built-in analyses, by a four-fold factor insome benchmarks.; Les Pentagons est un domaine abstrait inventé par Logozzo et Fähndrich pour la validation des accès tableaux dans les langages de programmation à bas niveau. Cette structure algébrique fournit une relation d’ordre partiel entre les variables entières du programme. Il s’agit d’une relation "plus petit que". Dans ce papier, nous montrons comment utiliser l’idée des Pentagons pour concevoir et implémenter une nouvelle analyse d’alias. Ce nouvel algorithme nous permet de désambiguiser, d’une manière précide et efficace, des pointeurs avec des offsets fréquemment utlisés dans l’arithmétique des pointeurs en C. Nous décrivons, en plus de ce nouveau domaine abstrait, plusieurs détails d’implémentation qui nous ont permis de produire un algorithme d’analyse de pointeurs dans LLVM. Notre analyse est capable de traiter des programmes aussi larges que gcc de SPEC en quelques minutes seulement. Par ailleurs, pour certains benchmarks, nous avons réussi à améliorer par facteur de quatre le pourcentage de paires de pointeurs désambiguisés, étant comparé aux analyses existantes dans LLVM.
Databáze: OpenAIRE