Findings

@michael-schwarz and I did some runs of Goblint (master) on the SQLite amalgamation, and investigated performance using perf and the firefox-profiler. We looked at the high run time of (on my system) BaseDomain.fun_6129, which we conjectured to be BaseDomain.equal_basecomponents_t.

Further investigation with Stats.time on a ~1 minute run of SQLite showed that a significant amount of time is used in HoarePO.equal:

TOTAL                          55.185 s
  parse                           0.463 s
  convert to CIL                  0.568 s
  mergeCIL                        0.136 s
  analysis                       54.019 s
    createCFG                       0.836 s
      handle                          0.293 s
      iter_connect                    0.479 s
        computeSCCs                     0.217 s
    global_inits                    0.403 s
      HoareDomain.equal               0.001 s
    solving                        52.741 s
      S.Dom.equal                     0.199 s
      HoareDomain.equal              18.238 s
Timing used

/goblint ../sqlite-amalgamation-3370200/sqlite3.c ../sqlite-amalgamation-3370200/sqlite3.h ../sqlite-amalgamation-3370200/sqlite3ext.h ../sqlite-amalgamation-3370200/shell.c -v --set pre.cppflags[+] -DSQLITE_DEBUG --disable ana.base.context.non-ptr --disable sem.unknown_function.spawn --set ana.thread.domain plain --enable exp.earlyglobs --set ana.base.privatization none --set pre.cppflags[+] -DGOBLINT_NO_BSEARCH --set pre.cppflags[+] -DGOBLINT_NO_ASSERT --set result json-messages

Problems With Current Implementation

The current implementation of HoarePO.equal relies on checking HoarePO.leq in both directions.
The implementation of leq in turn uses

• for_all, which transforms the argument Hoare-map to a list,
• and mem, which also transforms its Hoare-map argument to a list. The function mem may be called for each element in a Hoare-map.

It thus seems like the current implementation could be optimized considerably.

Goals

The implementation of HoarePO.equal and HoarePO.leq should perform a bucket-wise comparison, as all comparable elements have the same hash and are contained in the same bucket. One may also consider implementing equal directly, instead of relying on leq

Edit: Changed HoareDomain to HoarePO, as that's what I was talking about.