Preuve que le code mort ne peut pas être détecté par les compilateurs

32

Je prévois d'enseigner un cours d'hiver sur un nombre variable de sujets, dont l'un sera les compilateurs. Maintenant, je suis tombé sur ce problème en pensant aux affectations à donner tout au long du trimestre, mais cela m'a déconcerté, je pourrais donc l'utiliser à titre d'exemple.

public class DeadCode {
  public static void main(String[] args) {
     return;
     System.out.println("This line won't print.");
  }
}

Dans le programme ci-dessus, il est évident que l'instruction print ne s'exécutera jamais à cause de return. Les compilateurs donnent parfois des avertissements ou des erreurs concernant le code mort. Par exemple, le code ci-dessus ne se compilera pas en Java. Cependant, le compilateur javac ne détectera pas toutes les instances de code mort dans chaque programme. Comment pourrais-je prouver qu'aucun compilateur ne peut le faire?

Thomas
la source
29
Quel est votre parcours et dans quel contexte vous enseignerez? Pour être franc, je suis légèrement inquiet que vous deviez demander cela, vu que vous allez enseigner. Mais bon appel à demander ici!
Raphael
9
@ MichaelKjörling La détection de code mort est impossible même sans ces considérations.
David Richerby
2
BigInteger i = 0; while(isCollatzConjectureTrueFor(i)) i++; printf("Hello world\n");
user253751
2
@immibis La question demande une preuve que la détection de code mort est impossible . Vous avez donné un exemple où la détection d'un code mort correct nécessite de résoudre un problème ouvert en mathématiques. Cela ne prouve pas que la détection de code mort est impossible .
David Richerby

Réponses:

57

Tout cela vient de l'indécidabilité du problème de l'arrêt. Supposons que nous ayons une fonction de code mort "parfait", une machine de Turing M et une chaîne d'entrée x, et une procédure qui ressemble à ceci:

Run M on input x;
print "Finished running input";

Si M s'exécute pour toujours, nous supprimons l'instruction print, car nous ne l'atteindrons jamais. Si M ne s'exécute pas indéfiniment, nous devons conserver l'instruction print. Ainsi, si nous avons un suppresseur de code mort, il nous permet également de résoudre le problème d'arrêt, nous savons donc qu'il ne peut pas y avoir un tel suppresseur de code mort.

Nous pouvons contourner ce problème par «approximation conservatrice». Donc, dans mon exemple de Turing Machine ci-dessus, nous pouvons supposer que l'exécution de M sur x peut se terminer, donc nous le faisons en toute sécurité et ne supprimons pas l'instruction d'impression. Dans votre exemple, nous savons que, quelles que soient les fonctions qui s'arrêtent ou non, il n'y a aucun moyen d'atteindre cette instruction d'impression.

Habituellement, cela se fait en construisant un "graphique de flux de contrôle". Nous faisons des hypothèses simplificatrices, telles que "la fin d'une boucle while est connectée au début et à l'instruction après", même si elle s'exécute pour toujours ou ne s'exécute qu'une seule fois et ne visite pas les deux. De même, nous supposons qu'une instruction if peut atteindre toutes ses branches, même si en réalité certaines ne sont jamais utilisées. Ces types de simplifications nous permettent de supprimer le "code manifestement mort" comme l'exemple que vous donnez, tout en restant décidable.

