Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Related Changesets ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001025Frama-CKernelpublic2011-11-21 11:452014-02-12 16:58
Reporterfgarnier 
Assigned Toyakobowski 
PrioritylowSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Carbon-20110201 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001025: Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
DescriptionHello,
I am developing some Frama-c plugin to extract some counter
automata based models of C programs, and I am currently developing
this plugin using the Carbon-20110201 release.

To generate our model, I am using some graph traversal algorithm on
the Control flow graph computed by Cil, and I do perform
some analysis on the the arguments of the instructions.

At some point, I do traverse a "Skip" type instruction, and the value
contained in the the Cil_types.location argument is :


"In file : Cabs2cil_start, from line 0 col -1 to line 0 col -1."
The file Cabs2cil_start appears to be some Framac file, issued in
the carbon version. This is strange, because others instruction that
contains location positions, used to contain value that deal with
the analyzed C source code -- And I was expecting to get such a value.

After some time spent on the Mantis BTS, I noticed that some issues
were the name "Cabs2cil_start" appeared, were solved, but I
can't figure out if this will solve the problem I get. Maybe I won't get
this problem anymore, when I will migrate from Carbon to the new
Nitrogen version, but I prefer to point this strange thing to you.

I have two extra questions : Concerning the Skip instruction, does it
mean that the control goes through the statement without performing
any operation ?

Is it still worth reporting bugs on the Carbon version of Frama-C ?

Best regards,
 Florent Garnier.
Additional InformationThe Skip "instruction" is defined in the file Cil_types.ml.


and stmtkind =
  | Instr of instr
  (** An instruction that does not contain control flow. Control
   * implicitly falls through. *)

  | Return of exp option * location
   (** The return statement. This is a leaf in the CFG. *)


 [...]

 and instr =
    Set of lval * exp * location (** An assignment. A cast is present
                                             if the exp has different type
                                             from lval *)
  [...]

  | Skip of location

  | Code_annot of code_annotation * location
TagsNo tags attached.
Attached Filestgz file icon debug.tgz [^] (3,537 bytes) 2011-11-22 11:49
? file icon vis.ml [^] (627 bytes) 2011-11-25 10:58 [Show Content]
tgz file icon Debug_plugin.tgz [^] (9,211 bytes) 2011-11-28 15:59

- Relationships

-  Notes
(0002492)
fgarnier (reporter)
2011-11-21 15:29

I did port my current implementation of the plugin so that it compiles and run
using the nitrogen version of Frama-c. I still have the same problem.


Best regards,
 Florent.
(0002496)
monate (reporter)
2011-11-21 20:51

Hi,
Thanks for your report. Could you post the C source code that leads to such inconsistant locations?
(0002497)
yakobowski (manager)
2011-11-21 23:34

Hi Florent;

Regarding your other questions

- it is still worth reporting bugs in Carbon, but reproducing them on Nitrogen beforehand would be a strong plus;

- the Skip instruction of Cil is supposed to be a Nop. Neither the control-flow nor the memory state are changed.
(0002500)
fgarnier (reporter)
2011-11-22 11:48

Thank you for your fast answers !

I have to correct something concerning the "bug" under the Nitrogen Version,
I think I get confused at some point while testing the plugin after I made
it compliant with the Nitrogen release -- I think I launched frama-c carbon
from a shell in which my environment variables weren't yet updated, sorry for that.

By the way,
I don't get this "Cabs2cil_start, from line 0 col -1 to line 0 col -1." anymore, while pretty printing location information under Nitrogen.

I either get :

In statement :42, skipping to statement 43, located at In file : , from line 0 col -1 to line 0 col -1.

or

In statement :57, skipping to statement 58, located at In file : examples/veridyc/main.c, from line 25 col 8 to line 25 col 35.


which looks fine. I bet in this case that "from line 0 col -1 to line 0 col -1." correspond to a statment added by Cil, that does not correspond to a real
source file location.


I am uploading the C-source file of the example that generates the aforementioned behavior under the Carbon release.

Best regards,
 Florent.
(0002501)
fgarnier (reporter)
2011-11-22 11:50

ps : The file that generates this problem under the carbon verion is : main.c .

Florent.
(0002502)
yakobowski (manager)
2011-11-24 12:14
edited on: 2011-11-25 09:51

Hi Florent,

I've partly reproduced the bug. Those skip statements are introduced inside "undefined sequences" compound statements. It seems that Cil replaces some subparts of those "undefined sequences", and replaces them by Skip.

However, with my visitor, all statements have a correct location, even the Skip ones. Does your plugin use a copy visitor somewhere?

(0002504)
yakobowski (manager)
2011-11-25 10:57

Ok, after a careful analysis, the Skip are here for a good reason. In a line such as "if (strstr(line, "put") == line)", there is a possible unspecified sequence, because line is used both in the call and in the comparison. The Skip are used to encode which expressions overlap. So the generated code is in fact

{ // Unspecified sequence
tmp = strstr(line, "put");
// Skip statement, that carries the fact that 'line' is used by a second statement later
}
if (tmp == line) {...}

It is essentially equivalent to

{// Unspecified sequence
tmp1 = strstr(line, "put");
tmp2 = tmp1 == line;
}
if (tmp2)

In this form, the unspecified sequence is much more obvious, but the 'if' is less legible, and there is one more temporary.


Back to the original point, can you reproduce the bug on Nitrogen without your plugin? I'm using the visitor attached to see the locations on the Skip.
(0002505)
fgarnier (reporter)
2011-11-25 14:50

Hi Boris,
 Since I migrated under Frama-c Nitrogen, I have not been concerned again with
the problem I first described. I fetched the visitor you uploaded, I will try
to see what happen if I use the it.


I am using inplace visitors, and I only perform reading operation on the AST.

