diff options
| -rw-r--r-- | readme.pdf | bin | 221365 -> 236320 bytes | |||
| -rw-r--r-- | readme.tm | 245 |
2 files changed, 223 insertions, 22 deletions
| Binary files differ @@ -1443,7 +1443,185 @@ <section|Implémentation> - \; + Le projet scade-analyzer propose une implémentation simple des composants + suivants : + + <\itemize> + <item>parser, lexer, typeur pour notre sous-ensemble de SCADE (source des + fichiers dans <verbatim|frontend/>) + + <item>interprète pour la sémantique cocnrète + (<verbatim|interpret/interpret.ml>) + + <item>implémentation de la transformation d'un programme en formule + 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>deux domaines abstraits et analyseur statique correspondant + (<verbatim|abstract/abs_interp.ml>, <verbatim|abstract/abs_interp_edd.ml>) + </itemize> + + En nous basant sur les options de la ligne de commande, nous allons + maintenant décrire les différentes fonctionnalités. + + <subsection|Parsing et affichage de programmes SCADE> + + <\itemize> + <item><verbatim|--dump> : parse un fichier SCADE et le ré-affiche en + sortie + + <item><verbatim|--dump-rn> : parse un fichier SCADE et le ré-affiche en + sortie, après une étape de renommage qui consiste à rendre les noms + unique au sein d'un noeud. Cette passe est implémentée dans + <verbatim|frontend/rename.ml>. + </itemize> + + <subsection|Interprète SCADE> + + <\itemize> + <item><verbatim|--test> : execute le programme SCADE donné en argument, + avec l'interprète <verbatim|interpret/interpret.ml> basé sur la + sémantique à réduction. Le programme doit satisfaire la spécification + suivante : avoir un noeud <verbatim|test> qui servira de racine, ce noeud + devant prendre une unique entrée, <verbatim|i>, qui est un compteur + incrémenté à chaque cycle, et renvoyant trois entiers, <verbatim|a>, + <verbatim|b> et <verbatim|c> (qui seront affichés en sortie), ainsi qu'un + booleen <verbatim|exit> qui indiquera que l'interprète doit terminer. Cf + fichiers dans <verbatim|tests/source/*.scade> pour des exemples. + + <item><verbatim|--vtest> : pareil mais affiche plus de détails (tout le + contenu de la mémoire est affiché à chaque cycle). + </itemize> + + <subsection|Analyse statique par interprétation abstraite> + + <subsubsection|Domaine à disjonctions simples> + + Cette analyse est implémentée dans <verbatim|abstract/abs_interp.ml>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-itv> : fait une passe d'analyse statique par + interprétation abstraite utilisant le domaine à disjonctions simples, et + 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 + </itemize> + + <paragraph|Options de l'analyse> + + <\itemize> + <item><verbatim|--root \<less\>noeud\<gtr\>> : spécifie le noeud racine + dont on veut faire l'analyse (par défaut : <verbatim|test>) + + <item><verbatim|--ai-vci> : affiche des détails sur le contenu de + l'accumulateur à chaque itération + + <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) + + <item><verbatim|--disj \<less\>vars\<gtr\>> : variables à utiliser comme + variables de disjonction (par défaut : aucune) + + <item><verbatim|--no-time \<less\>scopes\<gtr\>> : donne un certain + nombre de scopes pour lesquels ne pas introduire de variable + <verbatim|time> (par défaut <verbatim|all>, c'est-à-dire que + <verbatim|time> n'est jamais introduite). Lorsqu'une variable + <verbatim|time> est introduite, on génère les équations qui font en sorte + que <verbatim|time> soit égal au numéro du cycle depuis le début de + l'exécution du programme. + + <item><verbatim|--init \<less\>scopes\<gtr\>> : donne un certain nombre + de scopes pour lesquels introduire une variable <verbatim|init> (par + défaut <verbatim|all>). Il est envisageable de remplacer la variable + <verbatim|init> de chaque scope par une variable <verbatim|time>, les + disjonctions de cas init/non init se feront alors selon la condition + <math|time=0> ou <math|time\<geqslant\>1>. En ne générant ni variable + <verbatim|time> ni variable <verbatim|init>, la disjonction n'est pas + faite. + </itemize> + + <subsubsection|Domaine à disjonction par graphe de décision> + + Cette analyse est implémentée dans <verbatim|abstract/abs_interp_edd.ml>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-itv-edd> : fait une passe d'analyse statique + 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 + </itemize> + + <paragraph|Options de l'analyse> + + <\itemize> + <item><verbatim|--root> + + <item><verbatim|--ai-vci>, <verbatim|--ai-vvci> + + <item><verbatim|--ai-wd> + + <item><verbatim|--no-time>, <verbatim|--init> + + <item>Non implémenté : paramètre <verbatim|--disj> pouvant intervenir sur + le choix des variables à considérer dans le graphe de décision + (actuellement toutes sont nécessairement considérées). + </itemize> + + <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>. + + <paragraph|Modes d'analyse> + + <\itemize> + <item><verbatim|--ai-s-itv-dp> : analyse par partitionnement dynamique, + utilise un domaine simple non-relationnel pour les valeurs énumérées et + les intervalles pour la partie numérique + + <item><verbatim|--ai-edd-itv-dp> : analyse par partitionnement dynamique, + 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-edd-rel-dp> + </itemize> + + <paragraph|Paramètres de l'analyse> + + <\itemize> + <item><verbatim|--root> + + <item><verbatim|--ai-wd> + + <item><verbatim|--ai-vci>, <verbatim|--ai-vvci> + + <item><verbatim|--no-time>, <verbatim|--init> + + <item><verbatim|--ai-max-dp-depth> : profondeur maximale de + partitionnement + + <item><verbatim|--ai-max-dp-width> : largeur maximale de partitionnement + (ie nombre maximal de parties à considérer) + </itemize> </body> <\initial> @@ -1461,31 +1639,43 @@ <associate|auto-13|<tuple|2.4|6>> <associate|auto-14|<tuple|2.4.1|6>> <associate|auto-15|<tuple|2.4.2|7>> - <associate|auto-16|<tuple|3|8>> + <associate|auto-16|<tuple|3|7>> <associate|auto-17|<tuple|4|8>> <associate|auto-18|<tuple|4.1|8>> <associate|auto-19|<tuple|4.1.1|8>> <associate|auto-2|<tuple|2|1>> <associate|auto-20|<tuple|4.1.2|9>> - <associate|auto-21|<tuple|4.2|10>> + <associate|auto-21|<tuple|4.2|9>> <associate|auto-22|<tuple|5|11>> <associate|auto-23|<tuple|5.1|11>> <associate|auto-24|<tuple|5.2|13>> - <associate|auto-25|<tuple|5.2.1|13>> - <associate|auto-26|<tuple|5.2.2|13>> - <associate|auto-27|<tuple|5.2.3|13>> + <associate|auto-25|<tuple|5.2.1|14>> + <associate|auto-26|<tuple|5.2.2|14>> + <associate|auto-27|<tuple|5.2.3|14>> <associate|auto-28|<tuple|5.2.4|15>> - <associate|auto-29|<tuple|5.2.5|15>> + <associate|auto-29|<tuple|5.2.5|16>> <associate|auto-3|<tuple|2.1|1>> <associate|auto-30|<tuple|5.2.3.3|?>> - <associate|auto-31|<tuple|5.2.5.2|?>> - <associate|auto-32|<tuple|6|?>> + <associate|auto-31|<tuple|5.2.5.2|16>> + <associate|auto-32|<tuple|6|16>> + <associate|auto-33|<tuple|6.1|?>> + <associate|auto-34|<tuple|6.2|?>> + <associate|auto-35|<tuple|6.3|?>> + <associate|auto-36|<tuple|6.3.1|?>> + <associate|auto-37|<tuple|6.3.1.1|?>> + <associate|auto-38|<tuple|6.3.1.2|?>> + <associate|auto-39|<tuple|6.3.2|?>> <associate|auto-4|<tuple|2.2|2>> - <associate|auto-5|<tuple|2.3|2>> + <associate|auto-40|<tuple|6.3.2.1|?>> + <associate|auto-41|<tuple|6.3.2.2|?>> + <associate|auto-42|<tuple|6.3.3|?>> + <associate|auto-43|<tuple|6.3.3.1|?>> + <associate|auto-44|<tuple|6.3.3.2|?>> + <associate|auto-5|<tuple|2.3|3>> <associate|auto-6|<tuple|2.3.1|3>> <associate|auto-7|<tuple|2.3.2|3>> <associate|auto-8|<tuple|2.3.3|3>> - <associate|auto-9|<tuple|2.3.4|3>> + <associate|auto-9|<tuple|2.3.4|4>> </collection> </references> @@ -1584,29 +1774,40 @@ simple <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-23>> - <with|par-left|<quote|1.5fn>|5.2<space|2spc>Domaine à arbre de - disjonctions <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>> + <with|par-left|<quote|1.5fn>|5.2<space|2spc>Domaine à 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-24>> - <with|par-left|<quote|6fn>|Variables et contraintes. + <with|par-left|<quote|3fn>|5.2.1<space|2spc>Variables et contraintes <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-25><vspace|0.15fn>> + <no-break><pageref|auto-25>> - <with|par-left|<quote|6fn>|Domaine numérique. + <with|par-left|<quote|3fn>|5.2.2<space|2spc>Domaine numérique <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-26><vspace|0.15fn>> + <no-break><pageref|auto-26>> - <with|par-left|<quote|6fn>|Les EDD. + <with|par-left|<quote|3fn>|5.2.3<space|2spc>Les EDD <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-27><vspace|0.15fn>> + <no-break><pageref|auto-27>> - <with|par-left|<quote|6fn>|Opérateur de widening. + <with|par-left|<quote|3fn>|5.2.4<space|2spc>Opérateur de widening <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-28><vspace|0.15fn>> + <no-break><pageref|auto-28>> + + <with|par-left|<quote|3fn>|5.2.5<space|2spc><assign|paragraph-numbered|<quote|false>><assign|paragraph-prefix|<quote|<macro|<compound|the-paragraph>.>>><assign|paragraph-nr|<quote|1>><hidden|<tuple>><assign|subparagraph-nr|<quote|0>><flag|table + des matières|dark green|what><assign|auto-nr|<quote|30>><label|auto-30><write|toc|<with|par-left|<quote|6fn>|Itérations + chaotiques. <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-30><vspace|0.15fn>>><no-indent><with|math-font-series|<quote|bold>|font-series|<quote|bold>|<vspace*|0.5fn>Itérations + chaotiques.<space|2spc>> <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-30>> <with|par-left|<quote|6fn>|Itérations chaotiques. <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-29><vspace|0.15fn>> + <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>> + <no-break><pageref|auto-32><vspace|0.5fn> </associate> </collection> </auxiliary>
\ No newline at end of file |