Frama-C Bug Tracking System - Frama-C
View Issue Details
0000787Frama-CPlug-in > slicingpublic2011-04-11 23:362014-02-12 16:54
pascal 
Anne 
normalminoralways
closedfixed 
Frama-C GIT, precise the release id 
Frama-C Nitrogen-20111001 
0000787: same conditions as 786, sliced program does not terminate when original does (csmith)
cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11231600.1.s.c show_each.c cuoq@ns61143:~/csmith-2.0.0$ ./a.out ^C cuoq@ns61143:~/csmith-2.0.0$ gcc -I runtime s.11231600.1.c show_each.c cuoq@ns61143:~/csmith-2.0.0$ ./a.out [value] Called Frama_C_show_each({4020548907; })
No tags attached.
parent of 0000789closed Anne 12825, sliced program does not terminate 
related to 0000802closed Anne r12951, sliced program does not terminate 
tgz slice_infinite_loop.tgz (38,082) 2011-04-11 23:36
https://bts.frama-c.com/file_download.php?file_id=196&type=bug
Issue History
2011-04-11 23:36pascalNew Issue
2011-04-11 23:36pascalStatusnew => assigned
2011-04-11 23:36pascalAssigned To => Anne
2011-04-11 23:36pascalFile Added: slice_infinite_loop.tgz
2011-04-12 11:38AnneNote Added: 0001734
2011-04-12 11:41AnneNote Added: 0001735
2011-04-12 11:45AnneNote Added: 0001736
2011-04-12 13:47AnneNote Added: 0001738
2011-04-12 16:13AnneNote Added: 0001741
2011-04-12 17:03AnneRelationship addedparent of 0000789
2011-04-13 10:21patrickNote Added: 0001744
2011-04-13 11:12AnneNote Added: 0001745
2011-04-13 14:48AnneNote Added: 0001748
2011-04-13 14:54pascalNote Added: 0001749
2011-04-13 16:00svnCheckin
2011-04-21 09:09AnneRelationship addedrelated to 0000802
2011-04-28 00:12yakobowskiNote Added: 0001807
2011-04-28 00:41yakobowskiNote Added: 0001808
2011-04-28 03:56AnneNote Added: 0001809
2011-04-28 08:55AnneNote Added: 0001810
2011-04-28 09:14yakobowskiNote Added: 0001811
2011-04-28 12:41AnneNote Added: 0001812
2011-04-28 12:51pascalNote Added: 0001813
2011-04-28 13:19AnneNote Added: 0001814
2011-04-28 13:36pascalNote Added: 0001815
2011-04-28 13:50AnneNote Added: 0001816
2011-04-28 14:00AnneNote Added: 0001819
2011-04-28 14:00AnneStatusassigned => resolved
2011-04-28 14:00AnneResolutionopen => fixed
2011-10-10 14:13signolesFixed in Version => Frama-C Nitrogen-20111001
2011-10-10 14:14signolesStatusresolved => closed

