Source

TyLLVM / README

TyLLVM: Librairie de génération sûre d'assembleur LLVM en OCaml

Résumé:
    TyLLVM est une librairie OCaml permettant de générer de
    l'assembleur LLVM qui respecte au possible les spécifications du
    langage grâce au système types d'OCaml.

Introduction:
    LLVM est une infrastructure de compilateur ayant l'architecture suivante:
        - Le front-end spécifique à chaque langages compilant vers le code
            intermédiaire LLVM.
        - Un compilateur compilant de l'assembleur LLVM (code intermédiaire)
            vers du bytecode LLVM.
        - Un back-end transformant depuis le bytecode LLVM vers une
            architecture donnée

    La présente librairie permet donc de générer du code intermédiaire LLVM
    à partir de code OCaml. Il doit pour cela présenter un ensemble de fonctions
    générant les différents type et structures possible en LLVM-IR.

    LLVM inclue déjà un binding de leur API pour générer du LLVM-IR [1].
    Seulement, ce n'est qu'un bind des fonctions C++ correspondant qui est
    non complet et pouvant occasionner des « segmentation fault ».

    La vraie différence de TyLLVM avec ce binding, en plus de pallier à ces
    problèmes mentionnés précédemment, est qu'il propose un moyen d'éviter un
    certain nombre d'erreurs grâce au système de types d'OCaml.

    Le projet s'inspire de projets telle que TyXML [3] ou MaCaQue [4].
    On s'articule donc autour de la puissance du système de type d'OCaml
    (typage, variant polymorphes, GADT) pour pouvoir générer du code LLVM-IR
    dont une analyse statique aura déjà était faite.

Le Projet:
    LLVM-IR s'articule autour de 2 modules. L'un correspond à proprement parler
    du code LLVM-IR tandis que l'autre offre une abstraction aux données associées
    à leurs types. En combinant les deux, on parvient à déceler des erreurs de
    types basiques.

    LLVM:

    Le module LLVM s'organise sur 3 niveau. Une implémentation semblable en Coq [2]
    valide cette prise de position. Il s'agit, au premier niveau, de pouvoir
    définir des variables globales ou des fonctions mais aussi de pouvoir
    déclarer des fonctions externes. Le deuxième niveau correspond à la définition
    des labels et de l'instruction `ret` qui est très spécifique. Enfin, le
    troisième niveau correspond au code proprement parlé à l'aide d'un arbre
    d'instruction qui n'est pas uniforme dans le typage.

    C'est ensuite en utilisant la structure des listes qui permet de compléter le
    code comme c'est déjà le cas dans TyXML. Ensuite, à l'aide d'un ensemble de
    fonctions internes au module, nous générons sur la sortie standard du code
    LLVM-IR.

    Certains points peuvent être notés comme l'utilisation dans certaines
    situations des variants polymorphes afin d'étayer le système de type sur
    les différents attributs que peuvent prendre la déclaration de fonction et
    la définition de variable global notamment. L'idée est d'interdire
    l'utilisateur de l'API de pouvoir mettre un mauvais linkage sur la
    déclaration de fonction (ce qui aurait été possible dans le système de sous
    typage d'OCaml).

    Même si nous avons réussi à faire respecter certaines règles de façon statique
    dans la génération du code LLVM-IR, il reste tout de même des points qui ne
    peuvent être vérifier sans un système plus fort que celui d'OCaml. En effet,
    on peut parler de l'attribut `asign` qui ne peut prendre que des puissances de
    2 entant que paramètres. Il nous aurait fallut un système de type de dépendant
    comme celui de Coq pour y parvenir.

    D'autres situations plus difficiles à contextualiser montrent aussi les
    limites du système de typage de l'OCaml mais même si c'est le cas, il faut
    aussi accorder une certaines confiance à l'utilisateur.

    LLVM_types:

    Le module LLVM_types contient trois grosse parties:
        - Le sous-module N_star qui modèlise l'ensemble N*
            (entier naturel non-nulle)
        - Le type t qui modèlise un type de LLVM-IR
        - Le type value qui modèlise un type et sa valeur
    Les GADT se révèlent ici très utile pour créer les types N_star.t
    et le type f (servant à modéliser le type des fonctions).

Le résultat:
    Même si nous avions certains problèmes lors de l'implémentation de TyLLVM,
    l'objectif est clairement de pouvoir donner une API plus stable et se
    rapprochant le plus possible de la philosophie de l'OCaml.

    Ainsi, nous avons essayé de générer comme point de départ un simple code
    de LLVM-IR qui affiche un « Hello World ! » afin de valider notre point de
    vu sur la génération d'un code LLVM-IR en OCaml.

    L'approche TyXML peut être critiquable (en prenant en comparaison la
    sémantique du XML et de LLVM-IR), néanmoins si nous arrivons à des
    résultats, c'est que ce style d'implémentation est tout à fait possible.

Références:
    [1]: https://llvm.org/viewvc/llvm-project/llvm/trunk/bindings/ocaml/llvm/llvm.mli?view=markup
    [2]: https://github.com/coq-ext-lib/coq-compile/blob/master/src/coq/LLVM.v
    [3]: https://ocsigen.org/tyxml/
    [4]: https://forge.ocamlcore.org/projects/macaque/
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.