Vérification de l’inférence dans les langages fonctionnels

Vérification de l’inférence dans les langages fonctionnels

La vérification de correction de l’inférence peut être intégrée dans le processus de compilation. La solution la plus évidente est alors de compiler un arbre de syntaxe typé vers un langage intermédiaire lui-même typé, et de vérifier un tel langage. Un tel processus a été implémenté pour des langages tels que SML dans les compilateurs TIL ([64]) et CakeML, mais aussi pour la vérification de programmes Haskell dans le compilateur ghc.

Typed Intermediate Languages

Le compilateur TIL [65] est l’une des premières occurrences de compilateur dont l’ensemble de la chaîne de compilation propage les informations de types issues de l’inférence. L’utilisation de représentations intermédiaires typées garantit que toutes les transformations de programmes sont correctes et conservent les types. Ainsi, il est possible d’écrire des passes d’optimisations en s’assurant que celles-ci ne génèreront pas d’erreurs de types à l’exécution, mais également que ces informations de types peuvent orienter les-dites optimisations, qui n’auraient pu être effectuées autrement. De cette manière, il est possible de vérifer l’inférence de types a posteriori, dès la compilation du langage de haut niveau vers le premier langage intermédiaire. Une chaîne de compilation entièrement typée permet également d’assurer une meilleure maintenabilité du code et de ses évolutions. En effet, être capable de typer et vérifier chacune des étapes de compilation rajoute une garantie que toute modification entraînant une erreur de types à l’exécution d’un programme sera rattrapée par l’une des représentations intermédaires. De plus, cela force toute évolution de système de types de surface (SML) à être compilée de manière sûre et à être correctement spécifiée. TIL sera suivi par TIL(T)[16, 15], une évolution du compilateur prenant en compte l’ensemble de SML, apportant notamment des améliorations du langage intermédaire [54] utilisant Système Fω .

TAL : Typed assembly language Un des travaux connexe à TIL est sans aucun doute celui sur Typed Assembly Language [51], une chaîne de compilation transformant un langage basé sur Système F vers un assembleur typé. Ce travail formalise les différentes étapes de transformation d’un lambda-calcul polymorphe vers plusieurs représentations intermédiaires typées, jusqu’à un assembleur RISC lui-même typé. Cette chaîne de compilation comprend une traduction en passage par continuation, une conversion des clotures typée, introduisant des types existentiels pour représenter les variables libres embarquées dans la clôture, et enfin une représentation intermédiaire permettant l’allocation mémoire, avant transformation vers l’assembleur typé.

Haskell : Core et Système FC

Haskell [55] est un langage fonctionnel dit “pur” : il n’est pas possible d’effectuer des effets de bords. Il possède également un mécanisme de polymorphisme ad-hoc [36] (on parlera également de surcharge), autrement dit plusieurs implémentations d’une même fonction pour des types différents. À la compilation, une implémentation est choisie en fonction du type de ses arguments. Un tel mécanisme permet principalement de spécialiser certaines opérations en fonction d’un type donné. A cela s’ajoute un système de kinding, soit une manière de classifier les types et de rendre le langage de types plus expressif. Pour accompagner ceux-ci, le langage possède un système de familles de types, autrement dit des fonctions de types vers types. Enfin, tout comme OCaml, Haskell est capable d’exprimer des types algébriques gardés. L’ensemble de ces constructions rendent alors le système de types et l’inférence assez complexe à mettre en oeuvre et à vérifier. La solution adoptée pour vérifier un tel langage est la compilation vers un langage intermédiaire lui-même typé explicitement, où toutes les égalités de types sont de premier ordre : Système FC. Système FC [62, 46, 67, 66] est une extension de Fω, lui-même une extension de Système F avec classification des types à l’aide d’un système de kinding. FC ajoute dans le langage de kinds un mécanisme d’égalités de types, ainsi qu’un opérateur de coercions. Le langage possède également des types algébriques accompagnés d’une construction pour effectuer du filtrage. Ce langage intermédiaire fait suite à une version de Système F dans lequel sont directement ajoutés les GADTs, langage intermédiaire introduit pour gérer l’ajout de cette construction dans le langage source (Haskell).

