Total LLoC depends on analysis

[sim642]

While writing up my thesis I found that the total LLoC we report for some benchmarks differs between three papers:

Benchmark	traces paper	more-traces paper	unassume paper	42848ea
pfscan	600	550	559	559
aget	603	581	587	587
ctrace	665	651	–	657
knot	987	973	981	981
smtprc	3102	3013	3037	3037

I also ran the current version of Goblint on them and got even more different results.
And found that @michael-schwarz's PhD thesis has an even different one for pfscan: 562.

All five programs have been unchanged for 18 years, so that's not the cause for the differences.
b6e8132 and bddbd0f (and possibly others) refactored this logic a long time ago (outside of any PR it seems?!), which doesn't explain the change since more-traces.

Our calculation of the total is quite suspicious:

analyzer/src/framework/control.ml

Lines 202 to 207 in 42848ea

	let dead_total = !count + uncalled_fn_loc in
	let total = live_count + dead_total in (* We can only give total LoC if we counted dead code *)
	M.msg_group severity ~category:Deadcode "Logical lines of code (LLoC) summary" [
	(Pretty.dprintf "live: %d" live_count, None);
	(Pretty.dprintf "dead: %d%s" dead_total (if uncalled_fn_loc > 0 then Printf.sprintf " (%d in uncalled functions)" uncalled_fn_loc else ""), None);
	(Pretty.dprintf "total lines: %d" total, None);

This is basically

$$ \text{total} = (\text{live from analysis result}) + (\text{dead from analysis result}) + (\text{all from functions uncalled according to the analysis result}). $$

Only the last summand is computed purely syntactically with a CIL visitor (but still depending on which functions were uncalled by the analysis). The proper way would be to just compute the total fully syntactically to begin with. This would by construction avoid any possible dependence on the analysis because it's supposed to be an independent measure.

Of course the live and dead things from the analysis result should make up the total, but both of these are subtly affected by much more complicated logic:

• The analysis result is for a constraint system, which is based on CFGs, but our CFG construction can omit some nodes, e.g. when following multiple goto-s.
• The constraint system solution is perhaps not guaranteed to have computed something for all CFG nodes, if they're not depended on. In some obscure cases (e.g. remove superfluous edges in CFG #231), CFGs can contain weird vestigial parts that aren't (and don't need to be) properly connected.
  We check that the CFG is connected, but not that all paths from entry eventually end up at exit.

[michael-schwarz]

The includes also differ between the different analyses:

See the following remark in my thesis draft:

The number of LLoC differs by a few lines between the relational and non-relational analyses due to the preprocessor not including some stub files in the former setting. For the sake of internal consistency, we list the number of LLoC computed by the non-relational analysis (as in Table 5.4) here.

[sim642]

The includes also differ between the different analyses:

These benchmarks are combined with CIL and have no #includes. So even if the standard library headers differed in the bodies of inline functions, this shouldn't be making a difference here.

[michael-schwarz]

I think it's about including the stub for bsearch or not iirc.

[sim642]

If our own stubs are included in LLoC then I would consider that a/the bug.
Although I still suspect there could be more to it: the stub bodies haven't changed since the beginning.