Other attempted projects

[michael-schwarz]

• https://github.com/ggreer/the_silver_searcher (2k LoC)

  • parsing succeeds, compilation DB succeeds
  • with default options: stack overflow after 3min
  • with --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --enable dbg.print_dead_code: 16s

• https://github.com/wg/wrk

  • generation of the compilation database fails

• https://www.sqlite.org/amalgamation.html (with --set cppflags[+] -DSQLITE_DEBUG)

• https://github.com/git/git

  • compiledb needs some manual fixes to the compilation database (issues with missing \" around strings)
  • Generalize handling of .d files: Accept .d files with multiple targets, eat -MF arguments to preprocessor analyzer#557 required
  • Combine takes >5min and > 15GB RAM
  • With ./goblint ../git --set ana.ctx_n_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --enable dbg.print_dead_code &> git_base_insens.txt -v

    Found dead code on 125453 lines (including 125190 in uncalled functions)!
    Total lines (logical LoC): 129533
    

  • git.fixed-cil.zip

• FFmpeg (https://github.com/FFmpeg/FFmpeg) (see FFmpeg #18)

• Possible query: https://github.com/search?p=7&q=stars%3A%3E100+size%3A%3E10000+language%3AC&type=Repositories

[michael-schwarz]

git.fixed-cil.zip

Edit: This once again is hodgepodge of different executables, so analyzing it is not really meaningful.

[michael-schwarz]

For FFmpeg with goblint/cil#80 and corresponding fix in Goblint, CIL succeeds to parse and combine everything. However, the analysis then gets stuck at:

Adding constructors to: main
And now...  the Goblin!
Startfuns: [main]
Exitfuns: []
Otherfuns: []
Using new format for phases!
Activated analyses for phase 0: expRelation, base, threadid, threadflag, threadreturn, escape, mutex, access, mallocWrapper, mhp
Activated transformations for phase 0: 
Generating the control flow graph.

using up >250GB of RAM. To me, it seems like there is something wrong in the CFG generation here then.

[sim642]

To me, it seems like there is something wrong in the CFG generation here then.

It would be useful to make Goblint temporarily print the function name whose CFG is being constructed, so we can quickly find a minimal example I could look at.

[michael-schwarz]

The problem more is that we have Number of globals 510848. CFG generation does not freeze but become increasingly slow and RAM usage goes up to ridiculous numbers ~220GB before it also runs out of RAM on the server and dies.

[sim642]

That's the number of globals, but surely they aren't most functions, but just variables.

[michael-schwarz]

Still, the numbers of functions is also at least >20k (at which point I aboated it)

An interesting observation is that the check whether everything is connected dominates the actual computation of CFGs by a factor of 200:

    makeCFG                         1.047 s
    connect                        171.697 s

[michael-schwarz]

@sim642 wrote:

The check whether everything is connected dominates the actual computation of CFGs by a factor fo 200:

    makeCFG                         1.047 s
    connect                        171.697 s

Also what program is this on where it has terminated?

[sim642]

Since the_silver_searcher is on master in gobpie-demos, I looked at the races Goblint finds from it. At least half of them are simply because of assignments to unknown pointer, which through some fabulous logic distributes the write access to every field of every global. These might again be due to our missing realloc (goblint/analyzer#701) handling.
Given the "quality" of the_silver_searcher, I suspect there are actual races to be found as well, although there's also too much noise.

[michael-schwarz]

If the sever is the bottleneck: If you write a script with the steps, I can run it on our sever with 512GB of RAM, though that is the biggest one we have.

[sim642]

I moved the discussion about git to a separate issue (#62) and hid those comments from here.