[klee-dev] KLEE SMT query overhead

[Frank Busse]

Hi,


On Tue, 8 Mar 2022 13:58:57 -0500
William Leeson <wel2vw at virginia.edu> wrote:

> I'm finding that the Elapsed time reported by KLEE in solver-queries.smt2
> for a single query is  different from the time reported by the solver klee
> is built on (stp_simple in the docker /tmp folder). Orders of magnitude
> different. I confirmed this on a local install of KLEE with Z3-4.8.4 as the
> backend solver.

Are we talking about "orders of magnitude" in the milli/micro-second
range or about really expensive queries?

> I was wondering if this is to be expected. Is there some overhead KLEE
> incurs when calling the solvers? Is the solver being fed more than Query #X
> from solver-queries.smt2 (For example, is it an incremental solve with
> previous queries taken into account?)

There is no incremental solving in upstream KLEE. The time is measured
by another pseudo-solver in the solving chain (QueryLoggingSolver) in
front of the core solvers (STP, Z3, MetaSMT). Hence, there is overhead
involved, e.g. the conversion of KLEE's native expressions into
solver-specific queries or for STP even a call of fork() depending on
the configuration.

Are you using the solvers in the container directly or via kleaver?


Kind regards,

Frank