Implémentation des intervalles ; début rédaction du rapport.

4 files changed, 378 insertions, 4 deletions

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 @@
+<TeXmacs|1.0.7.21>
+
+<style|<tuple|article|french>>
+
+<\body>
+  <doc-data|<doc-title|Rapport de projet : interprétation
+  abstraite>|<doc-author|<author-data|<author-name|Alex AUVOLAT>>>>
+
+  <section|Introduction>
+
+  <subsection|Analyse statique abstraite>
+
+  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.
+
+  <subsection|Notre tâche>
+
+  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>
+    <item>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 <verbatim|if>, <verbatim|while>, <verbatim|assert>,
+    <verbatim|print>, <verbatim|halt> ;
+
+    <item>Prise en charge du non-déterminisme (fonction <verbatim|rand>) ;
+
+    <item>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).
+  </itemize>
+
+  Notre code s'appuie sur de nombreux éléments extérieurs :
+
+  <\itemize>
+    <item>La bibliothèque <name|zarith>, pour la manipulation d'entiers en
+    précision arbitraire ;
+
+    <item>La bibliothèque <name|apron>, pour la manipulation du domaine des
+    polyhèdres ;
+
+    <item>Un lexer et un parser pour notre fragment de C fourni par
+    l'enseignant.
+  </itemize>
+
+  <section|Découpage des modules>
+
+  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 <verbatim|Z.t>
+  de la bibliothèque <name|zarith>, qui permet de manipuler des entiers en
+  précision arbitraire.
+
+  <subsection|La signature de module <verbatim|ENVIRONMENT_DOMAIN>>
+
+  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
+  <verbatim|Interpret.Make>, qui contient le c÷ur de l'interpréteur abstrait.
+
+  <verbatim|>
+
+  <\itemize>
+    <item><verbatim|type t>
+
+    Le type abstrait représentant un environnement abstrait de notre
+    interpréteur.
+
+    <item><verbatim|val init, bottom : t>
+
+    Représentations respectives de <math|\<top\>> et <math|\<bot\>>. Remarque
+    : l'environnement représentant <math|\<top\>> est différent en fonction
+    des variables que cet environnement contient. <verbatim|init> est
+    l'environnement <math|\<top\>> ne contenant aucune variable. Il y a une
+    fonction de test <verbatim|is_bot> mais pas de test <verbatim|is_top> car
+    celui-ci n'est pas nécessaire.
+
+    <item><verbatim|val addvar, rmvar : t -\<gtr\> id -\<gtr\> t>
+
+    Ajoute une variable à un environnement (elle est initialisée sans aucune
+    contrainte, c'est-à-dire à <math|\<top\>> dans le cas des environnements
+    non-relationnels) ; supprime une variable d'un environnement.
+
+    <item><verbatim|val assign : t -\<gtr\> id -\<gtr\> expr ext -\<gtr\> t>
+
+    Réalise l'affectation d'une expression à une variable :
+    <math|S<around*|\<llbracket\>|x\<leftarrow\>e|\<rrbracket\>>>.
+
+    <item><verbatim|val compare_leq, compare_eq : t -\<gtr\> expr ext
+    -\<gtr\> expr ext -\<gtr\> t>
+
+    Restreint le domaine abstrait à une portion vérifiant une équation :
+    <math|S<around*|\<llbracket\>|e<rsub|1>\<leqslant\>e<rsub|2>?|\<rrbracket\>>>
+    et <math|S<around*|\<llbracket\>|e<rsub|1>=e<rsub|2>?|\<rrbracket\>>>.
+
+    <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t>
+
+    Implémentation de l'union abstraite <math|\<sqcup\>>, de l'intersection
+    abstraite <math|\<sqcap\>> et de l'opération de widening
+    <math|\<nabla\>>.
+
+    <item><verbatim|val subset: t -\<gtr\> t -\<gtr\> bool>
+
+    Implémentation de la condition d'inclusion <math|\<sqsubseteq\>>. Une
+    seule implication : <verbatim|subset a b>
+    <math|\<Rightarrow\>a\<sqsubseteq\>b>.
+  </itemize>
+
+  \ 
+
+  <subsection|La signature de module <verbatim|VALUE_DOMAIN>>
+
+  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 <verbatim|NonRelationnal> qui
+  contient le code générique pour un <verbatim|ENVIRONMENT_DOMAIN> non
+  relationnel.
+
+  <\itemize>
+    <item><verbatim|type t>
+
+    Le type abstrait d'une valeur abstraite
+
+    <item><verbatim|val top, bottom : t>
+
+    Les représentations de <math|\<top\>> et <math|\<bot\>>. Il n'y a pas de
+    fonctions de tests <verbatim|is_bot> et <verbatim|is_top>, les
+    représentations sont uniques.
+
+    <item><verbatim|val const : Z.t -\<gtr\> t>
+
+    Obtenir la représentation d'une constante.
+
+    <item><verbatim|val rand : Z.t -\<gtr\> Z.t -\<gtr\> t>
+
+    Obtenir la représentation d'un intervalle.
+
+    <item><verbatim|val subset : t -\<gtr\> t -\<gtr\> bool>
+
+    Implémentation de la relation d'inclusion <math|\<sqsubset\>> sur les
+    valeurs.
+
+    <item><verbatim|val join, meet, widen : t -\<gtr\> t -\<gtr\> t>
+
+    Implémentation de l'union <math|\<sqcup\>>, de l'intersection
+    <math|\<sqcap\>> et du widening <math|\<nabla\>>.
+
+    <item><verbatim|val neg : t -\<gtr\> t>
+
+    Négation unaire abstraite
+
+    <item><verbatim|val add, sub, mul, div, rem : t -\<gtr\> t -\<gtr\> t>
+
+    Opérateurs binaires abstraits
+
+    <item><verbatim|val leq : t -\<gtr\> t -\<gtr\> t * t>
+
+    Restreint deux valeurs <math|a\<nocomma\>> et <math|b> aux meilleurs
+    sur-approximations que l'on peut avoir en restreignant le domaine avec
+    une condition de la forme <math|a\<leqslant\>b>.
+  </itemize>
+
+  <subsection|Le module <verbatim|Constants>>
+
+  Ce module implémente un <verbatim|VALUE_DOMAIN> correspondant au treillis
+  des constantes. Le code est extrêmement simple et implémente directement la
+  sémantique vue en cours.
+
+  <subsection|Le module <verbatim|Intervals>>
+
+  Ce module implémente un <verbatim|VALUE_DOMAIN> correspondant au treillis
+  des intervales. Le code est extrêmement simple et implémente directement la
+  sémantique vue en cours.
+
+  <subsection|Le module <verbatim|NonRelationnal>>
+
+  Ce module implémente toutes les fonctions communes aux domaines
+  non-relationnels (constantes, intervalles). Il est paramétré par un
+  <verbatim|VALUE_DOMAIN> <verbatim|V>.
+
+  <\itemize>
+    <item>Le type <verbatim|t> représentant un environnement abstrait est
+    soit un map des identifieurs vers les éléments de <verbatim|V>, soit
+    <math|\<bot\>>. Dès qu'une valeur vaur <math|\<bot\>>, on s'interdit de
+    la mettre dans le map et on transforme tout l'environnement abstrait en
+    <math|\<bot\>>. La fonction <verbatim|strict> permet de s'en assurer.
+
+    <item>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 <verbatim|V> 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 <verbatim|compare_leq> et <verbatim|compare_eq>.
+
+    <item>Pour un opérateur <math|\<ltimes\>\<in\><around*|{|\<leqslant\>,=|}>>,
+    les filtrages du type <math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>>
+    sont implémentés comme suit (fonction <verbatim|compare>) :
+
+    <\itemize>
+      <item><math|S<around*|\<llbracket\>|x\<ltimes\>y?|\<rrbracket\>>> : on
+      applique l'opérateur (<verbatim|leq> pour <math|\<leqslant\>> ou
+      <verbatim|meet> pour <math|=>) de <verbatim|V> sur les deux valeurs, ce
+      qui donne deux nouvelles valeurs pour <math|x> et <math|y> (ou deux
+      fois <math|\<bot\>> si la conditin ne peut pas être remplie). On
+      utilise ces deux valeurs pour mettre à jour l'environnement.
+
+      <item><math|S<around*|\<llbracket\>|x\<ltimes\>e?|\<rrbracket\>>> et
+      <math|S<around*|\<llbracket\>|e\<ltimes\>x?|\<rrbracket\>>> : on évalue
+      l'expression <math|e> et on applique l'opérateur de <verbatim|V> sur
+      cette valeur et la valeur de <math|x>, ce qui restreint éventuellement
+      la valeur de <math|x>, ou peut donner <math|\<bot\>>.
+
+      <item><math|S<around*|\<llbracket\>|e<rsub|1>\<ltimes\>e<rsub|2>?|\<rrbracket\>>>
+      : on évalue les expressions <math|e<rsub|1>> et <math|e<rsub|2>> et on
+      applique l'opérateur de <verbatim|V>. Aucune valeur n'est restreinte
+      dans l'environnement mais on peut détecter une condition impossible,
+      auquel cas l'environnement est passé à <math|\<bot\>>.
+    </itemize>
+
+    <item>Les opérateurs <math|\<sqcup\>>, <math|\<sqcap\>> et
+    <math|\<nabla\>> 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.
+
+    <item>L'opérateur <math|\<sqsubset\>> 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.
+  </itemize>
+
+  <subsection|Le module <verbatim|RelationnalDomain>>
+
+  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.
+
+  <subsection|Le module <verbatim|Interpret.Make>>
+
+  TODO
+</body>
+
+<\initial>
+  <\collection>
+    <associate|page-medium|paper>
+    <associate|page-screen-margin|false>
+  </collection>
+</initial>
+
+<\references>
+  <\collection>
+    <associate|auto-1|<tuple|1|1>>
+    <associate|auto-10|<tuple|2.6|?>>
+    <associate|auto-11|<tuple|2.7|?>>
+    <associate|auto-2|<tuple|1.1|1>>
+    <associate|auto-3|<tuple|1.2|1>>
+    <associate|auto-4|<tuple|2|2>>
+    <associate|auto-5|<tuple|2.1|2>>
+    <associate|auto-6|<tuple|2.2|2>>
+    <associate|auto-7|<tuple|2.3|2>>
+    <associate|auto-8|<tuple|2.4|2>>
+    <associate|auto-9|<tuple|2.5|2>>
+  </collection>
+</references>
+
+<\auxiliary>
+  <\collection>
+    <\associate|toc>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|1<space|2spc>Introduction>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-1><vspace|0.5fn>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|2<space|2spc>Découpage
+      des modules> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-2><vspace|0.5fn>
+
+      <with|par-left|<quote|1tab>|2.1<space|2spc>La signature de module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|ENVIRONMENT_DOMAIN>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-3>>
+
+      <with|par-left|<quote|1tab>|2.2<space|2spc>La signature de module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|VALUE_DOMAIN>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-4>>
+
+      <with|par-left|<quote|1tab>|2.3<space|2spc>Le module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|Constants>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-5>>
+
+      <with|par-left|<quote|1tab>|2.4<space|2spc>Le module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|Intervals>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-6>>
+
+      <with|par-left|<quote|1tab>|2.5<space|2spc>Le module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|NonRelationnal>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-7>>
+
+      <with|par-left|<quote|1tab>|2.6<space|2spc>Le module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|RelationnalDomain>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-8>>
+
+      <with|par-left|<quote|1tab>|2.7<space|2spc>Le module
+      <with|font-family|<quote|tt>|language|<quote|verbatim>|Interpret.Make>
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-9>>
+    </associate>
+  </collection>
+</auxiliary>
\ No newline at end of file