search

goblint / bench

The benchmark suite
4 stars 5 forks source link

redis #38

Open sim642 opened 1 year ago

sim642 commented 1 year ago

https://github.com/redis/redis

Initial attempt

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

Checked out git tag 7.0.4 and executed:

bear -- make
goblint -v compile_commands.json

Crashes due to parsing error in vendored jemalloc:

``` Frontc is parsing /home/simmo/Desktop/redis/.goblint/preprocessed/deps/jemalloc/src/jemalloc_cpp.i /usr/include/x86_64-linux-gnu/c++/11/bits/c++config.h[278:0-0] : syntax error Parsing errorFatal error: exception GoblintCil__Frontc.ParseError("Parse error") Raised at GoblintCil__Errormsg.parse_error in file "src/ocamlutil/errormsg.ml", line 330, characters 2-27 Called from Stdlib__Parsing.yyparse.loop in file "parsing.ml", line 152, characters 8-44 Called from Stdlib__Parsing.yyparse in file "parsing.ml", line 165, characters 4-28 Re-raised at Stdlib__Parsing.yyparse in file "parsing.ml", line 184, characters 8-17 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 GoblintCil__Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 189, characters 15-90 Re-raised at GoblintCil__Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 205, characters 6-73 Called from GoblintCil__Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 121, characters 13-38 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 ```

For some reason we get some C++ wrapper as input as well.

sim642 commented 1 year ago

jemalloc disabled attempt

The problem can be bypassed by using libc's malloc instead of jemalloc.

Same versions as above, but with:

bear -- make MALLOC=libc
goblint -v compile_commands.json

This reaches a new parsing error:

``` Frontc is parsing /home/simmo/Desktop/redis/.goblint/preprocessed/src/rax.i src/rax.c[204:16-23] : syntax error Parsing errorFatal error: exception GoblintCil__Frontc.ParseError("Parse error") Raised at GoblintCil__Errormsg.parse_error in file "src/ocamlutil/errormsg.ml", line 330, characters 2-27 Called from Stdlib__Parsing.yyparse.loop in file "parsing.ml", line 152, characters 8-44 Called from Stdlib__Parsing.yyparse in file "parsing.ml", line 165, characters 4-28 Re-raised at Stdlib__Parsing.yyparse in file "parsing.ml", line 184, characters 8-17 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 GoblintCil__Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 189, characters 15-90 Re-raised at GoblintCil__Frontc.parse_to_cabs_inner in file "src/frontc/frontc.ml", line 205, characters 6-73 Called from GoblintCil__Frontc.parse_to_cabs in file "src/frontc/frontc.ml", line 121, characters 13-38 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 ```

The offending line is

    rax *rax = rax_malloc(sizeof(*rax));

Here a previous typedef has the same name as the local variable being defined, which is confusing the parser (https://github.com/goblint/cil/issues/114).

karoliineh commented 9 months ago

I ran this on 2cf50ddbad1b8169ed31c913d6e6c860e4736f80.

  1. I renamed the variables
    • rax -> raxv in rax.c function raxNew and
    • stream -> streamv in module.c function RM_RdbStreamCreateFromFile.
  2. bear -- make MALLOC=libc redis-server in src, as there are also many main functions.
  3. goblint --conf examples/large-program.json -v compile_commands.json

After this, Goblint was able to parse and analyze. However, on my computer, it got killed after roughly 4.5 hours:

runtime: 04:25:15.887
vars: 276649, evals: 3510071

|rho|=276649
|stable|=252845
|infl|=275370
|wpoint|=1088
|sides|=22793
|side_dep|=0
|side_infl|=0
|var_messages|=0
|rho_write|=0
|dep|=230145
|called|=80
Found 12713 contexts for 1375 functions. Top 5 functions:
1007    contexts for L:entry state of memcpy (1152689) on /usr/include/x86_64-linux-gnu/bits/string_fortified.h:25:1-31:1
723     contexts for L:entry state of vsnprintf (1152655) on /usr/include/x86_64-linux-gnu/bits/stdio2.h:81:1-87:1
386     contexts for L:entry state of dictAdd (8179) on dict.c:424:1-431:1
374     contexts for L:entry state of dictAddRaw (8186) on dict.c:451:1-461:1
374     contexts for L:entry state of dictFindPositionForInsert (8193) on dict.c:1452:1-1481:1

Memory statistics: total=49150542.55MB, max=6608.90MB, minor=49148338.11MB, major=1925292.69MB, promoted=1923088.26MB
    minor collections=23436912  major collections=1773 compactions=0

Killed