Devoir 2

Le but de ce devoir est de mettre en pratique les concepts d’exécution symbolique vus dans le chapitre 4 du cours. Il se compose de 2 tâches à réaliser. Chaque tâche compte pour la moitié des points. Ce travail est à réaliser 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

Vous pouvez réutiliser le même fork que vous avez fait pour votre premier devoir.

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.

Dépendance

Afin de pouvoir exécuter le moteur d’exécution symbolique, il faut installer la bibliothèque Java de Z3. Sous debian, c’est le paquet libz3-java.

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 mars à 23:59. Veuillez remettre le rapport par courriel à l’adresse suivante : stievenart.quentin@uqam.ca.

1. Ajouts d’opérateurs binaires

Soit le programme suivant :

int div(int n, int d) {
    int s = 1;
    if(n<0) {
        n = 0 - n;
        s = 0 - 1;
    }
    int q = 0;
    while(d<n+1) {
        n = n - d;
        q = q + 1;
    }
    return q*s;
}

int main() {
    int c1 = getchar();
    int a = 97;
    int eof = 0-1;
    if (c1 != 112) { return 0; }
    int c2 = getchar();
    if (c2 != c1 + 2) { return 0; }
    int c3 = getchar();
    if (c3 != (c1 ^ 31)) { return 0; }
    int c4 = getchar();
    if (c4 != (2 | (a & (a | a) & a) | 4)) { return 0; }
    int c5 = getchar();
    if (c5 != (c1 | c2)) { return 0; }
    int c6 = getchar();
    if (c6 != a + (c2 ^ c5)) { return 0; }
    int c7 = getchar();
    if (c7 != ((c4 | a) & a) + (c1 - 100)) { return 0; }
    int c8 = getchar();
    if (c8 - 1 != (c1 - 100) << 3) { return 0; }
    int c9 = getchar();
    if (c9 != c3 + eof) { return 0; }
    int c10 = getchar();
    if (c10 != 0 - (eof * a * (c9 - c7))) { return 0; }
    int c11 = getchar();
    if (c11 != c9 - (c9 - c7) - (c9 - c7)) { return 0; }
    int c12 = getchar();
    if (c12 != div(c9, 10) * div(c9, 10)) { return 0; }
    int c13 = getchar();
    if (c13 != (c10 & 123 & 456) * 2 - (c12 - c11)) { return 0; }
    int c14 = getchar();
    if (c14 != (c12 & c7)) { return 0; }
    int c15 = getchar();
    if (c15 != ((c2 & c3) | c13)) { return 0; }
    return 1;
}

On souhaite pouvoir analyser ce programme MiniC afin de trouver l’entrée standard qui ferait retourner la valeur 1. Cependant, l’implémentation actuelle de MiniC ne supporte tous les opérateurs utilisés, en particulier les opérateurs bits-à-bits (^, &, |, <<) ainsi que l’opérateur de différence (!=). Le but ici est donc de rajouter le support de ces opérateurs.

Implémentation

1. Ajoutez le support des nouveaux opérateurs à MiniC. Vous pouvez appliquer le patch operators.patch pour ajouter le support de ces opérateurs dans l’analyse syntaxique ainsi que dans le compilateur MiniCC2. Il vous reste alors à ajouter le support pour ces opérateurs dans l’interpréteur générique (GenericInterpreter) et le moteur d’exécution symbolique (dans la gestion des valeurs ainsi que la génération de contraintes (ConstraintSolver)). Après cette étape, vous devriez être capable d’exécuter l’exécution symbolique sur le programme donné.
2. On souhaite trouver l’entrée standard qui mène à un retour de 1. Adaptez la classe ConcolicInterpreter pour arrêter son exécution dès qu’un chemin qui retourne 1 est trouvé. Lors de cet arrêt, reconstruisez l’entrée standard qui a été utilisée pour arriver à ce chemin et affichez la.

Points de discussion

1. Décrivez brièvement comment vous avez ajouté le support des opérateurs en question dans l’interpréteur générique et dans le moteur d’exécution symbolique.
2. Décrivez brièvement comment vous reconstruisez l’entrée standard qui permet d’explorer le chemin voulu.
3. Donner l’entrée standard en question.

