sturdy

La version Haskell de Sturdy n'est plus maintenue. Le projet robuste a été réimplémenté à Scala et est disponible sur https://gitlab.rlp.net/plmz/sturdy.scala.

Robuste

Sturdy est une bibliothèque pour créer des analyses statiques sonores dans Haskell. Les analyses statiques sont des outils qui produisent des informations sur les programmes informatiques sans exécuter réellement le programme. Des exemples d'analyses statiques sont les vérificateurs de type, les chercheurs de bogues (par exemple Java Findbugs), les analyses pour la sécurité (par exemple, les analyses de souillure) et les analyses qui sont utilisées pour les optimisations du compilateur.

Ce projet se concentre sur des analyses statiques sonores . Une analyse statique est solide si les résultats de l'analyse reflètent le comportement d'exécution réel du programme et que les utilisateurs peuvent s'appuyer sur les résultats. Par exemple, si une analyse statique utilisée pour les optimisations du compilateur n'était pas solide, l'optimisation pourrait modifier la sémantique du programme, ce qui conduit à un comportement inattendu au moment de l'exécution. À cette fin, Sturdy suit la théorie des preuves de solidité de composition des interprètes abstraits et des composants sonores et réutilisables pour l'interprétation abstraite afin de simplifier les preuves de solidité des analyses statiques.

Sturdy factorisant l'interprète en béton et l'interprète abstrait (l'analyse statique) dans un interprète générique . Cet interprète générique est paramétré par des interfaces qui contiennent des opérations primitives qui décrivent la sémantique de la langue, telles que try , catch et finally pour des exceptions. L'interpréteur en béton et abstrait instancie ensuite l'interpréteur générique en implémentant ces interfaces. Cette réorganisation découplle non seulement différentes préoccupations dans la mise en œuvre de l'analyse statique, mais simplifie également sa preuve de solidité. Plus de détails peuvent être trouvés dans notre papier ICFP.

Sturdy permet de construire des analyses statiques modulairement à partir de composants d'analyse réutilisables. Chaque composant d'analyse encapsule une seule préoccupation d'analyse et peut être prouvée sonore indépendamment de l'analyse où elle est utilisée. De plus, la théorie des composants d'analyse garantit qu'une analyse statique est solide, si toutes ses composantes d'analyse sont saines. Cela signifie que les développeurs d'analyse n'ont pas à se soucier de la solidité tant qu'ils réutilisent des composants d'analyse sonore. Plus de détails peuvent être trouvés dans notre papier Oopsla.

Commencer

Pour construire, installer l'outil de construction de pile et exécuter stack build à partir du répertoire racine du projet.

Le projet robuste contient actuellement des interprètes concrets et abstraits et génériques pour les langues suivantes:

• PCF , un langage fonctionnel d'ordre supérieur
• Tandis que , une langue impérative avec des conditions et des boucles
• Schéma , un langage de langue fonctionnelle dans la famille Lisp.
• Stratego , une langue pour les transformations de programme
• Lambdajs , une représentation intermédiaire de JavaScript
• Jimple , un bytecode java adapté à une analyse statique (travail en cours)

Pour exécuter les tests d'une langue particulière, utilisez stack test sturdy-$(lang) , par exemple,

 stack test sturdy-pcf

Publications

Algorithmes de point de fixation des combinateurs pour les interprètes abstraits en grosses étapes
Sven Keidel, Sebastian Erdweg, Tobias Hombücher
Conférence internationale sur la programmation fonctionnelle (ICFP). ACM, 2023. [PDF]

Interprètes de définition modulaire abstraits pour WebAssembly
Katharina Brandl, Sebastian Erdweg, Sven Keidel, Nils Hansen
Conférence européenne sur la programmation orientée objet (ECOOP). ACM, 2023. [PDF]

Une approche systématique de l'interprétation abstraite des transformations du programme
Sven Keidel et Sebastian Erdweg.
Vérification, vérification du modèle et interprétation abstraite (VMCAI). Springer, 2020. [PDF]

Composants sonores et réutilisables pour l'interprétation abstraite
Sven Keidel et Sebastian Erdweg.
Programmation, systèmes, langages et applications orientés objet (OOPSLA). ACM, 2019 [PDF] [Talk]

Représeurs de la solidité de la composition des interprètes abstraits
Sven Keidel, Casper Bach Poulsen et Sebastian Erdweg.
Conférence internationale sur la programmation fonctionnelle (ICFP). ACM, 2018 [PDF] [Talk]

Remerciements

Le projet robuste est un effort conjoint des personnes suivantes (par ordre alphabétique):

Casper Bach Poulsen, Jente Hidskes, Matthijs Bijman, Sarah Müller, Sebastian Erdweg, Sven Keidel, Tobias Hombücher, Wouter Raateland