0000969: Sliced program computes differently from original (csmith)

(0002283)
Anne (reporter)
2011-09-19 16:37
edited on: 2011-09-19 16:39

Waouh... ça a été vite ! :-(
Merci quand même... je regarde ça.

(0002284)
pascal (reporter)
2011-09-19 16:45

> Waouh... ça a été vite !

Non, j'avais laissé 8 instances trouver tous les bugs qu'elles pouvaient pendant plusieurs jours, et j'ai seulement rejoué le test des exemples qui ne passaient déjà pas avant tes derniers correctifs. Il y en avait une page dans ls, et il n'en restait plus que deux après nettoyage, les deux que tu vois.

(0002292)
yakobowski (manager)
2011-09-19 22:03

Je vous laisse vérifier si ce n'était pas le même problème que le 968, je n'ai pas trouvé l'incantation magique pour générer la trace.

(0002293)
pascal (reporter)
2011-09-19 22:07

Le bug est toujours présent dans 15182 après correction du 968.

Boris: La commande slice_src_dest.sh fournie dans 968.tgz génère un programme slicé, qu'il faut compiler en 64-bit pour le comparer à l'original. J'ai un script plus automatique pour passer sur des accumulations de programmes douteux obtenues pendant que d'autres bugs sont en train d'être regardés, donc ça n'est jamais la peine de faire ces vérifications manuellement.

(0002294)
Anne (reporter)
2011-09-20 08:01
edited on: 2011-09-20 08:04

Bon, enfin un problème différent des dépendances de contrôle,mais peut-être pas directement lié au slicing...
Voilà un petit exemple du problème :
---------------------------------------------------------
struct S0 { signed f1 : 29; };
int main (void) {
  int g_341;
  struct S0 l_175[1];
  int l_275 = 0;
  g_341 = (l_175[l_275].f1 = (int)0x8C8AB594L);
  Frama_C_show_each (g_341);
}
---------------------------------------------------------
et voilà les commandes :

echo "===== Generate slice"
frama-c -slice-calls Frama_C_show_each toto.c \
-then-on 'Slicing export' -print -ocode toto.s.i

echo "===== Compile original"
gcc toto.c show_each.c -o toto

echo "===== Compile slice"
gcc toto.s.i show_each.c -o toto.s

echo "===== Run original"
./toto

echo "===== Run slice"
./toto.s
---------------------------------------------------------
Le résultat est étrange :
[value] Analyzing a complete application starting at main
[value] Called Frama_C_show_each({-1937066604})
===== Run original
[value] Called Frama_C_show_each({210417044})
===== Run slice
[value] Called Frama_C_show_each({2357900692})

---------------------------------------------------------
La décomposition par CIL fait intervenir :
int __attribute__((__FRAMA_C_BITFIELD_SIZE__(29))) tmp;
c'est peut-être ça la problème ?

Je continue à regarder.

(0002295)
Anne (reporter)
2011-09-20 08:23

Le slicing me parait correct...

Je vous laisse regarder, car je ne vois pas quoi faire de plus. On a le problème sans passer par le slicing en faisant :

frama-c toto.c -print -ocode toto.s.i

Je pense que le problème est que la compilation ne tient pas compte de l'attribut de taille, et donc la valeur de la constante n'est pas tronquée. Ça se voit mieux avec : (int)0x8F000000

===== Run original
[value] Called Frama_C_show_each({0xf000000})
===== Run slice
[value] Called Frama_C_show_each({0x8f000000})

(0002296)
pascal (reporter)
2011-09-20 08:44

Ça ressemble à un bug connu mais pas encore corrigé, le 933.

(0002297)
Anne (reporter)
2011-09-20 08:49

Oui, en effet, ça semble être le même problème...

(0002298)
Anne (reporter)
2011-09-20 08:50

Plus d'autres bugs ? :-D

(0002300)
pascal (reporter)
2011-09-20 09:33

Fixed by commit 15185.

(0002394)
pascal (reporter)
2011-10-13 14:37

Peuh! Déjà corrigé.

Issue History
Date Modified	Username	Field	Change
2011-09-19 16:16	pascal	New Issue
2011-09-19 16:16	pascal	Status	new => assigned
2011-09-19 16:16	pascal	Assigned To	=> Anne
2011-09-19 16:16	pascal	File Added: 969.tgz
2011-09-19 16:37	Anne	Note Added: 0002283
2011-09-19 16:39	Anne	Note Edited: 0002283
2011-09-19 16:45	pascal	Note Added: 0002284
2011-09-19 22:03	yakobowski	Note Added: 0002292
2011-09-19 22:07	pascal	Note Added: 0002293
2011-09-20 08:01	Anne	Note Added: 0002294
2011-09-20 08:02	Anne	Note Edited: 0002294
2011-09-20 08:04	Anne	Note Edited: 0002294
2011-09-20 08:23	Anne	Note Added: 0002295
2011-09-20 08:44	pascal	Note Added: 0002296
2011-09-20 08:45	pascal	Relationship added	related to 0000933
2011-09-20 08:49	Anne	Note Added: 0002297
2011-09-20 08:50	Anne	Note Added: 0002298
2011-09-20 08:55	pascal	Assigned To	Anne => pascal
2011-09-20 09:33	pascal	Note Added: 0002300
2011-09-20 09:33	pascal	Status	assigned => resolved
2011-09-20 09:33	pascal	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-10-13 14:36	pascal	Status	closed => feedback
2011-10-13 14:36	pascal	Resolution	fixed => reopened
2011-10-13 14:36	pascal	Category	Plug-in > slicing => Kernel
2011-10-13 14:37	pascal	Note Added: 0002394
2011-10-13 14:37	pascal	Status	feedback => closed
2011-10-13 14:37	pascal	Resolution	reopened => fixed
2011-12-18 20:08	pascal	Status	closed => feedback
2011-12-18 20:08	pascal	Resolution	fixed => reopened
2011-12-18 20:08	pascal	View Status	private => public
2011-12-19 09:50	pascal	Status	feedback => closed
2011-12-19 09:50	pascal	Resolution	reopened => fixed

Notes
(0002283) Anne (reporter) 2011-09-19 16:37 edited on: 2011-09-19 16:39	Waouh... ça a été vite ! :-( Merci quand même... je regarde ça.

(0002284) pascal (reporter) 2011-09-19 16:45	> Waouh... ça a été vite ! Non, j'avais laissé 8 instances trouver tous les bugs qu'elles pouvaient pendant plusieurs jours, et j'ai seulement rejoué le test des exemples qui ne passaient déjà pas avant tes derniers correctifs. Il y en avait une page dans ls, et il n'en restait plus que deux après nettoyage, les deux que tu vois.

(0002292) yakobowski (manager) 2011-09-19 22:03	Je vous laisse vérifier si ce n'était pas le même problème que le 968, je n'ai pas trouvé l'incantation magique pour générer la trace.

(0002293) pascal (reporter) 2011-09-19 22:07	Le bug est toujours présent dans 15182 après correction du 968. Boris: La commande slice_src_dest.sh fournie dans 968.tgz génère un programme slicé, qu'il faut compiler en 64-bit pour le comparer à l'original. J'ai un script plus automatique pour passer sur des accumulations de programmes douteux obtenues pendant que d'autres bugs sont en train d'être regardés, donc ça n'est jamais la peine de faire ces vérifications manuellement.

(0002294) Anne (reporter) 2011-09-20 08:01 edited on: 2011-09-20 08:04	Bon, enfin un problème différent des dépendances de contrôle,mais peut-être pas directement lié au slicing... Voilà un petit exemple du problème : --------------------------------------------------------- struct S0 { signed f1 : 29; }; int main (void) { int g_341; struct S0 l_175[1]; int l_275 = 0; g_341 = (l_175[l_275].f1 = (int)0x8C8AB594L); Frama_C_show_each (g_341); } --------------------------------------------------------- et voilà les commandes : echo "===== Generate slice" frama-c -slice-calls Frama_C_show_each toto.c \ -then-on 'Slicing export' -print -ocode toto.s.i echo "===== Compile original" gcc toto.c show_each.c -o toto echo "===== Compile slice" gcc toto.s.i show_each.c -o toto.s echo "===== Run original" ./toto echo "===== Run slice" ./toto.s --------------------------------------------------------- Le résultat est étrange : [value] Analyzing a complete application starting at main [value] Called Frama_C_show_each({-1937066604}) ===== Run original [value] Called Frama_C_show_each({210417044}) ===== Run slice [value] Called Frama_C_show_each({2357900692}) --------------------------------------------------------- La décomposition par CIL fait intervenir : int __attribute__((__FRAMA_C_BITFIELD_SIZE__(29))) tmp; c'est peut-être ça la problème ? Je continue à regarder.

(0002295) Anne (reporter) 2011-09-20 08:23	Le slicing me parait correct... Je vous laisse regarder, car je ne vois pas quoi faire de plus. On a le problème sans passer par le slicing en faisant : frama-c toto.c -print -ocode toto.s.i Je pense que le problème est que la compilation ne tient pas compte de l'attribut de taille, et donc la valeur de la constante n'est pas tronquée. Ça se voit mieux avec : (int)0x8F000000 ===== Run original [value] Called Frama_C_show_each({0xf000000}) ===== Run slice [value] Called Frama_C_show_each({0x8f000000})

(0002296) pascal (reporter) 2011-09-20 08:44	Ça ressemble à un bug connu mais pas encore corrigé, le 933.

(0002297) Anne (reporter) 2011-09-20 08:49	Oui, en effet, ça semble être le même problème...

(0002298) Anne (reporter) 2011-09-20 08:50	Plus d'autres bugs ? :-D

(0002300) pascal (reporter) 2011-09-20 09:33	Fixed by commit 15185.

(0002394) pascal (reporter) 2011-10-13 14:37	Peuh! Déjà corrigé.