Sommaire

Devoir 1

Le but de ce devoir est de mettre en pratique les concepts d’analyse dataflow vus dans le chapitre 2 du cours. Il se compose de 4 tâches, mais vous ne devez en réaliser que 3 (au choix). Chaque tâche vaut pour 1/3 des points du devoir, et le total maximum est plafonné à 100%. Ce travail est à faire seul sans utilisation d’outils d’IA générative.

Vous aurez à implémenter des analyses dans MiniC, que vous pouvez récupérer depuis le dépôt git suivant : https://gitlab.info.uqam.ca/inf889a/minic

Chaque tâche comporte plusieurs points de discussion. Vous rendrez une implémentation (sous forme de changements au projet MiniC) et un rapport PDF. Dans le rapport, il est important de clairement répondre à chaque point de discussion.

Livrables

Vous devez rendre deux livrables.

  1. Une implémentation, sous forme d’un fork privé du dépôt de MiniC, auquel vous aurez ajouté l’enseignant comme mainteneur (nom d’utilisateur GitLab: quentin).
  2. Un rapport au format PDF qui répond aux différents points de discussion pour chacune des tâches. Incluez un lien vers votre dépôt d’implémentation dans le rapport. Il n’y a pas de limite de page, mais visez à aller à l’essentiel.

La date limite de remise est le dimanche 15 février à 23:59. Veuillez remettre le rapport par courriel à l’adresse suivante : stievenart.quentin@uqam.ca.

1. Analyse d’expression fort occupée

La définition d’une expression fort occupée est la suivante :

Une expression est fort occupée si et seulement si il est garantit que cette expression va être évaluée dans le futur avant que sa valeur ne change.

On souhaite implémenter une telle analyse.

Implémentation

Implémentez cette analyse dans le fichier src/minic/dataflow/analysis/VeryBusyExpressionAnalysis.java, qui contiendra:

  • la définition du treillis si nécessaire
  • une classe VeryBusyExpressionTransfer qui définit la fonction de transfert
  • un point d’entrée dans la classe VeryBusyExpressionAnalysis

Points de discussion

  1. Décrire s’il s’agit d’analyse de type may ou must ? Justifier pourquoi.
  2. Décrire s’il s’agit d’une analyse en avant (forward) ou en arrière (backward) ? Justifier pourquoi.
  3. Définir précisément le treillis à utiliser pour cette analyse.
  4. Donner les équations de l’analyse, de façon similaire à comment les équations d’autres analyses ont été décrites dans les diapositives du cours. Inclure également l’équation pour l’élément initial de l’analyse (à l’entre ou sortie du programme).
  5. Décrire brièvement votre stratégie d’implémentation.
  6. Donner le résultat de votre analyse sur le fichier examples/dataflow/verybusy.c
  7. Discuter des résultats de votre analyse sur le fichier d’exemple. On s’attend à obtenir les résultats exacts si l’analyse est implémentée correctement.

2. Treillis d’analyse de signe

On considère ici la fonction suivante :

int f(int x) {
  int a = 0;
  if (x < 0) {
    a = 5;
  }
  return a;
}

On souhaite prouver que la valeur retournée par cette fonction n’est jamais négative.

Points de discussion

  1. Exécuter l’analyse de signe actuelle sur cette fonction. Est-ce que la propriété souhaitée (f ne retourne pas de nombre négative) a pu être prouvée automatiquement ?
  2. À quel point de l’analyse se situe le problème ?
  3. Afin de régler ce problème, il est possible de rajouter des éléments à notre treillis, en particulier on souhaite ajouter deux éléments : un élément correspondant aux valeurs nulles ou positives, et un élément correspondant aux valeurs nulles ou négatives. Définir ce treillis, soit via son diagramme de Hasse complet, soit en définissant l’ensemble et la relation d’ordre partiel.
  4. Expliquer comment ce nouveau treillis permet de résoudre le problème sur le programme d’exemple.
  5. Décrire brièvement votre stratégie d’implémentation.
  6. Donner les résultats de votre implémentation sur le programme d’exemple. Peut-on prouver automatiquement la propriété souhaitée ?

Implémentation

Implémentez vos changement à l’analyse de signe directement dans l’implémentation du treillis src/minic/dataflow/lattice/SignLattice.java

