<\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 (primitives , , ...) blocs automates simples, à transitions faibles seulement, sans actions sur les transitions (les transitions de type sont prises en compte) Dans ce document nous mettrons 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) Par la suite, nous ne considérons que des programmes SCADE bien typés. <\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. Un scope > correspond à un ensemble de définitions (de variables, d'automates, ou de blocs activate), identifiés par un chemin. Chaque scope dispose d'une horloge propre. 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 |)>=tt>, 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. Pour chaque e>, on introduit la variable > qui enregistre la valeur de dans le cycle courant et qui sert de mémoire pour le pre lors du cycle suivant. 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 \S avec la mémoire , on peut déduire du système l'état (partiel) \T. Les déductions de la forme e\>v> signifient \S avec la mémoire et l'état partiellement calculé , l'expression calculée dans le scope > prend la valeur \T (la flèche >> correspond à une réduction par valeur dans le scope >). On notera \x=e> pour signifier \S dans le scope > on a la définition \T, de même pour les définitions de blocs activate et d'automates. On notera \pre e> pour signifier que e> apparaît dans le scope >. 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\tt|]>\ff|]>> \; 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>\tt|]>> <\equation*> s>||\r>>||>|)>=tt>>>>>|l\s>\ff|]>> <\equation*> s>||\r>>||>|)>=ff>>>>>|l\s>\l>|)>|]>> \; En particulier, pour le scope racine on instancie ces règles avec r|)>\l|)>=tt> Ces règles permettent d'exprimer le calcul d'une expression. On note > le scope dans lequel l'expression est évaluée. On note > n'importe quel opérateur binaire : ,/,mod,\,\,\,\,=,\,\,\>. <\eqnarray*> c\>c>,c\\>||\\|l,s\x\>s>,x\\>>>> <\equation*> pre e\>l|)>> <\equation*> e\>v>||e\>v>>>>>|l,s\e\e\>v\v> <\eqnarray*> >|)>=tt>||e\>v>>>>>|l,s\\e|)>\>v>>||>|)>=ff>||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>||>|)>=tt>||e\>v>>>>>|l\s\v|]>>,\\pre e <\equation*> s>||>|)>=ff>>>>>|l\s\l|)>|]>>,\\pre e <\equation*> \; Pour toute définition apparaissant dans le scope >, on donne la règle suivante : <\equation*> s>||>|)>=tt>||e\>v>>>>>|l\sv|]>>,\\x=e 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>||>|)>=ff>>>>>|l\s>\ff|]>>\ff|]>> <\eqnarray*> s>||>|)>=tt>||c\>tt>>>>>|l\s>\tt|]>>\ff|]>>>||s>||>|)>=tt>||c\>ff>>>>>|l\s>\ff|]>>\tt|]>>>>>> (implicitement sur toutes les règles : \activate if c then b else b>) Les deux scopes > et > héritent de la condition de reset du scope >. On se place dans le cadre \A>. On note > l'état initial de . 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 : <\eqnarray*> s>||r>>>>>>|l\s=s|]>>>||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 : <\eqnarray*> s>|||)>=s>>>>>|l\s>=tt|]>>>||s>|||)>\s>>>>>|l\s>=ff|]>>>>>> 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 à dès que l'on emprunte une transition qui reset, et à le reste du temps. La règle pour une transition |c>s> sont du style : <\equation*> s>|||)>=s>||c\>tt>>>>>|l\s\s|]>> À cela, il faut rajouter les conditions qui disent que l'on emprunte 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 : <\eqnarray*> s|l\s\tt|]>\ff|]>>>||s >|||)>=tt>>>>>|l\s\tt|]>>>>>> <\eqnarray*> s >|||)>=ff>|||)>=tt>>>>>|l\s\ff|]>>>||s >|||)>=ff>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> Définition (la réduction par valeur de en une valeur se fait selon les règles données ci-dessus) : <\equation*> s>|||)>=tt>||a-b\v>>>>>|l\sv|]>> Définitions de > et : <\equation*> s>|||)>=tt>||pre|)> a\v>>>>>|l\sv|]>> <\equation*> s>|||)>=tt>||pre b|)>\v>>>>>|l\sv|]>> Définition de : <\equation*> s>|||)>=tt>||not pre half|)>\v>>>>>|l\sv|]>> Mémorisation des valeurs pour , et (on écrit aussi les règles pour le cas où le scope est inactif à titre d'exemple simplement ; en pratique celles-ci sont éliminées puisque le scope racine est toujours actif) : <\eqnarray*> s>|||)>=tt>||a\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> <\eqnarray*> s>|||)>=tt>||b\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> <\eqnarray*> s>|||)>=tt>||half\v>>>>>|l\s\v|]>>>||s>|||)>=ff>>>>>|l\s\l|)>|]>>>>>> Activation des deux moitiés du activate : <\eqnarray*> s>|||)>=tt>||half\tt>>>>>|l\s:=tt|]>\ff|]>>>||s>|||)>=tt>||half\ff>>>>>|l\s:=ff|]>\tt|]>>>>>> <\equation*> s>|||)>=ff>>>>>|l\s:=ff|]>\ff|]>> Définition de et dans la première moitié : <\eqnarray*> s>|||)>=tt>||la+1\v>>>>>|l\sv|]>>>||s>|||)>=tt>||lb\v>>>>>|l\sv|]>>>>>> Et dans la deuxième moitié : <\eqnarray*> s>|||)>=tt>||la\v>>>>>|l\sv|]>>>||s>|||)>=tt>||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 formule à 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 être une formule booléenne. Les règles sont les suivantes : <\eqnarray*> ,,e,\,e|)>,w|)>>||,e,\f.T,,\,e|)>,w,\,\,\|]>|)>|)>>>|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, on définira la fonction de traduction d'une définition par : <\eqnarray*> ,x=e|)>>||,e,s=\|)>>>>> Dans le cas d'une multi-affectation ,\,x=e>, on utilisera la traduction suivante : <\eqnarray*> ,,\,x=e|)>|)>>||,e,s|)>=\\*\*\s|)>=\|)>>>>> Dans le cas où l'on doit traduire une instanciation de noeud ,\,v|)>> (c'est le cas dans notre implémentation puisqu'on ne fait pas d'inlining), on nomme ,\,r> les valeurs renvoyées par le noeud et on utilise la règle ,n,\,v|)>,w|)>=w|)>,\,s|)>|]>>. Il faut par ailleurs générer la traduction des définitions données dans le noeud et s'occuper de passer les arguments (nommés ,\,arg>), en introduisant des équations du type ,v,s|)>=\|)>>. <\example> Effectuons par exemple la traduction de 0 then y else -y> : <\eqnarray*> ||,if y\0 then y else -y,s=\|)>>>|||,y\0,\|)>\T,y,s=\|)>|)>\T,y\0,\|)>\T,-y,s=\|)>|)>>>|||\0\s=s|)>\\0|)>\s=-s|)>>>>> <\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>|)>\T,1,|s=l|)>+\|)>|)>|)>>>|||>|)>\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 \S else b> \T sera du style T|)>\T|)>|)>\c\T|)>\T|)>|)>>. Tout ceci 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. 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 à appeler pour que cette valeur soit calculée et rajoutée à . La procédure de calcul consiste à activer le scope racine, puis à appeler 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 définition de variable , 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 renvoyé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 renvoyé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. Le calcul de la valeur prise par une expression , utilisée dans une condition ou pour une définition de variable, peut faire appel à d'autres variables du programme. À ce moment si une valeur a été mémorisée on l'utilise, sinon on appelle la fonction de calcul pour cette variable. Lorsque le calcul d'une variable est \S en cours \T, ce statut est enregistré dans , ce qui permet de détecter les cycles de dépendances. 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 > l'ensemble des variables de type énumération et > les variables de type numérique, de sorte que =\\\>. 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|)>=tt|}>>>>> 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 mémoires 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 préfixe standard, \S \T, qui indique que ce sont des variables de type , c'est-à-dire des copies de valeurs du cycle précédent. On note cette fonction de cycle \\|)>> ; 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 répétée 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 quelles 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 donnée par les directives . On s'intéresse maintenant à la sémantique non déterministe suivante : <\eqnarray*> >||\ \| s|)>=tt|}>>>|>|||)>>>|>||x>,a\c,q|)>=tt|}>>>>> \; 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 polyè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 polyè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 équations (é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 disparaît 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. <\example> Soit le programme suivant : <\verbatim> node counter() returns(x: int) \ \ x = 0 -\ (if pre x = 5 then 0 else pre x + 1) Celui-ci est traduit par une formule du style : <\eqnarray*> ||\Lnreset>>||>|\ff>>||>||\tt\x=0|)>>>|>|\ff\|x=0|)>>>|>|5\x=Lx+1|)>>>>>>|)>|)>>>>>>|)>>>>> Les deux variables qui ont besoin d'être perpétuées d'un cycle au suivant sont > et , la fonction de cycle > est donc définie à partir de ,x|}>>. La fonction >, quant à elle, reflète directement la structure de la formule : <\eqnarray*> >|||init\Lnreset|\>\|nreset\ff|\>||init\tt|\>\|x=0|\>>>|>||init\ff|\>||Lx=5|\>\|x=0|\>>>|>||Lx\5|\>\|x=Lx+1|\>>>>>>|)>>>>>>|)>>>>> 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 ,\, mod,=,\,\>. 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 transformations 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 de façon exacte les valeurs d'énumérations ayant plus de deux éléments (puisqu'on se restreint à une enveloppe convexe). 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 des 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 selon 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|\>> avec \>. 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 amené à 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, ainsi que > son opérateur de widening. On note |\|\>> la fonction de restriction par une contrainte. La particularité des variables de disjonction 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 appelle toujours =\\\>, où =\\\\\>. On a une injection évidente de > dans |)>>, on identifie donc \> à \\|\x\\,s=d|}>>. De même on identifie \> à \ \| \x\\\\,s=e|}>>. 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 de >. 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|\>|)>>. Pour \\>, notons > : \\\> tel que >=\d.>|d>>|>|>>>>>> Le principe des itérations chaotiques peut s'écrire comme suit : <\itemize> Poser : <\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 connaît. 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. Nous proposons comme forme final le processus d'itération suivant : <\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. Nous proposons dans ce paragraphe un second domaine abstrait capable de faire des disjonctions de cas, et qui permet de mieux traîter des problèmes ayant un nombre important de variables de type énuméré reliées entre elles par des relations complexes. 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\\|)>> (avec =\\\\\>) 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|)>>>|>|,v\s,\,v\s|)>>>>>>>||,v\s\s,\,v\s\s|)>>>|,v\s,\,v\s|)>\s>|\|)>>>>>||x,\s\s>>|>>|\s\s>>>>>|)>|\>>>>>>>>>> et symé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\\\\|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>|\x|)>>|j>>|,v\c\v|)>,\,v\c\v|)>|)>>>>> et symétriquement lorsque i>. On peut ensuite poser, pour \> : <\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 selon 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 à : \S cette feuille est nouvelle, il faut l'analyse comme nouveau cas \T, et l'indice \> correspond à : \S cette feuille est là depuis itérations \T, où le permet d'implémenter un délai de widening. On se donne > un délai de widening, paramètre de l'analyse. On définit maintenant une fonction d'accumulation > comme suit : <\eqnarray*> b>||>>>|>,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|)>|)>>>>> Nous sommes maintenant en mesure de décrire le processus d'itérations chaotiques à proprement parler. 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 disparaître. Si il n'existe pas de telle feuille étoilée dans > : <\eqnarray*> >||> \ g|)>|)>>>>> Dans ce cas, on s'arrête si =s>. Le projet scade-analyzer propose une implémentation simple des composants suivants : <\itemize> parser, lexer, typeur pour notre sous-ensemble de SCADE (source des fichiers dans ) interprète pour la sémantique cocnrète () implémentation de la transformation d'un programme en formule logique ; quelques simplifications sur les formules logiques (, ). domaine numérique non-relationnel basé sur les intervalles ; domaine relationnel basé sur la bibliothèque externe Apron (, , , ...) deux domaines abstraits et analyseur statique correspondant (, ) En nous basant sur les options de la ligne de commande, nous allons maintenant décrire les différentes fonctionnalités. <\itemize> : parse un fichier SCADE et le ré-affiche en sortie : 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 . <\itemize> : execute le programme SCADE donné en argument, avec l'interprète basé sur la sémantique à réduction. Le programme doit satisfaire la spécification suivante : avoir un noeud qui servira de racine, ce noeud devant prendre une unique entrée, , qui est un compteur incrémenté à chaque cycle, et renvoyant trois entiers, , et (qui seront affichés en sortie), ainsi qu'un booleen qui indiquera que l'interprète doit terminer. Cf fichiers dans pour des exemples. : pareil mais affiche plus de détails (tout le contenu de la mémoire est affiché à chaque cycle). Cette analyse est implémentée dans . <\itemize> : 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 : de même mais utilise le domaine abstrait relationnel basé sur Apron (polyèdres) pour la partie numérique <\itemize> noeud\> : spécifie le noeud racine dont on veut faire l'analyse (par défaut : ) : affiche des détails sur le contenu de l'accumulateur à chaque itération : affiche encore plus de détails n\> : définit un délai pour les opérations de widening (par défaut 5) vars\> : variables à utiliser comme variables de disjonction (par défaut : aucune) scopes\> : donne un certain nombre de scopes pour lesquels ne pas introduire de variable (par défaut , c'est-à-dire que n'est jamais introduite). Lorsqu'une variable est introduite, on génère les équations qui font en sorte que soit égal au numéro du cycle depuis le début de l'exécution du programme. scopes\> : donne un certain nombre de scopes pour lesquels introduire une variable (par défaut ). Il est envisageable de remplacer la variable de chaque scope par une variable , les disjonctions de cas init/non init se feront alors selon la condition ou 1>. En ne générant ni variable ni variable , la disjonction n'est pas faite. Cette analyse est implémentée dans . <\itemize> : fait une passe d'analyse statique utilisant le domaine à base d'EDD et en utilisant les intervalles comme domaine de valeurs numériques : de même mais utilise le domaine abstrait relationnel basé sur Apron (polyèdres) pour la partie numérique <\itemize> , , Non implémenté : paramètre pouvant intervenir sur le choix des variables à considérer dans le graphe de décision (actuellement toutes sont nécessairement considérées). Une troisième forme d'analyse, basée sur un partitionnement dynamique de > 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 . <\itemize> : analyse par partitionnement dynamique, utilise un domaine simple non-relationnel pour les valeurs énumérées et les intervalles pour la partie numérique : 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 <\itemize> , , : profondeur maximale de partitionnement : largeur maximale de partitionnement (ie nombre maximal de parties à considérer) <\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 définitions de variables |.>>>>|> > |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 à graphe de décision |.>>>>|> > |5.2.1Variables et contraintes |.>>>>|> > |5.2.2Domaine numérique |.>>>>|> > |5.2.3Les EDD |.>>>>|> > |5.2.4Opérateur de widening |.>>>>|> > |5.2.5>.>>>>>>>|Itérations chaotiques. |.>>>>|> >>|font-series||Itérations chaotiques.> |.>>>>|> > |Itérations chaotiques. |.>>>>|> > |math-font-series||6Implémentation> |.>>>>|>