diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/readme.pdf | bin | 236320 -> 263955 bytes | |||
| -rw-r--r-- | doc/readme.tm | 224 |
2 files changed, 157 insertions, 67 deletions
diff --git a/doc/readme.pdf b/doc/readme.pdf Binary files differindex 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 |