Validation of YAML witnesses takes undue amount of time compared to analyis

[michael-schwarz]

For ctrace enhanced with 2036 location invariants (generation of YAML file takes much less than a minute), validation takes undue amounts of time (5s of solving vs over 6min of validation).

/home/michael/Documents/goblint-cil/analyzer/goblint --conf /home/michael/Documents/goblint-cil/analyzer/conf/traces-rel.json --set dbg.timeout 2000 --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet --sets ana.apron.domain interval ctrace_comb.c --enable allglobs --enable dbg.timing.enabled -v --set witness.yaml.validate ./ctrace_comb_traces_rel.yml

[Info] Timings:
                                  cputime   walltime   allocated   count
Default                          352.111s   352.219s 534714.18MB      1×
  preprocess                         0.022s     0.020s      0.01MB      1×
  FrontC                             0.006s     0.006s      4.49MB      3×
  Cabs2cil                           0.011s     0.011s      6.87MB      3×
  mergeCIL                           0.007s     0.007s      2.70MB      1×
  analysis                         352.055s   352.164s 534695.06MB      1×
    createCFG                          0.020s     0.020s      6.60MB      1×
      handle                             0.014s     0.015s      3.61MB     34×
      iter_connect                       0.005s     0.005s      2.63MB     34×
        computeSCCs                        0.004s     0.004s      2.29MB     34×
    global_inits                       0.011s     0.011s      5.22MB      1×
      reachability                       0.001s     0.001s      0.03MB      4×
    reachability                       0.001s     0.001s      0.01MB      1×
    solving                            4.848s     4.848s   7503.26MB      1×
      S.Dom.equal                        0.025s     0.046s      2.74MB   8142×
      reachability                       0.038s     0.041s     51.36MB   1453×
      cheap_full_reach                   0.008s     0.008s      4.23MB      1×
      postsolver                         1.195s     1.195s   1632.60MB      1×
        postsolver_iter                    1.178s     1.178s   1623.39MB      1×
          reachability                       0.010s     0.011s     11.71MB    366×
    warn_global                        0.015s     0.015s     21.88MB      1×
      race                               0.012s     0.012s     17.85MB     38×
    FrontC                             0.116s     0.121s     43.33MB   2036×
    Cabs2cil                           4.393s     4.518s   1993.57MB  35014×
    result output                      0.001s     0.001s      0.01MB      1×

For the Octagon configuration, we even have a timeout after 30mins, even though analysis only takes 12.2s.

[sim642]

Whether the validation time is excessive depends mostly on how long the analysis takes when all the same invariants are integrated as assertions and done during the analysis. Assert-instrumentation probably produces differently placed invariants than witness generation, so this might be difficult to compare.

I suspect it's just the overhead of actually abstractly evaluating thousands of expressions that simply adds up. It's the reason the benchmark scripts did two runs I think: one for performance and another for precision checking (or something like that).

[michael-schwarz]

Disabling check for InvariantParser.parse_cil expressions yields a speedup of about 1/5.

[michael-schwarz]

Most of the time is spent evaluating four of the invariants that contain a total of 7 disjunctions.

[michael-schwarz]

On the faster server, 60 minutes seems to be enough to get verdicts everywhere, but it still seems odd that this takes orders of magnitude longer than analysis.