Skip to content

Analyze time for transfer relation in Fuzzle benchmarks

When we run the following command line with 1h of time limit, we get the below statistics (shortened):

bin/cpachecker --heap 10000M --timelimit 1h --no-output-files --svcomp25 --stats --spec test/programs/benchmarks/properties/unreach-call.prp --64 test/programs/benchmarks/fuzzle-programs/05_fuzzle_70x70.c
PredicateCPA statistics
-----------------------
Time for post operator:                                1.908s
  Time for path formula creation:                      1.891s
Time for strengthen operator:                          0.060s
Time for prec operator:                                0.050s
  Time for abstraction:                  0.001s (Max:     0.001s, Count: 1)
    Solving time:                        0.000s (Max:     0.000s)
    Model enumeration time:              0.000s
    Time for BDD construction:           0.000s (Max:     0.000s)
Time for merge operator:                              13.778s
Time for coverage checks:                              0.002s
Total time for SMT solver (w/o itp):     0.000s

ValueAnalysisCPA statistics
---------------------------
Time for transfer relation:                            1.410s

AutomatonAnalysis (SVCOMP) statistics
-------------------------------------
Total time for successor computation:                  0.057s

CPA algorithm statistics
------------------------
Total time for CPA algorithm:       781.546s (Max:   781.546s)
  Time for choose from waitlist:      0.089s
  Time for precision adjustment:      3.072s
  Time for transfer relation:       763.041s
  Time for merge operator:           14.728s
  Time for stop operator:             0.255s
  Time for adding to reached set:     0.211s

Only BMC is executed, and we can see that the time for the transfer relation was 763s. However, the time measurements for the transfer relations of the PredicateCPA, ValueAnalysisCPA, and AutomatonCPA are all below 2s each.

The full list of used CPAs is this:

cpa.arg.ARGCPA
cpa.location.LocationCPA
cpa.callstack.CallstackCPA
cpa.functionpointer.FunctionPointerCPA
cpa.predicate.PredicateCPA
cpa.assumptions.storage.AssumptionStorageCPA
cpa.loopbound.LoopBoundCPA
cpa.value.ValueAnalysisCPA

We need to investigate which of these takes so much time.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information