Cette thèse présente une extension du compilateur CompCert permettant de fournir des garanties formelles de préservation sémantique à des programmes auxquels CompCert n'en donne pas. CompCert est un compilateur pour le langage C vers différentes architectures qui fournit, en plus d'un exécutable compilé, des garanties formelles concernant le comportement du programme assembleur généré. En particulier, tout programme C ayant une sémantique définie selon le standard C est compilé en un programme assembleur équivalent, c'est-à-dire qui a la même sémantique. En revanche, ce théorème n'assure aucune garantie lorsque le programme source n'a pas de sémantique définie : on parle en C de comportement indéfini. Toutefois, des programmes C issus de réels projets largement utilisés contiennent des comportements indéfinis. Cette thèse détaille dans un premier temps un certain nombre d'exemples de programmes C qui déclenchent des comportements indéfinis. Nous argumentons que ces programmes devraient tout de même bénéficier du théorème de préservation sémantique de CompCert, d'abord parce qu'ils apparaissent dans de vrais projets et parce que leur utilisation des comportements indéfinis semble légitime. Dans ce but, nous proposons d'abord un modèle mémoire pour CompCert qui définit l'arithmétique arbitraire de pointeurs et la manipulation de données non initialisées, à l'aide d'un formalisme de valeurs symboliques qui capturent la sémantique d'opérations non définies dans le standard. Nous adaptons l'intégralité du modèle mémoire de CompCert avec ces valeurs symboliques, puis nous adaptons les sémantiques formelles de chacun des langages intermédiaires de CompCert. Nous montrons que ces sémantiques symboliques sont un raffinement des sémantiques existantes dans CompCert, et nous montrons par ailleurs que ces sémantiques capturent effectivement le comportement des programmes sus-cités. Enfin, afin d'obtenir des garanties similaires à celles que CompCert fournit, nous devons adapter les preuves de préservation sémantique à notre nouveau modèle. Pour ce faire, nous généralisons d'importantes techniques de preuves comme les injections mémoire, ce qui nous permet de transporter les preuves de CompCert sur nos nouvelles sémantiques. Nous obtenons ainsi un théorème de préservation sémantique qui traite plus de programmes C. / This thesis presents an extension of the CompCert compiler that aims at providing formal guarantees about the compilation of more programs than CompCert does. The CompCert compiler compiles C code into assembly code for various architectures and provides formal guarantees about the behaviour of the compiled assembly program. It states that whenever the C program has a defined semantics, the generated assembly program behaves similarly. However, the theorem does not provide any guarantee when the source program has undefined semantics, or, in C parlance, when it exhibits undefined behaviour, even though those behaviours actually happen in real-world code. This thesis exhibits a number of C idioms, that occur in real-life code and whose behaviour is undefined according to the C standard. Because they happen in real programs, our goal is to enhance the CompCert verified compiler so that it also provides formal guarantees for those programs. To that end, we propose a memory model for CompCert that makes pointer arithmetic and uninitialised data manipulation defined, introducing a notion of symbolic values that capture the meaning of otherwise undefined idioms. We adapt the whole memory model of CompCert with this new formalism and adapt the semantics of all the intermediate languages. We prove that our enhanced semantics subsumes that of CompCert. Moreover, we show that these symbolic semantics capture the behaviour of the previously undefined C idioms. The proof of semantic preservation from CompCert needs to be reworked to cope with our model. We therefore generalize important proof techniques such as memory injections, which enable us to port the whole proof of CompCert to our new memory model, therefore providing formal guarantees for more programs.

La chanson québécoise actuelle paraît réconcilier la chanson dite «à texte» et la chanson populaire, comme ce fut le cas pour la chanson engagée des années 1970. Si le thème de l’engagement soutenait plusieurs œuvres chansonnières de cette décennie, celui de la mélancolie semble pouvoir définir une certaine tendance actuelle. Ce mémoire s’intéresse au thème de la mélancolie dans la chanson québécoise contemporaine et plus précisément dans les albums Tu m’intimides de Mara Tremblay, La forêt des mal-aimés de Pierre Lapointe et À Paradis City de Jean Leloup. À la fois auteurs, compositeurs et interprètes, ces trois artistes s’inscrivent dans le champ populaire de la chanson québécoise en créant des œuvres où le texte et la musique mettent la mélancolie en valeur. Dans cette étude, la mélancolie est étudiée en fonction de trois aspects, soit l’être mélancolique, la temporalité mélancolique et l’espace mélancolique. C’est à travers l’exploration de ces trois aspects que sont analysées les chansons du corpus, surtout à partir des textes, mais en considérant aussi certains éléments musicaux.

