Le cadre de cette thèse est l'analyse statique modulaire par interprétation abstraite de logiciels en vue de leur vérification automatique. Nous nous intéressons en particulier aux programmes comportant des objets alloués dynamiquement sur un tas et repérés par des pointeurs. Le but final étant de trouver des erreurs dans un programme (problèmes de déréférencements et d'alias) ou de prouver qu'un programme est correct (relativement à ces problèmes) de façon automatique. Isthiaq, Pym, O'Hearn et Reynolds ont développé récemment des logiques de fragmentation (separation logics) qui sont des logiques de Hoare avec un langage d'assertions/de prédicats permettant de démontrer qu'un programme manipulant des pointeurs sur un tas est correct. La sémantique des triplets de la logique ({P}C{P

Dans la thèse nous présentons un cadre pour l'analyse statique de langages orientés objets qui tient compte des propriétés de modularité de ces langages. Il y a plusieurs défis à relever pour obtenir une analyse statique efficace de langages orientés objet. Tout d'abord, elle doit gérer les particularités de ces langages telles que l'héritage, le polymorphisme et la résolution de méthodes virtuelles. Deuxièmement, elle doit être modulaire. En fait, les programmes orientés objet typiques sont fait de plusieurs milliers de classes et une analyse monolithique du programmes complet peut être trop coûteuse pour être pratiquée. Troisièmement, la technologie orientée objet favorise la programmation par composants, en cela qu'un composant (une classe) est développée une fois pour toute et utilisée dans de nombreux contextes différents. Aussi, une analyse statique efficace doit pouvoir inférée des propriétés des composants valides pour toutes les instantiations possibles de contextes. Dans cette thèse, nous présentons une analyse qui relève les défis esquissés ci-dessus. En particulier, nous nous concentrons sur une analyse qui peut inférer des invariants de classe. Un invariant de classe est une propriété d'une classe valide pour chaque instanciation, avant et après l'exécution de n'importe quelle méthode de la classe. Notre analyse a plusieurs avantages. Elle est indépendante du langage, elle exploite la structure modulaire des langages orientés objet et elle gère les principales fonctionnalités de ces langages, à savoir l'héritage, le polymorphisme et l'encapsulation. Le cadre présenté dans cette thèse est très flexible. En particulier, il permet de régler finement l'analyse selon les trois axes orthogonaux suivants: - Domaine abstrait sous-jacent: une classe peut être analysée en utilisant soit un domaine abstrait générique soit un domaine abstrait symbolique de façon à obtenir une analyse plus efficace mais moins précise. - Gestion de l'héritage: une sous-classe peut être analysée soit directement, en expansant syntaxiquement la relation de sous-classe, soit indirectement, en utilisant l'invariant du parent afin d'éviter une explosion quadratique de la complexité. -Traitement des contextes d'instantiation: une classe peut être utilisée soit indépendamment du contexte, afin d'obtenir un résultat valable dans tous les contextes, soit en utilisant une approximation du contexte afin d'obtenir un résultat plus précis mais moins général.

Les contraintes arithmétiques sont largement utilisées dans les langages formels comme les expressions, les grammaires d'arbres et les chemins réguliers. Ces contraintes sont utilisées dans les modéles de contenu des types (XML Schemas) pour imposer des bornes sur le nombre d'occurrences de nœuds. Dans les langages de requêtes (XPath, XQuery), ces contraintes permettent de sélectionner les nœuds ayant un nombre limité de nœuds accessibles par une expression de chemin donnée. Les types et chemins étendus avec les contraintes de comptage constituent le prolongement naturel de leurs homologues sans comptage déjà considérés comme des constructions fondamentales dans les langages de programmation et les systèmes de type pour XML. Un des défis majeurs en programmation XML consiste à développer des techniques automatisées permettant d'assurer statiquement un typage correct et des optimisations de programmes manipulant les données XML. À cette fin, il est nécessaire de résoudre certaines tâches de raisonnement qui impliquent des constructions telles que les types et les expressions XPath avec des contraintes de comptage. Dans un futur proche, les compilateurs de programmes XML devront résoudre des problèmes de base tels que le sous-typage afin de s'assurer au moment de la compilation qu'un programme ne pourra jamais générer de documents non valides à l'exécution. Cette thèse étudie les logiques capables d'exprimer des contraintes de comptage sur les structures d'arbres. Il a été montré récemment que le mu-calcul sur les graphes, lorsqu'il est étendu à des contraintes de comptage portant exclusivement sur les nœuds successeurs immédiats est indécidable. Dans cette thèse, nous montrons que, sur les arbres finis, la logique avec contraintes de comptage est décidable en temps exponentiel. En outre, cette logique fournit des opérateurs de comptage selon des chemins plus généraux. En effet, la logique peut exprimer des contraintes numériques sur le nombre de nœuds descendants ou même ascendants. Nous présentons également des traductions linéaires d'expressions XPath et de types XML comportant des contraintes de comptage dans la logique.

Ce travail s'inscrit dans le cadre des recherches menées autour de l'analyse et la visualisation des logiciels, notamment les logiciels à objets, et en particulier Java. Très brièvement, on peut dire que le but de cette thèse revient à tenter de répondre à une question fondamentale: comment faire pour faciliter la compréhension du logiciel par ses développeurs et concepteurs ? Ce travail de recherche est basé en grande partie sur deux axes principaux. Le premier consiste à analyser l'exécution des programmes, non seulement au niveau de la méthode, mais bien au niveau du bloc de base, pour recueillir des données d'exécutions avec un maximum de précision comme par exemple les différents types d'instances sur les sites d'appels. Le second axe considère l'utilisation des informations apportées par notre analyse dynamique de l'exécution pour permettre la visualisation de ces données. En effet, ces informations offrent des détails intéressants sur le fonctionnement du programme et aident à expliquer le comportement du logiciel, aussi bien pour déceler les problèmes de performance que les problèmes de codages. Nous proposons une technique souple et efficace qui effectue une analyse dynamique de l'exécution de programmes Java. Nous introduisons ainsi une nouvelle technique et un nouvel outil permettant de recueillir des informations encore non proposées par d'autres analyseurs. Cette approche trace l'exécution précise des programmes tout en ayant une baisse des performances d'exécution acceptable, laissant le programme final utilisable. De plus, nous proposons et expérimentons une approche basé sur la visualisation des relations au sein d'une représentation du logiciel par une métaphore de ville. Nous introduisons une nouvelle technique de représentation des relations nommée "3D Hierarchical Edge Bundles" qui est basée sur une représentation 2D existante nommée "Hierarchical Edge Bundles". Cette approche conserve la puissance de visualisation du logiciel offerte par la métaphore de la ville tout en ajoutant la représentation des relations, et cela d'une façon lisible. Ces travaux sont validés entre autres par le développement d'un outil d'analyse nommé VITRAIL JBInsTrace et d'un outil de visualisation nommé VITRAIL Visualizer. Ces outils sont la base de nos recherche actuelles sur l'étude de l'exécution des programmes objets.

La bonne gestion des déréférencements de nul dans les langages à objets statiquement typés est un problème complexe qui est loin d'être nouveau. Plusieurs approches existent, mais aucune n'est parfaite. Les diverses solutions au déréférencement de nul se partagent trois dimensions : (1) la simplicité, (2) l'exactitude des résultats et (3) le typage statique. Présentement, à notre connaissance, aucune solution ne présente ces trois dimensions. Un des problèmes majeurs de la gestion des déréférencements de nul est la gestion des attributs, notamment lors de l'instantiation des objets. L'approche que nous présentons ici pour gérer les déréférencements de nul est une approche (1) simple et (2) exacte. Bien que notre approche présente un composant de typage statique, nous ajoutons aussi des tests dynamiques pour la compléter, ce qui fait qu'elle ne respecte pas totalement les trois dimensions. Nous introduisons aussi des analyses statiques pour détecter l'initialisation d'attributs dans les constructeurs pour ensuite, à l'aide d'optimisations, supprimer les tests dynamiques que nous avons ajoutés à la phase précédente. Pour un programme de grande taille (110.000 lignes de code), nous parvenons, avec nos analyses et nos optimisations, à supprimer 100% des tests dynamiques que nous avions introduits, tout en garantissant de façon statique qu'aucune erreur en lien avec le déréférencement de nul ne pourra se produire lors de l'exécution du programme. En conséquence, notre solution améliorée par les analyses statiques proposées permet de présenter les trois dimensions recherchées pour un sous-ensemble des programmes, ce qui fait un compromis très intéressant. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : compilation, analyse statique, optimisation, types nullables, validation d'attributs, Nit

La notion de système réactif désigne des systèmes qui maintiennent une<br />interaction permanente avec un environnement donné. La famille des<br />langages synchrones regroupe un des langages de programmation<br />dédiés à la conception de tels systèmes. De manière générale, ces langages<br />permettent de décrire le comportement de composants parallèles qui<br />s'exécutent de manière synchrone, relativement à une horloge logique sur<br />laquelle repose un mécanisme de diffusion instantanée de l'information.<br />La conception de ces langages permet un ordonnancement statique des composants<br />parallèles et une compilation des programmes vers du code séquentiel, des<br />automates à états finis ou des circuits. En contrepartie, les contraintes<br />imposées sur ces langages limitent leur utilisation à des domaines très<br />spécifiques. La programmation réactive désigne un paradigme de programmation<br />qui repose sur une relaxation de ces contraintes. Ce paradigme de<br />programmation, inspiré plus particulièrement par le langage Esterel, propose<br />un type de programmation concurrente plus général ayant pour objectif la<br />réalisation, par exemple, de controleurs "event driven", d'interfaces graphiques<br />, de simulations physiques, de service web et de jeux multi-joueurs.<br />Ce document porte sur la notion de logiciel sur dans le cadre de la<br />programmation réactive.<br />Dans la première partie, nous nous intéressons à la question du<br />controle statique des ressources nécessaires à l'exécution d'un programme<br />pour une algèbre de processus synchrone inspirée par le paradigme réactif.<br />Dans la seconde partie, nous nous intéressons à la question de<br />l'utilisation de la programmation réactive pour le développement<br />d'applications adaptées aux architectures multicores.<br />Plus précisèment, nous nous reposerons sur une analyse statique<br />des programmes permettant d'étendre dans un cadre plus générale<br />(vrai concurrence) les avantages d'une approche purement coopérative<br />de l'ordonnancement des threads choisie par plusieurs implémentations<br />de langages basés sur le paradigme réactif.

Le langage d'assignation statique unique, SSA, est l'une des représentations intermédiaires les plus communément utilisées dans les compilateurs industriels. Cependant l'intérêt de la communauté d'analyse statique de programmes est minime, un fait dû aux faibles fondations formelles du langage SSA. Cette thèse présente une sémantique dénotationelle du langage SSA, permettant des définitions formelles des analyses statiques du langage SSA en se basant sur les méthodes classiques de l'interprétation abstraite. D'un point de vue pratique, cette thèse présente l'implémentation des analyseurs statiques définis formellement dans un compilateur industriel, la Collection de Compilateurs GNU, GCC.

L'analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes,...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu'elles représentent des ensembles de données de taille importante ou inconnue, et que l'adressage des données dans ces ensembles est calculé (indexation, indirection). Si la vérification de la validité des accès aux tableaux a été l'une des motivations initiales de l'interprétation abstraite, la recherche de propriétés concernant le contenu des tableaux est quant à lui un sujet récent. La plupart des travaux sur le sujet reposent sur un partitionnement des tableaux. On est ainsi amenés à considérer un certain nombre de fragments de tableau desquels on cherche à trouver des propriétés. Le choix de cette partition est un problème difficile et chacune des méthodes proposées peut être mise en défaut. Par ailleurs, les représentations classiques des partitions de tableau donnent à ces analyses une complexité exponentielle. Nous proposons d'une part de généraliser le concept de partitionnement de tableau à celui de "fragmentation" permettant à la fois le chevauchement des fragments, la manipulation de fragments potentiellement vides et la sélection de relations spécialisées. D'autre part, nous proposons une abstraction de ces fragmentations en terme de graphes appelés "Diagrammes de tranches" ainsi que les opérations pour les manipuler et assurant une complexité polynomiale à l'analyse. Enfin, nous proposons un nouveau critère de fragmentation sémantique inspiré de ceux de la littérature et tentant d'en corriger les défauts. Ces méthodes ont été implémentées dans un analyseur statique. L'expérimentation démontre qu'elles peuvent analyser avec efficacité et précision un certain nombre d'exemples constituant des défis de l'analyse statique de programmes manipulant des tableaux.

L'analyse statique a pour but de vérifier qu'un programme a le comportement souhaité c.à.d. satisfait des propriétés de sûreté. Toutefois, inférer les propriétés vérifiées par un programme est un problème difficile : le théorème de Rice énonce que toute propriété non triviale d'un langage de programmation Turing-complet est indécidable. Afin de contourner cette difficulté, les analyses statiques effectuent des approximations des comportements possibles du programme. La théorie de l'interprétation abstraite permet de donner un cadre formel à ces approximations. Cette théorie, introduite par Cousot & Cousot propose un cadre d'approximation basé sur la notion de treillis, de connexion de Galois et de calculs de points fixes par itération. Ce cadre permet de définir la qualité des approximations effectuées et notamment la notion de meilleure approximation. À l'opposé, les notions quantitatives n'apparaissent pas naturellement dans ce cadre. Nous nous sommes donc posés la question de l'inférence, par analyse statique, de propriétés s'exprimant de manière quantitative (telles que l'utilisation de la mémoire ou le temps d'exécution).

Thèse diffusée initialement dans le cadre d'un projet pilote des Presses de l'Université de Montréal/Centre d'édition numérique UdeM (1997-2008) avec l'autorisation de l'auteur.