goblint / bench

The benchmark suite
4 stars 5 forks source link

netdata #37

Open sim642 opened 1 year ago

sim642 commented 1 year ago

https://github.com/netdata/netdata

Initial attempt

Goblint version: heads/master-0-ge223b4f36-dirty.

Checked out git tag v.1.36.1 and executed:

autoreconf -ivf
./configure
bear -- make
goblint -v compile_commands.json

Crashes due to parsing errors in vendored SQLite (somehow not a problem in #19):

``` Frontc is parsing /home/simmo/Desktop/netdata/.goblint/preprocessed/database/sqlite/sqlite3.i Converting CABS->CIL database/sqlite/sqlite3.c:27415: Error: Cannot resolve variable mutexIsInit. database/sqlite/sqlite3.c:27928: Error: Cannot find field nRef database/sqlite/sqlite3.c:27955: Error: Cannot find field id database/sqlite/sqlite3.c:27998: Error: Cannot find field id database/sqlite/sqlite3.c:28059: Error: Cannot find field nRef database/sqlite/sqlite3.c:28059: Error: Cannot find field id database/sqlite/sqlite3.c:51964: Error: Cannot resolve variable nPage. database/sqlite/sqlite3.c:51964: Error: Cannot resolve variable nPage. database/sqlite/sqlite3.c:52333: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52333: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52334: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52334: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52334: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52334: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52335: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52335: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52335: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52335: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52336: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52336: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52336: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52336: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:52337: Error: Cannot resolve variable pCache. database/sqlite/sqlite3.c:52337: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:58943: Error: Cannot resolve variable pPager. database/sqlite/sqlite3.c:58943: Error: expecting a pointer to a struct database/sqlite/sqlite3.c:64105: Error: Cannot find field lockError database/sqlite/sqlite3.c:64970: Error: Cannot find field lockError database/sqlite/sqlite3.c:67540: Error: Cannot resolve variable debuginfo. database/sqlite/sqlite3.c:67540: Error: Expected an lval in MEMBEROF (field nSize) database/sqlite/sqlite3.c:67561: Error: Cannot resolve variable debuginfo. database/sqlite/sqlite3.c:67561: Error: Expected an lval in MEMBEROF (field nSize) database/sqlite/sqlite3.c:70211: Error: Cannot resolve variable nRef. database/sqlite/sqlite3.c:74113: Error: Cannot resolve variable nCellAtStart. database/sqlite/sqlite3.c:74772: Error: Cannot resolve variable balance_deeper_called. database/sqlite/sqlite3.c:74815: Error: Cannot resolve variable balance_quick_called. database/sqlite/sqlite3.c:76684: Error: Cannot resolve variable nRef. database/sqlite/sqlite3.c:76798: Error: Cannot resolve variable nRef. database/sqlite/sqlite3.c:77640: Error: Cannot resolve variable rc2. database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93391: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93396: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93396: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93396: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93396: Error: Cannot find field seekOp database/sqlite/sqlite3.c:93396: Error: Cannot find field seekOp database/sqlite/sqlite3.c:95984: Error: Cannot resolve variable nExtraDelete. database/sqlite/sqlite3.c:98136: Error: Cannot resolve variable iSz. database/sqlite/sqlite3.c:114795: Error: Cannot resolve variable pOld. database/sqlite/sqlite3.c:114795: Error: Cannot resolve variable pOld. database/sqlite/sqlite3.c:114822: Error: Cannot resolve variable nLookaside. database/sqlite/sqlite3.c:114822: Error: Cannot resolve variable nLookaside. database/sqlite/sqlite3.c:122763: Error: Cannot find field bInverse database/sqlite/sqlite3.c:133357: Error: Cannot resolve variable rcp. database/sqlite/sqlite3.c:167979: Error: Cannot resolve variable startedWithOom. Frontc is parsing /home/simmo/Desktop/netdata/.goblint/preprocessed/database/KolmogorovSmirnovDist.i Error: There were parsing errors in /home/simmo/Desktop/netdata/.goblint/preprocessed/database/KolmogorovSmirnovDist.i Fatal error: exception GoblintCil__Errormsg.Error Raised at GoblintCil__Errormsg.s in file "src/ocamlutil/errormsg.ml" (inlined), line 49, characters 17-28 Called from GoblintCil__Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 123, characters 4-57 Called from GoblintCil__Frontc.parse_helper in file "src/frontc/frontc.ml", line 256, characters 13-32 Called from GoblintCil__Frontc.parse in file "src/frontc/frontc.ml" (inlined), line 264, characters 32-55 Called from Goblint_lib__Cilfacade.parse in file "src/util/cilfacade.ml", line 30, characters 2-44 Called from BatList.map.loop in file "src/batList.mlv", line 237, characters 28-33 Called from BatList.map in file "src/batList.mlv", line 240, characters 4-12 Called from Goblint_lib__Maingoblint.preprocess_parse_merge in file "src/maingoblint.ml", line 392, characters 2-45 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 31, characters 17-27 Re-raised at CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 36, characters 4-11 Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 32, characters 17-32 Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63 Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61 Called from Std_exit in file "std_exit.ml", line 18, characters 8-20 ```
sim642 commented 1 year ago

SQLite fixed attempt

The problem was caused by our redefinition of assert not accounting forSQLITE_DEBUG, which is easily fixed.

Same as above, but with

goblint -v compile_commands.json --set pre.cppflags[+] '-DSQLITE_DEBUG'

Gets past the SQLite issue but crashes due to conflicting global initializers during merging:

``` Final merging phase (35): /home/simmo/Desktop/netdata/.goblint/preprocessed/daemon/common.i /usr/include/x86_64-linux-gnu/bits/stdio.h:55: Warning: Duplicate definition of node getc_unlocked(35) at indices 2412(/usr/include/x86_64-linux-gnu/bits/stdio.h:65) and 2411(/usr/include/x86_64-linux-gnu/bits/stdio.h:55) /usr/include/x86_64-linux-gnu/bits/stdio.h:100: Warning: Duplicate definition of node fputc_unlocked(35) at indices 2415(/usr/include/x86_64-linux-gnu/bits/stdio.h:90) and 2416(/usr/include/x86_64-linux-gnu/bits/stdio.h:100) /usr/include/x86_64-linux-gnu/bits/stdio2.h:183: Warning: Duplicate definition of node __asprintf(35) at indices 2446(/usr/include/x86_64-linux-gnu/bits/stdio2.h:190) and 2445(/usr/include/x86_64-linux-gnu/bits/stdio2.h:183) /usr/include/x86_64-linux-gnu/bits/stdlib-bsearch.h:19: Warning: def'n of func bsearch at /usr/include/x86_64-linux-gnu/bits/stdlib-bsearch.h:19 (sum 90592995) conflicts with the one at /home/simmo/dev/goblint/sv-comp/goblint/_opam/share/goblint/includes/stdlib.c:38 (sum 1086600); keeping the one at /home/simmo/dev/goblint/sv-comp/goblint/_opam/share/goblint/includes/stdlib.c:38. daemon/common.c:15: Error: global var netdata_configured_host_prefix at daemon/common.c:15 has different initializer than libnetdata/required_dummies.h:36 error when merging global #line 15 "daemon/common.c" char *netdata_configured_host_prefix = (char *)((void *)0); : GoblintCil__Errormsg.ErrorFatal error: exception GoblintCil__Errormsg.Error Raised at GoblintCil__Mergecil.oneFilePass2.processOneGlobal in file "src/mergecil.ml", line 1601, characters 7-14 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from GoblintCil__Mergecil.oneFilePass2 in file "src/mergecil.ml", line 1604, characters 3-39 Called from GoblintCil__Mergecil.merge.(fun) in file "src/mergecil.ml", line 1674, characters 7-21 Called from Stdlib__List.iter in file "list.ml", line 110, characters 12-15 Called from GoblintCil__Mergecil.merge in file "src/mergecil.ml", line 1672, characters 3-86 Called from GoblintCil__Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 105, characters 10-15 Re-raised at GoblintCil__Stats.repeattime.repeatf in file "src/ocamlutil/stats.ml", line 109, characters 1-8 Called from Goblint_lib__Cilfacade.getMergedAST in file "src/util/cilfacade.ml", line 240, characters 15-72 Called from Goblint_lib__Maingoblint.merge_parsed in file "src/maingoblint.ml", line 381, characters 12-37 Called from Stdlib__Fun.protect in file "fun.ml", line 33, characters 8-15 Re-raised at Stdlib__Fun.protect in file "fun.ml", line 38, characters 6-52 Called from CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 31, characters 17-27 Re-raised at CamlinternalLazy.force_lazy_block in file "camlinternalLazy.ml", line 36, characters 4-11 Called from Dune__exe__Goblint.main in file "src/goblint.ml", line 32, characters 17-32 Called from Stdlib.at_exit.new_exit in file "stdlib.ml", line 560, characters 59-63 Called from Stdlib.do_at_exit in file "stdlib.ml" (inlined), line 566, characters 20-61 Called from Std_exit in file "std_exit.ml", line 18, characters 8-20 ```

The two initializers are:

char *netdata_configured_host_prefix         = NULL;
char *netdata_configured_host_prefix = "";

I guess GCC is somehow fine with this and picks one of the two using whatever logic (linker arguments order?).