MLton 

MLton est un compilateur optimisant pour SML, dont chaque étape de transformation du programme est optimisée. Chacun des langages intermédiaire est lui-même typé, à l’exception de la dernière représentation “Machine”, évidemment proche du langage machine. Après analyse syntaxique, le programme est traduit sous la forme de “CoreML”, une représentation proche de ML dans laquelle les foncteurs et modules ont été éliminés grâce notamment à une passe d’alphaconversion rendant tous les noms uniques, et donc ne nécessitant plus l’utilisation de modules. Une étape de beta-réducation a lieu pour les foncteurs, avant d’être effectivement éliminés comme des modules classiques. Les abréviations de types sont également expansées. CoreML est une représentation intermédiaire dans laquelle les types sont propagés, mais le compilateur n’est pas capable d’en vérifier la cohérence.

Cette représentation intermédiaire est ensuite traduite vers une nouvelle représentation appelée “XML”  , une représentation du programme où tous les nœuds sont annotés, et la quantification explicite : chaque valeur (ou fonction) est annotée avec une liste de variables, celles-ci étant les variables généralisées par la-dite valeur (ou fonction). Réciproquement, les instantiations de types polymorphes sont explicites, et comme nous le verrons plus tard, ont lieu exclusivement au niveau des occurrences de variables. La transformation de CoreML vers XML est principalement utilisée pour la compilation du filtrage de motifs et pour séparer les élements dits dynamiques (les valeurs) des élements statiques (les déclarations de types algébriques) : ceux-ci sont alors tous remontés au début du programme. Cette représentation intermédiaire possède un vérificateur de types qui n’est présent que pour permettre de s’assurer de la correction de la transformation et potentiellement de l’inférence. Celui-ci n’est d’ailleurs pas activé par défaut. Enfin, le programme est ensuite monomorphisé : il s’agit du langage SXML. À ce niveau du programme, chaque valeur polymorphe est dupliquée pour chaque instance à laquelle elle apparaît. La monomorphisation est également appliquée sur l’ensemble des types algébriques. SXML est ensuite tranformé vers une représentation sous forme SSA  , elle-même typée. S’ensuivent un ensemble de transformations jusqu’au langage “Machine” et à l’assembleur. L’étape de vérification du langage intermédiaire XML est proche de l’approche étudiée dans cette thèse : le programme est annoté par un type à chaque nœud, et la vérification s’assure de la cohérence d’un nœud sachant les annotations de ses nœuds fils. Néanmoins, le langage est plus restreint que le TypedTree d’OCaml. Au delà des constructions supplémentaires que compte OCaml, les modules et foncteurs ont déjà été éliminés, les abréviations de types ont été expansées, ce qui réduit alors la complexité du système de types qui doit être mis en oeuvre pour vérifier un tel langage. La différence principale que l’on cherchera à traiter est surtout l’absence de quantifications des variables de types polymorphes et d’instanciations explicites des schémas de types, informations présentes dans le cas de XML. Cette vérification effectuée par MLton permet donc de s’assurer de la correction de l’inférence, mais ne peut être considérée comme une implémentation du système de types de SML, comme l’est un vérificateur de types pour le TypedTree d’OCaml.

Vérification de l’inférence : machine virtuelles typées

