[klee-dev] KLEE SMT query overhead

[William Leeson]

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

Expensive. If it helps, I ran klee for 5 hours on the most recent version
of find with the following settings:

klee --simplify-sym-indices --write-cvcs --write-cov --output-module
--max-memory=2000 --disable-inlining --optimize --use-forked-solver
--use-cex-cache --libc=uclibc --posix-runtime --external-calls=all
--only-output-states-covering-new --use-query-log=solver:smt2
--env-file=test.env --run-in-dir=/tmp/sandbox --write-smt2s
--max-sym-array-size=4096 --max-time=300min --watchdog
--max-memory-inhibit=false --max-static-fork-pct=1 --max-static-solve-pct=1
--max-static-cpfork-pct=1 --switch-type=internal --search=random-path
--search=nurs:covnew --use-batching-search --batch-instructions=10000
findutils-4.9.0/obj-llvm/find/find.bc -sym-args 0 3 20 -sym-files 1 40
-sym-stdin 40

There are 10 queries listed as taking over 100s in the solver-queries.smt2
file, but when I ask STP to solve them, it takes somewhere between 0.6 and
1.7 seconds to solve.

Are you using the solvers in the container directly or via kleaver?
>
The results described above, directly in the container. However, I have
replicated it on a full install of klee with Z3. Should I be using kleaver?

Sorry for the duplicate message. I just realized I didn't reply all.

Thank you,
Will

On Wed, Mar 9, 2022 at 10:57 AM Frank Busse <f.busse at imperial.ac.uk> wrote:

> 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
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
-------------- next part --------------
HTML attachment scrubbed and removed