2. Stratégie d’exploration

Pour réaliser cette tâche, il est nécessaire d’avoir implémenté l’opérateur != de la tâche précédente.

Soit le programme suivant :

int error() {
  return 1;
}

int main() {
    int c1 = getchar();
    int c2 = getchar();
    int c3 = getchar();
    int c4 = getchar();
    int c5 = getchar();
    int c6 = getchar();
    int c7 = getchar();
    int c8 = getchar();
    int c9 = getchar();
    int c10 = getchar();
    int c11 = getchar();

    int a = 97;
    if (c1 != a) {
        if (c2 != a) {}
        if (c3 != a) {}
        if (c4 != a) {}
        if (c5 != a) {}
        if (c6 != a) {}
        if (c7 != a) {}
        if (c8 != a) {}
        if (c9 != a) {}
        if (c10 != a) {}
        if (c11 != a) {}
    } else {
        if (!(c2 != a+11) && !(c3 != a+12) && !(c4 != a+13) && !(c5 != a+14) &&
            !(c6 != a+15) && !(c7 != a+16) && !(c8 != a+17) && !(c9 != a + 18) &&
            !(c10 != a+19) && !(c11 != a+20)) {
            return error();
        }
    }

    return 0;
}

Implémentation

On souhaite trouver une entrée qui atteint la ligne return error(). Il est évident que la branche vraie du premier if est inutile pour détecter l’erreur. Cependant, l’implémentation actuelle de notre exécution symbolique ne permet pas de trouver ce chemin en un nombre raisonnable d’itérations. Afin de résoudre cela, on va adapter la stratégie d’exploration pour utiliser une stratégie dirigée vers l’erreur.

Cette nouvelle stratégie d’exploration consiste à prioriser les chemins qui se rapprochent d’un état d’erreur, ici représenté par l’appel à la fonction error(). En se rendant compte que la première branche est inutile, la nouvelle stratégie d’exploraation privilégiera l’exploration de la seconde branche. Plutôt que d’utiliser une stratégie DFS ou BFS, on va donc, pour sélectionner le nœud suivant d’exploration :

• lister tous les nœuds candidats possibles
• sélectionner celui qui a le score le plus élevé

Comme score, on utilisera une approximation de la distance avec un nœud contenant une erreur. Celle-ci peut être calculée comme suit :

• avant l’exécution symbolique, on identifie quels blocs contiennent un appel à error. On appelle ces blocs des blocs d’erreur. On peut alors parcourir en chemin inverse les blocs jusqu’à l’entrée de la fonction pour pré-calculer la distance entre chaque bloc et le bloc d’erreur. Ainsi, si on a un chemin L1 -> L2 -> L3 où L3 contient un appel à error, L3 aura une distance de 0, L2 aura une distance de 1, et L1 aura une distance de 2. Les blocs n’ayant pas de chemin vers l’erreur ont une distance de 10000.
• on peut stocker dans chaque nœud de branchement de l’arbre d’exécution le bloc auquel il correspond, accessible dans le champ currentBlock de l’interpréteur générique
• le score étant calculé sur des nœuds non exploré, on ne sait pas à quel bloc ils correspondent. On calcule donc le score en se basant sur le bloc du parent : le score d’un nœud non-exploré est la distance entre le parent de ce nœud et un nœud d’erreur.

Tous les changements se font uniquement dans le fichier ConcolicInterpreter.java. Vous pouvez faire cela au dessus des changements faits pour la tâche 1; c’est d’ailleurs recommandé.

Points de discussion

1. Combien de chemins différents sont possibles dans la première branche ? (Quand c1 != a est vrai)
2. Exécuter l’implémentation de l’exécution symbolique avec la stratégie par défaut sur ce programme, pour au moins quelques itérations. Que se passe-t-il ?
3. Changer la stratégie pour utiliser une exploration DFS. Que se passe-t-il ? Est-ce que cela résout le problème ?
4. Implémenter la stratégie “erreur en premier” et décrivez brièvement votre implémentation.
5. Exécuter la stratégie “erreur en premier” sur le programme. Est-ce que cela résout le problème ?