From f55d48487697c358b8d3a3fa9c90f3f61596ba53 Mon Sep 17 00:00:00 2001 From: Alex Auvolat Date: Tue, 15 Jul 2014 18:05:47 +0200 Subject: Begin redaction of README. --- readme.pdf | Bin 0 -> 211011 bytes readme.tm | 1560 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 1560 insertions(+) create mode 100644 readme.pdf create mode 100644 readme.tm diff --git a/readme.pdf b/readme.pdf new file mode 100644 index 0000000..a0d4280 Binary files /dev/null and b/readme.pdf differ diff --git a/readme.tm b/readme.tm new file mode 100644 index 0000000..2f0e33f --- /dev/null +++ b/readme.tm @@ -0,0 +1,1560 @@ + + + + +<\body> + |> + + + + Le projet consiste en la réalisation d'un analyseur statique pour des + programmes SCADE, utilisant l'interprétation abstraite comme base de + travail. Les objectifs attendus sont : + + <\itemize> + Preuve de propriétés de sûreté sur des programmes + + Étude d'intervalles de variation pour des variables + + + L'expérience a été menée sur un sous-ensemble très restreint du langage + SCADE, comportant notamment : + + <\itemize> + noyau dataflow (opérations arithmétiques élémentaires, opérateurs + > et ), pas de prise en charge des + horloges explicites (primitves , , ...) + + blocs + + automates simples, à transitions faibles seulement, sans actions + sur les transitions (les transitions de type sont + prises en compte) + + + Dans ce document nous metterons au clair les points suivants : + + <\enumerate> + Spécification du sous-ensemble de SCADE considéré + + Explication du fonctionnement de l'interprète pour la sémantique + concrète + + Explication de la traduction d'un programme SCADE en une formule + logique représentant le cycle du programme + + Explications sur l'interprétation abstraite en général, sur les + domaines numériques, sur la recherche de points fixe + + Explications sur notre adaptation de ces principes à l'analyse du + langage SCADE, en particulier : + + <\itemize> + itérations chaotiques + + domaines capables de faire des disjonctions de cas (graphes de + décision) + + + + + + + + <\verbatim-code> + <\verbatim> + decl \ \ \ := CONST id: type = expr; + + \ \ \ \ \ \ \ \ \ \| NODE (var_def;*) RETURNS (var_def;*) VAR var_def;* + body + + var_def := (PROBE? id),* : type + + body \ \ \ := LET eqn;* TEL + + \ \ \ \ \ \ \ \ \ \| eqn; + + type \ \ \ := INT \| BOOL \| REAL \| (TYPE,+) + + eqn \ \ \ \ := id = expr + + \ \ \ \ \ \ \ \ \ \| GUARANTEE id : expr + + \ \ \ \ \ \ \ \ \ \| ASSUME id : expr + + \ \ \ \ \ \ \ \ \ \| AUTOMATON state* RETURNS id,* + + \ \ \ \ \ \ \ \ \ \| ACTIVATE scope_if RETURNS id,* + + scope_if := (VAR var_def;*)? body + + \ \ \ \ \ \ \ \ \ \| IF expr THEN scope_if ELSE scope_if + + state \ \ \ := INITIAL? STATE id + + \ \ \ \ \ \ \ \ \ \ \ \ \ body + + \ \ \ \ \ \ \ \ \ \ \ \ \ until* + + until \ \ \ := UNTIL IF expr (RESUME\|RESTART) id + + expr \ \ \ \ := int_const \| real_const \| TRUE \| FALSE \| id + + \ \ \ \ \ \ \ \ \ \ \| unary_op expr \| expr bin_op expr + + \ \ \ \ \ \ \ \ \ \ \| IF expr THEN expr ELSE expr + + \ \ \ \ \ \ \ \ \ \ \| id ( expr,* ) + + unary_op := - \| PRE \| NOT + + bin_op \ \ := + \| - \| * \| / \| -\ \| AND \| OR \| MOD + + + \ \ \ \ \ \ \ \ \ \ \| = \| \\ \| \ \| \ \| + \= \| \= + + + + + Pour simplifier, on considère dans cette section que tous les noeuds ont + été inlinés. + + On note > l'ensemble des variables définies dans le texte du + programme, et on note > l'ensemble des valeurs qui peuvent + être prises. + + Un environnement de valeurs est une fonction + \\> qui décrit un état de la mémoire + du programme. On définit aussi un sous-ensemble + \\> de variables dont les valeurs + sont des entrées du système. + + L'exécution d'un programme est une séquence d'états mémoire + \,s,\,s,\> + conforme à la spécification du programme et à une série d'entrées. On note + : + + <\equation*> + s|i>s|i>s\\ + + + Dans la sémantique par traduction, la sémantique d'un programme est définie + par traduction du programme en une formule logique telle + que : + + <\eqnarray*> + |i>s>|>|x\\,s=i>>|,s|)>>>>>>>>>> + + + Dans la sémantique par réduction, la sémantique d'un programme est définie + par un ensemble de règles de réduction qui aboutissent à + + <\eqnarray*> + |i>s>|>|\i|s\s>>>>> + + + Pour un programme bien typé, étant donné > et + >, il existe un unique état > qui remplit la + condition. + + Pour traduire l'init et le reset, on introduit dans chaque scope + > plusieurs variables : + + <\itemize> + >> : indique que le scope devra être + reset lors du prochain cycle + + >> : indique que le scope est à l'état + initial dans ce cycle + + >> : indique qu'un scope est actif dans + ce cycle + + + Un nouveau scope est introduit dans chaque body d'un bloc activate ou d'un + état d'automate. + + De même, les automates introduisent deux variables :\ + + <\itemize> + >, qui définit l'état de l'automate à ce cycle + + >, qui définit l'état de l'automate au cycle + suivant, en supposant qu'il n'y a pas de reset du scope où l'automate est + défini + + + L'état > est défini par |)>=true>, + où est le scope racine englobant tout le programme ; toutes les + autres variables de > pouvant prendre n'importe quelle + valeur. + + On suppose que chaque instance de est numérotée, et pour + chaque e>, on introduit la variable > qui + enregistre la valeur de dans l'état et qui sert de mémoire pour le + pre. + + Par la suite, que ce soit dans l'étude de la sémantique par réduction ou + par traduction, on notera toujours la mémoire (c'est-à-dire + >) et l'état courant (c'est-à-dire + >, sur lequel on travaille). + + + + On définit notre ensemble d'environnements comme étant + \\\|}>>, la + valeur > signifiant qu'une variable n'a pas encore pris sa + valeur. + + Pour chaque élément de programme, on va introduire un certain nombre de + règles de réduction. On applique ces règles jusqu'à en déduire + s>, avec x\\,s\\>. + + Les déductions de la forme s> signifient ``avec la + mémoire , on peut déduire du système l'état (partiel) ''. + Les déductions de la forme e\>v> + signifient ``avec la mémoire et l'état partiellement calculé + , l'expression calculée dans le scope > + prend la valeur ''. + + + + On note les entrées du système à ce cycle ; on fait par définition + l'hypothèse i>, c'est-à-dire qu'on peut obtenir + l'environnement où seules les variables d'entrée sont définies. On + introduit ensuite la règle suivante, qui dit que le scope racine est + toujours actif et jamais reset par la suite : + + <\equation*> + s|l\s\t|]>\f|]>> + + + \; + + + + Pour tout scope > défini dans le programme, qui est reset si + et seulement si la condition r> est vraie, on rajoute les + règles de réduction suivantes qui permettent de déterminer si le scope est + init ou pas : + + <\equation*> + s>||r>>>>>>|l\s>\t|]>> + + + <\equation*> + s>||\r>>||>|)>=t>>>>>|l\s>\f|]>> + + + <\equation*> + s>||\r>>||>|)>=f>>>>>|l\s>\l>|)>|]>> + + + \; + + En particulier, pour le scope racine on instancie ces règles avec + r|)>\l|)>=t> + + + + Ces règles permettent d'exprimer le calcul d'une expression. On note + > le scope dans lequel l'expression est évaluée. + + <\equation*> + c\>c>,c\\ + + + <\equation*> + \\|l,s\x\>s>,x\\ + + + <\equation*> + pre e\>l|)>> + + + <\equation*> + e\>v>||e\>v>>>>>|l,s\e\e\>v\v> + + + <\equation*> + >|)>=t>||e\>v>>>>>|l,s\\e|)>\>v> + + + <\equation*> + >|)>=f>||e\>v>>>>>|l,s\\e|)>\>v> + + + <\equation*> + etc\ + + + + + Pour chaque expression e> introduite dans le scope + >, on donne les deux règles suivante : + + <\equation*> + s>||>|)>=t>||e\>v>>>>>|l\s\v|]>> + + + <\equation*> + s>||>|)>=f>>>>>|l\s\l|)>|]>> + + + + + Pour toute affectation apparaissant dans le scope + >, on donne la règle suivante : + + <\equation*> + s>||>|)>=t>||e\>v>>>>>|l\sv|]>> + + + + + Pour tout bloc else b> + apparaissant dans le scope >, on crée deux nouveaux scopes + > et > dans lesquels on + rajoute les règles de réductions pour > et > + respectivement, et on rajoute les règles suivantes qui régissent + l'activation des deux scopes > et + > : + + <\equation*> + s>||>|)>=f>>>>>|l\s>\f|]>>\f|]>> + + + <\equation*> + s>||>|)>=t>||c\>t>>>>>|l\s>\t|]>>\f|]>> + + + <\equation*> + s>||>|)>=t>||c\>f>>>>>|l\s>\f|]>>\t|]>> + + + Les deux scopes > et > + héritent de la condition de reset du scope >. + + + + On note l'automate, > son état initial. Les règles + d'activation des différents scopes des états se font en fonction de la + variable > définie pour l'automate comme suit : + + <\equation*> + s>||r>>>>>>|l\s=s|]>> + + + <\equation*> + s>||\r>>>>>>|l\s=l|)>|]>> + + + Puis pour chaque état >, on définit > + son scope dans lequel on traduit son corps, puis on rajoute la règle + d'activation suivante : + + <\equation*> + s>|||)>=s>>>>>|l\s>=t|]>> + + + <\equation*> + s>|||)>\s>>>>>|l\s>=f|]>> + + + Dans tous les scopes >, la condition de reset peut + être éventuellement augmentée d'un > avec une condition du + type >|)>=t>, où la variable + >> est mise à true dès que l'on emprunte + une transition qui reset, et à false le reste du temps. + + La règle pour une transition |c>s> + sont du style : + + <\equation*> + s>|||)>=s>||c\>t>>>>>|l\s\s|]>> + + + À cela, il faut rajouter les conditions qui disent que l'on emprune + exactement une transition à chaque cycle, ainsi que la partie qui définit + les variables >>. + + <\example> + On va écrire les règles de réduction qui définissent le programme suivant + : + + <\verbatim-code> + node half() returns(c: int) + + var half: bool; + + \ \ \ \ a, b: int; + + \ \ \ \ la, lb: int; + + let + + \ \ half = true -\ not pre half; + + \ \ activate + + \ \ \ \ if half then let + + \ \ \ \ \ \ \ \ a = la + 1; + + \ \ \ \ \ \ \ \ b = lb; + + \ \ \ \ tel else let + + \ \ \ \ \ \ \ \ a = la; + + \ \ \ \ \ \ \ \ b = lb + 1; + + \ \ \ \ tel + + \ \ returns a, b; + + \ \ la = 0 -\ pre a; + + \ \ lb = 0 -\ pre b; + + \ \ c = a - b; + + tel + + + Les règles de calcul des expressions sont tout le temps les mêmes. Les + règles déduites de la structure du programme sont les suivantes : + + Initialisation : + + <\equation*> + s|l\s\t|]>\f|]>> + + + <\equation*> + s + >|||)>=t>>>>>|l\s>\t|]>> + + + <\equation*> + s + >|||)>=f>|||)>=t>>>>>|l\s\f|]>> + + + <\equation*> + s + >|||)>=f>|||)>=f>>>>>|l\s\l|)>|]>> + + + Affectation : + + <\equation*> + s>|||)>=t>||a-b\v>>>>>|l\sv|]>> + + + Affectations de > et : + + <\equation*> + s>|||)>=t>||pre|)> + a\v>>>>>|l\sv|]>> + + + <\equation*> + s>|||)>=t>||pre + b|)>\v>>>>>|l\sv|]>> + + + Affectation de : + + <\equation*> + s>|||)>=t>||not + pre half|)>\v>>>>>|l\sv|]>> + + + Mémorisation des valeurs pour , et + : + + <\equation*> + s>|||)>=t>||a\v>>>>>|l\s\v|]>> + + + <\equation*> + s>|||)>=t>||b\v>>>>>|l\s\v|]>> + + + <\equation*> + s>|||)>=t>||half\v>>>>>|l\s\v|]>> + + + <\equation*> + s>|||)>=f>>>>>|l\s\l|)>|]>> + + + <\equation*> + s>|||)>=f>>>>>|l\s\l|)>|]>> + + + <\equation*> + s>|||)>=f>>>>>|l\s\l|)>|]>> + + + Activation des deux moitiés du activate : + + <\equation*> + s>|||)>=t>||half\t>>>>>|l\s:=t|]>\f|]>> + + + <\equation*> + s>|||)>=t>||half\f>>>>>|l\s:=f|]>\t|]>> + + + <\equation*> + s>|||)>=f>>>>>|l\s:=f|]>\f|]>> + + + Affectation de et dans la première moitié : + + <\equation*> + s>|||)>=t>||la+1\v>>>>>|l\sv|]>> + + + <\equation*> + s>|||)>=t>||lb\v>>>>>|l\sv|]>> + + + Et dans la deuxième moitié : + + <\equation*> + s>|||)>=t>||la\v>>>>>|l\sv|]>> + + + <\equation*> + s>|||)>=t>||lb+1\v>>>>>|l\sv|]>> + + + Et c'est tout. + + + (il faudrait faire un exemple avec des automates, mais ça risque d'être + encore plus long !) + + + + On définit la traduction de en une formule + > comme suit. + + + + On utilise des formules ``à trous'' pour faire la traduction. Un trou + > correspond à la fonction e>, une formule + x=\> correspond à la fonction + a\x=e>, etc. L'argument d'une fonction trou peut + aussi être un couple d'expressions, ainsi + +\> correspond à la fonction + \e+f>. + + On définit la fonction ,e,w|)>> comme étant la + traduction de l'expression considérée dans le scope + > et devant être placée dans le trou . En pratique, + on divise en deux fonctions, une pour les expressions booléennes + et une pour les expressions numériques. Le résultat d'une traduction doit + généralement être une formule booléenne. + + On note > n'importe quel opérateur binaire : + ,/,mod,\,\,\,\,=,\,\,\>. + + Les règles sont les suivantes : + + <\eqnarray*> + ,,e,\,e|)>,w|)>>||,e,\|)>,\,T,e,\|)>|]>>>|c\\,T,c,w|)>>||>>|x\\,T,x,w|)>>|||]>>>|,pre + e,w|)>>|||)>|]>>>|,e\e,w|)>>||>|)>\T,e,w|)>|)>\s>|)>\T,e,w|)>|)>>>|,e\e,w|)>>||,,e|)>,w\\|]>|)>>>|,if + c then e else e,w|)>>||,c,\|)>\T,e,w|)>|)>\T,c,\|)>\T,e,w|)>|)>>>|,-e,w|)>>||,e,w|]>|)>>>|,\e,w|)>>||,e,w\|]>|)>>>>> + + + Par la suite, une affectation sera traduite par la formule + booléenne ,e,x=\|)>>. + + <\example> + Effectuons par exemple la traduction de 0 then y + else -y> : + + <\eqnarray*> + ||,if + y\0 then y else -y,x=\|)>>>|||,y\0,\|)>\T,y,x=\|)>|)>\T,y\0,\|)>\T,-y,x=\|)>|)>>>|||0\x=y|)>\0|)>\x=-y|)>>>>> + + + + <\example> + Effectuons la traduction de pre x + 1>. + + <\eqnarray*> + ||,0\prex + + 1,s=\|)>>>|||>|)>\T,0,s=\|)>|)>\s>|)>\T,prex + + 1,s=\|)>|)>>>|||>|)>\s=0|)>\s>|)>\T,x,1|)>,s=\+\|)>|)>>>|||>|)>\s=0|)>\s>|)>\=\+\|)>,prex,\|)>,T,1,\|)>|)>|)>>>|||>|)>\s=0|)>\s>|)>\=\+\|)>|)>,1|)>|)>>>|||>|)>\s=0|)>\s>|)>\s=l|)>+1|)>>>>> + + + Remarque : dans une étape à part, il faut penser à mémoriser une valeur + pour >, c'est-à-dire à introduire l'équation + |)>=s> + + + + + On définit une traduction complète pour les programmes, en pensant à + introduire les équations de persistance de la mémoire pour les pre. On + introduit aussi des équations qui déterminent si un scope est actif ou + inactif, si il est init ou pas, si il doit être reset ou pas, en fonction + des divers paramètres du programme (états d'automates, conditions de blocs + activate). De manière générale, un scope a deux traductions qui sont + produites : une pour le cas où ce scope est actif, et une pour le cas où il + est inactif (dans le cas inactif, il s'agit simplement de perpétuer les + mémoires). Ainsi la traduction d'un bloc `` else b>'' sera du style + T|)>\T|)>|)>\c\T|)>\T|)>|)>>. + + Tout cela est long à écrire, aussi nous nous contenterons de donner un + exemples. + + <\example> + Traduction du programme : + + <\verbatim-code> + node test() returns(x: int) + + var lx: int; + + let + + \ \ lx = 0 -\ pre x; + + \ \ x = if lx \= 5 then 0 else lx + 1; + + tel + + + On obtient la formule : + + <\eqnarray*> + ||>||||||)>\s|)>>>|>|l|)>\|||)>\\s|)>>>|>|l|)>\s|)>=l|)>>>>>>|)>>>>>>|)>>>||>||)>>>||>|s|)>>>||>||)>\s=0|)>\s|)>\s=l|)>|)>>>||>|\5\s=0|)>\\5\s=s+1|)>>>||>||)>=s>>>> + + + + Pour d'autres traductions, voir les sorties produites par + . + + + + Une première façon de faire un interprète pour la sémantique concrète + serait de faire un interprète de formules logiques, et d'appliquer la + formule obtenue par traduction répétitivement jusqu'à obtenir un point + fixe. + + Ce n'est cependant pas cette solution que nous avons choisi de mettre en + place, notre solution est plus proche de la sémantique par réduction + définie plus haut. + + Nous avons choisi de représenter un état du programme en cours de + calcul comme une valeur mutables, où les variables sont calculées au fur et + à mesure qu'on les demande. La structure peut donc contenir à un + instant donné pour une certaine variable soit une valeur, soit une fonction + à appeller pour que cette valeur soit calculée et rajoutée à . + + La procédure de calcul consiste à activer le scope racine, puis à appeller + les fonctions de calcul sur les variables de sortie jusqu'à ce qu'on + obtienne des valeurs. On enregistre ensuite la portion d'état qui nous + intéresse pour le cycle suivant. + + L'activation d'un scope se fait selon la procédure suivante : + + <\itemize> + Pour une affectation , rajouter dans pour la + variable la fonction qui calcule et rajoute la valeur + trouvée dans . + + Pour un bloc activate, rajouter dans pour toutes les + variables returnées par le bloc, la fonction qui choisit la branche à + activer en calculant les conditions et active le scope correspondant. + + Pour un automate, rajouter dans pour toutes les variables + returnées par l'automate, la fonction qui choisit l'état à activer en se + basant sur l'état enregistré au cycle précédent, et active le scope + correspondant. + + + L'étape d'enregistrement des variables d'intérêt pour le cycle suivant + comporte notamment une phase de calcul des transitions faibles empruntées + par les automates du programme, pour qu'à l'étape suivante le calcul puisse + reprendre directement. Les restart sont aussi traités à ce moment là, avec + une fonction pour reset un scope qui remet toutes les variables init à true + et tous les états à l'état initial, récursivement. + + + + \; + + > + > + + \; + + \; + + Le but de l'interprétation abstraite est de prouver certaines propriétés + sur un programme. Pour cela, nous passons par une première approximation, + la sémantique collectrice, que nous approximons une seconde fois en la + passant dans un domaine de représentation abstraite. + + + + + + Notons > l'ensemble des variables. On note + =\\\> : c'est l'union + des variables de type énumération et des variables de \ type numérique. + + Un état du système est une fonction \\>, + où > représente l'ensemble des valeurs (numériques ou + énumération). On note =\\\> + l'ensemble des états du système. + + Avant le premier cycle, le système peut être dans n'importe quel état de + : + + <\eqnarray*> + ||\ + \| s|)>=t|}>>>>> + + + Entre deux cycles, les variables qui comptent réellement dans sont + les variables actif et reset pour les scopes, les variables d'état pour les + automates, et les valeurs des . + + Vision habituelle : on a une suite d'états + ,s,\> qui représentent la mémoire entre deux + cycles. > est défini. On a une relation de transition qui + prend > et les entrées > et qui calcule les + sorties > et l'état suivant > : + + <\equation*> + s|i>o,s|i>o,s|i>o,s\*\* + + + Nous introduisons ici une seconde notation pour ce fonctionnement. + + Les variables de l'état précédent >, au lieu d'être + considérées comme un lieu à part, sont partiellement copiées dans l'état + > par une fonction que l'on appellera fonction de cycle. + Cette fonction copie uniquement les variables dont les valeurs précédentes + sont utiles pour le calcul de la transition, et préfixe leur noms d'un + prefixe standard, ``L'', qui indique que ce sont des variables , + c'est-à-dire qu'on a leur valeur du cycle précédent. + + La fonction de cycle \\|)>> + s'occupe de faire passer les valeurs suivantes aux valeurs actuelles (nous + écrivons cette fonction comme non-déterministe car après cette fonction un + certain nombre de variables sont oubliées et on considère que leurs valeurs + n'ont pas d'importance). Elle peut être définie à partir d'un ensembles de + variables , qui sont les variables qui nous intéresseront lors du + calcul de la transition : + + <\eqnarray*> + >||\\ + \| \x\C,s=s|}>>>>> + + + \; + + Déroulement d'un cycle : on prend l'état après passage par la + fonction de cycle, on y met les valeurs des entrées du système. On applique + ensuite la fonction \\> qui calcule + toutes les variables du système (elle peut être définie comme la saturation + de la sémantique par réduction, comme le point fixe de l'application d'une + formule, ou plus classiquement comme l'application d'une série + d'instructions en style impératif, résultat de la compilation du + programme). On peut à ce moment récupérer les valeurs de sorties. + + Avec nos notations : > est la restriction de + |)>+i|)>> aux variables de + sortie , où |)>+i> correspond à + définir les variables de |)>> et de + >. + + <\remark> + En principe, quel que soit c|)>>, + |)>> ne peut être qu'un seul + environnement, car le programme est déterministe. C'est pourquoi on se + permet l'abus de notation |)>+i|)>>. + + + + + On s'intéresse maintenant à l'exécution d'un programme SCADE quel que + soient ses entrées >. On peut faire des hypothèses sur ces + entrées en utilisant la directive du langage. On suppose + que l'on dispose d'une fonction \> qui nous dit si un environnement + est conforme à la spécification. + + On s'intéresse maintenant à la sémantique non déterministe suivante : + + <\eqnarray*> + >||\ + \| s|)>=t|}>>>|>|||)>>>|>||x>,a\c,q|)>=t|}>>>>> + + + \; + + La valeur > contient tous les environnements possibles pour + le système à la -ème étape, quelles que soient les entrées jusque + là. + + On définit maintenant la sémantique collectrice du programme comme étant la + valeur : + + <\eqnarray*> + ||> + s.s\g|)>>>||>||)>>>>> + + + représente ici exactement l'ensemble de tous les états accessibles + par le système, à tout moment, quelles que soient les valeurs en entrée. + + Toute la suite de notre travail consistera à construire une approximation + la meilleure possible de . + + + + Une abstraction est définie par une correspondance de Galois entre + |)>> et >, + représentation abstraite d'une partie de >. L'abstraction + peut être caractérisée par sa fonction de concrétisation : + + <\eqnarray*> + >>||\\|)>>>>> + + + \ On peut aussi généralement s'appuyer sur l'existence d'une + fonction d'abstraction : + + <\eqnarray*> + >>|||)>\\>>>> + + + Cette fonction fait correspondre à une partie de > sa + meilleure approximation dans le domaine abstrait (par exemple dans le cas + des polyhèdres, l'abstraction d'un ensemble fini de points est leur + enveloppe convexe, mais un cercle n'a pas de meilleure abstraction). + + Dans tous les cas, on s'attend à ce que + x\\,x\\|)>> + d'une part et y\\|)>,y\\|)>> + d'autre part. + + De base ici, nous avons deux choix simples pour > : + les intervalles et les polyhèdres convexes. Ceux-ci sont considérés acquis + pour la suite ; on les note > et + >, avec les fonctions de concrétisation + > et > associées. + + On note > l'ensemble des égalités et inégalités sur des + variables de >. Par exemple les éléments suivants sont des + équations de > : 5*x-2>. + + Pour \> et \>, on note + e> si l'expression est vraie dans l'état . + + Pour un domaine abstrait > et pour une expression + \>, on suppose que l'on a une fonction sémantique + |e|\> : + \\\> qui restreint + l'abstraction > en une sur-approximation (la meilleure + possible) de \|)> + \| s\e|}>|)>> : + + <\eqnarray*> + \|)> + \| s\e|}>>|>||e|\>|)>|)>>>>> + + + La fonction de transition est représentée dans l'abstrait par une + fonction > qui correspond à l'application d'un certain + nombre de contraintes de >, ainsi que de disjonction de cas. + On remarque que l'aspect impératif disparait complètement, on n'a plus + qu'un ensemble d'équations et de disjonctions. La traduction du programme + SCADE en formule logique donne directement une formule de ce style que l'on + peut appliquer sur un environnement abstrait. + + La fonction de cycle correspond à conserver un certain nombre de + variables en tant que \S mémoires \T, en préfixant leur noms d'un \S L \T + pour . Notons l'ensemble des variables à conserver. Cette + fonction peut être représentée dans l'abstrait par l'opérateur + > dont une définition est : + + <\eqnarray*> + >||\\ + \| \x\C,\\\\\|\=\|}>|)>>>>> + + + (cette définition n'est pas constructive car on n'implémente jamais + > directement) + + Cela correspond à oublier un certain nombre de variables qui ne nous + intéressent plus, et à renommer celles que l'on garde. + + Par facilité, on note =c\f>. Étant + donné qu'un programme est essentiellement une grosse boucle, la valeur qui + nous intéresse est l'abstraction de donnée par : + + <\eqnarray*> + >||>i.I\g|)>>>>> + + + Où > est l'état initial du système et est défini par + =|i|\>|)>>, + où est une équation du type =tt>. + + Nous en venons donc à chercher des domaines abstraits les mieux à même de + représenter les différentes contraintes exprimables dans >. + Dans notre cas, celles-ci se divisent essentiellement en deux catégories : + + <\itemize> + Contraintes numériques : les variables sont dans + >, les constantes dans > (ou + >), les opérateurs sont + ,\,=,\,\>. On note + > l'ensemble de telles contraintes. + + Contraintes énumérées : les variables sont dans + >, les constantes dans un ensemble fini qui dépend + du types des variables, les opérateurs sont ,\>. + On note > l'ensemble de telles contraintes. + + + Les domaines numériques > et + > ne sont pas à même de représenter + correctement les contraintes de >. Généralement, on + définit : + + <\eqnarray*> + e\\\,|e|\>>||>>>|e\\,|e|\>>||>>>>> + + + Les variables booléennes peuvent être représentées par et + , par exemple on peut introduire les restrictions suivantes (en + notant > l'ensemble des variables à valeurs + booléennes) : + + <\eqnarray*> + x\\,|x=tt|\>>|||x=1|\>>>|x\\,|x=ff|\>>|||x=0|\>>>|x,y\\,|x=y|\>>|||x=y|\>>>|x,y\\,|x\y|\>>|||x=1-y|\>>>>> + + + Les résultats sont généralement plus que médiocres. De plus, on ne peut pas + représenter ainsi les valeurs d'énumérations ayant plus de deux éléments. + + + + Pour l'analyse de programmes SCADE, l'analyse de l'ensemble de la boucle de + contrôle comme une seule valeur dans un environnement abstrait numérique + est insuffisante. Il nous a donc été crucial de développer deux domaines + abstraits capables de faire des disjonctions de cas afin de traiter de + manière plus fine l'évolution du programme. + + Nous souhaitons pouvoir faire des disjonctions de cas selons les valeurs + des variables de >. Par exemple si on a un automate + dont la variable d'état s'appelle et évolue dans + l'ensemble >, on voudrait + pouvoir isoler cette variable des autres, ne plus l'inclure dans le domaine + abstrait et l'utiliser pour différencier plusieurs valeurs abstraites. Il + nous faut donc redéfinir le domaine abstrait > et surtout la + fonction d'application d'une condition |e|\>>. + + + + Supposons que l'on ait maintenant trois ensembles de variables : + + <\itemize> + > : variables numériques + + > : variables énumérées non considérées + comme variables de disjonction + + > : variables de disjonction, prenant leurs + valeurs dans > un ensemble fini (pour être précis, + il faudrait noter x\\>, + > l'ensemble des valeurs possibles + pour la valeur , qui peut être différent selon la variable - on + est ammené à faire un peu de typage, il faut en particulier s'assurer que + les contraintes que l'on donne sont entre deux variables pouvant prendre + les mêmes valeurs). + + + On considère dans cette section que l'on a un domaine abstrait + > capable de gérer les contraintes sur les variables + numériques et sur les variables énumérées, mais sans relation entre les + deux. Le domaine > représente une abstraction de + =\\|)>\\>. + On note > et > les éléments + bottom et top de ce treillis, > et + > les bornes inf et sup de ce treillis. + + La particularité des variables d'état est que l'on ne réalise pas + d'abstraction sur celles-ci : on représente directement un état par une + valuation de ces variables, dans \\=\>. + On peut le munir d'une structure de treillis : + \,\|}>> forme un + treillis plat : x,y\\,x\y\x=y>, + x\\,\\x\\> + (l'utilité de cette structure n'apparait pas.) + + On appelle toujours =\\\>, où + =\\\\\>. + On a une injection évidente de > dans + |)>>, on identifie donc + \> à \\|\x\\,s=\|}>>. + De même on identifie \> à + \ \| \x\\\\,s=\|}>>. + + On construit maintenant le domaine abstrait disjonctif comme suit : + + <\eqnarray*> + >||\\>>|>||\>d\\|)>>>>> + + + Les éléments > et > sont définis comme suit : + + <\eqnarray*> + >||d.\>>|>||d.\>>>> + + + On vérifie bien que |)>=\> + et |)>=\>. + + On peut aussi définir les opérations > et > : + + <\eqnarray*> + t>||d.\t|)>>>|t>||d.\t|)>>>>> + + + Enfin, la partie intéressante : on peut définir un certain nombres + d'opérateurs de restriction : + + <\itemize> + x,y\\,\s\\>, + + <\eqnarray*> + |x=y|\>>||d.>|=d>>|>|>>>>>>||x\y|\>>||d.>|\d>>|>|>>>>>>>> + + + x\\,\v\\>, + + <\eqnarray*> + |x=v|\>>||d.>|=v>>|>|>>>>>>||x\v|\>>||d.>|\v>>|>|>>>>>>>> + + + + |e|\>> est donc défini correctement + pour tout \>, où > est + l'ensemble des conditions sur variables de disjonction. Pour toute + expression \> ou + \>, le domaine > est + sensé savoir les prendre en compte de manière satisfaisante, on définit + donc : + + <\eqnarray*> + e\\\\,|e|\>>||d.|e|\>|)>>>>> + + + L'opérateur de widening reste problématique. On peut définir un opérateur + de widening point par point : + + <\eqnarray*> + + t>||d.s\t>>>> + + + Mais celui-ci est peu satisfaisant car chaque état + \> représente potentiellement un état d'un + système de transitions, pouvant déboucher sur lui-même ou sur un autre + état, et il faut savoir prendre en compte ces disjonctions à un niveau plus + fin. Il faut donc plutôt voir le tout comme un système de transitions. + + Étant donné notre système représenté par une fonction de transition + > et une fonction de cycle > (par facilité, + on notera =c\f>), l'ensemble des + états accessible par le système est =lfp>s.I\g|)>>, + où =|i|\>|)>>. + + Définitions : pour \\>, notons + > : \\\> + tel que >=\d.>|d>>|>|>>>>>> + + Le principe des itérations chaotiques peut s'écrire comme suit : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>>> + + + Tant que \\>, on répète le + processus suivant : + + <\eqnarray*> + >|>| + >>|>||>|)>|)>>>|>||\D>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + Intuitivement : > représente l'ensemble des états + possibles pour notre système de transition. À chaque itération, on choisit + un état qui a grossi depuis la dernière fois. On calcule ses successeurs et + on met à jour l'ensemble des états que l'on connait. + + Problème : ici on ne fait pas de widening, et on peut être à peu près sûr + que l'analyse ne terminera pas (sauf cas simples). Pour cela, on introduit + un ensemble >\\> qui + représente l'ensemble des états que l'on devra faire grossir par widening + et non par union simple dans le futur. La définition devient alors : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>|,0>>||>>>> + + + <\eqnarray*> + >|>| + >>|>||>|)>|)>>>|>||d.\D>|K,n>>>|\D>|>>>>>>|,n+1>>||,n>\\\| + s\\\s\s|}>>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + Ie : si un état est apparu à une étape, et si à une étape ultérieure il + grossit, alors lors de toutes les étapes suivantes on le fera grossir non + pas par union simple mais par élargissement. + + Reste une question : comment prendre en compte les conditions de boucle qui + permettent de réduire le domaine abstrait ? La définition précédente n'est + peut-être pas la bonne, car elle risque d'appliquer des élargissements que + l'on ne sait plus ensuite comment rétrécir pour refaire apparaître les + bonnes conditions. Cherchons une autre forme d'itération, par exemple : + + <\eqnarray*> + >||>>|>||\\| + s\\|}>>>|,0>>||>>>> + + + <\eqnarray*> + >|>| + >>|>||>|)>>i.r>\g|)>|)>>>|>||\g|)>>>|>||d.\D>|K,n> et d\a>>|\D>|>>>>>>|,n+1>>||,n>\\\| + s\\\s\s|}>>>|>||\\|}>|)>\\\|s\s|}>>>>> + + + Où le point fixe > est calculé avec appel au + widening au besoin, et en faisant une ou des itérations décroissantes à la + fin. Intuitivement : on fait grossir un état au maximum, en cherchant son + point fixe en boucle sur lui-même. Ensuite seulement on s'occupe de savoir + ce qu'il peut propager aux autres états. + + + + Définition du domaines abstraits avec graphes de décision : on va écrire + ici une définition mathématique des opérateurs que l'on a implémenté. On + fait abstraction des problématiques de mémoisation et de partage des + sous-graphes, qui font tout l'intérêt de la technique d'un point de vue + pratique mais qui peuvent être considérés comme un traitement à part (ce + n'est rien de plus que de la mémoisation et du partage). + + Il y a deux domaines de variables, + > pour les énumérés et > pour + les variables numériques. Il y a deux domaines pour les contraintes, + > les contraintes sur les énumérés (de la forme + y> ou v,v\\>) et + > les contraintes sur les variables numériques + (égalités ou inégalités). + + On note > le domaine des + valeurs numériques et >, >, + |\|\>>, + >, >, + >, >, + > les éléments correspondants dans ce domaine. On + considère que : + D\\\\\\|)>> + donne toutes les valuations possibles pour les variables de + >. + + On définit un ordre sur les variables de + > : =,x,\,x|}>> + (bien choisi pour réduire la taille du graphe). + + On définit ensuite une valeur du domaine disjonctif, ie un EDD, par un type + somme comme suit : + + <\eqnarray*> + |>|D|)>>>|||,v\s,v\s,\,v\s|)>>>>> + + + Si on voit ça comme un arbre, alors il faut que si un noeud + ,\|)>> est ancêtre d'un noeud + ,\|)>>, alors j> (par + rapport à l'ordre donné sur >).\ + + Pour faciliter les notations, on introduit le rang d'un noeud : + + <\eqnarray*> + ,v\s,\,v\s|)>|)>>||>||)>>||>>>> + + + La contrainte se traduit par, pour tout noeud + ,v\s,\,v\s|)>>, + on a j,i\\|)>>. + + On définit aussi la contrainte suivante : on n'a pas le droit d'avoir de + noeud ,v\s,v\s,\,v\s|)>> + si =s=*\*=s>. Cela implique + l'unicité de l'arbre qui représente un environnement donné. + + La concrétisation est définie comme suit : + + <\eqnarray*> + |)>>||>>|,v\s,\,v\s|)>|)>>||\|)> + \| s|)>=v|}>>>>> + + + Les éléments > et > sont définis comme suit : + + <\eqnarray*> + >|||)>>>|>|||)>>>>> + + + Pour assurer l'unicité lors des transformations, on définit la fonction de + réduction : + + <\eqnarray*> + |x,v\s,\,v\s|)>|\>>||>|=s=*\*s>>|,v\s,\,v\s|)>>|>>>>>>>> + + + L'opération > est définie comme suit : + + <\eqnarray*> + \V|)>>||t|)>>>|,v\s,\,v\s|)>\C,v\s,\,v\s|)>>||,v\s\s,\,v\s\s|)>>>|,v\s,\,v\s|)>\s>|\|)>>>>>||x,\s\s>>|>>|\s\s>>>>>|)>|\>>>>>>>>>> + + + et symmétriquement lorsque \\|)>> + (le noeud le plus haut est celui correspondant à la variable d'indice le + plus faible, pour respecter l'ordre). + + L'opération > est définie pareil. + + Si \>, on définit + |e|\>> par : + + <\eqnarray*> + |e|\>|)>>|||e|\>|)>>>||e|\>,v\s,\,v\s|)>|)>>||,v\|e|\>|)>,\,v\|e|\>|)>|)>>>>> + + + Pour les conditions sur les énumérés, on définit d'abord : + + <\eqnarray*> + v|)>>||V|)>,v\V|)>,v\\\\|)>>>|v|)>>||V|)>,v\V|)>,v\\\\|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>>> + + + et symmétriquement lorsque i>. + + On peut ensuite poser : + + <\eqnarray*> + |e|\>>||\s>>>> + + + L'égalité entre les valeurs représentées par deux EDD correspond à + l'égalité de ces deux EDD (c'est une CNS). + + L'inclusion est également définie par induction : + + <\eqnarray*> + \V|)>>|>|t>>|,v\s,\,v\s|)>\C,v\s,\,v\s|)>>|>|s\s>>|C,v\s,v\s,\,v\s|)>>||lorsque + \\i>>|s\s>>|,v\s,v\s,\,v\s|)>\s>||lorsque + i\\|)>>>|s\s>>>> + + + Sur nos EDD, on définit une opération + :D\D\D> comme suit : + + <\eqnarray*> + ,V|)>>||>|>>|>|>>>>>>|,C,v\s,\,v\s|)>|)>>||,v\\,s|)>,\,v\\,s|)>|)>>>>> + + + Explication : cette fonction extrait d'un EDD la fonction booléenne qui + mène vers exactement une certaine valeur abstraite des numériques. + + On introduit maintenant un opérateur de widening sur nos arbres : + + <\eqnarray*> + b>||>>>|>,V|)>|)>>||t|)>>|=\,b|)>>>|t|)>>|>>>>>>|>,v\s,\,v\s|)>|)>>|\>>|,\f>|)>>>|>>|\f>|)>>>>>>|)>>>>> + + + Les autres cas sont définis exactement pareil (cf définition de + >, plus on passe et à notre fonction + >>). Explication : lorsque l'on doit faire l'union de + deux feuilles, on fait un widening si et seulement si les deux feuilles + sont accessibles selont exactement la même formule booléenne sur les + énumérés dans et . + + On enrichit un peu notre arbre au niveau + des feuilles pour enregistrer quelques informations supplémentaires : + + <\eqnarray*> + |>|>>|||>>>|||,v\s,v\s,\,v\s|)>>>>> + + + L'étoile correspondra à : ``cette feuille est nouvelle, il faut l'analyse + comme nouveau cas'', et l'indice \> correspond à : + ``cette feuille est là depuis itérations'', où le permet + d'implémenter un délai de widening. + + On définit maintenant une fonction d'accumulation > comme + suit (> correspond à un delai de widening) : + + <\eqnarray*> + + b>||>>>|>|)>,V|)>>|\>>|>>|>>,V|)>|)>>||>>>|>>,V|)>|)>>||t|)>>>|=\,b|)>\ + i\\>>|t|)>>>|>>>>>>|>,v\s,\,v\s|)>|)>>|\i>>|,\f>|)>>>|>>|\f>|)>>>>>>|)>>>>> + + + (où > correspond à soit une étoile soit pas d'étoile) + + (les autres cas se font par appel récursif encore une fois comme dans le + cas de l'union) + + Puis une fonction de détection des cas nouveaux par rapport à une valeur + précédente : + + <\eqnarray*> + >>||>,s,s|)>>>|>,s,V|)>>||>>|\s|)>\s>>|>|>>>>>>|>,s,V>|)>>||>>>|>,s,C,v\s,\,v\s|)>|)>>||,v\f>,s,s|)>,\,v\f>,s,s|)>|)>>>>> + + + On commence avec : + + <\eqnarray*> + >||> + I>>>> + + + (appliquer > de la sorte permet de faire que toutes les + feuilles soient étoilées) + + Puis pour les itérations, deux cas : + + <\itemize> + Si il existe |)>>> + une feuille étoilée dans > : on marque + > l'arbre > où toutes les + feuilles |)>> sont dé-étoilées, puis : + + <\eqnarray*> + >||,s|)>>>|>||\s>i.c\\g|)>|)>>>|>||\g|)>>>|>||> + \ D|)>>>>> + + + (où le point fixe > est fait en faisant appel à + > et > définis précédemment, avec un délai + de widening convenable) + + Dans tous les cas, on refait une itération. Les étoiles finiront bien par + disparaitre. + + Si il n'existe pas de telle feuille étoilée dans > : + + <\eqnarray*> + >||> + \ g|)>|)>>>>> + + + Dans ce cas, on s'arrête si =s>. + + + +<\initial> + <\collection> + + + + +<\references> + <\collection> + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + > + + + +<\auxiliary> + <\collection> + <\associate|toc> + |math-font-series||1Introduction> + |.>>>>|> + + + |math-font-series||2Spécification> + |.>>>>|> + + + |2.1Grammaire + |.>>>>|> + > + + |2.2Sémantique concrète + |.>>>>|> + > + + |2.3Sémantique par réduction + |.>>>>|> + > + + |2.3.1Règles de réduction pour + l'activation du scope racine |.>>>>|> + > + + |2.3.2Règles de réduction pour + l'init dans tous les scopes |.>>>>|> + > + + |2.3.3Règles de réduction + d'expressions |.>>>>|> + > + + |2.3.4Règles de réduction pour + les pre |.>>>>|> + > + + |2.3.5Règles de réduction pour + les affectations |.>>>>|> + > + + |2.3.6Règles de réduction pour + les blocs activate |.>>>>|> + > + + |2.3.7Règles de réduction pour + les automates |.>>>>|> + > + + |2.4Sémantique par traduction, + règles de traduction |.>>>>|> + > + + |2.4.1Traduction des expressions + numériques et booléennes |.>>>>|> + > + + |2.4.2Traduction de scopes et de + programmes |.>>>>|> + > + + |math-font-series||3Interprète + pour sémantique concrète> |.>>>>|> + + + |math-font-series||4Interprétation + abstraite> |.>>>>|> + + + |4.1Sémantique collectrice + |.>>>>|> + > + + |4.1.1Nouvelle notation : + fonction de transition |.>>>>|> + > + + |4.1.2Suppression des entrées, + sémantique collectrice |.>>>>|> + > + + |4.2Généralités sur + l'interprétation abstraite |.>>>>|> + > + + |math-font-series||5Domaines + abstraits et disjonction de cas> |.>>>>|> + + + |5.1Domaine à disjonction + simple |.>>>>|> + > + + |5.2Domaine à arbre de + disjonctions |.>>>>|> + > + + |Variables et contraintes. + |.>>>>|> + > + + |Domaine numérique. + |.>>>>|> + > + + |Les EDD. + |.>>>>|> + > + + |Opérateur de widening. + |.>>>>|> + > + + |Itérations chaotiques. + |.>>>>|> + > + + + \ No newline at end of file -- cgit v1.2.3