\section{Analyse de type} \subsection{Présentation} L'analyse de type dans un décompilateur s'ajoute à tout le travail précédent. Le but de cette étape est d'ajouter des informations de type au code de haut niveau généré jusque là. Le code que l'on a est du C non typé, il ne manipule que des types que l'assembleur connaît, c'est à dire des mots machine (courts, simples ou doubles). A partir de cela on aimerait récuperer tout le confort de typage d'un langage de haut niveau, par exemple en C, les structures, les tableaux, et les unions.\\ Dans le processus de compilation les informations de type sont présentes dans l'analyse sémantique (avant la transcription en représentation intermédiaire). Par la suite elles disparaissent, l'assembleur n'étant pas typé. Les informations de types peuvent toute fois être sauvegardés pour diverses utilitées comme pour l'implémentation d'un ramasse miettes, ou encore pour la vérification de code (comme dans l'IDL de .NET de Microsoft \cite{Mic}, ou dans Java de Sun \cite{Sun}). Dans ce cas l'analyse de type en est grandement facilitée, voir triviale.\\ Pour l'instant il n'existe pas de décompilateur permettant la reconnaissance de type. Ceci car il y a très peu de compilateur opérationnels, de plus le travail sur les système de typage est récents (voir ML \cite{CAML} ou Haskell \cite{GHC}). Les documents abordants le sujet sont aussi très rares. La référence en la matière étant aujourd'hui le travail de Alan Mycroft ``Type Based Decompilation''\cite{Myc99}. C'est d'ailleurs de celui ci que nous allons nous inspirer, les idées principales ainsi que les exemples proviennent directement de A. Mycroft.\\ Pour réaliser l'analyse de type, nous allons nous baser sur la forme SSA, grâce à laquelle nous allons générer des contraintes de type, puis nous ferons tourner l'algorithme d'inférence de type de Hindley-Milner \cite{Mil78}. Grâce à celui ci nous allons récuperer des informations de type qui nous permettrons de décrire le code C non typé et de le retravailler afin de le rendre plus proche d'un code humainement écrit. \subsection{Inférence de type} L'inférence de type est le procédé permettant de retrouver le type d'une variable à partir de ces utilisations. Elle est surtout utilisée dans les langages fonctionnels (comme ML et Haskell). C'est Hindler et Milner qui ont indépendament découvert une méthode d'inférence de type à la compilation. L'inférence de type est basée sur la preuve automatique de théorèmes utilisée en logique.\\ L'algorithme Milner-Hindley propose de reduire le probleme d'inférence de type à un problème d'unification. Nous avons un ensemble de types définis (\texttt{int}, \texttt{bool}, \ldots) et de type variables. A partir du code nous allons produire un certain nombre de variables à type variable, et des contraintes sur ces variables, celui-ci est appelé l'environnement. Grâce à cet environnement nous allons pouvoir unifier le type d'une variable avec l'environnement en lui donnant un type. Une fois cette variable typée, nous allons pouvoir faire une substitution dans l'environnement et générer de nouvelles contraintes de types qui pourrons alors nous servir pour l'unification. Le détail de l'algorithme dépasse le cadre de cet article et peut être trouvé soit dans Milney \cite{Mil78} ou Appel \cite{App98} dans le chapitre 'Polymorphic Types'.\\ Dans notre cas, contrairement à dans un compilateur, le typage est forcement bon. L'unification doit toujours réussir. C'est donc cette phase qui sera la principale différence avec l'algorithme d'origine.\\ Le typage du language C ne satisfait pas tous les besoins que nous avons pendant la reconstruction de type, donc comme le propose A. Mycroft, nous utilisons donc notre propre structure de type. La règle 't' est pour les types, 's' pour les champs d'une structure et 'r' pour les registres. \begin{align*} t &::= \textsl{char} | \textsl{short} | \textsl{int} | \textsl{ptr}(t) | \textsl{array}(t) | \textsl{mem}(s) \\ s &::= n_1 : t_1, \ldots, n_k : t_k \: \textrm{avec} \: n_i \in N \; \textrm{et} \; k > 0 \\ r &::= \textsl{int} | \textsl{ptr}(t) \end{align*} La notation \textsl{mem(s)} représente une \texttt{struct} C. Les $n_i$ décrit l'octet où se trouve le champ dans une structure. On peut noter que les unions peuvent être simulées par \textsl{mem(0: $t_1$,\ldots, 0 : $t_k$)}.\\ Grâce à cette notation on va pouvoir décrire toutes les instructions en ajoutant des contraintes. Voici quelques exemples, proposées par A. Mycroft, en adoptant la notation 'rX' pour un registre et 'tX' son type associé.\\ \begin{center} \begin{tabular}[t]{l|l} instruction & contraintes générées \\ \hline mov r4, r6 & t6 = t4 \\ ld.w 6[r3], r5 & t3 = \textsl{ptr}(\textsl{mem}(6 : t5)) \\ xor ra2, r1b, r1c & t2a = \textsl{int}, t1b = \textsl{int}, t1c = \textsl{int} \\ add r2a, r1b, r1c & t2a = \textsl{ptr}($\alpha$), t1b = \textsl{int}, t1c = \textsl{ptr}($\alpha$) $\vee$ \\ & t2a = \textsl{int}, t1b = \textsl{ptr}($\alpha$'), t1c = \textsl{ptr}($\alpha$') $\vee$\\ & t2a = \textsl{int}, t1b = \textsl{int}, t1c = \textsl{int}\\ ld.w (r5)[r0], r3 & t0 = \textsl{ptr}(\textsl{array}(t3)), t5 = \textsl{int} $\vee$ \\ & t0 = \textsl{int}, t5 = \textsl{ptr}(\textsl{array}(t3))\\ mov \#42, r7 & t7 = \textsl{int}\\ mov \#0, r7 & t7 = int $\vee$ t7 = \textsl{ptr}($\alpha$'') \\ \end{tabular} \end{center} On note que l'operarion '+' est surchargée et donne lieu à des contraintes disjonctives. En effet l'addition peut soit s'appliquer sur les pointeurs soit sur des entiers, contrairement au \textsl{xor} qui lui ne s'applique que sur des entiers. De même ceci s'applique aux instructions de chargement et de sauvegarde indexées, ainsi qu'à la constante 0 qui signifie généralement le pointeur \texttt{null}. \subsection{Exemple} Mycroft nous propose d'illustrer l'algorithme avec le code suivant: \\ \begin{verbatim} ; struct A { int hd; struct A *tl; }; ; ; int f(struct A *x) ; { ; int r = 0; ; for ( ; x != 0; x = x->tl) ; r += x->hd; ; return r; ; f: mov #0, r1 cmp #0, r0 beq L4F2 L3F2: ld.w 0[r0], r2 add r2, r1, r1 ld.w 4[r0], r0 cmp #0, r0 bne L3F2 L4F2: mov r1, r0 ret \end{verbatim} C'est une fonction qui somme un liste écrite de façon itérative. A partir du code assembleur, nous allons essayer de retrouver le code source initial, indiqué en commentaires. On notera que la structure A est définie récursivement, ce qui pourait sembler être un problème.\\ La première étape de notre reconstruction de type est de mettre le code assembleur sous la forme SSA, afin de pouvoir générer les contraintes de type. Voici ce qu'on obtient:\\ \begin{center} \begin{tabular}[t]{llll} f: & & & tf = t0 $\leftarrow$ t99 \\ & mov & r0, r0a & t0 = t0a \\ & mov & \#0, r1a & t1a = \textsl{int} $\vee$ t1a = \textsl{ptr}($\alpha_1$)\\ & cmp & \#0, r0a & t0a = \textsl{int} $\vee$ t0a = \textsl{ptr}($\alpha_2$)\\ & beq & L4F2 & \\ L3F2: & mov & $\phi$(r0a, r0c), r0b & t0b = t0a, t0b = t0c \\ & mov & $\phi$(r1a, r1c), r1b & t1b = t1a, t1b = t1c \\ & ld.w & 0[r0b], r2a & t0b = \textsl{ptr}(\textsl{mem}(0 : t2a))\\ & add & r2a, r1b, r1c & t2a = \textsl{ptr}($\alpha_3$), t1b = \textsl{int}, t1c = \textsl{ptr}($\alpha_3$) $\vee$ \\ & & & t2a = \textsl{int}, t1b = \textsl{ptr}($alpha_4$), t1c = \textsl{ptr}($alpha_4$), $\vee$ \\ & & & t2a = \textsl{int}, t1b = \textsl{int}, t1c = \textsl{int} \\ & ld.w & 4[r0b], r0c & t0b = \textsl{ptr}(\textsl{mem}(4 : t0c))\\ & cmp & \#0, r0c & t0c = \textsl{int} $\vee$ t0c = \textsl{ptr}($\alpha_5$)\\ & bne & L3F2 & \\ L4F2: & mov & $\phi$(r1a, r1c), r1d & t1d = t1a, t1d = t1c \\ & mov & r1d, r0d & t0d = t1d \\ & ret & & t99 = t0d \\ \end{tabular} \end{center} Les $\alpha_x$ sont différents types que l'algorithme d'inférence doit déterminer.\\ On lance alors l'algorithme d'inférence de type. Celui ci n'est pas d'écrit en détail, mais on va tomber sur une inconsistance: \begin{center} t0c = t0b = \textsl{ptr}(\textsl{mem}(4 : t0c)) = \textsl{ptr}(\textsl{mem}(0 : t2a)) \end{center} Pour résoudre cela on introduit: \begin{center} \texttt{struct} G \{ t2a m0; t0c m4; \ldots \} \\ t0c = \textsl{ptr}(\textsl{mem}(0 : t2a, 4 : t0c)) = \textsl{ptr}(\texttt{struct} G) \end{center} On obtient donc les solutions suivantes: \begin{align*} t0 = t0a = t0b = t0c &= \textsl{ptr}(\texttt{struct} G) \\ t99 = t1a = t1b = t1c = t1d = t2a = t0d &= \textsl{int} \\ tf &= \textsl{ptr}(\texttt{struct} G) \leftarrow \textsl{ptr}(\textsl{int}) \end{align*} ou \begin{align*} t0 = t0a = t0b = t0c &= \textsl{ptr}(\texttt{struct} G) \\ t2a &= \textsl{int} \\ t99 = t1a = t1b = t1c = t1d = t0d &= \textsl{ptr}(\alpha_4) \\ tf &= \textsl{ptr}(\texttt{struct} G) \leftarrow \textsl{ptr}(\alpha_4) \end{align*} La deuxième solution est due à la surcharge de l'opérateur '+' dans l'ajout des elements de la liste. Le type \textsl{ptr}($\alpha_4$) correspond au \texttt{void \*} du C. Les deux cas sont bien sur plausible, mais intuitivement on preferara le premier cas. Pour lever cette ambiguité on peut imaginer une prioritée dans les types, avec les pointeurs ayant la plus faible.\\ Une autre singularité à noter c'est que la structure G contient des champs indéfinis, c'est à dire qu'ils sont inutilisés dans cette fonction. Mycroft propose alors d'ajouter un champs optionnel qui permet de bloquer de la place pour eventuellements d'autres champs.\\ Le programme final obtenu, à partir de la reconnaissance de type et du l'analyse du flot de données et de contrôle est le suivant: \begin{verbatim} struct G { int m0; struct G *m4; Tpad m8; }; int f(struct G *x) { int r = 0; if (x != 0) { do { r += x->m0; x = x->m4; } while (x != 0); return r; } \end{verbatim} Le résultat obtenu est satisfaisant, il est proche de celui d'origine\footnote{Pour transformer la boucle \texttt{do...while} en \texttt{for} on peut utiliser un postprocesseur}, et facilement comprehensible. \subsection{Structures contre Tableaux} Différencier les structures des tableaux est une tâche difficile. Nous sommes obligé de faire des choix, pour automatiser le processus, qui ne sont pas forcement les bons. On pourrait par contre imaginer une interface demandant de choisir entre plusieurs types possibles.\\ \noindent Comme vu precedemment, on a: \begin{center} \begin{tabular}[t]{lll} ld.w &6[r3], r5 & t3 = \textsl{ptr}(\textsl{mem}(6 : t5)) \\ ld.w &(r5)[r0], r3 & t0 = \textsl{ptr}(\textsl{array}(t3)), t5 = \textsl{int} $\vee$ \\ & & t0 = \textsl{int}, t5 = \textsl{ptr}(\textsl{array}(t3))\\ \end{tabular} \end{center} Cela vient du fait que nous considerons un accès fait grâce à une constante comme un accès à un champ d'une structure, et un accès fait par une variable comme un tableaux. Cette décision vient du fait qu'on utilise la plus part du temps un indice pour acceder aux tableaux, tandis que les accès à un champ d'une structure sont générés par le compilateur avec des décalages constants.\\ \noindent Un code du type: \begin{verbatim} ld.b 0[r0], r1 ld.b 48[r0], r2 ld.w (r5)[r0], r3 \end{verbatim} Aura comme resultat: \begin{verbatim} union G { struct { char m0; char pad1[47]; char m48; } u1; int u2[]; } *r0; \end{verbatim} On voit tout de suite que le resultat n'est pas très bon, et qu'il est difficile de bien interprété un tel code. De plus il est impossible de connaître la taille du tableau\footnote{A moins que le binarire contienne des informations pour vérifier l'intégrité du code, comme pour le \textit{bound checking}}.\\ Mais pire encore, il est impossible de faire la différence entre differentes structures: \begin{verbatim} struct S1 { int a; int b[4]; int c; int d[4]; } x1; struct S2 { int a; int b[4]; } x2[2]; struct S3 { struct S2 c; struct S2 d; } x3; \end{verbatim} Donc, en général, le melange de structures et de tableaux est très difficile à gérer.