Skip to Main content Skip to Navigation
Theses

Abstractions relationnelles de la mémoire pour une analyse compositionnelle de structures de données

Hugo Illous 1, 2
2 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria de Paris
Résumé : Les analyses statiques ont pour but d’inférer des propriétés sémantiques de programmes. Nous distinguons deux importantes classes d’analyses statiques : les analyses d’états et les analyses relationnelles. Alors que les analyses d’états calculent une sur-approximation de l’ensemble des états atteignables d’un programme, les analyses relationnelles calculent des propriétés fonctionnelles entre les états d’entrée et les états de sortie d’un programme. Les analyses relationnelles offrent plusieurs avantages, comme leur capacité à inférer des propriétés sémantiques plus expressives par rapport aux analyses d’états. De plus, elles offrent également la possibilité de rendre l’analyse compositionnelle, en utilisant les relations entrée-sortie comme des résumés de procédures, ce qui est un avantage pour le passage à l’échelle. Dans le cas des programmes numériques, plusieurs analyses ont été proposées qui utilisent des domaines abstraits numériques relationnels, pour décrire des relations. D’un autre côté, modéliser des abstractions de relations entre les états mémoires entrée-sortie tout en prenant en compte les structures de données est difficile. Dans cette Thèse, nous proposons un ensemble de nouveaux connecteurs logiques, reposant sur la logique de séparation, pour décrire de telles relations. Ces connecteurs peuvent exprimer qu’une certaine partie de la mémoire est inchangée, fraîchement allouée, ou désallouée, ou que seulement une seule partie de la mémoire est modifiée (et de quelle manière). En utilisant ces connecteurs, nous construisons un domaine abstrait relationnel et nous concevons une analyse statique compositionnelle par interprétation abstraite qui sur-approxime des relations entre des états mémoires contenant des structures de données inductives. Nous avons implémenté ces contributions sous la forme d’un plug-in de l’analyseur FRAMA-C. Nous en avons évalué l’impact sur l’analyse de petits programmes écrits en C manipulant des listes chaînées et des arbres binaires, mais également sur l’analyse d’un programme plus conséquent qui consiste en une partie du code source d’Emacs. Nos résultats expérimentaux montrent que notre approche permet d’inférer des propriétés sémantiques plus expressives d’un point de vue logique que des analyses d’états. Elle se révèle aussi beaucoup plus rapide sur des programmes avec un nombre conséquent d’appels de fonctions sans pour autant perdre en précision.
Document type :
Theses
Complete list of metadatas

Cited literature [110 references]  Display  Hide  Download

https://tel.archives-ouvertes.fr/tel-02399767
Contributor : Abes Star :  Contact
Submitted on : Friday, March 20, 2020 - 5:36:08 PM
Last modification on : Tuesday, August 4, 2020 - 3:39:54 AM
Document(s) archivé(s) le : Sunday, June 21, 2020 - 4:41:34 PM

File

Illous-2019-These.pdf
Version validated by the jury (STAR)

Identifiers

  • HAL Id : tel-02399767, version 2

Collections

Citation

Hugo Illous. Abstractions relationnelles de la mémoire pour une analyse compositionnelle de structures de données. Langage de programmation [cs.PL]. PSL Research University, 2019. Français. ⟨NNT : 2019PSLEE015⟩. ⟨tel-02399767v2⟩

Share

Metrics

Record views

157

Files downloads

76