search

goblint / bench

The benchmark suite
4 stars 6 forks source link

MTAR #13

Open michael-schwarz opened 2 years ago

michael-schwarz commented 2 years ago

https://github.com/johnno1962/mtar

michael-schwarz commented 2 years ago

On the server, the creation of the compilation database fails due to not finding pthread (maybe gcc called without -pthread?). Locally, it succeeds though.

michael-schwarz commented 2 years ago

I left it running for a while and after about 30s, we get:

runtime: 00:27:04.665
vars: 714507, evals: 1363491

|rho|=714507
|called|=15410
|stable|=414656
|infl|=699151
|wpoint|=283
Found 40732 contexts for 548 functions. Top 5 functions:
3662    contexts for entry state of archive_string_append on libarchive/archive_string.c:201:1-210:1
3206    contexts for entry state of memcpy on /usr/include/x86_64-linux-gnu/bits/string_fortified.h:30:1-35:1
3039    contexts for entry state of make_table_recurse on libarchive/archive_read_support_format_rar.c:2501:1-2553:1
2828    contexts for entry state of archive_string_ensure on libarchive/archive_string.h:141:23-142:55
2648    contexts for entry state of archive_strappend_char on libarchive/archive_string.h:77:23-78:54

Memory statistics: total=1223221.04MB, max=2857.20MB, minor=1223073.81MB, major=14353.89MB, promoted=14206.66MB
    minor collections=583276  major collections=54 compactions=0

vars = 714507    evals = 1363491  

Timings:
TOTAL                          23.544 s
  parse                           9.736 s
  convert to CIL                 13.808 s
  analysis                        0.000 s
    global_inits                    8.983 s
    solving                        1578.766 s
      S.Dom.equal                     2.564 s
Timing used
Memory statistics: total=1223221.05MB, max=2857.20MB, minor=1223073.83MB, major=14353.89MB, promoted=14206.66MB
    minor collections=583276  major collections=54 compactions=0

Fatal error: exception Stack overflow
Raised by primitive operation at Stdlib__list.assoc in file "list.ml", line 192, characters 19-30
Called from MCP.MCP2.filter_presubs.f in file "src/analyses/mCP.ml", line 170, characters 18-41
Called from BatList.map in file "src/batList.mlv", line 239, characters 23-28
Called from MCP.MCP2.query'.f in file "src/analyses/mCP.ml", line 344, characters 21-47
...
sim642 commented 2 years ago

make_table_recurse sounds like a recursive function, which would explain |called|=15410, i.e. such a deep solver call stack.