lart

LART: LLVM Abstraction and Raffinement Tool

LART = LLVM Abstraction & Raffinement Tool. L'objectif de cet outil est de fournir des transformations LLVM à LLVM qui implémentent diverses abstractions de programme. En ce qui concerne l'ensemble d'instructions, les programmes résultants sont des programmes LLVM normaux et concrets qui peuvent être exécutés et analysés. Des informations supplémentaires sur les abstractions en vigueur sur un programme (Fragment) sont insérées à l'aide de fonctions intrinsèques LLVM spéciales et de nœuds de métadonnées LLVM. LART fournit à la fois un outil autonome qui traite les fichiers bitcodes sur disque, ainsi qu'un cadre qui peut être intégré dans des outils basés sur LLVM complexes. La principale motivation derrière LART est de fournir un "préprocesseur" pour les vérificateurs de modèles basés sur LLVM et d'autres outils d'analyse, simplifiant leur travail en réduisant la taille du problème sans compromettre la solidité des analyses. Les abstractions mises en œuvre par LART peuvent être généralement raffinées sur la base d'instructions spécifiques sur lesquelles la "partie" de l'abstraction est trop rugueuse (une abstraction trop rude créera des erreurs parasites visibles pour les analyses ultérieures mais pas présente dans le programme d'origine).

Abstractions pour le code binaire LLVM

Le but de l'ensemble de l'exercice est de résumer les informations de Bitcode LLVM, ce qui rend les analyses ultérieures plus efficaces (au détriment d'une certaine précision). À cette fin, nous devons principalement être en mesure de coder le choix non déterministe dans les programmes LLVM, ce qui peut être fait simplement via une fonction à usage spécial (similaire à l'intrinssique LLVM). La fonction est nommée @lart.choice , prend une paire de limites en arguments et renvoie non déterministe une valeur qui se situe entre ces limites.

Cette extension à la sémantique LLVM doit être reconnue par l'outil en aval. Il s'agit également du seul écart crucial par rapport à Bitcode LLVM standard. De nombreux outils d'analyse implémenteront déjà un mécanisme similaire, en interne ou même avec une interface externe. Les outils d'adaptation sans support pour @lart.choice pour travailler avec LART sont généralement très simples.

Il existe d'autres fonctions à usage spécial fournies par LART, à savoir la famille @lart.meta.* @llvm.dbg.* Les transformations du programme devraient conserver ces appels au cas où LART serait appelé pour affiner une abstraction (chaque abstraction fournie par LART est livrée avec une procédure de raffinement correspondante, qui devra souvent trouver les appels @lart.meta insérés par l'abstraction).

Alors que la plupart des moteurs d'abstraction traditionnels fonctionnent comme interprètes, les abstractions peuvent également être "compilées" dans des programmes. Au lieu d'interpréter les instructions symboliquement, les instructions symboliques peuvent être compilées. En cas d'abstraction de prédicat, le code binaire résultant manipulera directement et utilisera directement les évaluations des prédicats au lieu de variables en béton. Comme expliqué ci-dessus, la différence importante est que le code binaire doit faire des choix non déterministes, car certains prédicats peuvent avoir des évaluations indéterminées (sont à la fois vraies et fausses). Certaines variables pourraient être même entièrement abstraites, et tous les tests sur de telles variables donneront des réponses oui et non.

Construire

Utilisez ou répétez la configuration à partir de ./devcontainer/Dockerfile pour le moment.

Puis utilisez:

 ./scripts/build.sh

Exécuter le compilateur

 ./build/bin/lartcc <domain> <compiler arguments> in.c

OPTER

 opt -load build/lib/cc/liblart_module.so -lart < in.bc > out.bc

Test

 lit -v build/test

Remarque: build/lartcc/lartcc doit avoir des permis d'exacutabple.