dbg.print_dead_code is not complete and reports statements inserted by CIL

[vogler]

The behavior of the dead code reporting might confuse people.

#include <assert.h>

int main() {
  int x;
  if (1)
    x = 1;
  else
    x = 2;
  if (x)
    x = 1;
  else
    x = 2;
  assert(x > 1 && x < 0);
}

$ ./goblint --html dead.c
File 'dead.c':
  function 'main' has dead code on lines: 12, 14
Found dead code on 2 lines!
Dead code: the then branch over expression 'x > 1' is dead! (dead.c:13)
Dead code: the else branch over expression 'x' is dead! (dead.c:12)
Writing xml to temp. file: /var/folders/0j/1lq15k654zg7cf1rh9_gqty80000gn/T/ocaml61b1c3tmp
Time needed: 413 ms

It only reports dead code for nodes for which the solver calculated a value, but line 8 above is also dead (like all nodes that have no value).
On the other hand it reports about statements inserted by CIL, like the then-branch of the assert above.

Also, it might be useful to sort the output by line number.

[michael-schwarz]

A student of mine discovered some time ago that code such as line 8 is optimized out by CIL already: it does that for code when the condition is the constant 0 or 1:

./goblint 1.c --enable justcil

[...]
int main(void) 
{ 
  int x ;
  int tmp ;

  {
#line 6
  x = 1;
#line 9
  if (x) {
#line 10
    x = 1;
  } else {
#line 12
    x = 2;
  }
#line 13
  if (x > 1) {
#line 13
    if (x < 0) {
#line 13
      tmp = 1;
    } else {
#line 13
      tmp = 0;
    }
  } else {
#line 13
    tmp = 0;
  }
#line 13
  assert(tmp);
#line 14
  return (0);
}
}

so this is something that one could patch away in CIL.

[vogler]

Also the wording is confusing if there are no dead lines (No dead code vs. dead code):

No dead code found!
Dead code: the else branch over expression 'y == 4' is dead! (tests/regression/27-inv_invariants/01-ints.c:18)
Dead code: the else branch over expression 'y <= 8' is dead! (tests/regression/27-inv_invariants/01-ints.c:21)
Dead code: the else branch over expression 'y / -3 == -2' is dead! (tests/regression/27-inv_invariants/01-ints.c:26)
Dead code: the else branch over expression 'x <= -2' is dead! (tests/regression/27-inv_invariants/01-ints.c:30)
Dead code: the else branch over expression 'y >= -8' is dead! (tests/regression/27-inv_invariants/01-ints.c:24)

[vogler]

Changed the wording and now sorted by location (the dead line ranges are already sorted via BatISet).

[sim642]

One of the culprits is that dead_lines is a weird thing to calculate since it's later filtered by live_lines anyway. The appropriate thing to do would be to go through all the CFGs to construct total_lines and subtract live_lines from it to get a more appropriate dead_lines.

The dead branch detection also needs to be looked at, because it uses a completely separate dead_locations, which isn't filtered like that right now either.

And the whole dead code thing should integrate better with dbg.uncalled.

[michael-schwarz]

In e7d9b8d I used a visitor to count lines of code based on the CIL AST.
This is likely one of the ingredients to get to a cleaner solution of this overall issue.