Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0000787Frama-CPlug-in > slicingpublic2011-04-11 23:362014-02-12 16:54
Reporterpascal 
Assigned ToAnne 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Nitrogen-20111001 
Summary0000787: same conditions as 786, sliced program does not terminate when original does (csmith)
Descriptioncuoq@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; })
TagsNo tags attached.
Attached Filestgz file icon slice_infinite_loop.tgz [^] (38,082 bytes) 2011-04-11 23:36

- Relationships
parent of 0000789closedAnne 12825, sliced program does not terminate 
related to 0000802closedAnne r12951, sliced program does not terminate 

-  Notes
(0001734)
Anne (reporter)
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 (reporter)
2011-04-12 11:41

First of all, the loop :
  for (l_316 = 0; (l_316 == 21); ...)
is useless.
(0001736)
Anne (reporter)
2011-04-12 11:45

Sorry : this seems to be a wrong hint... The problem is probably elsewhere...
(0001738)
Anne (reporter)
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 (reporter)
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 (developer)
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 (reporter)
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 (reporter)
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 (reporter)
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 (manager)
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 (manager)
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 (reporter)
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 0000802 which involves syntactically unreachable code.
(0001810)
Anne (reporter)
2011-04-28 08:55

Maybe [From] should use [PostdominatorsValue] as well ?
(0001811)
yakobowski (manager)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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 (reporter)
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.

- Issue History
Date Modified Username Field Change
2011-04-11 23:36 pascal New Issue
2011-04-11 23:36 pascal Status new => assigned
2011-04-11 23:36 pascal Assigned To => Anne
2011-04-11 23:36 pascal File Added: slice_infinite_loop.tgz
2011-04-12 11:38 Anne Note Added: 0001734
2011-04-12 11:41 Anne Note Added: 0001735
2011-04-12 11:45 Anne Note Added: 0001736
2011-04-12 13:47 Anne Note Added: 0001738
2011-04-12 16:13 Anne Note Added: 0001741
2011-04-12 17:03 Anne Relationship added parent of 0000789
2011-04-13 10:21 patrick Note Added: 0001744
2011-04-13 11:12 Anne Note Added: 0001745
2011-04-13 14:48 Anne Note Added: 0001748
2011-04-13 14:54 pascal Note Added: 0001749
2011-04-13 16:00 svn Checkin
2011-04-21 09:09 Anne Relationship added related to 0000802
2011-04-28 00:12 yakobowski Note Added: 0001807
2011-04-28 00:41 yakobowski Note Added: 0001808
2011-04-28 03:56 Anne Note Added: 0001809
2011-04-28 08:55 Anne Note Added: 0001810
2011-04-28 09:14 yakobowski Note Added: 0001811
2011-04-28 12:41 Anne Note Added: 0001812
2011-04-28 12:51 pascal Note Added: 0001813
2011-04-28 13:19 Anne Note Added: 0001814
2011-04-28 13:36 pascal Note Added: 0001815
2011-04-28 13:50 Anne Note Added: 0001816
2011-04-28 14:00 Anne Note Added: 0001819
2011-04-28 14:00 Anne Status assigned => resolved
2011-04-28 14:00 Anne 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


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker