search

goblint / cil

C Intermediate Language
https://goblint.github.io/cil/
Other
40 stars 16 forks source link

Merging: Treat inlines as if they were static when mergeInlines is off #86

Closed michael-schwarz closed 2 years ago

michael-schwarz commented 2 years ago

This should hopefully fix all issues with merging of inlines. The logic now is as follows:

If merge_inlines is off (default), inline functions are handled as if they were static, meaning they will always be renamed. This should fix any unintended instances of multiple fundecs for one given varinfo.

michael-schwarz commented 2 years ago

It seems that this does indeed fix the issues. On e7121bf4c936e9790ad0644b72df1dba2a2a8459 with mergeInlines off on FFmpeg, I ran out of patience after ~600s

TOTAL                          103.047 s
  parse                          46.625 s
  convert to CIL                 56.422 s
  analysis                        0.000 s
    createCFG                      516.978 s
      handle                          1.650 s
      iter_connect                   473.773 s
        computeSCCs                    233.188 s

with this fix, createCFG terminates after ~80s.

TOTAL                          102.306 s
  parse                          46.239 s
  convert to CIL                 56.068 s
  analysis                        0.000 s
    createCFG                      77.478 s
      handle                         10.272 s
      iter_connect                   63.263 s
        computeSCCs                     5.309 s

with cfgF (bindings=2681395 buckets=2097152 max_length=9 histo=566502,761686,488614,200968,61356,14658,2790,510,59,9 load=1.278589), cfgB (bindings=2670407 buckets=2097152 max_length=9 histo=569323,763227,486315,200119,60610,14216,2819,440,68,15 load=1.273350)

This interestingly is still an order of magnitude slower than with mergeInlines on, 

TOTAL                          103.190 s
  parse                          46.476 s
  convert to CIL                 56.714 s
  analysis                        0.000 s
    createCFG                       7.516 s
      handle                          2.453 s
      iter_connect                    4.487 s
        computeSCCs                     1.484 s

with

cfgF (bindings=829707 buckets=524288 max_length=9 histo=107465,170628,135133,71058,28129,8921,2283,562,95,14 load=1.582541), cfgB (bindings=829631 buckets=524288 max_length=9 histo=107450,170648,135211,71016,28104,8843,2360,545,92,19 load=1.582396).

Aside: I might also try to script some walltime comparison, to see how much of a difference it makes overall (the CIL times reported above do not seem accurate, I think it accounts only for parts of process), as the merging of inlines is supposed to make CIL an order of magnitude slower.

Regardless, I am pretty sure, we have now fixed the broken invariant.

michael-schwarz commented 2 years ago

Actually, all that was needed to get better number is wrapping the merging into a call to Stas.time inside Goblint.

michael-schwarz commented 2 years ago

With merging of inlines:

  mergeCIL                       285.114 s
  analysis                        0.000 s
    createCFG                      14.989 s
      handle                          4.853 s
      iter_connect                    8.983 s
        computeSCCs                     4.394 s

Without it:

  mergeCIL                       66.626 s
  analysis                        0.000 s
    createCFG                      71.905 s
      handle                          9.731 s
      iter_connect                   57.776 s
        computeSCCs                     7.778 s

So it looks like it buys us 2x speedup to not merge inlines (at least until the start of analysis).