redis

[sim642]

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]

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 (goblint/cil#114).

[karoliineh]

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