summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-16 15:50:02 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-16 15:50:02 +0200
commitbebab48e94ad156341f12fe90224e67e98477ca8 (patch)
tree0282cb54a9f40feef0979a8a63b89e6e7e2d0d97
parent2c9a9bd84bd4da750b6baf8e08ca3fdde5c63247 (diff)
downloadscade-analyzer-bebab48e94ad156341f12fe90224e67e98477ca8.tar.gz
scade-analyzer-bebab48e94ad156341f12fe90224e67e98477ca8.zip
More doc : command lien options;
-rw-r--r--readme.pdfbin221365 -> 236320 bytes
-rw-r--r--readme.tm245
2 files changed, 223 insertions, 22 deletions
diff --git a/readme.pdf b/readme.pdf
index c97712f..4a97029 100644
--- a/readme.pdf
+++ b/readme.pdf
Binary files differ
diff --git a/readme.tm b/readme.tm
index c7a0b2f..0d6388c 100644
--- a/readme.tm
+++ b/readme.tm
@@ -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