"
class flatac_visitor (prj : Project.t ) = object (self)
  inherit Visitor.generic_frama_c_visitor (prj) (Cil.inplace_visit())
"

I wrote a simpler debugging visitor that showed me the same problem under
Carbon -- In order to better locate the source of my issue, however, it seems that everything is correct under Nitrogen for both my visitors. I will
reinstall the Carbon version at home this week-end to check how your visitor
behaves under Carbon.

Bests,
 Florent.
 
 ps : Thank you for your support !
(0002506)
yakobowski (manager)
2011-11-25 15:13

Hi Florent !

Actually I was refering to your note 0002500, were you mentioned you sometimes still got messages like
"In statement :42, skipping to statement 43, located at In file : , from line 0 col -1 to line 0 col -1."

The final location corresponds to Cil_datatype.Location.unknown, which we try to eradicate from our ast. If you can get this message on Nitrogen with an unmodified Ast (and your visitor seems okay regarding this point), we are definetely interested. And no need to test this on Carbon.
(0002509)
fgarnier (reporter)
2011-11-28 16:14

Hi Boris,
 I uploaded some small plugin that performs the traversal of the control
flow graph computed thanks to the primitives of the Cfg module, using the successor relation defined in the Cil_types.stmt type definition.

I don't get the problem using your visitor, which performs well. So, maybe
there is rather an issue with the Cfg --prepareCfg, computeCfginfo-- than
than something else. I included it as well in the tarball, so that you can
compare the output of both visitors. I still have the problem when I use


To be short :
The plugin only performs a graph traversal of the Cfg computed using Frama-c,
then builds an instance of the class cautomaton defined in the file cautomata.ml.

I do print the location informations in the method add_trans_from_stmt of the
class panalyse defined in the file c2cautomatanalys.ml.

I lacked time to write a shorter plugin that displays the problem, however, I
will be able to do so, if it helps you.

Best regards,
 Florent.
(0002510)
fgarnier (reporter)
2011-11-28 16:16

The pluging is a dynamic one and should compile and install
using make && make install.

Bests,
 Florent.
(0002511)
fgarnier (reporter)
2011-11-28 16:25

The file main.c provided in the debug.tgz tarball shows the issue.
 Florent.
(0002678)
yakobowski (manager)
2012-02-08 21:38

Hi Florent,

Sorry for having left this bug dormant so long. As you thought, the issue lies in the cfg normalization function. More precisely, Cfg.prepareCFG uses Location.unknown for the labels it inserts when removing 'continue', 'break' or 'switch' instructions. This can be fixed, but there is no good location to use: those statements are not part of the original source, and do not really correspond to an original statement either.

Also, you might possibly avoid calling Cfg.prepareCFG yourself entirely. Indeed, Frama-C "-simplify-cfg" option does essentially the same thing. For some reason, it also inserts less useless labels (hence less Skip), which results in a cleaner AST.

Hope this helps
(0002679)
yakobowski (manager)
2012-02-08 21:52

Ok, I have found some good locations, that will hopefully not interfere with pre-existing ones. This bug will thus be fixed in the next version of Frama-C. If it is useful, I can send you the patch privately.
(0004680)
yakobowski (manager)
2014-02-12 16:58

Fix committed to stable/neon branch.

- Issue History
Date Modified Username Field Change
2011-11-21 11:45 fgarnier New Issue
2011-11-21 14:45 signoles Status new => assigned
2011-11-21 14:45 signoles Assigned To => virgile
2011-11-21 15:29 fgarnier Note Added: 0002492
2011-11-21 20:51 monate Note Added: 0002496
2011-11-21 23:34 yakobowski Note Added: 0002497
2011-11-22 11:48 fgarnier Note Added: 0002500
2011-11-22 11:49 fgarnier File Added: debug.tgz
2011-11-22 11:50 fgarnier Note Added: 0002501
2011-11-24 12:14 yakobowski Note Added: 0002502
2011-11-24 12:15 yakobowski Status assigned => confirmed
2011-11-24 12:48 yakobowski Note Added: 0002503
2011-11-25 09:49 yakobowski Note Deleted: 0002503
2011-11-25 09:51 yakobowski Note Edited: 0002502
2011-11-25 10:57 yakobowski Note Added: 0002504
2011-11-25 10:58 yakobowski File Added: vis.ml
2011-11-25 10:58 yakobowski Status confirmed => feedback
2011-11-25 14:50 fgarnier Note Added: 0002505
2011-11-25 15:13 yakobowski Note Added: 0002506
2011-11-28 15:59 fgarnier File Added: Debug_plugin.tgz
2011-11-28 16:14 fgarnier Note Added: 0002509
2011-11-28 16:16 fgarnier Note Added: 0002510
2011-11-28 16:25 fgarnier Note Added: 0002511
2012-01-18 23:29 yakobowski Status feedback => assigned
2012-01-18 23:29 yakobowski Assigned To virgile => yakobowski
2012-02-08 21:38 yakobowski Note Added: 0002678
2012-02-08 21:40 yakobowski Priority normal => low
2012-02-08 21:40 yakobowski Status assigned => confirmed
2012-02-08 21:40 yakobowski Summary Unsound lexing position --Cil_types.location-- given as argument of the Skip(loc) -- type : Cil_types.instr, in the Carbon-2011 => Cil.prepareCfg (or -simplify-cfg option) insert dummy locations in the ast
2012-02-08 21:52 yakobowski Note Added: 0002679
2012-02-08 22:16 svn Checkin
2012-02-08 22:16 svn Status confirmed => resolved
2012-02-08 22:16 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2014-02-12 16:58 yakobowski Note Added: 0004680
2014-02-12 16:58 yakobowski Status closed => resolved


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker