Open michael-schwarz opened 2 years ago
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
@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
.
./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
With the fix from https://github.com/goblint/analyzer/pull/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
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.
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.
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
|