Combining Range and Inequality Information for Pointer Disambiguation

Résumé : 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.
Type de document :
Rapport
[Research Report] RR-9076, ENS Lyon; CNRS; INRIA. 2016
Liste complète des métadonnées

Littérature citée [62 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01429777
Contributeur : Maroua Maalej <>
Soumis le : dimanche 11 juin 2017 - 12:56:02
Dernière modification le : mardi 16 janvier 2018 - 15:34:55
Document(s) archivé(s) le : mercredi 13 décembre 2017 - 06:45:54

Fichier

RR-9076.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01429777, version 2

Collections

Citation

Maroua Maalej, Vitor Paisante, Fernando Magno Quintão Pereira, Laure Gonnord. Combining Range and Inequality Information for Pointer Disambiguation. [Research Report] RR-9076, ENS Lyon; CNRS; INRIA. 2016. 〈hal-01429777v2〉

Partager

Métriques

Consultations de la notice

81

Téléchargements de fichiers

41