Pour clarifier quelques confusions des commentaires:

  1. Nitpick: pour M fixe, c'est toujours décidable. M doit être l'entrée

    Comme le dit Raphaël, dans mon exemple, nous considérons la machine de Turing comme une entrée. L'idée est que, si nous avions un algorithme DCE parfait, nous serions en mesure de construire l'extrait de code que je donne pour n'importe quelle machine de Turing , et avoir un DCE résoudrait le problème d'arrêt.

  2. pas convaincu. retourner comme une instruction franche dans une exécution directe sans branche n'est pas difficile à décider. (et mon compilateur me dit qu'il est capable de comprendre cela)

    Pour le problème soulevé par njzk2: vous avez absolument raison, dans ce cas, vous pouvez déterminer qu'il n'y a aucun moyen d'obtenir une déclaration après le retour. Cela est dû au fait qu'il est suffisamment simple pour décrire son inaccessibilité à l'aide de contraintes de graphique de flux de contrôle (c'est-à-dire qu'il n'y a pas de fronts sortants d'une déclaration de retour). Mais il n'y a pas d'éliminateur de code mort parfait, ce qui élimine tout le code inutilisé.

  3. Je ne prends pas de preuve dépendante de l'entrée pour une preuve. S'il existe un tel type d'entrée utilisateur qui peut permettre au code d'être fini, il est correct pour le compilateur de supposer que la branche suivante n'est pas morte. Je ne vois pas à quoi servent tous ces votes positifs, c'est à la fois évident (par exemple stdin sans fin) et faux.

    Pour TomášZato: ce n'est pas vraiment une preuve dépendante de l'entrée. Interprétez-le plutôt comme un "forall". Cela fonctionne comme suit: supposons que nous avons un algorithme DCE parfait. Si vous me donnez une machine de Turing M arbitraire et saisissez x, je peux utiliser mon algorithme DCE pour déterminer si M s'arrête, en construisant l'extrait de code ci-dessus et en voyant si l'instruction d'impression est supprimée. Cette technique, consistant à laisser un paramètre arbitraire pour prouver une instruction forall, est courante en mathématiques et en logique.

    Je ne comprends pas bien le point de TomášZato sur le code étant fini. Certes, le code est fini, mais un algorithme DCE parfait doit s'appliquer à tout le code, qui est un ensemble infini. De même, alors que le code lui-même est fini, les ensembles potentiels d'entrée sont infinis, tout comme le temps d'exécution potentiel du code.

    Quant à considérer que la branche finale n'est pas morte: elle est sûre en termes d '"approximation conservatrice" dont je parle, mais ce n'est pas suffisant pour détecter toutes les instances de code mort comme l'OP le demande.

Considérez le code comme ceci:

while (true)
  print "Hello"
print "goodbye"

De toute évidence, nous pouvons supprimer print "goodbye"sans modifier le comportement du programme. C'est donc du code mort. Mais s'il y a un appel de fonction différent au lieu de (true)dans la whilecondition, alors nous ne savons pas si nous pouvons le supprimer ou non, conduisant à l'indécidabilité.

Notez que je ne propose pas cela tout seul. C'est un résultat bien connu dans la théorie des compilateurs. Il en est question dans The Tiger Book . (Vous pourrez peut-être voir de quoi ils parlent dans Google Books .

jmite
la source
1
@ njzk2: Nous essayons de montrer qu'il est impossible de construire un éliminateur de code mort qui élimine tout le code mort, pas qu'il soit impossible de construire un éliminateur de code mort qui élimine du code mort. L'exemple d'impression après retour peut être éliminé facilement en utilisant des techniques de graphique de flux de contrôle, mais tous les codes morts ne peuvent pas être éliminés de cette façon.
user2357112 prend en charge Monica
4
Cette réponse fait référence à des commentaires. En lisant la réponse, je dois sauter dans les commentaires, puis revenir à la réponse. C'est déroutant (d'autant plus quand on considère que les commentaires sont fragiles et peuvent être perdus). Une réponse autonome serait beaucoup plus facile à lire.
TRiG
1
@ TomášZato - considérez le programme qui incrémente une variable et vérifie si est un nombre parfait impair, se terminant uniquement lorsqu'il trouve un tel nombre. Il est clair que ce programme ne dépend d'aucune entrée externe. Affirmez-vous qu'il est facile de déterminer si ce programme se termine ou non? nnn
Gregory J. Puleo
3
@ TomášZato Vous vous trompez dans votre compréhension du problème d'arrêt. Étant donné une machine de Turing finie et une entrée finie , il est impossible de déterminer si boucle indéfiniment lors de l'exécution sur . Je n'ai pas prouvé cela rigoureusement parce que cela a été prouvé à maintes reprises, et c'est un principe fondamental de l'informatique. Il y a un joli croquis de la preuve sur Wikipédiax M xMxMx
jmite
1
jmite, veuillez incorporer des commentaires valides dans la réponse afin que la réponse soit autonome. Signalez ensuite tous les commentaires obsolètes en tant que tels afin que nous puissions les nettoyer. Merci!
Raphael
14

