[klee-dev] Timed-out solver queries

[Frank Busse]

Hi,


On Tue, 14 Apr 2020 16:18:59 +0200
Hooman wrote:

> As you rightfully mentioned I am not sure that any of the queries 
> time-out. However, I am also not sure if I should use all 
> -use-query-log=solver:smt2 -min-query-time-to-log=20 
> --max-solver-time=20 options or klee will report timed-out queries 
> itself by default. (as -log-timed-out-queries option is true by 
> default). I also appreciate to have a response for my second question.

1. "-use-query-log=solver:smt2" enables query logging
2. "-min-query-time-to-log=20" sets a threshold to only log more
   expensive queries
3. "-max-solver-time=20" sets a time limit for the core (constraint)
   solver; keep in mind, that KLEE disables that limit in certain places
4. "-log-timed-out-queries" enables logging of timed out queries

As you wrote, 4) is enabled by default. In KLEE it is used in a
disjunction with 2). That means 2) prevents you from logging queries
that didn't ran into the timeout. 1) is mandatory, otherwise KLEE
doesn't log anything.


On Tue, 14 Apr 2020 09:39:42 +0200
Hooman wrote:

> 2- How is it possible to associate a timed-out query with certain
> part of the code. So to understand what parts klee was not able to
> cover.

IMHO there is no mechanism in upstream KLEE. Easiest way is probably to
modify KLEE's solver API: pass the corresponding state and print the
current code location (prevPC).


Kind regards,

Frank