3. Tests de monotonicité et de sûreté

L’implémentation des opérations (addition, soustraction, multiplication) sur le treillis de l’analyse de signe est faite sur base de tables, où il est facile de commettre une erreur. Même si on aurait prouvé que ces opérations sont correctes à la main, il est probable qu’on ait commis une erreur lors de la retranscription en table. On souhaite alors ici vérifier que ces opérations sont monotones et sûres.

Pour l’opérateur d’addition, on souhaite les deux propriétés suivantes :

  • l’opération sur le treillis est monotone, c’est-à-dire : \( \forall x, x’, y, y’ \in \textit{SignLattice}: x \sqsubseteq x’ \wedge y \sqsubseteq y’ \implies x \hat{+}  y \sqsubseteq x’  \hat{+}  y’\)
  • l’opération sur le treillis est sûre, c’est-à-dire : \( \forall x, y \in \mathbb{Z}: \alpha(x + y) \sqsubseteq \alpha(x) \hat{+} \alpha(y) \)

On souhaite que les propriétés équivalentes soient vraies également pour la soustraction et la multiplication.

Nous allons vérifier ici que ces propriétés sont vraies pour notre implémentation, de la manière suivante :

  • pour la monotonicité, il suffit de vérifier que la propriété est vraie pour toute valeur de x, x’, y, y’ appartenant à notre treillis.
  • pour la sûreté, on ne peut pas vérifier que c’est vrai pour tout entier, mais on peut choisir des entiers spécifiques de façon à couvrir toutes les valeurs de notre treillis: un entier positif, un entier négatif, et zéro suffisent.

Implémentation

Implémenter la vérification des deux propriétés pour chacune des trois opérations.

Points de discussion

  1. Décrire brièvement votre stratégie d’implémentation.
  2. Exécuter l’implémentation. Est-ce que les tables implémentées dans SignLattice.java sont monotones et correctes ?
  3. Introduire une erreur dans une des tables et vérifier que c’est bien attrapé par l’implémentation.

4. Sensibilité au contrôle

Nous avons vu au cours que notre analyse de signe ne permet pas de vérifier que la fonction abs suivante retourne toujours une valeur non négative.

int abs(int x) {
  int y = 0;
  if (0 < x) {
    y = x;
  }
  if (x < 0) {
    y = 0-x;
  }
  return y;
}

Le problème est que l’on n’utilise pas l’information venant des conditions. Cette information permettrait de raffiner les valeurs dans notre treillis :

  • dans le premier if, on sait que 0 < x, ce qui implique que x est strictement positif,
  • dans le second if, on sait que x < 0, ce qui implique que x est strictement négatif.

Pour pallier à cela, on va ajouter des appels de fonction factices dans chaque branche: assertlt(0, x) dans la première branche et assertlt(x, 0) dans la seconde branche. L’analyse peut alors se baser sur ces appels pour raffiner les valeurs de x. Ces appels pourraient être ajoutés automatiquement, mais pour des soucis de simplicité on va les ajouter nous-même, et transformer la fonction comme suit :

int abs(int x) {
  int y = 0;
  if (0 < x) {
    assertlt(0, x);
    y = x;
  }
  if (x < 0) {
    assertlt(x, 0);
    y = 0-x;
  }
  return y;
}

On peut alors définir une fonction de transfert spécifique pour les appels à assertlt, afin de raffiner les valeurs de notre treillis.

Implémentation

Adapter la fonction de transfert de src/minic/dataflow/analysis/SignAnalysis.java afin de prendre en compte la présence d’assertion de type assertlt pour raffiner les valeurs.

En bonus, vous pouvez adapter le compilateur MiniC afin qu’il procède automatiquement à l’ajout des assertlt en présence de conditions de type A < B. Cela dépasse le cadre du cours et requiert d’aller toucher au compilateur MiniC.

Points de discussion

  1. Décrire brièvement la stratégie d’implémentation.
  2. Exécuter l’analyse améliorée sur la version initiale de abs ainsi que sur la version transformée. Quelles sont les différences ?
  3. Est-ce que la propriété à prouver (abs ne retourne pas de nombre négatif) a pu être prouvée automatiquement ?