hash.tex

%!TEX root = root.tex

%% Dans cette section, nous formalisons la prise d'empreintes des
%% définitions. Dans la section~\ref{sec:lambda}, nous donnons la syntaxe
%% du langage~$\LambdaCode$ ainsi que les deux normalisations que nous
%% appliquons à ses termes. Dans la section~\ref{sec:fingerprint},
%% nous donnons la définition précise de notre fonction de prise
%% d'empreintes.

\subsection{$\LambdaCode$ normalisé}
\label{sec:lambda}

\paragraph{Présentation de $\LambdaCode$}

\input{lambda-syntax}

La syntaxe du langage $\LambdaCode$ est donnée dans la
figure~\ref{fig:lambda-syntax}. Il s'agit d'un $\lambda$-calcul avec
quelques spécificités par rapport à celui que l'on trouve dans les
présentations à saveur plus théoriques. Tout d'abord, les fonctions ne
sont pas unaires : elles ont une arité potentiellement supérieure
à~$1$. Ensuite, on distingue les primitives des constantes : les
primitives sont nécessairement appliquées. Le langage contient un
fragment impératif permettant d'affecter des variables, d'itérer
\textit{via} des boucles \iocaml{for} et \iocaml{while}, et enfin de
détourner le flot du contrôle \textit{via} les différents mécanismes
de lancement et rattrapage d'exceptions. L'appel de méthode est la
construction qui nous rappelle qu'{\OCaml} est un aussi un langage à
objets. Pour finir, $\LambdaCode$ n'a pas d'analyse de motifs mais est
muni d'un branchement n-aire introduit par le mot-clé~\iocaml{switch}.
%
Par manque de place, nous ne donnons pas les règles de sémantique de
ce langage et nous laissons au lecteur le soin de réfléchir à ces
dernières. Par contre, pour se convaincre que l'on ne perd pas trop de
structure en calculant la redondance sur des termes de {\LambdaCode}
et non des termes {\OCaml}, il faut prendre le temps d'expliquer les
différences entre ces deux langages.

\paragraph{Absence de types}
{\LambdaCode} est un langage non typé. On n'y retrouve donc aucune
déclaration de types. Cette absence limite donc d'emblée le champ
d'application de {\Asak}: nous ne pouvons pas détecter de déclarations
de type redondantes. Cependant, cette limitation a un avantage :
lorsque l'on oublie les types, on se donne la possibilité de détecter
plus de redondances entre des programmes de types distincts mais
partageant la même structure. En revenant aux définitions des types
qui interviennent dans deux programmes ayant la même structure, on
peut espérer détecter indirectement des redondances entre les
définitions de types.
%
Un exemple d'une telle situation sera présentée
et discutée dans la section~\ref{sec:redundancy}.