L'utilisation des méthodes formelles est de plus en plus courante dans le développement logiciel, et les systèmes de types sont la méthode formelle qui a le plus de succès. L'avancement des méthodes formelles présente de nouveaux défis, ainsi que de nouvelles opportunités. L'un des défis est d'assurer qu'un compilateur préserve la sémantique des programmes, de sorte que les propriétés que l'on garantit à propos de son code source s'appliquent également au code exécutable. Cette thèse présente un compilateur qui traduit un langage fonctionnel d'ordre supérieur avec polymorphisme vers un langage assembleur typé, dont la propriété principale est que la préservation des types est vérifiée de manière automatisée, à l'aide d'annotations de types sur le code du compilateur. Notre compilateur implante les transformations de code essentielles pour un langage fonctionnel d'ordre supérieur, nommément une conversion CPS, une conversion des fermetures et une génération de code. Nous présentons les détails des représentation fortement typées des langages intermédiaires, et les contraintes qu'elles imposent sur l'implantation des transformations de code. Notre objectif est de garantir la préservation des types avec un minimum d'annotations, et sans compromettre les qualités générales de modularité et de lisibilité du code du compilateur. Cet objectif est atteint en grande partie dans le traitement des fonctionnalités de base du langage (les «types simples»), contrairement au traitement du polymorphisme qui demande encore un travail substantiel pour satisfaire la vérification de type. / Formal methods are rapidly improving and gaining ground in software. Type systems are the most successful and popular formal method used to develop software. As the technology of type systems progresses, new needs and new opportunities appear. One of those needs is to ensure the faithfulness of the translation from source code to machine code, so that the properties you prove about the code you write also apply to the code you run. This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler's code. Our compiler implements the essential code transformations for a higher-order functional language, namely a CPS conversion and closure conversion as well as a code generation. The thesis presents the details of the strongly typed intermediate representations and the constraints they set on the implementation of code transformations. Our goal is to guarantee type preservation with a minimum of type annotations, and without compromising readability and modularity of the code. This goal is already a reality for simple types, and we discuss the problems remaining for polymorphism, which still requires substantial extra work to satisfy the type checker.

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage. / In computer science, structures with variable binders are very common. Program- ming languages and logical frameworks are examples of structures with binders. Thus writing programs that deal with these kinds of data benefits with explicit support for data binding. The Beluga programming environment is an example of such a system. In this work we develop and present a compiler for the system. Many of the programs that Beluga is specially well suited for writing can benefit from a compiler. For example, some of the kinds programs that would benefit more are type-checkers, compilers and interpreters that take advantage of the binder support and dependent types present in the language, and also require a reasonably fast run-time. Our goal in this work, is to present a compiler for the Beluga system, that uses a very versatile internal representation that helps with the development of the system, and allows a sharing of code between several back-ends. Furthermore, we present a way of compiling the uniquely powerful pattern language supported by Beluga.

Les systèmes critiques, parmi lesquels les systèmes embarqués construits autour d'un microprocesseur mono-cœur exécutant un logiciel d'application, ne sont pas à l'abri d'interférences naturelles ou malveillantes qui peuvent provoquer des fautes transitoires. Cette thèse porte sur des protections qui peuvent être implantées pour détecter les effets de telles fautes transitoires sans faire d'hypothèses sur la multiplicité des erreurs générées. De plus, ces erreurs peuvent être soit des erreurs de flot de contrôle soit des erreurs sur les données. Une nouvelle méthode de vérification de flot de contrôle est tout d'abord proposée. Elle permet de vérifier, sans modifier le système initial, que les instructions du programme d'application sont lues sans erreur et dans le bon ordre. Les erreurs sur les données sont également prises en compte par une extension de la vérification de flot de contrôle. La méthode proposée offre un bon compromis entre les différents surcoûts, le temps de latence de détection et la couverture des erreurs. Les surcoûts peuvent aussi être ajustés aux besoins de l'application. La méthode est mise en œuvre sur un prototype, construit autour d'un microprocesseur Sparc v8. Les fonctions d'analyse de criticité développées dans le cadre de la méthodologie proposée sont également utilisées pour évaluer l'impact des options de compilation sur la robustesse intrinsèque du logiciel d'application. / Critical systems, including embedded systems built around a single core microprocessor running a software application, can be the target of natural or malicious interferences that may cause transient faults. This work focuses on protections that can be implemented to detect the effects of such transient faults without any assumption about the multiplicity of generated errors. In addition, those errors can be either control flow errors or data errors. A new control flow checking method is first proposed. It monitors, without modifying the original system, that the instructions of the microprocessor application program are read without error and in the proper order. Data errors are also taken into account by an extension of the control flow checking. The proposed method offers a good compromise between overheads, latency detection and errors coverage. Trade-offs can also be tuned according to the application constraints. The methodology is demonstrated on a prototype built around a Sparc v8 microprocessor. Criticality evaluation functions developed in the frame of the proposed methodology are also used to evaluate the impact of compilation options on the intrinsic robustness of the application software.

