curl

[sim642]

https://github.com/curl/curl

Initial attempt

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

Checked out git tag curl-7_85_0 and executed:

autoreconf -fi
./configure --without-ssl
bear -- make
goblint -v compile_commands.json

Crashes due to parsing errors due to enum values (goblint/cil#112):

Frontc is parsing /home/simmo/Desktop/curl/.goblint/preprocessed/lib/content_encoding.i
Converting CABS->CIL
/usr/include/brotli/decode.h:202: Warning: MEMOF in constant
/usr/include/brotli/decode.h:202: Warning: Cannot represent the length of array as an attribute
/usr/include/brotli/decode.h:202: Warning: MEMOF in constant
/usr/include/brotli/decode.h:202: Warning: Cannot represent the length of array as an attribute
lib/content_encoding.c:477: Error: Cannot resolve variable GZIP_OK.
lib/content_encoding.c:477: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
lib/content_encoding.c:483: Error: Cannot resolve variable GZIP_UNDERFLOW.
lib/content_encoding.c:483: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
lib/content_encoding.c:501: Error: Cannot resolve variable GZIP_BAD.
lib/content_encoding.c:501: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
lib/content_encoding.c:522: Error: Cannot resolve variable GZIP_OK.
lib/content_encoding.c:522: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
lib/content_encoding.c:531: Error: Cannot resolve variable GZIP_UNDERFLOW.
lib/content_encoding.c:531: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
lib/content_encoding.c:535: Error: Cannot resolve variable GZIP_BAD.
lib/content_encoding.c:535: Error: Case statement with a non-constant
Error in doStatement (GoblintCil__Errormsg.Error)
Frontc is parsing /home/simmo/Desktop/curl/.goblint/preprocessed/lib/content_encoding.i
Error: There were parsing errors in /home/simmo/Desktop/curl/.goblint/preprocessed/lib/content_encoding.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

[stilscher]

I retried this benchmark because the parsing issue was fixed. The analysis ran through, but most of the lines are dead. These are the results for a minimal from-scratch analysis:

./goblint -v --set ana.activated '["base", "mallocWrapper"]' --set ana.base.privatization none --enable exp.earlyglobs --set ana.base.context.non-ptr false --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_QSORT ../curl

vars = 716295    evals = 2458230    narrow_reuses = 152631

Timings:
                                  cputime   walltime   allocated   count
Default                          875.112s   875.310s2517702.12MB      1×
  preprocess                         6.289s     6.344s      0.31MB      1×
  FrontC                             6.529s     6.530s  10252.06MB    364×
  Cabs2cil                           7.419s     7.420s  12156.89MB    364×
  mergeCIL                           7.332s     7.333s   3279.82MB      1×
  analysis                         847.159s   847.296s2491592.88MB      1×
    createCFG                          2.252s     2.252s   1809.18MB      1×
      handle                             0.411s     0.416s    592.62MB  12869×
      iter_connect                       1.731s     1.735s   1118.50MB  12869×
        computeSCCs                        0.266s     0.271s    350.40MB  12869×
    global_inits                       0.534s     0.534s    365.90MB      1×
    solving                          837.809s   837.945s2488865.14MB      1×
      S.Dom.equal                        1.835s     3.423s    877.25MB2610861×
      cheap_full_reach                   7.306s     7.307s    226.24MB      1×
      postsolver                        98.862s    98.926s 212557.20MB      1×
        postsolver_iter                   93.181s    93.235s 212130.55MB      1×
    warn_global                        0.025s     0.025s     18.73MB      1×
    result output                      0.001s     0.001s      0.01MB      1×

Logical lines of code (LLoC) summary:
  live: 7004
  dead: 36454 (36260 in uncalled functions)
  total: 43458

[michael-schwarz]

Did you check if there are any messages that both branches are dead somewhere?