[klee-dev] question on klee-stats options

[Frank Busse]

Hi,


On Fri, 2 Apr 2021 19:05:04 +0300
Aleksei Pleshakov <qroort at gmail.com> wrote:

> Currently I am trying to understand what particular KLEE execution
> statistics are important for me to know

Depends on what you're doing. As a user you are probably interested in
coverage (ICov), as a developer in the stats you try to optimise (e.g.
solving time, coverage, cache hits).

> so could you please elaborate on the meaning of "active states"? I
> assume that is about ExectionState object, and active state means
> being processed in the engine at the moment. So does the option
> MaxStates stand for the number of forks that are analyzed
> simultaneously?

"Active states" is the number of states that are handled at some point
in time during execution. (This does not include states that were
already terminated.) When you dump the corresponding sqlite file
(run.stats) you get the time stamps and the number of states at that
time. You can also visualise the data in Grafana (see docs). The last
row for run.stats is usually written after terminating all states,
hence the "States" statistic is empty when using klee-stats.

"AvgStates" is the average value of the corresponding column
(NumStates) and "MaxStates", similarly, the maximum value of that
column. Be careful when using those statistics, some benchmarks start
with hundreds of thousands of states but degrade to a single one due to
memory pressure. You might miss such cases just by looking at avg/max. 

> Also, could you please hint me what wrt and wall time are?

wrt - "with respect to"

wall time - execution time of KLEE (wall clock time, opposed to
user/system time etc.)

> And would you mind what time does Tfork measure?

This is roughly the time spent in KLEE's branch/fork functions and
includes things as checking path feasibility, attaching constraints and
maintaining the process tree. It is not the time spent forking STP ;).


Kind regards,

Frank