libvips

[karoliineh]

While reading papers, I looked into some projects that have been used for benchmarking. One project that seemed promising is libvips, "a fast image processing library with low memory needs", which is also part of the PARSEC benchmark (a benchmark suite composed of multithreaded programs).

By this paper, lipvips has 269975 LOC, and running a quick git ls-files | xargs wc -l in lipvips/lipvips gave a total of 269249.

It also seems well maintained, with the first commit from 2007 and constant contributions with the latest being just today.

Unfortunately, on the latest commit currently (3191e5c), Goblint will not succeed with parsing:

/usr/include/glib-2.0/glib/gspawn.h[76:0-21] : syntax error
Parsing errorFatal error: exception GoblintCil__Frontc.ParseError("Parse error")

The code in gspawn.h[76:0-21] being:

...
75  G_SPAWN_ERROR_TOO_BIG,/* execv() returned E2BIG */
76  G_SPAWN_ERROR_2BIG GLIB_DEPRECATED_ENUMERATOR_IN_2_32_FOR(G_SPAWN_ERROR_TOO_BIG) = G_SPAWN_ERROR_TOO_BIG,
77  G_SPAWN_ERROR_NOEXEC, /* execv() returned ENOEXEC */
...

Would this be worth a try?

[michael-schwarz]

Absolutely, thanks for identifying it! Usually the parsing issues with CIL can be fixed without requiring major reworking, I can have a look at that once we're back from the AVM workshop next week.

[sim642]

A few comments:

1. The parsing error appears to be some macro stuff in the middle of an enum definition. You can use Goblint's pre.keep and look in .goblint to see what the preprocessed code that we parse looks like.
2. It appears to use at least one library (glib), which has been another limiting factor for us, unless we figure out a way to also include the sources (not just the headers) of all dependencies.
3. The project seems to be a library, but we need an executable program (with a single main function) to analyze. Looks like it might include a command-line program as well, so that's what we'll have to analyze.

[sim642]

One project that seemed promising is libvips, "a fast image processing library with low memory needs", which is also part of the PARSEC benchmark (a benchmark suite composed of multithreaded programs).

We looked into it today and noticed it didn't use pthreads at all. Looks like it uses glib's threading instead: https://libsoup.org/glib/glib-Threads.html. It should be possible to add LibraryFunctions support for these into Goblint, but that's just extra work on top of the parsing error.