La compilation en informatique est abordée par la littérature dans ses aspects techniques, et non sous la forme d’un concept à part entière. Si l’on regarde plus précisément les transformations effectuées par un compilateur, ce dernier synthétise un ensemble de définitions en une seule unité appelée « programme », en fonction des propriétés mêmes associées à ces définitions et indépendamment du compilateur lui-même. La notion de compilation peut ainsi être pensée pour elle-même indépendamment du langage ou des représentations de haut niveau et du modèle de machine cible. Les transformations d’arbres doublement orientés, appelés treilles, et non plus celles des arbres de la théorie des graphes qui sont simplement orientés, caractérisent le noyau dur de la compilation. Une structure algébrique, appelée T[Σ]-algèbre, isomorphe aux transformations de treilles, permet de formaliser ces transformations directement à partir des notions de sorte et d’opérateur et non plus à partir de celle de terme. Des rapports entre cette structure algébrique (J.-P. Desclés, 1980) et l’algèbre de combinateurs (H. Curry, 1958) sont établis à partir des treilles, indépendamment de tout support technique. En s’appuyant sur une dualité entre opérateur et opération, ce concept de compilation ainsi formalisé, permet d’éclairer sous un angle nouveau les rapports entre interprétation et syntaxe, logiciel et matériel, pensée et cerveau. En traversant les domaines de la chimie, de la biologie et de la linguistique, la compilation dès lors généralisée, offre un cadre formel opératoire et explicatif en sciences cognitives, exprimé par la formule de J. Ladrière : « l’esprit est adhérent à la matière ». / Compilation in computer science is more often introduced by its technical side rather than in terms of a notion as a whole. If we look more precisely at the transformations performed by a compiler, it synthetizes a set of definitions in a single unit called “program”, using properties of the definitions themselves and independently of the compiler itself. Thus, compilation may be though by itself, independently of high level representations or formal languages and of targeted computers. Bi-ordered tree transformations, called treille (in French) form the core of compilers that we distinguish from simply ordered trees of the graph theory. An algebraic structure, called T[Σ]-algebra, which is isomorphic to treille transformations, build the formalism with sorts and operators, instead of terms algebra. Relationships between this algebraic structure (J.-P. Desclés, 1980) and the algebra of combinators (H. Curry, 1958) are established thanks to the formalism of treille, independently of any technical architecture. Relying on a duality between operator and operation, this concept of compilation thereby formalized, allows shedding light on the relationship between interpretation and syntax, software and hardware, thought and brain. Through the various fields of chemistry, biology and computational linguistic, general compilation gives an explanatory and operational formal framework for cognitive science, that J. Ladrière expressed by “Mind adheres to material”.

La plupart des processus informatiques mettent en jeu la notion de transformation, en particulier la compilation. Nous nous intéressons dans cette thèse à fournir des outils et des méthodes, utilisant la réécriture, permettant d'accroître la confiance que l'on peut placer dans ces processus. Nous développons dans un premier temps un cadre permettant de valider la compilation de constructions de filtrage, produisant une preuve formelle de la validité de la compilation, ainsi qu'un témoin de cette preuve, à chaque exécution du compilateur. Afin de permettre l'écriture sûre de transformations complexes, nous proposons un générateur de structures de données efficaces intégrant des invariants algébriques, et un langage de stratégies permettant de contrôler l'application des transformations. Ces résultats constituent donc une avancée vers la constitution de methodes génériques sûres pour le développement de transformations de confiance. / Most computer processes involve the notion of transformation, in particular the compilation processes. We interest in this thesis in providing tools and methods, based on rewriting, giving the opportunity to increase the confidence we can place into those processes. We develop first a framework used to validate the compilation of matching constructs, building a formal proof of the validity of the compilation process along with a witness of this proof, for each run of the compiler. Then, in order to allow one to write safely complex transformations, we propose a tool that generates an efficient data structure integrating algebraic invariants, as well as a strategy language that enables to control the application of transformations. Those results can be seen as a first step towards the constitution of generic and safe methods for the development of trustworthy transformations.

