Plug into Apron Box domain for intervals.

2 files changed, 157 insertions, 67 deletions

diff --git a/doc/readme.pdf b/doc/readme.pdf
index 4a97029..aa680ca 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
diff --git a/doc/readme.tm b/doc/readme.tm
index 8622a9a..f21a66c 100644
--- a/doc/readme.tm
+++ b/doc/readme.tm
@@ -823,20 +823,22 @@
   peut être caractérisée par sa fonction de concrétisation :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|\<gamma\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-D\><rsup|#>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
+    <tformat|<table|<row|<cell|\<gamma\>>|<cell|:>|<cell|\<cal-D\><rsup|#>\<rightarrow\>\<cal-P\><around*|(|\<bbb-M\>|)>>>>>
   </eqnarray*>
 
   \ On peut aussi généralement s'appuyer sur l<math|>'existence d'une
   fonction d'abstraction :
 
   <\eqnarray*>
-    <tformat|<table|<row|<cell|\<alpha\><rsub|\<bbb-M\>>>|<cell|:>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>\<rightarrow\>\<cal-D\><rsup|#>>>>>
+    <tformat|<table|<row|<cell|\<alpha\>>|<cell|:>|<cell|\<cal-P\><around*|(|\<bbb-M\>|)>\<rightarrow\>\<cal-D\><rsup|#>>>>>
   </eqnarray*>
 
   Cette fonction fait correspondre à une partie de <math|\<bbb-M\>> sa
-  meilleure approximation dans le domaine abstrait (par exemple dans le cas
-  des polyèdres, l'abstraction d'un ensemble fini de points est leur
-  enveloppe convexe, mais un cercle n'a pas de meilleure abstraction).
+  meilleure approximation dans le domaine abstrait, lorsque celle-ci existe
+  (par exemple dans le cas des polyèdres, l'abstraction d'un ensemble fini de
+  points est leur enveloppe convexe, mais un cercle n'a pas de meilleure
+  abstraction). En pratique la fonction d'abstraction n'est pas très
+  utilisée.
 
   Dans tous les cas, on s'attend à ce que
   <math|\<forall\>x\<in\>\<cal-D\><rsup|#>,x\<sqsubseteq\>\<alpha\><around*|(|\<gamma\><around*|(|x|)>|)>>
@@ -1441,11 +1443,65 @@
     Dans ce cas, on s'arrête si <math|s<rsub|n+1>=s<rsub|n>>.
   </itemize>
 
-  <section|Partitionnement dynamique>
+  <subsection|Partitionnement dynamique>
 
-  Une autre approche à base de partitionnement dynamique a été tentée, mais
-  elle n'a pas donné de très bons résultats par manque d'une heuristique sur
-  les partitionnements à effectuer. Détails à venir.
+  Une autre approche à base de partitionnement dynamique a été tentée (cf
+  <em|Dynamic Partitionning in Analyses of Numerical Properties>), mais elle
+  n'a pas donné de très bons résultats par manque d'une heuristique sur les
+  partitionnements à effectuer.
+
+  L'idée de base consiste à se donner une liste de conditions
+  <math|d<rsub|1>,d<rsub|2>,\<ldots\>,d<rsub|n>> qui définissent <math|n>
+  parties de <math|S<rsup|#>> (en principe disjointes, mais les
+  approximations mènent parfois à des recoupenents). On étudie les parties
+  (ou <em|lieux>) <math|S<rsub|i><rsup|#>=<around*|\<llbracket\>|d<rsub|i>|\<rrbracket\>><around*|(|S<rsup|#>|)>>
+  comme un système de transitions pour lequel on calcule un point fixe par
+  itérations chaotiques.
+
+  Les conditions <math|d<rsub|i>> sont données par une heuristique qui
+  découpe à chaque rafinement un des lieux <math|S<rsub|i><rsup|#>> en
+  plusieurs sous-lieux.
+
+  <paragraph|Découpage de base.>Le découpage de base est généralement : init
+  ; non init et propriété vérifiée ; non init et propriété non vérifiée.
+
+  <paragraph|Rafinement.>On note <math|S<rsub|i><rsup|#>\<rightarrow\>S<rsup|#><rsub|j>>
+  si dans notre sur-approximation on peut être à un cycle dans
+  <math|S<rsub|i><rsup|#>> et dans le suivant dans <math|S<rsub|j><rsup|#>>.
+
+  On recherche un lieu <math|S<rsub|i><rsup|#>> et une condition <math|c>
+  apparaissant dans le programme (ou la négation d'une telle condition) tel
+  qu'il existe un état <math|S<rsub|j><rsup|#>> ayant les propriétés
+  suivantes :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S<rsub|j><rsup|#>>|<cell|\<rightarrow\>>|<cell|S<rsub|i><rsup|#>>>|<row|<cell|S<rsub|j><rsup|#>>|<cell|\<nrightarrow\>>|<cell|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>>>>>
+  </eqnarray*>
+
+  On peut aussi le faire dans l'autre sens :
+
+  <\eqnarray*>
+    <tformat|<table|<row|<cell|S<rsub|i><rsup|#>>|<cell|\<rightarrow\>>|<cell|S<rsub|j><rsup|#>>>|<row|<cell|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>>|<cell|\<nrightarrow\>>|<cell|S<rsub|j><rsup|#>>>>>
+  </eqnarray*>
+
+  Si une telle condition est détectée, alors on peut diviser le lieu
+  <math|S<rsub|i><rsup|#>> en deux parties,
+  <math|<around*|\<llbracket\>|c|\<rrbracket\>>S<rsub|i><rsup|#>> et
+  <math|<around*|\<llbracket\>|\<neg\>c|\<rrbracket\>>S<rsub|i><rsup|#>>,
+  c'est-à-dire qu'on pose comme nouvelles définitions
+  <math|d<rsub|1>,\<ldots\>,d<rsub|i-1>,c\<wedge\>d<rsub|i>,\<neg\>c\<wedge\>d<rsub|i>,d<rsub|i+1>,\<ldots\>,d<rsub|n>>.
+  On refait ensuite un point fixe. Notre analyse est en principe plus fine,
+  donc on espère trouver des lieux inacessibles.
+
+  <subparagraph|Observations.>En pratique ça ne marche pas très bien car les
+  rafinements ne sont pas effectués dans le bon ordre. Dans le papier
+  sus-cité, une double analyse en avant et en arrière était utilisée pour
+  trouver l'intersection des valeurs accessibles depuis l'état initial et
+  co-accessibles jusqu'à un état qui provoque une erreur (ie dont la
+  définition est : la propriété est violée), mais nous n'avons pas tenté
+  d'implémenter une telle analyse, qui serait sans doute bien plus précise.
+  Remarquons que l'implémentation de <name|B.Jeannet> pour LUSTRE est
+  disponnible sur sa page web (c'est l'outil NBac).
 
   <section|Implémentation>
 
@@ -1463,13 +1519,20 @@
     logique ; quelques simplifications sur les formules logiques
     (<verbatim|abstract/formula.ml>, <verbatim|abstract/transform.ml>).
 
-    <item>domaine numérique non-relationnel basé sur les intervalles ;
-    domaine relationnel basé sur la bibliothèque externe Apron
-    (<verbatim|abstract/num_domain.ml>, <verbatim|abstract/nonrelational.ml>,
-    <verbatim|abstract/apron_domain.ml>, ...)
+    <item>trois domaines numériques basés sur Apron : intervalles, polyèdres
+    et octogones (<verbatim|abstract/apron_domain.ml>)
+
+    <item>vestige d'une implémentation \S maison \T d'un domaine
+    non-relationnel à base d'intervalles (<verbatim|abstract/num_domain.ml>,
+    <verbatim|abstract/nonrelational.ml>,
+    <verbatim|abstract/value_domain.ml>, <verbatim|abstract/intervals_domain.ml>)
 
-    <item>deux domaines abstraits et analyseur statique correspondant
-    (<verbatim|abstract/abs_interp.ml>, <verbatim|abstract/abs_interp_edd.ml>)
+    <item>deux domaines abstraits à disjonctions et procédures d'analyse
+    statique correspondantes (<verbatim|abstract/abs_interp.ml>,
+    <verbatim|abstract/abs_interp_edd.ml>)
+
+    <item>procédure d'analyse par partitionnement dynamique
+    (<verbatim|abstract/abs_interp_dynpart.ml>)
   </itemize>
 
   En nous basant sur les options de la ligne de commande, nous allons
@@ -1518,8 +1581,10 @@
     en s'appuyant sur le domaine non-relationnel à base d'intervalles pour la
     partie numérique
 
-    <item><verbatim|--ai-rel> : de même mais utilise le domaine abstrait
-    relationnel basé sur Apron (polyèdres) pour la partie numérique
+    <item><verbatim|--ai-poly> : de même mais utilise le domaine abstrait
+    relationnel basé sur les polyèdres d'Apron pour la partie numérique
+
+    <item><verbatim|--ai-oct> : de même mais utilise les octogones
   </itemize>
 
   <paragraph|Options de l'analyse>