Certains langages permettent la compilation vers une machine virtuelle : cela permet une meilleure portabilité des programmes puisque la gestion des différents systèmes est déférée à la machine virtuelle. Pour rendre celles-ci plus robustes, il est possible de leur envoyer un bytecode typé qui sera vérifié avant sont exécution, et ainsi en vérifier sa cohérence. Cela permet entre autres d’envoyer des programmes avec une forme de garantie sans avoir besoin de fournir les sources pour s’assurer que le programme est effectivement bien typé. Java [33] est compilé vers une machine virtuelle : la Java Virtual Machine [43]. Celle-ci effectue de base une étape de vérification de cohérence avant de charger du bytecode, et rejette tout code qui pourrait causer une erreur de types. Stephen Freund [26] présente une formalisation du système de types pour un sous-ensemble de la JVM. Ce système de de types et le vérificateur associé permettent entre autres de s’assurer que des objets sont bien initilialisés avant d’être utilisés, en plus de vérifier la compilation des méthodes dont la compilation peut-être affectée par l’utilisation d’exceptions et donc du gestionnaire d’erreurs. Certains aspects du langage ne sont pas gérés, comme les modificateurs final ou static, la concurrence ou la vérification des packages, le mécanisme d’espaces de noms. La vérification se fait en trois étapes distinctes : la génération du flot de contrôle, l’identification des parties polymorphes du programme et l’inférence de types à l’aide d’une analyse de flots de données. Cette analyse va plus loin que la simple vérification de cohérence, et permet par exemple de vérifier l’utilisation correcte des objets, et permet également d’éliminer des vérifications de pointeurs non nuls à certains endroits du programme. On notera des expérimentations [5] de la compilation de SML vers la machine virtuelle Java, qui donnera lieu par la suite à SML.NET[6], son équivalent pour la machine virtuelle .Net[61]. Ce compilateur pour Standard ML propose un ensemble langages intermédiaires tous typés, permettant alors de garantir que le typage est conservé à chaque transformation.

Table des matières

Introduction
1 Etat de l’art
1.1 Vérification de l’inférence dans les langages fonctionnels
1.1.1 Typed Intermediate Languages
1.1.2 Haskell : Core et Système FC
1.1.3 MLton
1.2 Vérification de l’inférence : machine virtuelles typées
1.3 Programmes avec preuve embarquée
1.4 Programmes en tant que preuves
2 MiniML
2.1 MiniML : définition
2.1.1 Expressions et algèbre de types
2.2 Inférence : génération du TAST
2.3 Représentation Coq
2.4 Règles de vérification de types
2.4.1 Manipulation et vérification de types
2.4.2 Environnement
2.4.3 Vérification d’expressions annotées
2.4.4 Implémentation d’un vérificateur de types de MiniML
2.5 Sémantique opérationelle du TAST
2.5.1 Représentation Coq de la sémantique de MiniML
2.5.2 Implémentation d’un évaluateur en OCaml
2.6 État des lieux de la vérification de types de TAST
3 Définition du Typedtree, l’arbre annoté d’OCaml
3.1 Définitions internes du compilateur
3.2 Algèbre de types
3.3 Typedtree : expressions
3.4 Typedtree : modules, structures et signatures
3.4.1 Signatures et types de modules
3.4.2 Syntaxe des types de modules
3.5 Environnements
3.6 Moteur d’inférence de types
3.6.1 Niveaux
4 Implémentation d’un vérificateur de types pour OCaml
4.1 Environnements
4.2 Comparaison et vérification de types
4.2.1 Équivalence de types
4.2.2 Instanciation de types
4.2.3 Vérification de bonne formation/construction
4.2.4 Filtrage de types
4.2.5 Vérification d’équations de types
4.3 Algorithme de vérification des expressions
4.3.1 ML
4.3.2 Généralisation et restriction souple de valeurs
4.3.3 Types algébriques gardés
4.3.4 Extensions
4.4 Résultats et limitations
4.4.1 Exemples d’erreurs de l’inférence
5 Sémantique opérationnelle du Typedtree
5.1 Sémantique du noyau ML d’OCaml
5.2 Filtrage, n-uplets et constructeurs de données
5.3 Enregistrements
5.4 Récursion
5.5 Extensions impératives
5.6 Exceptions
5.7 Evaluation paresseuse
Conclusion

Télécharger le rapport complet