SQLite Amalgamation

[michael-schwarz]

While looking at other potential benchmarking projects, I came across the sqlite amalgamation (https://www.sqlite.org/amalgamation.html).

It is one file that contains all of sqlite, plus a header and a driver program that gives you a command line utility.

• Parsing succeeds, compilation DB etc is not needed
• There is a target in the Makefile to create this amalgamation, so we are not limited on running on releases, but can do so for every commit
• The program seems to be multi-threaded (contains calls to pthread_create)
• ./goblint ../../bench-repos/sqlite-amalgamation-3370200/sqlite3.c ../../bench-repos/sqlite-amalgamation-3370200/sqlite3.h ../../bench-repos/sqlite-amalgamation-3370200/sqlite3ext.h ../../bench-repos/sqlite-amalgamation-3370200/shell.c -v --set cppflags[+] -DSQLITE_DEBUG --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 --set cppflags[+] -DGOBLINT_NO_BSEARCH --set cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages|
• Problem:

  Found dead code on 52538 lines (including 52332 in uncalled functions)!
  Total lines (logical LoC): 52567
  

[michael-schwarz]

With ./goblint ../sqlite-amalgamation-3370200/sqlite3.c ../sqlite-amalgamation-3370200/sqlite3.h ../sqlite-amalgamation-3370200/sqlite3ext.h ../sqlite-amalgamation-3370200/shell.c -v --set cppflags[+] -DSQLITE_DEBUG --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 --set cppflags[+] -DGOBLINT_NO_BSEARCH --set cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages

I ran out of patience after 121h (on 2022-02-24 15:00:48, so it is presumably some older version of Goblint).

Timings:
TOTAL                           0.858 s
  parse                           0.393 s
  convert to CIL                  0.465 s
  analysis                        0.000 s
    makeCFG                         0.186 s
    connect                         0.433 s
    global_inits                    0.231 s
    solving                        436362.012 s
      S.Dom.equal                    405.413 s
Timing used
Memory statistics: total=456384797.63MB, max=94056.47MB, minor=456380955.41MB, major=4419733.41MB, promoted=4415891.19MB
    minor collections=217626012  major collections=977 compactions=0

[jerhard]

@stilscher IIRC, you mentioned that you were running Goblint master on the SQLite Amalgamation. What command line are you using? Because the above contains cppflags option, which is not merged into master.

[stilscher]

./goblint ../sqlite-amalgamation-3370200/sqlite3.c ../sqlite-amalgamation-3370200/sqlite3.h ../sqlite-amalgamation-3370200/sqlite3ext.h ../sqlite-amalgamation-3370200/shell.c -v --set pre.cppflags[+] -DSQLITE_DEBUG --disable ana.base.context.non-ptr --disable ana.int.def_exc --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages --set ana.activated "['base', 'mallocWrapper']" --set ana.ctx_insens[+] base --set ana.ctx_insens[+] mallocWrapper

[michael-schwarz]

With the fix from goblint/analyzer#802 and a fix to not track string pointers (but not the short-circuiting for the HoareDomain etc) it now terminates on sqlite. The runtime is still 13h, but at least it terminates and the amount of dead code seems reasonable.

Found dead code on 8654 lines (including 8357 in uncalled functions)!
Total lines (logical LoC): 53138

Timings:
TOTAL                          47303.587 s
  parse                           0.579 s
  convert to CIL                  0.699 s
  mergeCIL                        0.149 s
  analysis                       47302.162 s
    createCFG                       0.886 s
      handle                          0.311 s
      iter_connect                    0.515 s
        computeSCCs                     0.249 s
    global_inits                    0.316 s
    solving                        47298.215 s
      S.Dom.equal                    35.403 s
      postsolver                     52.210 s
    warn_global                     0.002 s
Timing used
Memory statistics: total=111569501.25MB, max=1878.66MB, minor=111568950.21MB, major=402051.11MB, promoted=401500.07MB
    minor collections=53201376  major collections=1108 compactions=1

[stilscher]

I rerun the analysis of sqlite (with the very basic config from above) on Friday:

Timings:
TOTAL                          13156.944 s
  parse                           0.592 s
  convert to CIL                  0.582 s
  mergeCIL                        0.141 s
  analysis                       13155.631 s
    createCFG                       0.889 s
      handle                          0.295 s
      iter_connect                    0.526 s
        computeSCCs                     0.255 s
    global_inits                    0.293 s
    solving                        13150.125 s
      S.Dom.equal                    32.908 s
      cheap_full_reach                0.206 s
      postsolver                     23.573 s
        postsolver_iter                22.519 s
    warn_global                     0.019 s
Timing used
Memory statistics: total=16264860.42MB, max=2484.53MB, minor=16264433.45MB, major=241228.49MB, promoted=240801.52MB
    minor collections=7755956  major collections=639 compactions=0

So with ~3.5 h it is at least much faster now.