formulog

Formilog

TL; DR: Écrivez des analyses de programme basées sur SMT (exécuteurs symboliques, vérificateurs de type de raffinement, etc.) dans un langage de type de données optimisé.

Datalig s'est avéré être un langage utile pour mettre en œuvre une gamme d'analyses de programme, mais les analyses qui utilisent la résolution de SMT ne peuvent pas être facilement écrites dans les versions traditionnelles de Datalog. Formulog se propose de combler cette lacune en augmentant la forme de données avec des moyens de construire et de raisonner sur les formules SMT, ainsi qu'une programmation fonctionnelle de premier ordre pour faciliter la vie.

Pourquoi rédiger votre analyse basée sur SMT dans Formilog?

1. En combinant la programmation logique, la programmation fonctionnelle et la résolution de SMT, le Forulog permet de coder de nombreuses analyses de manière déclarative au niveau de la spécification mathématique (par exemple, les règles d'inférence), la commission de l'espace entre la spécification et la mise en œuvre - et révélant souvent des bugs dans la SPEC!
2. Ce codage de haut niveau permet au Formilog d'appliquer des optimisations de haut niveau à votre analyse, comme la parallélisation automatique et l'évaluation dirigée par l'objectif.
3. Grâce à notre compilateur Formullog-to-Soufflé, vous pouvez générer automatiquement une version C ++ de l'analyse qui exploite des algorithmes et des structures de données très optimisés.

Intéressé? Pour plus d'informations, consultez les documents Forulog (également disponibles dans le répertoire DOCS), y compris les conseils sur le démarrage et la référence du langage. Pour avoir un sens pour ce qui est impliqué dans la création d'une analyse basée sur SMT non triviale dans Forulog, consultez notre tutoriel sur la mise en œuvre d'un vérificateur de type raffinement dans Forulog.

Contributif

Les contributions à ce projet sont les bienvenues! Veuillez ouvrir un problème GitHub, puis lier une demande de traction. Les demandes de traction doivent être dans le format Google Java avant d'être fusionnée. Pour reformater votre code, exécutez mvn spotless:apply ; Vous pouvez également vérifier si votre code est conforme (sans le reformater) en exécutant mvn spotless:check .

Licence et bibliothèques tierces

Formulog est publié sous une licence Apache 2.0.

Ce projet utilise des bibliothèques tierces. Vous pouvez générer une liste de ces bibliothèques et télécharger leurs licences associées à cette commande:

 mvn license:download-licenses

Le contenu généré peut être trouvé dans le target/generated-resources/ répertoire.