\paragraph{Absence de modules et de classes}
Les constructions de seconde classe (comme les définitions de modules
et de classes d'objets) ont disparu dans le programme traduit en
{\LambdaCode}. Cela limite notre capacité à détecter des modules
similaires ou des classes similaires. Comme pour les définitions de
type, nous pensons qu'en nous focalisant uniquement sur les aspects
calculatoires, nous pouvons détecter \textit{a posteriori} des
définitions de modules ou de classes similaires parce qu'elles
partagent des définitions similaires.

\paragraph{Absence d'analyse de motifs}
L'analyse de motifs d'{\OCaml} a été compilée en {\LambdaCode} sous la
forme d'arbres de décision, exprimés à l'aide d'expressions
conditionnelles et de branchements. Deux analyses de motifs distinctes
syntaxiquement en {\OCaml} peuvent être envoyées vers le même arbre de
décision et donc le même code~\LambdaCode: c'est par exemple le cas de deux
analyses à~trois branches sur le type \iocaml{color = Red | Black |
  White} car quelque soit l'ordre des branches de
l'analyse\footnote{En supposant qu'il n'y a pas de clause
  \iocaml{when} en jeu.}, celles-ci vont être traduites vers des
branchements à trois cas où l'ordre des cas correspond à l'ordre des
constructeurs de données dans la définition du type. Il s'agit donc
encore une fois d'une simplification favorable des termes sources
puisqu'elle envoie des termes sources syntaxiquement distincts mais
sémantiquement équivalents vers un unique terme~$\LambdaCode$.

\paragraph{$\alpha$-renommage}

Le nom des variables est pris en compte lors de la prise d'empreintes.
Naturellement, nous avons choisi de nous abstraire de ces noms en
détectant la redondance à $\alpha$-équivalence près. Il est donc
important de s'assurer que les noms de variables liées (par exemple
lors d'une définition de fonction) ne jouent aucun rôle. Pour cette
raison, nous renommons tous les identificateurs des variables liées en
des identificateurs canoniques qui codent leurs indices de De Bruijn.

\paragraph{Réduction des définitions locales inoffensives}

En {\OCaml}, et contrairement à {\Coq}, on ne peut pas facilement
comparer les termes modulo l'évaluation : en effet, l'évaluation d'un
terme peut diverger ou produire des effets de bord incontrôlés.
%
Par contre, le compilateur sait détecter des définitions locales
très simples dont l'expansion ne pose pas de problème. Ces définitions
sont marquées par une annotation du type suivant :

\begin{ocaml}
type let_kind = Strict | Alias | StrictOpt | Variable
\end{ocaml}

\noindent \iocaml{Strict} signifie que la définition peut faire
des effets de bord et ne doit pas être réduite (sauf s'il s'agit d'une
variable ou d'une constante) ; \iocaml{Alias} signifie que la
définition est pure et peut donc être réduite ; \iocaml{StrictOpt}
signifie que la définition dépend de la mémoire et ne peut donc pas
être réduite ; \iocaml{Variable} signifie que la définition sera
masquée dans la suite. Notre normalisation réduit les
définitions \iocaml{Strict} simples et les \iocaml{Alias} ce qui
nous permet d'égaliser des termes sources qui sont équivalents modulo
le dépliage de ces définitions.\footnote{Notons que cette normalisation
peut changer la complexité ce qui d'un certain point de vue ne préserve
pas la sémantique intentionnelle du programme source. Dans nos
expérimentations, ces considérations ne se sont pas montrées pertinentes
cependant.}

\subsection{Définition de la prise d'empreintes}
\label{sec:fingerprint}

Notre méthode de prise d'empreintes est une variante d'un calcul
d'empreinte de la littérature~\cite{chilowicz:hal-00627811}.
%
L'empreinte d'un arbre de syntaxe doit témoigner de la structure de
cet arbre ainsi que de l'ensemble des sous-arbres qui la constitue. Pour
des raisons d'efficacité, nous réduisons chaque sous-arbre à un entier
correspondant à son image par une fonction de hachage. Par ailleurs,
plus un sous-arbre a un grand nombre de n{\oe}uds et plus sa
contribution à l'arbre global est important : nous pondérons donc
la clé de hachage par ce nombre de n{\oe}uds.

\begin{defn}
On appelle $f$-\textit{glyphe d'un arbre de syntaxe}~$t$, le
couple~$H_f(t)$ formé d'un entier 63 bits correspondant à son nombre
de n{\oe}uds et d'un entier 128-bits correspondant à l'image de cet
arbre à travers une fonction de hachage~$f$ donnée. Pour un glyphe~$g$
donné, on note son poids~$w(g)$ et sa clé de hachage~$h(g)$.
\end{defn}

%% La définition des empreintes se dérive à partir de cette notion de glyphe
%% comme suit.

\begin{defn}
On appelle \textit{$f$-empreinte d'un arbre de syntaxe}~$t$, le
multi-ensemble~$E_f(t)$ formé des $f$-glyphes de ses sous-arbres
et de lui-même.
\end{defn}

Il reste maintenant à décider quelle fonction de hachage utiliser. Ne
nous intéressant pas à des questions de sécurité, nous avons décidé
d'utiliser intensivement la fonction de hachage cryptographique
MD5. Pour chaque n{\oe}ud de l'arbre, on calcule une clé de hachage
qui s'appuie sur le nom de la construction utilisée et, pour procéder
incrémentalement~\cite{DBLP:conf/ml/FilliatreC06}, sur les clés de
hachage des sous-arbres prise dans l'ordre, de gauche à droite.

Dans un programme, la valeur d'un littéral est très souvent liée au
contexte d'application. Du point de vue de la recherche de redondance, nous
estimons que ces valeurs constituent une forme de bruit à ignorer.
Pour que la valeur exacte des littéraux n'influence pas notre recherche
de redondance, nous avons donc décidé de ne pas prendre en compte leurs
valeurs dans le calcul de la clé de hachage.

%% Je garde ceci en commentaire car je ne suis pas sûr qu'il faille
%% le supprimer.
%%
%% Il y a un cas particulier où {\Asak} n'ignore pas la valeur d'un
%% litéral : lorsqu'un litéral est pris en argument de la primitive
%% \iocaml{GetField} sa valeur est prise en compte dans le calcul de la
%% clé de hachage. Pour comprendre ce qui motive ce cas particulier, il
%% faut observer le code~{\LambdaCode} produit par une référence à une
%% valeur externe au module courant comme dans le cas de la définition~$6$
%% de la section~\ref{sec:overview} dans la figure~\ref{fig:hash}.
%% %
%% %% \begin{ocaml}
%% %% let rev l = List.fold_left (fun acc x -> x :: acc) [] l
%% %% \end{ocaml}
%% %% \noindent est traduit en:
%% %% \begin{ocaml}
%% %% (function l/88 (apply (field 20 (global Stdlib__list!))
%% %%     (function acc/146 x/147 (makeblock 0 x/147 acc/146)) 0a l/88))
%% %% \end{ocaml}
%% %
%% Pour accéder à la fermeture de~\iocaml{List.fold_left}, il faut
%% extraire le champ~$20$ du module \iocaml{Stdlib.List}. Oublier ce
%% dernier identificateur est une approximation trop grossière de
%% la sémantique.

Pour finir cette section, il faut remarquer qu'il n'est pas pertinent
de garder tous les glyphes des sous-termes dans l'empreinte finale.
En effet, nous avons vu que la fonction de partitionnement utilise le
multi-ensemble des glyphes des sous-arbres pour identifier les
codes "proches". Comme nous travaillons en s'abstrayant les constantes
(c'est-à-dire que toutes les constantes ont le même glyphe), presque
tous les arbres partagent ces glyphes. Nous ne pouvons donc pas
conserver les empreintes de tous les sous-arbres.
%
Une approche consiste à ne conserver que les empreintes des "gros"
sous-arbres, afin d'éviter la pollution induite par les empreintes des
feuilles. La définition même de "gros" étant sujette à cautions, nous
proposons deux possibilités: (i) ne retenir que les empreintes des
sous-arbres ayant au moins un certain pourcentage~$p$ de nœuds comparé
au nombre de nœuds de l'arbre tout entier (utile quand on ne connaît
pas a priori la taille des définitions étudiées) ; ou bien (ii) ne
retenir que les empreintes des sous-arbres ayant un nombre~$n$ de
nœuds (utile quand on ne s'intéresse qu'aux fonctions dont on connaît
la taille). Il s'agit d'un paramètre global de~{\Asak}.