From 652d04c5476fdfb9cc7a2d93de3df4d76a6882ce Mon Sep 17 00:00:00 2001 From: Alex AUVOLAT Date: Sun, 1 Jun 2014 10:06:35 +0200 Subject: =?UTF-8?q?Impl=C3=A9mentation=20des=20intervalles=20;=20d=C3=A9bu?= =?UTF-8?q?t=20r=C3=A9daction=20du=20rapport.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- abstract/interpret.ml | 1 - abstract/intervals_domain.ml | 41 +++++- abstract/nonrelational.ml | 2 +- rapport.tm | 338 +++++++++++++++++++++++++++++++++++++++++++ 4 files changed, 378 insertions(+), 4 deletions(-) create mode 100644 rapport.tm diff --git a/abstract/interpret.ml b/abstract/interpret.ml index cb32e22..f6a6cb4 100644 --- a/abstract/interpret.ml +++ b/abstract/interpret.ml @@ -73,7 +73,6 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1)) env - | _ -> env end diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index b63f8a9..d95a938 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -33,6 +33,21 @@ module Intervals : VALUE_DOMAIN = struct | Int(x), Int(y) -> Int(Z.mul x y) | MInf, PInf | PInf, MInf -> MInf | MInf, MInf | PInf, PInf -> PInf + let bound_div a b = + match a, b with + | _, PInf | _, MInf -> Int Z.zero + | PInf, Int i -> + if i < Z.zero then MInf + else PInf + | MInf, Int i -> + if i < Z.zero then PInf + else MInf + | Int i, Int j -> + if j = Z.zero then + if i < Z.zero then MInf + else PInf + else Int (Z.div i j) + let bound_min a b = match a, b with | MInf, _ | _, MInf -> MInf @@ -50,6 +65,8 @@ module Intervals : VALUE_DOMAIN = struct | PInf -> MInf | MInf -> PInf | Int i -> Int (Z.neg i) + + let bound_abs a = bound_max a (bound_neg a) (* implementation *) let top = Itv(MInf, PInf) @@ -101,8 +118,28 @@ module Intervals : VALUE_DOMAIN = struct (bound_max (bound_mul b c) (bound_mul b d)))) - let div a b = top (* TODO *) - let rem a b = top (* TODO *) + let div a b = match a, b with + | Bot, _ -> Bot + | Itv(a, b), q -> + let p1 = match meet q (Itv(Int (Z.of_int 1), PInf)) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div a c) (bound_div a d), max (bound_div b c) (bound_div b d)) + in + let p2 = match meet q (Itv(MInf, Int (Z.of_int (-1)))) with + | Bot -> Bot + | Itv(c, d) -> + Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d)) + in + join p1 p2 + + let rem a b = match a, b with + | Bot, _ | _, Bot -> Bot + | Itv(a, b), Itv(c, d) -> + Itv( + Int Z.zero, + bound_max (bound_abs c) (bound_abs d) + ) let leq a b = match a, b with | Bot, _ | _, Bot -> Bot, Bot diff --git a/abstract/nonrelational.ml b/abstract/nonrelational.ml index aa34d14..188c8bc 100644 --- a/abstract/nonrelational.ml +++ b/abstract/nonrelational.ml @@ -110,7 +110,7 @@ module NonRelational (V : VALUE_DOMAIN) : ENVIRONMENT_DOMAIN = struct | Env m, Env n -> VarMap.for_all2o (fun _ _ -> true) - (fun _ _ -> true) + (fun _ v -> v = V.top) (fun _ a b -> V.subset a b) m n diff --git a/rapport.tm b/rapport.tm new file mode 100644 index 0000000..cb9a68b --- /dev/null +++ b/rapport.tm @@ -0,0 +1,338 @@ + + +> + +<\body> + |>>> + + + + + + L'analyse statique abstraite d'un programme consiste à exécuter ce + programme non pas sur une entrée particulière mais sur un domaine abstrait + qui représente toute un ensemble de données possibles. Cette façon de + tester permet de découvrir des propriétés qui sont vraies quelle que soit + l'entrée sur laquelle le programme est exécuté, et ce en une seule passe + d'analyse statique (dont on est sûre qu'elle termine - contrairement au + programme lui-même). + + L'analyse abstraite consiste à faire se propager le domaine abstrait à tous + les points du programme. En plaçant des assertions à des endroits + judicieux, on peut s'assurer que certaines conditions sont toujours + vérifiées. + + Le domaine abstrait ne peut pas représenter avec la précision nécessaire + (infinie) exactement tous les états du programme, c'est pourquoi nous + sommes obligés d'en considérer une sur-approximation. Le but du jeu étant + d'avoir la sur-approximation avec le moins de marge par rapport aux + ensembles d'états concrets représentés, afin de pouvoir prouver un maximum + de propriétés. + + + + Dans le cadre du cours \S sémantique et application à la vérification de + programmes \T, nous avons eu à travailler sur un interpréteur abstrait pour + un fragment du langage C. Le travail minimum demandé comportait les aspects + suivants : + + <\itemize> + Définition d'un interpréteur sur un domaine abstrait prenant en + compte les déclarations de variables locales, les affectations, ainsi que + les constructions , , , + , ; + + Prise en charge du non-déterminisme (fonction ) ; + + Interprétation possible dans plusieurs domaines abstraits : deux + domaines non-relationnels (treillis des constantes et treillis des + intervalles) et un domaine relationnel (domaine des polyhèdres). + + + Notre code s'appuie sur de nombreux éléments extérieurs : + + <\itemize> + La bibliothèque , pour la manipulation d'entiers en + précision arbitraire ; + + La bibliothèque , pour la manipulation du domaine des + polyhèdres ; + + Un lexer et un parser pour notre fragment de C fourni par + l'enseignant. + + + + + Pour réaliser ce projet, nous avons tenté de factoriser notre code au + maximum. Grâce à une interface de modules et de foncteurs astucieuse, nous + avons écrit un code dont la partie \S interprétation abstraite \T fait + moins de 1000 lignes. Nous présentons maintenant des extraits de cette + interface, largement inspirée de celle proposée par l'enseignant dans les + transparents de son cours \S Abstract Interpretation II \T. + + Dans tout le code, les entiers sont représentés par le type + de la bibliothèque , qui permet de manipuler des entiers en + précision arbitraire. + + > + + Cette signature de module définit les fonctions que doivent implémenter + tout module pouvant être utilisé comme domaine abstrait (relationnel ou non + relationnel). Il est utilisé pour paramétrer le module + , qui contient le c÷ur de l'interpréteur abstrait. + + + + <\itemize> + + + Le type abstrait représentant un environnement abstrait de notre + interpréteur. + + + + Représentations respectives de > et >. Remarque + : l'environnement représentant > est différent en fonction + des variables que cet environnement contient. est + l'environnement > ne contenant aucune variable. Il y a une + fonction de test mais pas de test car + celui-ci n'est pas nécessaire. + + id -\ t> + + Ajoute une variable à un environnement (elle est initialisée sans aucune + contrainte, c'est-à-dire à > dans le cas des environnements + non-relationnels) ; supprime une variable d'un environnement. + + id -\ expr ext -\ t> + + Réalise l'affectation d'une expression à une variable : + |x\e|\>>. + + expr ext + -\ expr ext -\ t> + + Restreint le domaine abstrait à une portion vérifiant une équation : + |e\e?|\>> + et |e=e?|\>>. + + t -\ t> + + Implémentation de l'union abstraite >, de l'intersection + abstraite > et de l'opération de widening + >. + + t -\ bool> + + Implémentation de la condition d'inclusion >. Une + seule implication : + a\b>. + + + \ + + > + + Cette signature de module définit les fonctions requises pour tout module + décrivant un domaine de valeurs pour une abstraction non relationnelle. + Cette signature est le paramètre du module qui + contient le code générique pour un non + relationnel. + + <\itemize> + + + Le type abstrait d'une valeur abstraite + + + + Les représentations de > et >. Il n'y a pas de + fonctions de tests et , les + représentations sont uniques. + + t> + + Obtenir la représentation d'une constante. + + Z.t -\ t> + + Obtenir la représentation d'un intervalle. + + t -\ bool> + + Implémentation de la relation d'inclusion > sur les + valeurs. + + t -\ t> + + Implémentation de l'union >, de l'intersection + > et du widening >. + + t> + + Négation unaire abstraite + + t -\ t> + + Opérateurs binaires abstraits + + t -\ t * t> + + Restreint deux valeurs > et aux meilleurs + sur-approximations que l'on peut avoir en restreignant le domaine avec + une condition de la forme b>. + + + > + + Ce module implémente un correspondant au treillis + des constantes. Le code est extrêmement simple et implémente directement la + sémantique vue en cours. + + > + + Ce module implémente un correspondant au treillis + des intervales. Le code est extrêmement simple et implémente directement la + sémantique vue en cours. + + > + + Ce module implémente toutes les fonctions communes aux domaines + non-relationnels (constantes, intervalles). Il est paramétré par un + . + + <\itemize> + Le type représentant un environnement abstrait est + soit un map des identifieurs vers les éléments de , soit + >. Dès qu'une valeur vaur >, on s'interdit de + la mettre dans le map et on transforme tout l'environnement abstrait en + >. La fonction permet de s'en assurer. + + Les expressions sont évaluées selont des modalités très simples : + on récupère les valeurs abstraites correspondant aux constantes et aux + variables et on applique les opérateurs de qui + correspondent, ce qui donne une nouvelle valeur. L'évaluation d'une + expression de cette manière est utiliée pour l'affectation ainsi que dans + les operations et . + + Pour un opérateur \,=|}>>, + les filtrages du type |e\e?|\>> + sont implémentés comme suit (fonction ) : + + <\itemize> + |x\y?|\>> : on + applique l'opérateur ( pour > ou + pour ) de sur les deux valeurs, ce + qui donne deux nouvelles valeurs pour et (ou deux + fois > si la conditin ne peut pas être remplie). On + utilise ces deux valeurs pour mettre à jour l'environnement. + + |x\e?|\>> et + |e\x?|\>> : on évalue + l'expression et on applique l'opérateur de sur + cette valeur et la valeur de , ce qui restreint éventuellement + la valeur de , ou peut donner >. + + |e\e?|\>> + : on évalue les expressions > et > et on + applique l'opérateur de . Aucune valeur n'est restreinte + dans l'environnement mais on peut détecter une condition impossible, + auquel cas l'environnement est passé à >. + + + Les opérateurs >, > et + > sur les environnements appliquent l'opérateur + correspondant sur les valeurs point-par-point pour chaque variable. Pour + que ces opérateurs n'échouent pas, il faut que les mêmes variables soient + déclarées dans les deux environnements. + + L'opérateur > sur les environnements fonctionne + aussi point-par-point mais n'échoue pas dans le cas de deux + environnements ne déclarant pas les mêmes variables. + + + > + + Ce module implémente le domaine abstrait des polyhèdres (domaine + relationnel) en faisant appel à la bibliothèque Apron. En pratique, ce + module fait une simple traduction entre les appels et structures de notre + programme et ceux de la bibliothèque Apron. + + > + + TODO + + +<\initial> + <\collection> + + + + + +<\references> + <\collection> + > + > + > + > + > + > + > + > + > + > + > + + + +<\auxiliary> + <\collection> + <\associate|toc> + |math-font-series||1Introduction> + |.>>>>|> + + + |math-font-series||2Découpage + des modules> |.>>>>|> + + + |2.1La signature de module + |language||ENVIRONMENT_DOMAIN> + |.>>>>|> + > + + |2.2La signature de module + |language||VALUE_DOMAIN> + |.>>>>|> + > + + |2.3Le module + |language||Constants> + |.>>>>|> + > + + |2.4Le module + |language||Intervals> + |.>>>>|> + > + + |2.5Le module + |language||NonRelationnal> + |.>>>>|> + > + + |2.6Le module + |language||RelationnalDomain> + |.>>>>|> + > + + |2.7Le module + |language||Interpret.Make> + |.>>>>|> + > + + + \ No newline at end of file -- cgit v1.2.3