tp.md

Analyse Statique de Programmes -- TP Analyse Statique

CentraleSupélec

Enseignant: Virgile Prevosto

Préliminaires

Ce TP utilise exclusivement Python. On pourra utiliser l'image Docker, comme au TP précédent, ou directement sa machine si Python y est installé.

Rappel Docker

L'image est ici: https://github.com/Frederic-Boulanger-UPS/docker-webtop-3asl et peut être utilisée soit localement, soit depuis MyDocker. De plus le répertoire config est monté automatiquement dans le container docker si vous utilisez les scripts associé (PowerShell pour Windows ou sh pour Linux/macOS/BSD). Ces scripts devraient automatiquement ouvrir un onglet de votre navigateur web avec une session IceWM. Si ce n'est pas le cas, vous pouvez le faire manuellement: http://localhost:3000

NB: l'interpréteur Python est python3 et non python.

Typage statique

Les fichiers proposés ont des annotations de types permettant de vérifier que les programmes sont bien typés avant de les exécuter. On pourra utiliser l'outil pyright pour la vérification. Il n'est pas présent sur l'image Docker, mais peut s'installer via les commandes suivantes:

sudo apt update
sudo apt install pipx
sudo apt install pyright

Il dispose également d'un plugin vscode.

Introduction

Le fichier syntax.py définit les différentes classes syntaxique du langage While vu en cours, soit les expressions arithmétiques, les expressions booléennes et les instructions.

Sémantique opérationnelle

Le fichier opsem.py donne un squelette des fonctions à écrire pour définir un interpréteur concret du langage While. Les fonctions eval_aexpr, et eval_bexpr permettent d'évaluer respectivement une expression arithmétique et une expression booléenne dans un environnement qui associe à des noms de variable une valeur entière. En cas d'erreur dans l'évaluation d'une (sous-)expression, on renverra None. La fonction eval_instr, renvoie l'environnement final obtenu en évaluant dans un environnement initial une instruction donnée. Là encore, en cas d'erreur au cours de l'évaluation, on renvoie None.

Compléter ces définitions, et tester le résultat à l'aide du fichier example_opsem.py, qui définit le programme de calcul de la factorielle, et l'évalue pour x = 4.

Calcul de point fixe

Le fichier cfg.py est donné. Il contient la définition des différents labels des arêtes du graphe de flot de contrôle (skip, affectation, test, et erreur). On a aussi une classe pour les nœuds, pour un graphe, et pour un CFG proprement dit, qui ajoute au graphe les informations sur le nœud initial, le nœud final, et le nœud d'erreur. Un CFG est construit à partir d'un programme, et cette construction est donnée également.

Le fichier iteration.py contient une classe abstraite Transfer qui permet d'implémenter des analyses statiques en donnant l'élément bottom du treillis, l'état initial, le join de deux états, le test d'inclusion, et les fonctions de transfert pour chaque étiquette.

Compléter la fonction fixpoint_iteration de ce fichier, qui prend en argument une instance de Transfer et un CFG, et calcule le point fixe associant à chaque nœud du CFG l'état correspondant. L'algorithme est le suivant (on ne se préoccupe pas de terminaison):

1. le mapping initial associe l'état initial au nœud initial, et bottom à tous les autres. On met toutes les arêtes qui partent du nœud initial dans la worklist.
2. tant que la worklist n'est pas vide, on prend son premier élément, une arête qui va du nœud src au nœud dst avec le label l.
3. on associe au nœud dst le join de son état actuel avec le résultat de la fonction de transfert pour l appliqué à l'état associé à src
4. si le nouvel état est inclus dans l'état associé précédemment à dst, on ne fait rien. Sinon, on ajoute les arêtes qui sortent de dst à la worklist
5. on revient en 2

NB: en pratique, une itération efficace sélectionne l'arête d'intérêt de manière beaucoup plus précise, mais cela sort du cadre de ce TP.

Tester le résultat avec le fichier example_iteration.py, qui définit une analyse statique minimaliste, qui propage un état non vide dans tous les nœuds sauf ceux qui sont gardés par une condition qui s'évalue à False dans un environnement vide. Le programme exemple a un CFG qui contient de telles arêtes. À quoi correspondent les nœuds indiqués comme inatteignables par l'analyse?

Propagation de constantes

Le fichier constant_propagation.py vise à implémenter la propagation de constantes dans le cadre défini précédemment. Pour cela, on donne un type de valeurs abstraites qui sont soit un entier (quand on est sûr qu'une variable est associé à cet entier), soit None, pour indiquer que plusieurs valeurs sont possibles. Un environnement abstrait associe à des variables des valeurs abstraites, et notre état sera un environnement abstrait ou None pour indiquer que le nœud associé n'est jamais atteint. On donne également les fonctions d'évaluation abstraite des expressions, dans un environnement abstrait et qui renvoient une valeur abstraite ou None si une erreur se produit.

Implémenter les différentes méthodes de la classe Constant_propagation. On définira un état initial où toutes les variables utilisées dans le programme sont associées à la valeur abstract_value(None), indiquant qu'elles sont présentes dans l'environnement mais peuvent avoir n'importe quelle valeur.

On testera le résultat à l'aide du fichier example_constant_propagation.py, qui définit un programme dont les variables reçoivent des valeurs constantes. NB: pour que l'analyseur arrive à montrer que c est constante en fin de programme, il faut raffiner la fonction de transfert du test, en réduisant l'état propagé quand le test est une égalité entre une variable et une expression qui s'évalue à une constante, pour tenir compte du fait que dans la branche correspondante, la variable est associée à une constante. Ce raffinement est facultatif.