Cette thèse traite de la compilation efficace des langages à objets en héritage multiple. La programmation objet est caractérisée par un mécanisme fondamental, emph{la liaison tardive} --- la méthode appelée dépend du type dynamique d'un paramètre distingué, le emph{receveur}. L'efficacité de ce mécanisme nécessite une implémentation adéquate qui est conditionnée par le schéma de compilation utilisé --- compilation séparée avec chargement dynamique, compilation globale, etc. Cependant la programmation par objets présente une apparente incompatibilité entre trois termes : l'héritage multiple, l'efficacité et l'owa --- en particulier, le chargement dynamique. Nous avons étudié les techniques d'implémentation compatibles avec l'héritage multiple couramment utilisées ainsi qu'une alternative prometteuse, le ph. Nous nous plaçons dans le cadre du typage statique, donc nos conclusions peuvent valoir pour des langages comme cpp, eiffel, java, csharp, etc. Différents schémas de compilation sont considérés, de l'owa à l'cwa. Ces techniques et ces schémas ont été mis en uvre dans le compilateur auto-gène du langage prm. L'influence sur l'efficacité de tous ces éléments a été testée dans un protocole expérimental rigoureux de méta-compilation et les tests ont été réalisés sur une variété de processeurs différents. Les résultats des ces expérimentations sont discutés et comparés aux évaluations a priori effectuées sur les techniques d'implémentation. Ils confirment aussi que le ph est une technique d'implémentation intéressante pour le sous-typage multiple à la java. / His thesis is about efficient compilation of object oriented language with multiple inheritance.Object oriented programing is characterized by a main mechanism, emph{late binding} --- invoked method only depends on the dynamic type of one special parameter, the emph{receiver}.In order to be efficient this mechanism needs an implementation which depends on some compilation scheme --- separate compilation with dynamic loading, global compilation, etc.However object oriented programming present akin of incompatibility between three terms: multiple inheritance, efficiency and open world assumption --- especially with dynamic loading.In this thesis, we have studied common implementation techniques compatible with multiple inheritance and a promising alternative, perfect class hashing.The context of this study is static typing, our conclusion holds for languages like cpp, eiffel, java, csharp, etc.Different compilation schemes are considered, from open world assumption to closed world assumption.These techniques and schemes are implemented in the prm bootstraped compiler.Efficiency influence of all this artifacts has been tested with a rigorous meta-compilation experimental protocol and these tests have been performed on a variety of different processors.Results of these experiments are discuss and compared to an a priori evaluations of implementations techniquesThey mainly confirm perfect class hashing as an interesting implementation for multiple subtyping, a la java.

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).

La compilation traditionnelle est confrontée à de nombreux défis face aux besoins d'optimisations de programmes pour architectures parallèles. Un défi particulier est la conception de langages et représentations intermédiaires (RIs) appropriés.Bien que différentes RIs aient été proposées pour repousser les limites de la compilation traditionnelle, la plupart ne sont toujours pas adaptées pour appliquer des transformations de programmes pertinentes.Différentes alternatives sont donc de plus en plus exploitées, telles que l'autotuning ou la compilation interactive. Ces dernières nécessitent l'usage de langages intermédiaires fondamentalement différents, par exemple, les méta-langages pour la transformation de programmes. Dans cette thèse, centrée sur les besoins en applications numériques, nous étudions ce type de meta-langages; nous adressons particulièrement quatre questions:(i) Comment introduire une expressivité spécifique à un domaine?(ii) Comment repenser leur conception pour améliorer leur flexibilité dans la composition de transformations et la génération de plusieurs variantes de programme?(iii) Jusqu'où pouvons-nous introduire du support pour le NUMA (Non-Uniform Memory Access)?(iv) En tant que nouvelle classe de méta-langages, comment formaliser leur sémantique? Nous répondons à ces questions au travers de la conception et la sémantique de TeML, un méta-langage pour l'optimisation d'applications tensorielles. / Traditional compilation faces numerous challenges with program optimizations for parallel architectures. A particular challenge is the design of proper intermediate languages and representations to enable the application of relevant optimization techniques.Various parallel intermediate representations and languages have been proposed.To overcome this issue, different alternatives are more and more exploitedsuch as empirical autotuning or interactive compilation. Such alernatives require fondamentally different typesof intermediates languages such as transformation meta-languages. In this thesis, we study transformation meta-languages for numerical applications: wa particularly address four questions:(i) How do we introduce domain-specific expressiveness?(ii) How do we rethink their design to enhance their flexibility in composing optimizations paths and generating multiple program variants?(iii) How far can we introduce NUMA (Non-Uniform Memory Access) awareness?(iv) As a new class of meta-languages, how do we formalize their semantics? We answer these questions through the design and semantics of TeML, a tensor optimizations meta-language.