Trying to analyse dead code in Frama-C

[tmarti2]

Hi,

I tried to run this on Frama-C, which contains a lot of dead code, but for some reason the tool finds only a really small portion of the dead code. I added -bin-annot as mentionned on the forum, and -keep-locs is activated by default, but it did not help. I also tried to tun the tool with all options and it changed nothing. Am I missing something ?

Thanks for the tool anyway !

[fantazio]

Hey, thanks for using the tool.

I'll try and look into it when I have time.

In the meantime, can you try running the command below ?

dead_code_analyzer --nothing --verbose <your_paths>

with <your_paths> whatever you were giving as input to the tool.
This should only print out a Scanning <file_path> line for each file analyzed. If you see any Ignoring <file_path> (no source?) line, that means the analyzer did not find the .ml/.mli file corresponding to the current .cmt/.cmi.

If you have any specific exported value that you know is dead (not referenced anywhere), and want to look for it specifically, you can reduce the volume of the report by using:

dead_code_analyzer --nothing -E all --references <your_paths> <file_path>

with <your_paths> whatever you were giving as input to the tool, and <file_path> the .cmi file of interest (corresponding to the .mli exporting the value). This will limit the reported values to those found in <file_path>.
In addition, using -E calls:<int> instead of -E all, with <int> greater than 0, will report exported values used at most <int> times and display their use-sites. This may be useful to see if the analyzer did not actually find uses of the value.

[tmarti2]

As you said, most of Frama-C's file are ignored with your first command (3000 files are ignored over 3800 files). I was trying the run the command on all sources, just to see what it does.

I tried the 2nd command you gave but it outputs the same thing as before, for instance :

❯ dead_code_analyzer --underscore --references . _build/default/src/.frama_c_kernel.objs/byte/frama_c_kernel__Logic_builtin.cmi
Scanning files...
 [DONE]

.> UNUSED EXPORTED VALUES:
=========================

Nothing else to report in this section
--------------------------------------------------------------------------------


.> UNUSED METHODS:
=================

Nothing else to report in this section
--------------------------------------------------------------------------------


.> UNUSED CONSTRUCTORS/RECORD FIELDS:
====================================

Nothing else to report in this section
*** INFO: Several binary files cannot be read.  Please run ./remove_bad_files.sh to remove them.
--------------------------------------------------------------------------------

This file contains an underscore definition let _list_of_integer = Ltype (list, [Linteger]) in which is not reported. Maybe it has to do with how Frama-C is designed ?

[fantazio]

After a deeper look, I can see 2 issues that will limit the analyzer's capabilities:

• The libraries are wrapped (see Wrapped libraries support #18)
• The source files are in not in places the analyzer would look for them at the moment. (see Stop relying on the cmti paths to find the corresponding source files #24)

Regarding the specific value that you are looking for (_list_of_integer), it is not exported so the analyzer would not be looking for it anyway.

[fantazio]

Hey @tmarti2 !
The branch fantazio:fix_wrapped provides all the necessary improvements identified. Feel free to try it out and provide a feedback (whether you still have any issue or are happy with this version).
It will probably be merged within the next couple of weeks.

[tmarti2]

Thanks ! I'll give it a try next week

[tmarti2]

Maybe I'm using it wrong, but I'm not able to detect anything in Frama-C's kernel. Just to clarify, Frama-C is a big project, and has a plug-in system. Your tool is able to detect some dead code in plug-ins, but not in the main sources, I'm not sure why.

I added -bin-annot -keep-locs in frama-c/src/dune flags for frama-c-kernel, and an unused exported value let foo = 42 and val foo: int in a random file frama-c/src/libraries/zarith/z.ml(i). But I don't find any combination of options/path to find this unexported value via the tool.

[fantazio]

I gave it a try on Frama-C 31.0¹ :

• Modified src/libraries/arithmetic/nat.ml(i) to export a val dead : int value.
• Compiled using dune build @check
• From the frama-c directory, ran <path_to/dead_code_analyzer> --nothing -E all _build
• After ~20s, I got this report
• /workspace_root/src/libraries/arithmetic/nat.mli:28: dead is reported in the UNUSED EXPORTED VALUE section and corresponds with the dead value I introduced

To replace /workspace_root in the reports by the actual absolute paths, you can add (map_workspace_root false) in the dune-project files. The new paths will point to the files in _build.

Do you have a link to a fork or a branch with your changes I could fetch to reproduce your example ?

Footnotes

1. The gitlab link for the project gives me a 404. I am testing on a version I cloned in September. ↩

[tmarti2]

Erf sorry our gitlab is having issues so we closed the public part... I totally forgot.

I'll try what you did tomorrow. For the record what does @check do ? I always use @install (for Frama-C I mean), maybe that's the issue ?

[fantazio]

The @check alias produces the .cmi and .cmt files. It is meant for quick builds and the production of files for dev tools as far as I understand.

I only learned about it recently and find it more convenient than adding the flags in dune files.

[tmarti2]

...
I'm so sorry, I did clone the right branch, but forgot to pin it so I was still using the 1.0 version...

It seems to work ! I did not check the output beside the nat modification, I'll have a look now.

[fantazio]

No worries. Please let us know if you have any other issue using the tool ;)

[tmarti2]

I was able to find some real dead code. The main issue with Frama-Cis that it's also a library. Many things are exported in the API, but we cannot check what external plug-ins are using. It is still really useful to do a quick pass to find things that should not be exported !

[tmarti2]

(Btw our public gitlab should be accessible now, sorry for that)