@@ -1534,10 +1599,17 @@
     <item><verbatim|--ai-vvci> : affiche encore plus de détails
 
     <item><verbatim|--ai-wd \<less\>n\<gtr\>> : définit un délai pour les
-    opérations de widening (par défaut 5)
+    opérations de widening (par défaut 5). Ce délai est utilisé à deux
+    endroits différents de l'analyse : pour le point fixe local de chaque
+    itération chaotique, et pour le point fixe global des itérations.
 
     <item><verbatim|--disj \<less\>vars\<gtr\>> : variables à utiliser comme
-    variables de disjonction (par défaut : aucune)
+    variables de disjonction (par défaut : aucune). Donner comme argument
+    <verbatim|all> permet d'utiliser toutes les variables énumérées pour les
+    disjonctions. Donner comme argument <strong|<verbatim|last>> permet
+    d'utilsier toutes les variables énumérées qui sont utilisées dans une
+    mémoire. On peut aussi utiliser la syntaxe <verbatim|last+v1,v2,v3> pour
+    rajouter des variables aux variables mémoire.
 
     <item><verbatim|--no-time \<less\>scopes\<gtr\>> : donne un certain
     nombre de scopes pour lesquels ne pas introduire de variable
@@ -1568,8 +1640,10 @@
     utilisant le domaine à base d'EDD et en utilisant les intervalles comme
     domaine de valeurs numériques
 
-    <item><verbatim|--ai-rel-edd> : de même mais utilise le domaine abstrait
-    relationnel basé sur Apron (polyèdres) pour la partie numérique
+    <item><verbatim|--ai-poly-edd> : de même mais utilise le domaine abstrait
+    relationnel basé sur les polyèdres d'Apron pour la partie numérique
+
+    <item><verbatim|--ai-oct-edd> : de même mais utilise les octogones
   </itemize>
 
   <paragraph|Options de l'analyse>
@@ -1590,10 +1664,7 @@
 
   <subsubsection|Analyse par partitionnement dynamique>
 
-  Une troisième forme d'analyse, basée sur un partitionnement dynamique de
-  <math|S<rsup|#>> a été tentée. Celle-ci n'a pas donné de très bons
-  résultats, mais nous indiquons néanmoins son existence ici.
-  L'implémentation existe dans <verbatim|abstract/abs_interp_dynpart.ml>.
+  Cette analyse est implémentée dans <verbatim|abstract/abs_interp_dynpart.ml>.
 
   <paragraph|Modes d'analyse>
 
@@ -1606,7 +1677,7 @@
     utilise des graphes de décision pour représenter les conditions sur les
     énumérées et les intervalles pour la partie numérique
 
-    <item><verbatim|--ai-s-rel-dp>
+    <item><verbatim|--ai-s-rel-dp> : utilise les polyèdres d'Apron
 
     <item><verbatim|--ai-edd-rel-dp>
   </itemize>
@@ -1670,7 +1741,7 @@
     ...) que l'on exécuterait comme pré-processing sur le programme.
   </itemize>
 
-  <section|Références>
+  <section*|Références>
 
   <\itemize>
     <item><name|N.Halbwachs>, <em|About synchronous programming and abstract
@@ -1723,26 +1794,29 @@
     <associate|auto-3|<tuple|2.1|1>>
     <associate|auto-30|<tuple|5.2.3.3|?>>
     <associate|auto-31|<tuple|5.2.5.2|16>>
-    <associate|auto-32|<tuple|6|16>>
-    <associate|auto-33|<tuple|7|?>>
-    <associate|auto-34|<tuple|7.1|?>>
-    <associate|auto-35|<tuple|7.2|?>>
-    <associate|auto-36|<tuple|7.3|?>>
-    <associate|auto-37|<tuple|7.3.1|?>>
-    <associate|auto-38|<tuple|7.3.1.1|?>>
-    <associate|auto-39|<tuple|7.3.1.2|?>>
+    <associate|auto-32|<tuple|5.3|16>>
+    <associate|auto-33|<tuple|5.3.0.3|?>>
+    <associate|auto-34|<tuple|5.3.0.4|?>>
+    <associate|auto-35|<tuple|5.3.0.4.1|?>>
+    <associate|auto-36|<tuple|6|?>>
+    <associate|auto-37|<tuple|6.1|?>>
+    <associate|auto-38|<tuple|6.2|?>>
+    <associate|auto-39|<tuple|6.3|?>>
     <associate|auto-4|<tuple|2.2|2>>