Ceci est une variante de la réponse de jmite qui contourne la confusion potentielle concernant la non-résiliation. Je vais donner un programme qui s'arrête toujours, peut avoir du code mort mais nous ne pouvons pas (toujours) décider de manière algorithmique si c'est le cas.

Considérez la classe d'entrées suivante pour l'identificateur de code mort:

simulateMx(n) {
  simulate TM M on input x for n steps
  if M did halt
    return 0
  else
    return 1
}

Depuis Met xsont fixes, simulateMsa un code mort avec return 0si et seulement si Mne s'arrête pas x.

Cela nous donne immédiatement une réduction du problème d'arrêt à la vérification du code mort: étant donné TM comme instance de problème d'arrêt, créez le programme ci-dessus avec le code de - il a du code mort si et seulement si ne s'arrête pas tout seul code.M MMxMM

Par conséquent, la vérification du code mort n'est pas calculable.

Dans le cas où vous n'êtes pas familier avec la réduction comme technique de preuve dans ce contexte, je recommande notre matériel de référence .

Raphaël
la source
5

Un moyen simple de démontrer ce type de propriété sans être embourbé dans les détails est d'utiliser le lemme suivant:

Lemme: Pour tout compilateur C pour un langage Turing-complet, il existe une fonction undecidable_but_true()qui ne prend aucun argument et renvoie le booléen true, de sorte que C ne peut pas prédire si undecidable_but_true()retourne vrai ou faux.

Notez que la fonction dépend du compilateur. Étant donné une fonction undecidable_but_true1(), un compilateur peut toujours être augmenté en sachant si cette fonction renvoie vrai ou faux; mais il y a toujours une autre fonction undecidable_but_true2()qui ne sera pas couverte.

Preuve: selon le théorème de Rice , la propriété «cette fonction retourne vraie» est indécidable. Par conséquent, aucun algorithme d'analyse statique ne peut décider de cette propriété pour toutes les fonctions possibles.

Corollaire: étant donné un compilateur C, le programme suivant contient du code mort qui ne peut pas être détecté:

if (!undecidable_but_true()) {
    do_stuff();
}

Une note à propos de Java: le langage Java exige que les compilateurs rejettent certains programmes qui contiennent du code inaccessible, tout en exigeant de manière raisonnable que le code soit fourni à tous les points accessibles (par exemple, le flux de contrôle dans une fonction non vide doit se terminer par une returninstruction). Le langage spécifie exactement comment l'analyse de code inaccessible est effectuée; sinon, il serait impossible d'écrire des programmes portables. Étant donné un programme du formulaire

some_method () {
    <code whose continuation is unreachable>
    // is throw InternalError() needed here?
}

il est nécessaire de spécifier dans quels cas le code inaccessible doit être suivi d'un autre code et dans quels cas il ne doit être suivi d'aucun code. Un exemple de programme Java contenant du code inaccessible, mais pas d'une manière que les compilateurs Java sont autorisés à remarquer, apparaît dans Java 101:

