Th. doct.-ing.--Inform.--Toulouse--I.N.P., 1984. N°: 353.

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.

Le modèle OFL (Open Flexible Languages) décrit et réifie le comportement des langages à objets à classes courants tels Java, C++ ou Eiffel et permet de modifier, d'adapter, ce comportement. Dans cette optique, les notions de classe --- généralisée sous le nom de "description" --- et de "relation entre descriptions" sont réifiées. Chaque langage est décrit sous la forme d'un ensemble de composants formé de types de description et de types de relation. Pour définir chaque composant, le méta-programmeur doit donner une valeur à un ensemble de paramètres qui décrivent la sémantique opérationnelle du composant. Par exemple, pour définir une nouvelle relation, il devra répondre aux questions : La relation définit-elle une utilisation ou une importation ? La relation permet-elle le polymorphisme ? Si oui, dans quel(s) sens ? Quelle est sa cardinalité maximale ? Peut-elle être circulaire, répétée ? Possède-t-elle une relation inverse ? Une fois ces types de description et de relation définis par le méta-programmeur, le programmeur est en mesure d'en faire usage pour la réalisation de son application. Le but du modèle OFL est d'aider à améliorer la qualité du code produit en donnant plus d'information et donc de précision sur les relations entre descriptions. Nous souhaitons de cette manière favoriser l'évolution et la maintenabilité des applications par l'intermédiaire d'une meilleure spécification, d'une documentation plus explicite, de contrôles automatiques plus pertinents, ... Il s'agit également d'offrir une plus grande souplesse au programmeur en lui permettant, par une phase de paramétrage ou de méta-programmation, de mieux adapter son langage de programmation de prédilection à ses besoins. L'objectif de cette thèse est de définir le modèle OFL et d'en présenter des exemples d'application.

Thèse de doctorat : Informatique : Nancy 1 : 2001. / Thèse : 2001NAN10123. Titre provenant de l'écran-titre.

Les systèmes embarqués sont largement utilisés de nos jours. Pour des raisons d'efficacité, les plus contraints en termes de ressources sont toujours programmés en C et en assembleur. L'adoption de langages de plus haut niveau tels que C# ou Java offrirait plus d'abstraction au programmeur, ce qui réduirait les temps de développement et par conséquent le coût de ces systèmes. Certains d'entre eux ont déjà migré vers de tels langages, comme les téléphones mobiles ou les tablettes tactiles, mais ils sont équipés d'une grande quantité de mémoire externe et ne reflètent pas la majorité des systèmes embarqués.Cette thèse s'intéresse à l'implémentation de Java et .NET pour l'embarqué, et plus spécifiquement à la compilation efficace du polymorphisme. Ce polymorphisme génère un certain coût à l'exécution, comme des indirections dans le cas des appels de méthodes (polymorphisme d'inclusion), ou de la duplication de code dans le cas de la généricité (polymorphisme paramétrique). De nombreuses techniques d'implémentation ont été proposées, notamment pour Java. Il reste cependant à identifier lesquelles sont applicables pour le type de systèmes que nous ciblons, et à en concevoir de nouvelles pour certains aspects comme la généricité. Nous partons du principe que les techniques globales (hypothèse du monde clos) sont les mieux adaptées. Par l'analyse de types, nous détectons qu'une partie importante des programmes est monomorphe et qu'elle peut donc être compilée sans surcoût. Pour implémenter le polymorphisme restant, nous choisissons la technique la mieux adaptée au matériel cible. Nous proposons également une implémentation de la généricité qui est adaptée aux systèmes embarqués. D'après nos évaluations, l'impact négatif du polymorphisme sur l'efficacité est largement réduit. L'efficacité du code optimisé devrait s'approcher de celle du C, et les techniques que nous employons pourraient être applicables dans le contexte plus général du chargement dynamique. / Nowadays, embedded systems are ubiquitous. For efficiency reasons, most constrained systems are still programmed in C and assembly. Adopting higher-level languages such as C# or Java should enhance the level of abstraction offered to programmers and reduce development time and cost for these systems. A small part of them have migrated to such languages, like smartphones and tablet computers, but they have a large amount of external memory available and do not represent the majority of embedded systems.This thesis focuses on the implementation of Java and .NET for embedded systems, and more especially on the efficient compilation of polymorphism. Polymorphism generates an overhead at run-time, such as indirections when methods are invoked (inclusion polymorphism) or code duplication in the case of generics (parametric polymorphism). Many implementation techniques have been proposed, especially for Java. However, it remains to identify which ones are applicable in the context of low-end embedded systems. We consider that whole program optimization (closed-world assumption) is well-suited in this context. Using type analysis, we observe that most part of programs is monomorph, therefore it can be compiled with no overhead with respect to C. In order to implement the remaining polymorphism, we choose the technique which is better suited for the target hardware. We also propose an appropriate implementation of run-time generics. Our results show that the negative impact of polymorphism is mostly reduced. The efficiency of the optimized code should be comparable with C, and the techniques we employ could be applicable in the context of dynamic loading (open-world assumption).

C++ est un des langages de programmation les plus utilisés en pratique, y compris pour le logiciel embarqué critique. C'est pourquoi la vérication de programmes écrits en C++ devient intéressante, en particulier via l'utilisation de méthodes formelles. Pour cela, il est nécessaire de se fonder sur une sémantique formelle de C++. De plus, une telle sémantique formelle peut être validée en la prenant comme base pour la spécication et la preuve d'un compilateur C++ réaliste, afin d'établir la confiance dans les techniques usuelles des compilateurs C++. Dans cette thèse, nous nous focalisons sur le modèle objet de C++. Nous proposons une sémantique formelle de l'héritage multiple en C++ comprenant les structures imbriquées à la C, sur laquelle s'appuie notre étude de la représentation concrète des objets avec optimisations des bases vides, à travers des conditions suffisantes que nous prouvons correctes vis-à-vis des accès aux champs et des opérations polymorphes. Puis nous spécifions un algorithme de représentation en mémoire fondé sur l'ABI pour Itanium, et une extension de cet algorithme avec optimisations des champs vides, et nous prouvons qu'ils satisfont nos conditions. Nous obtenons alors un compilateur vérifié et réaliste d'un sous-ensemble de C++ vers un langage à trois adresses et accès mémoire de bas niveau. Rajoutant à notre sémantique la construction et la destruction d'objets, nous étudions leurs interactions avec l'héritage multiple. Cela nous permet de formaliser la gestion de ressources, notamment le principe RAII (resource acquisition is initialization) via l'ordre de construction et destruction des sous-objets. Nous étudions aussi les effets sur les opérations polymorphes telles que la sélection de fonction virtuelle pendant la construction et la destruction, en généralisant la notion de type dynamique. Nous obtenons alors un compilateur vérifié pour notre sémantique étendue, notamment en prouvant la correction de l'implémentation des changements de types dynamiques. Toutes nos spécifications et preuves sont formalisées en Coq.