-    <associate|auto-40|<tuple|7.3.2|?>>
-    <associate|auto-41|<tuple|7.3.2.1|?>>
-    <associate|auto-42|<tuple|7.3.2.2|?>>
-    <associate|auto-43|<tuple|7.3.3|?>>
-    <associate|auto-44|<tuple|7.3.3.1|?>>
-    <associate|auto-45|<tuple|7.3.3.2|?>>
-    <associate|auto-46|<tuple|8|?>>
-    <associate|auto-47|<tuple|8.1|?>>
-    <associate|auto-48|<tuple|8.2|?>>
-    <associate|auto-49|<tuple|9|?>>
+    <associate|auto-40|<tuple|6.3.1|?>>
+    <associate|auto-41|<tuple|6.3.1.1|?>>
+    <associate|auto-42|<tuple|6.3.1.2|?>>
+    <associate|auto-43|<tuple|6.3.2|?>>
+    <associate|auto-44|<tuple|6.3.2.1|?>>
+    <associate|auto-45|<tuple|6.3.2.2|?>>
+    <associate|auto-46|<tuple|6.3.3|?>>
+    <associate|auto-47|<tuple|6.3.3.1|?>>
+    <associate|auto-48|<tuple|6.3.3.2|?>>
+    <associate|auto-49|<tuple|7|?>>
     <associate|auto-5|<tuple|2.3|3>>
+    <associate|auto-50|<tuple|7.1|?>>
+    <associate|auto-51|<tuple|7.2|?>>
+    <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|?>>
     <associate|auto-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
@@ -1876,61 +1950,77 @@
       <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-31><vspace|0.15fn>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Implémentation>
-      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Partitionnement
+      dynamique> <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-32><vspace|0.5fn>
 
-      <with|par-left|<quote|1.5fn>|6.1<space|2spc>Parsing et affichage de
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<space|2spc>Implémentation>
+      <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-33><vspace|0.5fn>
+
+      <with|par-left|<quote|1.5fn>|7.1<space|2spc>Parsing et affichage de
       programmes SCADE <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-33>>
+      <no-break><pageref|auto-34>>
 
-      <with|par-left|<quote|1.5fn>|6.2<space|2spc>Interprète SCADE
+      <with|par-left|<quote|1.5fn>|7.2<space|2spc>Interprète SCADE
       <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-34>>
+      <no-break><pageref|auto-35>>
 
-      <with|par-left|<quote|1.5fn>|6.3<space|2spc>Analyse statique par
+      <with|par-left|<quote|1.5fn>|7.3<space|2spc>Analyse statique par
       interprétation abstraite <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-35>>
+      <no-break><pageref|auto-36>>
 
-      <with|par-left|<quote|3fn>|6.3.1<space|2spc>Domaine à disjonctions
+      <with|par-left|<quote|3fn>|7.3.1<space|2spc>Domaine à disjonctions
       simples <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-36>>
+      <no-break><pageref|auto-37>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <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-37><vspace|0.15fn>>
+      <no-break><pageref|auto-38><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <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-38><vspace|0.15fn>>
+      <no-break><pageref|auto-39><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|6.3.2<space|2spc>Domaine à disjonction par
+      <with|par-left|<quote|3fn>|7.3.2<space|2spc>Domaine à disjonction par
       graphe de décision <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-39>>
+      <no-break><pageref|auto-40>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <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-40><vspace|0.15fn>>
+      <no-break><pageref|auto-41><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <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-41><vspace|0.15fn>>
+      <no-break><pageref|auto-42><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|6.3.3<space|2spc>Analyse par partitionnement
+      <with|par-left|<quote|3fn>|7.3.3<space|2spc>Analyse par partitionnement
       dynamique <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-42>>
+      <no-break><pageref|auto-43>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <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-43><vspace|0.15fn>>
+      <no-break><pageref|auto-44><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Paramètres de l'analyse
       <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-44><vspace|0.15fn>>
+      <no-break><pageref|auto-45><vspace|0.15fn>>
+
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|8<space|2spc>Prolongements
+      envisageables> <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-46><vspace|0.5fn>
+
+      <with|par-left|<quote|1.5fn>|8.1<space|2spc>Analyse des propriétés des
+      nombres flottants <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-47>>
+
+      <with|par-left|<quote|1.5fn>|8.2<space|2spc>Analyse de programmes \S
+      taille réelle \T <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-48>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Bibliographie>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|9<space|2spc>Références>
       <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-45><vspace|0.5fn>
+      <no-break><pageref|auto-49><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>
\ No newline at end of file