charon

Patinir, E., 1515-1524, paysage avec charon traversant le styx [huile sur bois]. Museo del Prado, Madrid. Source

Charon

Charon agit comme une interface entre le compilateur RustC et les projets de vérification du programme. Son objectif est de traiter les caisses de rouille et de les convertir en fichiers faciles à gérer par les vérificateurs de programme. Il est implémenté en tant que pilote personnalisé pour le compilateur RustC.

Charon est, dans la mythologie grecque, un vieil homme portant les âmes du défunt Accroffs the Styx, une rivière séparant le monde des vivants du monde des morts. Dans le contexte actuel, Charon nous permet de passer du monde des programmes de rouille au monde de la vérification formelle.

Nous sommes ouverts aux contributions ! Veuillez nous contacter afin que nous puissions nous coordonner, si vous êtes prêt à contribuer. À cette fin, vous pouvez rejoindre le Zulip.

LLBC

Charon convertit le code MIR en ULLBC (calcul d'emprunt de bas niveau non structuré) puis à LLBC. Les deux AST peuvent être sortis par Charon.

ULLBC est un MIR légèrement simplifié, où nous essayons de supprimer autant de redondances que possible. Par exemple, nous simplifions considérablement la représentation des constantes provenant du compilateur de rouille.

LLBC est ULLBC où nous avons restructuré le flux de contrôle avec des boucles, if ... then ... else ... , etc. au lieu de gotos. Par conséquent, nous fusions les instructions MIR et les terminateurs en un seul type d'instruction LLBC. Nous effectuons également des modifications supplémentaires, dont certaines sont répertoriées ci-dessous:

Remarque : La plupart des transformations qui transforment le MIR en ULLBC puis LLBC sont implémentées au moyen de micro-passes. Selon le besoin, nous pourrions les rendre facultatifs et les contrôler avec des drapeaux. Si vous voulez en savoir plus sur les détails, voir translate dans src/driver.rs , qui applique les micro-passes l'un après l'autre.

Remarque : Si vous voulez connaître tous les détails de (u) LLBC, jetez un œil: types.rs , values.rs , expressions.rs , ullbc_ast.rs et llbc_ast.rs .

L'AST extrait est sérialisé dans les fichiers .ullbc et .llbc (en utilisant le format JSON). Nous extrons une caisse entière dans un seul fichier.

Structure du projet

• charon : la mise en œuvre de la rouille.
• charon-ml : La bibliothèque ML. Fournit des services publics pour récupérer et manipuler l'AST dans l'OCAML (désérialisation, impression, etc.).
• tests et tests-polonius : Test Files répertoires. tests-polonius contient du code qui nécessite le vérificateur de Polonius.

Installation et construction

Vous devez d'abord installer rustup .

Comme Charon est configuré avec la cargaison, Rustup téléchargera et installera automatiquement les packages appropriés lors de la construction du projet. Si vous voulez seulement construire le projet Rust (dans ./charon ), exécutez simplement make build-charon-rust dans le répertoire supérieur.

Si vous souhaitez également construire la bibliothèque ML (dans ./charon-ml ), vous devrez installer OCAML et les dépendances appropriées.

Nous vous suggérons de suivre ces instructions et d'installer OPAM sur le chemin (mêmes instructions).

Pour Charon-ML, nous utilisons OCAML 4.13.1 : opam switch create 4.13.1+options

Les dépendances peuvent être installées avec la commande suivante:

 opam install ppx_deriving visitors easy_logging zarith yojson core_unix odoc menhir unionFind

Vous pouvez ensuite exécuter make build-charon-ml pour construire la bibliothèque ML, ou même simplement make pour construire l'ensemble du projet (Rust et OCAML). Enfin, vous pouvez exécuter les tests avec make test .

Alternativement, vous pouvez utiliser Nix et faire nix develop (ou utiliser https://direnv.net/ et direnv allow ) et toutes les dépendances doivent être rendues disponibles.

Documentation

Vous pouvez accéder à la documentation de la rouille en ligne.

Vous pouvez également exécuter make pour générer la documentation localement. Il générera une documentation accessible à partir de doc-rust.html (pour le projet Rust) et doc-ml.html (pour la bibliothèque ML).

Usage

Pour exécuter Charon, vous devriez exécuter le Binaron Charon à partir de la caisse que vous souhaitez compiler, comme si vous vouliez construire la caisse avec cargo build . L'exécutable Charon est situé à bin/charon .

Charon construira la caisse et ses dépendances, puis extraire l'AST. Charon fournit diverses options et drapeaux pour modifier son comportement: vous pouvez afficher une documentation détaillée avec --help . En particulier, vous pouvez imprimer le LLBC généré par Charon avec --print-llbc .

S'il y a un fichier Charon.toml à la racine de votre projet, Charon en tirera également des options. Le fichier prend en charge les mêmes options à l'interface CLI, à l'exception des options liées à l'entrée / sortie comme --print-llbc . Exemple Charon.toml :

[ charon ]
extract_opaque_bodies = true
[ rustc ]
flags = [ " --cfg " , " abc " ]

Remarque : Parce que Charon est compilé avec Rust Nigthly (c'est une exigence pour mettre en œuvre un pilote Rustc), il construira votre caisse avec Rust Nightly. Vous pouvez trouver la version nocturne épinglée pour Charon dans rust-toolchain.template .