[klee-dev] Klee path statistics and merging options

[RAJDEEP MUKHERJEE]

Hi,

Many thanks for your reply. I have few follow-up questions. It would be
great
if you could help understand these queries:

1> I used klee-stats (eg. klee-stats --print-all klee-last) to see the
statistics, but it does
not report any stats about the number of feasible and infeasible paths in
the program ?

When I run Klee on a program, the statistics dumped looks like as follows.
KLEE: done: total instructions = 272667
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Is the number of completed paths same as number of feasible paths in the
program ?

2> Does Klee invoke a SAT query at every branch point in the program by
default to determine
the eager infeasibility of a path ? Or is there other heuristics to
selectively chose branch points ?

3>  Does Klee support SAT solvers in the backend like MiniSAT etc ? I
believe that the default SMT solver
used is STP. The follow-up to this question is that are there options to
dump the path-constraints
in DIMACS format to use with a SAT solver.

Many thanks in advance.

Best regards,
Rajdeep




On Sat, Dec 19, 2015 at 11:23 AM, Carril Rodriguez, Luis Manuel (IPD) <
luis.rodriguez at kit.edu> wrote:

> Hi,
>
>    about the slicing this work could interest you:
>
> http://www.fi.muni.cz/~xstrejc/publications/tacas2013preprint.pdf
>
>
>    Basically they have a llvm pass that perform the program slicing before
> running it under KLEE, reducing effectively the search space.
>
>
> Cheers
>
> Luis M.
>
>
> ------------------------------
> *From:* klee-dev-bounces at imperial.ac.uk <klee-dev-bounces at imperial.ac.uk>
> on behalf of RAJDEEP MUKHERJEE <rajdeep.mukherjee87 at gmail.com>
> *Sent:* 17 December 2015 03:08
> *To:* klee-dev at imperial.ac.uk
> *Subject:* [klee-dev] Klee path statistics and merging options
>
>
> Hi,
>
> I have the following queries regarding Klee. I would really appreciate any
> help.
>
> 1> How to obtain the following statistics from Klee:
>   A> Total number of feasible paths,
>   B> Total number of infeasible paths,
>   C> Total number of paths in the program.
>   D> Total number of solver queries and
>   E> Total time spent in solver
>
> 2> Does Klee perform any state merging or path-merging ? What option to
> use for this ?
>
> 3> Does Klee perform property driven slicing before it begins symbolic
> execution ?
>
> Many thanks in advance.
>
> Best,
> Rajdeep
>
> --
>
>
>
>


-- 


Thank You
Rajdeep Mukherjee
D.Phil Student,
Dept. of Computer Science,
University of Oxford
Mob. :- 07405100369
Webpage :- http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/
<http://cse.iitkgp.ac.in/~rajmukh/#research>
-------------- next part --------------
HTML attachment scrubbed and removed