String day_of_week(int n) {
    switch (n % 7) {
    case 0: return "Sunday";
    case 1: case -6: return "Monday";
    …
    case 6: case -1: return "Saturday";
    }
    // return or throw is required here, even though this point is unreachable
}
Gilles, arrête de faire le mal
la source
Notez que certains compilateurs pour certaines langues peuvent détecter que la fin de day_of_weekest inaccessible.
user253751
@immibis Oui, par exemple, les étudiants CS101 peuvent le faire dans mon expérience (bien que les étudiants CS101 ne soient certes pas un analyseur statique du son, ils oublient généralement les cas négatifs). Cela fait partie de mon argument: c'est un exemple de programme avec du code inaccessible qu'un compilateur Java ne détectera pas (au moins, peut avertir, mais ne peut pas rejeter).
Gilles 'SO- arrête d'être méchant'
1
Je crains que la formulation du lemme soit trompeuse au mieux, avec une teinte de mal. L'indécidabilité n'a de sens que si vous l'exprimez en termes de jeux (infinis) d'instances. (Le compilateur fait produire une réponse pour toutes les fonctions, et nous savons qu'il ne peut pas être toujours correct, mais en disant qu'il ya une seule instance indécidable est désactivée.) Votre paragraphe entre le Lemme et la preuve (qui ne correspond pas tout à fait le Lemme comme indiqué) essaie de résoudre ce problème, mais je pense qu'il serait préférable de formuler un lemme clairement correct.
Raphael
@Raphael Uh? Non, le compilateur n'a pas besoin de répondre à la question «cette fonction est-elle constante?». Il n'est pas nécessaire de distinguer «je ne sais pas» de «non» pour produire du code de travail, mais ce n'est pas pertinent ici car nous ne sommes intéressés que par la partie d'analyse statique du compilateur, pas par la partie de traduction de code. Je ne comprends pas ce que vous trouvez trompeur ou incorrect au sujet de l'énoncé du lemme - à moins que vous ne vouliez que j'écrive «analyseur statique» au lieu de «compilateur»?
Gilles 'SO- arrête d'être méchant'
La déclaration sonne comme "indécidabilité signifie qu'il existe une instance qui ne peut pas être résolue", ce qui est faux. (Je sais que vous ne voulez pas dire cela, mais c'est ainsi que cela peut être lu aux imprudents / novices, à mon humble avis.)
Raphael
3

La réponse de jmite s'applique à savoir si le programme quittera jamais un calcul - simplement parce qu'il est infini, je n'appellerais pas le code après sa mort.

Cependant, il existe une autre approche: un problème pour lequel il existe une réponse mais inconnue:

public void Demo()
{
  if (Chess.Evaluate(new Chessboard(), int.MaxValue) != 0)
    MessageBox.Show("Chess is unfair!");
  else
    MessageBox.Show("Chess is fair!");
}

public class chess
{
  public Int64 Evaluate(Chessboard Board, int SearchDepth)
  {
  ...
  }
}

Cette routine sans aucun doute ne contient le code mort - la fonction renvoie une réponse qui exécute un chemin , mais pas l'autre. Bonne chance pour le trouver! Ma mémoire est qu'aucun ordinateur théorique ne peut résoudre ce problème pendant la durée de vie de l'univers.

Plus en détail:

La Evaluate()fonction calcule quel côté gagne un jeu d'échecs si les deux côtés jouent parfaitement (avec une profondeur de recherche maximale).

Les évaluateurs d'échecs regardent normalement à chaque déplacement possible une profondeur spécifiée, puis tentent de marquer le plateau à ce point (parfois, étendre certaines branches plus loin, car regarder à mi-chemin dans un échange ou similaire peut produire une perception très asymétrique.) Étant donné que la profondeur maximale réelle soit 17695 demi-coups la recherche est exhaustive, elle parcourra tous les échecs possibles. Étant donné que tous les jeux se terminent, il n'est pas question d'essayer de décider de la qualité d'une position de chaque plateau (et donc pas de raison de regarder la logique d'évaluation du plateau - elle ne sera jamais appelée), le résultat est soit une victoire, une perte ou un tirage au sort. Si le résultat est un match nul, le jeu est équitable, si le résultat n'est pas un match nul, c'est un jeu injuste. Pour l'étendre un peu, nous obtenons:

public Int64 Evaluate(Chessboard Board, int SearchDepth)
{
  foreach (ChessMove Move in Board.GetPossibleMoves())
    {
      Chessboard NewBoard = Board.MakeMove(Move);
      if (NewBoard.Checkmate()) return int.MaxValue;
      if (NewBoard.Draw()) return 0;
      if (SearchDepth == 0) return NewBoard.Score();
      return -Evaluate(NewBoard, SearchDepth - 1);
    }
}

Notez également qu'il sera pratiquement impossible pour le compilateur de réaliser que Chessboard.Score () est du code mort. Une connaissance des règles des échecs nous permet aux humains de comprendre cela, mais pour le comprendre, vous devez savoir que MakeMove ne peut jamais augmenter le nombre de pièces et que Chessboard.Draw () retournera vrai si le nombre de pièces reste statique pendant trop longtemps. .

Notez que la profondeur de recherche est en demi-coups, pas en mouvements entiers. C'est normal pour ce type de routine AI car c'est une routine O (x ^ n) - l'ajout d'un pli de recherche supplémentaire a un effet majeur sur la durée d'exécution.

Loren Pechtel
la source
8
Vous supposez qu'un algorithme de vérification devrait effectuer le calcul. Une erreur commune! Non, vous ne pouvez rien supposer du fonctionnement d'un vérificateur, sinon vous ne pouvez pas réfuter son existence.
Raphael
6
La question demande une preuve qu'il est impossible de détecter un code mort. Votre message contient un exemple de cas où vous pensez qu'il serait difficile de détecter un code mort. Ce n'est pas une réponse à la question posée.
David Richerby
2
@ LorenPechtel Je ne sais pas, mais ce n'est pas une preuve. Voir aussi ici ; un exemple plus clair de votre idée fausse.
Raphael
3
Si cela vous aide, considérez que rien n'empêche théoriquement quelqu'un d'exécuter son compilateur pendant plus que la durée de vie de l'univers; la seule limitation est d'ordre pratique. Un problème décidable est un problème décidable, même s'il appartient à la classe de complexité NONELEMENTARY.
Pseudonyme du
4
En d'autres termes, cette réponse est au mieux une heuristique destinée à montrer pourquoi il n'est probablement pas facile de construire un compilateur qui détecte tout le code mort - mais ce n'est pas une preuve d'impossibilité. Ce genre d'exemple pourrait être utile pour créer une intuition pour les élèves, mais ce n'est pas une preuve. En se présentant comme une preuve, il ne rend pas service. La réponse doit être modifiée pour indiquer qu'il s'agit d'un exemple de construction d'intuition mais pas d' une preuve d'impossibilité.
DW
-3

Je pense que dans un cours d'informatique, la notion de code mort est intéressante dans le contexte de la compréhension de la différence entre le temps de compilation et le temps d'exécution!

Un compilateur peut déterminer quand vous avez du code qui ne peut en aucun cas être parcouru au moment de la compilation, mais il ne peut pas le faire pour l'exécution. une simple boucle while avec entrée utilisateur pour le test de rupture de boucle le montre.

Si un compilateur pouvait réellement déterminer le code mort à l'exécution (c.-à-d. Discerner Turing complet), alors il y a un argument selon lequel le code n'a jamais besoin d'être exécuté, car le travail est déjà fait!

Si rien d'autre, l'existence de code qui passe les vérifications de code mort à la compilation illustre la nécessité d'une vérification pragmatique des limites des entrées et d'une hygiène de codage générale (dans le monde réel des projets réels).

Dwoz
la source
1
La question demande une preuve qu'il est impossible de détecter un code mort. Vous n'avez pas répondu à cette question.
David Richerby
En outre, votre affirmation selon laquelle "Un compilateur peut déterminer quand vous avez du code qui ne peut en aucun cas être parcouru lors de la compilation" est incorrecte et contredit directement ce que la question vous demande de prouver.
David Richerby
@David Richerby, je pense que vous m'avez peut-être mal lu. Je ne dis pas que la vérification à la compilation peut trouver TOUS les codes morts, certainement pas. Je suggère qu'il existe un sous-ensemble de l'ensemble de tous les codes morts qui est discernable au moment de la compilation. Si j'écris: if (true == false) {print ("something");}, cette instruction print sera discernable au moment de la compilation pour être du code mort. Êtes-vous en désaccord sur le fait qu'il s'agit d'un contre-exemple à votre affirmation?
dwoz
Bien sûr, vous pouvez déterminer un code mort. Mais si vous voulez dire "déterminer quand [vous avez un code mort]" sans aucune qualification, cela signifie pour moi trouver tout le code mort, pas seulement une partie.
David Richerby