CODEWITHSUNDEEP
frama-c
depechec0de
depechec0de

Reputation: 131

Sparecode analysis in Frama-C

Sorry if this is detailed somewhere, I tried searching in the different documentations of Frama-C without luck.

I'm trying to do dead code elimination in my code, but I don't understand the results of the tool. Is there any paper / documentation that explains how this plugin works? I only know that it uses the results of the Value analysis.

Upvotes: 2

Views: 84

Answers (1)

Virgile
Virgile

Reputation: 10148

Admittedly, the sparecode page on Frama-C's website is a bit terse. However, this is partly due to the fact that there's not much to parameterize in this plug-in. Mainly, it is a specialized form of the slicing plug-in, where the criterion is "preserve the state at the end of the program".

More generally, slicing consists in removing instructions that do not contribute to a user given criterion (e.g. the whole program state at a given point, the validity status of an ACSL annotation, or simply the fact that the program reaches a particular instruction).

In order to compute such slice, slicing, hence sparecode, indeed relies on the results of Eva, mainly to obtain an over-approximation (as always with Eva) of the dependencies between the various memory locations involved at each point in the program (you might want to have a look at Chapter 7 of the Eva manual which deals with dependencies. Very roughly speaking the slice will consist in the transitive closure of the dependencies for the memory locations involved in the criterion (in presence of pointers and branches, this notion of "transitive closure" becomes a bit complicated to define formally, but the essence is there).

Now, with respect to dead code, there are two points worth noting:

  • As mentioned before, Eva provides an over-approximation of the behavior of the program. For slicing, this means that some statements might be kept even though they do not contribute to the slicing criterion in any concrete trace, but appear to do so in the abstract trace due to over-approximation. On the other hand, if a statement is not included, then it definitely does not contribute to the criterion.
  • For sparecode, not contributing to the final state of the program does not mean that the code is dead, but merely that all its side-effects are shadowed by further instructions. The simplest example of that would be the following:
int x;
int main() {
  x = 1;
  x = 2; 
}

Here, the x=1 has no influence over the final state of the program, and only x=2 will be kept.

Upvotes: 2

Related Questions