Tu mélanges un peu deux choses différentes: une spécification peut être différente de la réalité, et aussi il y a des parties d'un programme à qui on ne sait pas forcément donner de spécification. Les erreurs trouvées par Csmith1 sont dans des parties du logiciel qui n'avaient pas de spécification formelle (par exemple l'affichage de code assembleur, depuis la représentation interne du compilateur à un fichier texte à passer à un outil externe), et pas dans des erreurs d'une spécification qui les couvrirait. (Je chipote; mais on ne peut pas vraiment parler de gap spécification/réalité ici.)
1: Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.
Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses. Il faut réfléchir à ça plus en détail mais je ne crois pas qu'il soit correct de dire que ce sont des bugs de Compcert. Dans un cas, c'est un comportement qui n'est pas défini selon la norme C, mais qui est défini par la spécification "Compcert C" qui est plus fine; ce n'est pas un bug, mais une différence d'interprétation. Le second "bug" concerne un comportement de l'interpréteur, pas du compilateur, et il s'agit d'un message d'erreur oublié pour une façon particulière de rejeter le programme sans l'exécuter—donc il n'y a même pas eu d'interprétation incorrecte. Dans le cas du premier soit-disant bug en tout cas, j'ai l'impression que les auteurs n'ont pas compris les garanties données par Compcert.
[^] # Re: Nuance
Posté par gasche . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 8.
Tu mélanges un peu deux choses différentes: une spécification peut être différente de la réalité, et aussi il y a des parties d'un programme à qui on ne sait pas forcément donner de spécification. Les erreurs trouvées par Csmith1 sont dans des parties du logiciel qui n'avaient pas de spécification formelle (par exemple l'affichage de code assembleur, depuis la représentation interne du compilateur à un fichier texte à passer à un outil externe), et pas dans des erreurs d'une spécification qui les couvrirait. (Je chipote; mais on ne peut pas vraiment parler de gap spécification/réalité ici.)
1: Csmith c'est ce que tu appelles "PLDI'11"; je ne suis pas convaincu par cette façon de nommer des articles qui tait l'important (le titre et les auteurs—et l'année) et montre la conférence, peu importante et source de vanité.
Les "erreurs" citées par l'article "Randomized Stress-Testing of Link-Time Optimizers" de Vu Le, Chengnian Sun et Zhendong Su me semblent extrêmement suspectes, pour ne pas dire foireuses. Il faut réfléchir à ça plus en détail mais je ne crois pas qu'il soit correct de dire que ce sont des bugs de Compcert. Dans un cas, c'est un comportement qui n'est pas défini selon la norme C, mais qui est défini par la spécification "Compcert C" qui est plus fine; ce n'est pas un bug, mais une différence d'interprétation. Le second "bug" concerne un comportement de l'interpréteur, pas du compilateur, et il s'agit d'un message d'erreur oublié pour une façon particulière de rejeter le programme sans l'exécuter—donc il n'y a même pas eu d'interprétation incorrecte. Dans le cas du premier soit-disant bug en tout cas, j'ai l'impression que les auteurs n'ont pas compris les garanties données par Compcert.