Proposal: Do not attempt to merge inline functions by default

[michael-schwarz]

Currently, CIL attempts to merge inline functions, such that there is only one definition of them, instead of renaming and keeping all appearing definitions.
With projects such as goblint/bench#16, we run into issues because we have static inline functions for which CIL merges the definitions but not the declarations, leading to warnings where we have multiple globals that have different varinfos that share the same name.
This (potentially) confuses the incremental analysis which assumes there is at-most one varinfo per global name in Goblint.
Also, having >100 of these warnings is also not too nice.

Advantages:

• Gets rid of these warnings
• Makes things easier for Goblint on the incremental side
• Potentially leads to a speed up of an order of magnitude according to comments
• Seems like the morally right thing to do for static inline functions: They are different if they come from different translation units, even if they happen to share the same code
• ...

Disadvantages:

• Potentially increases the size of the merged output (potentially leading to more code to analyze)
• ...

[michael-schwarz]

Potentially increases the size of the merged output (potentially leading to more code to analyze)

For zstd the difference is from

Found dead code on 3427 lines (including 3087 in uncalled functions)!
Total lines (logical LoC): 21415

to

Found dead code on 3535 lines (including 3149 in uncalled functions)!
Total lines (logical LoC): 21974

---

The failure for OS X is unrelated, some download from the OPAM repo failed there.

[sim642]

Could mergeInlines not be made a ref, such that we could configure it at runtime from Goblint's side?

Also, did you look into why it's supposedly so slow to merge them? And is the comment true that disabling it improves merging time by an order of magnitude?

[michael-schwarz]

Also, did you look into why it's supposedly so slow to merge them?

Without having looked at all the details, one reason seems to be that with mergeInlinesRepeat we sometimes need to go over (almost) all globals encountered in the files that were merged thus far again (potentially after each single file). This is the case whenever an inline was being used before, but we have now decided to remove its definition.

In a worst case scenario, this can be very expensive.

For the openSSL compilation database with no merging:

real    3m44,588s
user    3m26,613s
sys     0m17,990s

and with merging:

real    6m12,926s
user    5m55,207s
sys     0m17,758s

So not quite an order of magnitude, but still a noticeable difference.

[michael-schwarz]

Actually, this PR is the cause of many spurious functions: e.g. for the FFmpeg program, the number of functions(!) goes from 30k when merging inlines to over >440k when no longer merging inlines. This is definitely something we need to address.

[sim642]

I guess there's no Goblint option for this. That's probably the least we can do for the time being, allowing to choose it based on the benchmark if necessary.

[michael-schwarz]

I was thinking of some sort of optimization where we do not merge inlines, but drop those inlines that are static or have default linkage. This would get rid of the spurious unused copies, without removing all uncalled functions everywhere.

[sim642]

I currently overrode this back in Goblint (goblint/analyzer@62d7591) to work around the issues surrounding not merging for the time being.