Notes
(0001734)
Anne   
2011-04-12 11:38   
When looking at [func_1] in the GUI after : frama-c-gui -cpp-command "gcc -C -E -D__FRAMAC -I. -Iruntime " s.11231600.1.c \ -val -machdep x86_64 -slevel 5000 -slevel-function crc32_gentab:0 there is a lot of "red" code. Is this normal ? For instance, for the initial loop : for (g_113 = 21; (g_113 != 37); g_113 = safe_add_func_int64_t_s_s(g_113, 7)) the incrementation is marked as dead... which then makes an infinite loop. Do you have an idea of what happens here ?
(0001735)
Anne   
2011-04-12 11:41   
First of all, the loop : for (l_316 = 0; (l_316 == 21); ...) is useless.
(0001736)
Anne   
2011-04-12 11:45   
Sorry : this seems to be a wrong hint... The problem is probably elsewhere...
(0001738)
Anne   
2011-04-12 13:47   
I managed to build a small example where : frama-c -slice-return main toto.c -slice-print is ok without the unreachable [retrun] statement, but generate an infinite loop with the [return] ! Probably a problem in the control dependencies computation ? ------------------------------------ int G; void func_1(void) { for (int x = 0; x < 17; x++) { G = 3; if (G) break; // return; // <=== Problem } } int main (int n) { func_1 (); return G; }
(0001741)
Anne   
2011-04-12 16:13   
The problem is similar to the one explained in : https://bts-frama-c.cea.fr/index.php?do=details&task_id=181 We sometime use the value analysis to know if a statement is reachable, but we have to be very careful about that since it can lead to lose some dependencies. I think I will be able to fix the problem above soon, but the slicing will keep a little more things than what is really needed...
(0001744)
patrick   
2011-04-13 10:21   
There is the same problem with the previous code and the command: frama-c -slice-value G -main func_1 toto.c -slice-print.
(0001745)
Anne   
2011-04-13 11:12   
One can also change [for (int x = 0; x < 17; x++)] into [while (1)]. In the PDG, [while (1) S;] should be equivalent to [W: S; goto W;] but it seems that there are some difference in this example, because with the [return] statement, the [goto W] becomes syntactically unreachable. Hope I will find how to fix that !
(0001748)
Anne   
2011-04-13 14:48   
Well, I try hard, but I think there are only two solutions : 1- either we don't use [Db.Value.is_reachable_stmt] during the dataflow analysis used to build the PDG; 2- or we use [Db.Value.is_reachable_stmt] both in the PDG dataflow analysis AND during the postdominator computation used for the control dependencies. (1) is a quick fix, but we lose precision in the slicing computation. (2) needs some work, but would also make possible to deal with the old#181 mentioned above and would give better results.
(0001749)
pascal   
2011-04-13 14:54   
Copy of issue 181 from old Bug Tracking System: On avait décidé d’utiliser Locations.Location_Bytes.is_zero cond et not (Locations.Location_Bytes.intersects cond Locations.Location_Bytes.singleton_zero) pour savoir si une condition était toujours vraie ou fausse, et donc ne pas considérer le if correspondant comme une dépendance de contrôle dans le PDG. Malheureusement, ce traitement était un peu rapide car d’une part, on perd les dépendances indirectes : if (c) { x = 1; if (x>0) y = 3; } dans cet exemple, y ne dépend certes pas de x>0 qui est toujours vrai, mais il dépend de c que l’on a normalement indirectement via la dépendance de x>0. On pourrait envisager de gérer ce cas particulier, mais ça devient très compliqué en présence de code mal structuré (goto). Si on souhaite avoir cette fonctionnalité, il faudrait intervenir au niveau du CFG pour enlever les arrêtes impossible après analyse de valeur... En attendant, je suis obligé d’enlever ce traitement !
(0001807)
yakobowski   
2011-04-28 00:12   
Commit 13053 adds the second functionality of comment 0001748: postdominators that use the results of the value analysis, thanks to Pascal's efficient nudging and help. I tried to activate this within the slicing (just change Db.Postdominators.foo by Db.PostdominatorsValue.foo in pdg/ctrlDpds.ml), and some results are already more precise on some of the examples. I suppose that it is also possible to undo some of the changes of commit 12874, but I do not understand the slicing well enough to do that. Nevertheless, there are probably some bugs with this commit. For example, the third oracle for unitialized.c is ill-typed.
(0001808)
yakobowski   
2011-04-28 00:41   
Another remark, more distantly linked to this bug; it actually comes from reading the diff of commmit 12874. Lines such as "warning: no final state. Probably unreachable..." are emitted with ~current:true, which is good. But ~current probably depends on the way the last dataflow went, and does not necessarily point to a very meaningful location. Explicitly setting the loc to the last statement of the given function would be more robust.
(0001809)
Anne   
2011-04-28 03:56   
Thank you ! I'll have a look at [PostdominatorsValue] because I guess I have to do the same kind of things in the other data-flow analyses in PDG to get consistent results. I also have to figure out whether this is enough to solve the #802 which involves syntactically unreachable code.
(0001810)
Anne   
2011-04-28 08:55   
Maybe [From] should use [PostdominatorsValue] as well ?
(0001811)
yakobowski   
2011-04-28 09:14   
Regarding [From] and [PostdominatorsValue], we tried that yesterday. The results become sometimes hard to understand, because some dependencies disappear altogether. Pascal had a very reasonable explanation for this, but the intuition might be difficult to convey to the end-user.
(0001812)
Anne   
2011-04-28 12:41   
About your comment (0001808): you are right, I did the modification (not commited yet). About your last comment, do you really think that the end-user uses directly the result of [From] ? I think that it is more an internal tool to be used by other analyses, don't you think so ?
(0001813)
pascal   
2011-04-28 12:51   
Yes, there is a need for end-user-readable dependencies. The results of -deps are very readable and perfectly understandable. If we change the meaning of these dependencies so that, for instance, depending on a variable that can only have one value means not really depending on it, on the other hand, it will become very confusing. It is possible to have another notion of dependencies that milk the values for all they are worth to the detriment of intuition, but these should be available as a complement of the existing intuitive ones.
(0001814)
Anne   
2011-04-28 13:19   
Ok : I agree with you about the end-user-readable dependencies. I has to think a little more about it to what we could do to enhance the precision of the PDG. My first idea was more about cutting branches than really using the value, because when you have : int G, X; void f (void) { G = X; } ... X = 0; f(); I cannot say that G depends on nothing, else [X=0] would be removed ! Constant propagation would be more useful in this case... At the moment, I have modified the PDG computation, and tests seem ok (except variadic as I told you) and now, I am on my way to test on your big exemples, Pascal (crossing my fingers ;-) )
(0001815)
pascal   
2011-04-28 13:36   
Good point about X=0; G=X; In fact, there are three categories of dependencies: data, control, and address. Address dependencies are already exploited aggressively, because it's the only thing to do. On the program Y=12; *P=X; we do not say that Y depends on P and X just because if P had been different (pointed on Y) then Y would indeed have been computed from P and X. Control dependencies are what we can now exploit aggressively with the new post-dominators. Depending on a condition that is always true, etc. Data dependencies are not currently aggressively exploited but I thought we could go in that direction for consistency. So I am happy to see that you, Anne, for slicing, also do not wish dependencies that exploit the definition so aggressively, at least in the case of these latter ones. The problem for the end-user is that its look as strange to him when it happens for control than when it happens for data (so you can imagine how he would feel now).
(0001816)
Anne   
2011-04-28 13:50   
Yes... We have to find a good compromise... PS. I think that every thing is fine, now :-) I'll commit soon !
(0001819)
Anne   
2011-04-28 14:00   
Fixed in rev 13064. I close this issue since the From problem not really the same probleme : it is more about precision enhancement.