Bitbucket is a code hosting site with unlimited public and private repositories. We're also free for small teams!

Close
TyLLVM: Bibliothèque de génération sûre d'assembleur LLVM en OCaml

Résumé:
    TyLLVM est une bibliothèque 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 langage compilant vers le code
            intermédiaire LLVM.
        - Un compilateur compilant de l'assembleur LLVM (code intermédiaire)
            vers du bytecode LLVM.
        - Un back-end assemblant le bytecode LLVM pour une architecture donnée

    La présente bibliothèque permet donc de générer du code intermédiaire LLVM
    à partir de code OCaml. Celui-ci doit présenter un ensemble de fonctions
    générant les différents types et structures possibles en LLVM-IR.

    LLVM inclut déjà un binding de leur API pour générer du LLVM-IR [1].
    Seulement, ce n'est qu'une transcription des fonctions C++ correspondantes,
    qui n'est pas complète et qui peut amener à 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à été faite.

Le Projet:
    LLVM-IR s'articule autour de 2 modules. L'un correspond à proprement parler
    au 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 fonctions et
    la définition de variables globales notamment. L'idée est d'interdire
    à l'utilisateur de l'API de mettre un mauvais linkage sur la déclaration de
    fonctions (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érifiés 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 en tant que paramètres. Il nous aurait fallut un système de type dépendants
    comme celui de Coq pour y parvenir.

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

    LLVM_types:

    Le module LLVM_types contient trois grosses parties :
        - Le sous-module N_star qui modélise l'ensemble N*
            (entiers naturels non-nuls)
        - 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 utiles 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
    vue 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/

Recent activity

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.