Soutenance mémoire
Syntaxe du langage
La syntaxe du langage de pointeur que l’on souhaite définir est celle d’un langage impératif standard à ceci près qu’elle considère que les variables contiennent des adresses et non des entiers. On définit d’abord les domaines syntaxiques, puis les syntaxes des sous-expressions : expressions de variables, d’adresses, et booléennes. Enfin, on considère la syntaxe d’un programme. Comme évoqué précédemment, le langage utilisera des variables ; on a donc besoin d’un ensemble de variables Var. On définit de plus un ensemble d’étiquettes Label qui permettra d’identifier les expressions entre elles. On considère maintenant les sous expressions. Pour commencer, on définit l’ensemble des expressions de variables : ExprVar (figure 1a). On choisit de pouvoir exprimer une variable soit par la variable elle-même, soit par le déréférencement d’une autre variable à l’aide de l’opérateur ∗. Ensuite, on définit l’ensemble des expressions de valeurs : ExprVal (figure 1b). Une valeur peut être exprimée de trois manières : à l’aide d’une variable, par le truchement d’un déréférencement (opérateur ∗), ou en référençant une variable avec l’opérateur &. Enfin, on définit l’ensemble des expressions booléennes : Bool (figure 1c). Cet ensemble est défini inductivement de manière usuelle à la différence que l’on considère deux égalités. La première est le test d’égalité de variables : ǫ1 == ǫ2, ǫ1, ǫ2 ∈ ExprVar. Dans la section 3.3, on définira la sémantique du test == de sorte que si ǫ1 == ǫ2 est évaluée à true, cela signifie que modifier la valeur de ǫ1 revient à modifier celle de ǫ2 (et réciproquement). La seconde égalité est le test d’égalité de valeurs : e1 = e2, e1, e2 ∈ ExprVal. La syntaxe des sous-expressions ayant été définie, on considère maintenant le langage lui-même. Le langage, Statement, possède une syntaxe basique de langage impératif (figure 2). Il contient les instructions suivantes : skip, l’assignation d’une valeur à une variable, la séquence, un branchement conditionnel et une boucle. Les instructions sont étiquetées .
La syntaxe du langage ayant été définie, il faut maintenant donner un sens à toutes ces expressions. Dans les sous-sections suivantes, on définit donc la sémantique du programme. On considère en premier lieu les domaines sémantiques 3.2, ensuite les sémantiques des sous-expressions 3.3 et enfin la sémantique du programme lui même 3.4.
Domaines sémantiques du langage
Pour commencer, on définit donc les domaines sémantiques à savoir les ensembles dans lesquels les sémantiques des expressions et du programme prendront leurs arguments et leurs valeurs. Premièrement, trois ensembles sont définis : Add, l’ensemble des adresses utiliséesq Value l’ensemble des valeurs que peuvent contenir les zones mémoires (correspondant à des adresses) et {tt,ff} qui correspondent respectivement à vrai et à faux. Étant donné que l’on considère un langage de pointeur, on pose Value := Add. Cette égalité étant spécifique au cas présent et afin d’éviter toute confusion, nous utilisons tout de même les noms Add pour les adresses en tant que telles et Value pour les valeurs. Lorsque l’égalité entre ces deux ensembles sera nécessaire, nous l’utiliserons de manière explicite. Dans le paragraphe précédent nous avons implicitement évoqué l’ensemble des états : State= Add → Value ∪ {⊥}. Un état (σ ∈ State) associe à chaque adresse une valeur (que contient donc la zone mémoire correspondant à l’adresse) ou ⊥ si la zone mémoire correspondant à l’adresse n’a pas été initialisée. Afin d’obtenir une sémantique, il est nécessaire de lier les éléments syntaxiques (Var) et sémantiques (Add et Value). Pour cela, on définit l’ensemble des environnements Env = Var → Add ∪ {⊥} qui à chaque variable, associe l’adresse à laquelle elle correspond (ou ⊥ si la variable n’a pas d’adresse). Lest environnements sont noté ρ. Il est désormais possible de définir les sémantiques des sous-expressions.
Sémantiques des sous-expressions du langage
On définit d’abord la sémantique des expressions de variables, puis celle des expressions de valeurs, et enfin celle des expressions booléennes. Pour commencer, on s’intéresse donc à la sémantique des expressions de variables, à savoir Ea (figure 3a). Deux cas peuvent se présenter : x et ∗x (où x ∈ Var). Lorsque l’on utilise la variable x ∈ Var, on utilise en fait l’adresse qui y correspond : ρ x. Lorsque l’on déréférence la variable x ∈ Var, on s’intéresse à la valeur que « contient x » à savoir la valeur se trouvant à l’adresse correspondant à x : σ(ρ x). Dans ce dernier cas, il faut que la valeur soit une adresse, c’est le cas car Value = Add.
Ensuite, on définit la sémantique des expressions de valeurs : Ev (figure 3b). Trois cas peuvent échoir : x, ∗x, &x et (où x ∈ Var). La valeur qui correspond à une variable x est celle que contient son adresse, à savoir σ(ρ x). La valeur que l’on souhaite obtenir avec un déréférencement ∗x est la valeur se trouvant à l’adresse que « contient » x. La sémantique de ∗x est donc σ(σ(ρ x)) (pour x ∈ Var). Enfin, lorsque l’on référence une variable x avec &x, on s’intéresse simplement à l’adresse de cette variable : ρ x.
Sémantique du Langage
Notre but est de vérifier qu’un programme n’atteint jamais un état « dangereux ». C’est pour cela que l’on s’intéresse à la sémantique collectrice. Il s’agit en fait de collecter tous les états possiblement atteignables lors de l’exécution d’un programme. Pour réaliser une telle sémantique, on procède en deux étapes : d’abord on construit un graphe de flot de contrôle à partir de S , puis on « navigue » sur un tel graphe en respectant les conditions données par les arrêtes pour obtenir la sémantique du programme. La raison d’un tel choix est que cela permet d’obtenir une séparation claire entre les éléments structurant d’un programme (tel que la boucle) et les éléments affectant la mémoire. En effet, les premiers sont capturés dans la structure du graphe tandis que les seconds sont gérés par la façon dont le graphe est parcouru. On s’intéresse à la première étape. On souhaite donc générer un graphe de flot de contrôle cfg S que l’on définit par un quadruplet (Vertex, e, f,Edge) où Vertex est l’ensemble des nœuds du graphe, e, f ∈ Vertex sont respectivement l’entrée et la sortie du graphe, et Edge l’ensemble des arêtes du graphe. On pose que les nœuds sont les étiquettes du programme, donc Vertex := Label. Deux instructions qui partagent la même étiquette ne sont donc pas distinguées. En ce qui concerne les arêtes, on définit d’abord Inst = {skip, ǫ := e, assert b}. Cet ensemble comprend les « instructions » atomiques d’un programme, celles ayant un effet ou des conditions sur l’état courant. Le principe est de lier les arêtes à des instruction de sorte que l’on ne prendra les arêtes qu’en respectant l’effet des instructions sur la mémoire. Les nœuds ont été définis, e est simplement la première étiquette rencontrée dans S (appelée entry S ), f est choisie arbitrairement ; seules les arêtes sont toujours à définir. On définit les arêtes comme des triplets de Vertex × Inst × Vertex. Intuitivement, on souhaite que l’arête (v1, i, v2) corresponde au fait de pouvoir aller de l’étiquette v1 à l’étiquette v2 en effectuant l’instruction i. On génère les arêtes de cfgS inductivement en fonction des cas pouvant échoir à l’aide de fonction cfgl (figure 4) où l en indice est une étiquette. Le principe est de garder en mémoire où l’on souhaite se rendre (avec l’indice) et de construire les arêtes permettant de se rendre de l’étiquette courante (donnée par le programme en argument) vers l’étiquette cible (indice). Par exemple cfgl ′ (while l [b] do S end) est la réunion de trois ensembles : – {(l, assert b, entry S )} car si b est vérifié on se branche sur le corps de la boucle : S ,
– cfgl S car lorqu’on exécute le corps de la boucle et on revient au test,
– {(l, assert (not b), l ′ )} car si b n’est pas vérifié (assert (not b)) on sort de la boucle.
Au final le graphe de flot de contrôle d’un programme S ∈ Statement est le suivant : cfg S = (Label, entry S, f, cfgf S ).
|
Table des matières
1 Introduction
2 Travaux Connexes
3 Un langage de pointeur
3.1 Syntaxe du langage
3.2 Domaines sémantiques du langage
3.3 Sémantiques des sous-expressions du langage
3.4 Sémantique du Langage
4 Sémantique abstraite du langage
4.1 Abstraction par rapport à la sémantique de langage
4.2 Analyse dans la sémantique abstraite
5 Algorithme de vérification de résultats de l’analyse
5.1 Conception de l’algorithme
5.2 Vérification probabiliste d’une inclusion
5.3 Vérification de l’ensemble du résultat
5.4 Indépendance des inclusions
6 Implémentation et résultats expérimentaux
6.1 Implémentation
6.2 Résultats expérimentaux
7 Ouvertures
7.1 L’utilisation de martingales
7.2 Amélioration de l’implémentation
8 Conclusion
Télécharger le rapport complet
