summaryrefslogtreecommitdiff
path: root/doc/readme.tm
diff options
context:
space:
mode:
Diffstat (limited to 'doc/readme.tm')
-rw-r--r--doc/readme.tm224
1 files changed, 157 insertions, 67 deletions
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
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-19 16:38:40 +0000