Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000963Frama-CPlug-in > slicingpublic2011-09-14 14:132014-02-12 16:59
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000963: Sliced program computes differently from original (csmith)
DescriptionBon, j'ai peut-être un peu perdu la main, alors il faudra m'excuser si je rapporte un non-problème, ou si j'oublie des détails au début.

L'architecture cible est maintenant -machdep x86_64 (on a maintenant confiance dans l'analyse de valeurs sur cette architecture).

La commande de slicing utilisée est dans le script slice_src_dest.sh

Pour compiler l'original ou le programme slicé:

gcc -Iruntime s.14134425.9.c show_each.c -o orig
gcc -Iruntime s.14134425.9.s.c show_each.c -o slice

(c'est un gcc 64-bit)

J'obtiens les fichiers .exec et .execs, qui sont différents.
TagsNo tags attached.
Attached Filestgz file icon s.tgz [^] (107,419 bytes) 2011-09-14 14:13
c file icon s.c [^] (66,433 bytes) 2011-09-14 14:35 [Show Content]

- Relationships

-  Notes
(0002264)
pascal (reporter)
2011-09-14 14:36

Je savais bien que j'allais oublier quelque chose.
J'ai attaché une version avec substitution, non testée.
(0002265)
pascal (reporter)
2011-09-14 14:41

> J'en étais sure que tu en trouverais d'autres !

On est sur des périodes de 18h avec 12 processeurs, comparable au temps passé à trouver les précédents bugs. Je varie aussi certains paramètres de temps en temps pour essayer de dénicher tous les bugs qui peuvent être trouvés de cette façon. Celui-ci s'est montré rapidement après que j'aie réglé l'analyse de valeurs sur "moins précis", mais ça ne veut pas forcément dire grand-chose, ça peut être une coïncidence.
(0002268)
Anne (reporter)
2011-09-14 16:14

Le problème est le suivant :
- seule l'instruction [i = 0;] dépend du [goto];
- la boucle n'est pas considérée comme une vrai boucle car on emprunte jamais l'arc de bouclage ;
- le [i] n'est donc pas utile.

En bref, on ôte le [goto] parce qu'on a une boucle et on ôte la boucle puisqu'on a un goto : pas cool :-/
(0002269)
Anne (reporter)
2011-09-14 17:55

Je pense qu'il y a un défaut dans le calcul des dépendances de contrôle pour les boucles... J'avais essayé de réparer les cas qui conduisaient à introduire des boucles infinies, mais je n'avais pas vu que le problème était plus grave.

J'essaye de remettre tout ça à plat demain.
(0002275)
Anne (reporter)
2011-09-16 14:52

Oouuinn ! j'y arrive pas... :-(

Je vais déjà essayer de résumer le problème (surtout pour moi dans un premier temps, et pour mémoire quand je serai partie).

Quand on a [while(1) S; LS: ], on aimerait pouvoir générer les dépendances de contrôle pour le corps de boucle exactement comme si on avait [L: S; goto L; LS: ]. Dans le second cas, tout se passe bien parce que le [goto] est à la FIN du corps de boucle, si bien qu'il récupère les bonnes dépendances vis à vis des instructions de S. Dans le cas du while, comme il est au DEBUT du corps de boucle, on y passe déjà une première fois quand on entre dans la boucle, et non pas seulement en cas de bouclage réel.
Il est difficile de faire "semblant" d'avoir le [goto] car on utilise par exemple le calcul de post-dominateurs, qui utilise Dataflow, c'est-a-dire les successeurs calculés par Cil. Par ailleurs, ce ne sont pas directement les dépendances sur le [while] qui posent un problème, mais plutôt celles sur les [goto] situés dans la boucle.
Dans le cas présent, c'est le [goto L] qui devrait contrôler les instructions du début de boucle, et comme on garde [Frama_C_show_each], on garderait alors aussi le [goto]. Mais ce n'est pas le cas car le successeur lexical (*) du [goto] est le [while] et on a donc l'impression que le début de boucle ne dépend pas du [goto] (car on croit qu'on y va avec ou sans le goto). Dans ce cas très précis, on pourrait bricoler le successeur lexical quand on s'aperçoit que c'est une boucle, mais on aurait encore le problème dès qu'on ajouterait d'autres instructions en fin de boucle.

(*) successeur lexical = instruction sur laquelle on se retrouverait si on remplaçait le [goto] par un [nop].

Sur ce, je retourne agiter mes trois neurones pour essayer de trouver une solution.
(0002280)
Anne (reporter)
2011-09-19 11:26

Finalement, je suis en train de faire une analyse des post-dominateurs spécifiquement adaptée aux besoins du PDG. De toute façon, il y en avait déjà une pour gérer le cas des boucles infinies, et du coup, autant tout faire là.
L'objectif est de simuler la transformation [while] -> [goto].
(0002281)
Anne (reporter)
2011-09-19 11:50

Il faut que je vérifie plus en détail, car je n'en crois pas mes yeux 8-/ mais il semblerait qu'en calculant simplement les post-dominateurs "correctement", ça corrige le problème ci-dessus, plus divers bugs dans les oracles ! :-)
La différence proviendrait du fait que [!Db.Postdominators.stmt_postdominators kf stmt] contient [stmt] alors que normalement, une instruction ne se post-domine elle-même qu'en cas de boucle infinie. J'avais bricolé quelque chose pour néanmoins utiliser ce résultat, mais on dirait que c'était faux !!!
A confirmer, donc...
(0004736)
Anne (reporter)
2014-02-12 16:59

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-09-14 14:13 pascal New Issue
2011-09-14 14:13 pascal Status new => assigned
2011-09-14 14:13 pascal Assigned To => Anne
2011-09-14 14:13 pascal File Added: s.tgz
2011-09-14 14:35 pascal File Added: s.c
2011-09-14 14:36 pascal Note Added: 0002264
2011-09-14 14:41 pascal Note Added: 0002265
2011-09-14 16:14 Anne Note Added: 0002268
2011-09-14 17:55 Anne Note Added: 0002269
2011-09-16 14:52 Anne Note Added: 0002275
2011-09-19 11:26 Anne Note Added: 0002280
2011-09-19 11:50 Anne Note Added: 0002281
2011-09-19 15:50 svn Checkin
2011-09-19 15:50 svn Status assigned => resolved
2011-09-19 15:50 svn Resolution open => fixed
2011-10-10 14:13 signoles Fixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14 signoles Status resolved => closed
2011-12-18 20:09 pascal Status closed => feedback
2011-12-18 20:09 pascal Resolution fixed => reopened
2011-12-18 20:09 pascal View Status private => public
2011-12-19 09:51 pascal Status feedback => closed
2011-12-19 09:51 pascal Resolution reopened => fixed
2014-02-12 16:59 Anne Note Added: 0004736
2014-02-12 16:59 Anne Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker