[klee-dev] Klee path statistics and merging options

[RAJDEEP MUKHERJEE]

Hi Dan,

Many thanks for your reply. I have another query regarding the
klee-statistics.

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> How to get the statistics for the number of feasible, infeasible and
total paths ?

Many thanks in advance.

Best,
Rajdeep

On Tue, Jan 5, 2016 at 4:40 PM, Dan Liew <dan at su-root.co.uk> wrote:

> > 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 ?
>
> AFAIK KLEE issues a query at every branch point. This does not
> necessarily trigger a call to the underlying solver though as KLEE has
> some caching mechanisms that may fire.
>
> > 3>  Does Klee support SAT solvers in the backend like MiniSAT etc ?
>
> You are looking at the wrong level. KLEE works at the level of SMT
> solvers, not SAT solvers as it needs a logic over bitvectors, not
> booleans. Typically an SMT solver will be implemented in terms of a
> SAT solver but KLEE does not know this. STP itself supports two
> backends MiniSat and CryptoMinisat4. KLEE doesn't currently set the
> backend to use in STP but support could be added. I would happily
> review a pull request that added this.
>
> KLEE supports a few other SMT solvers via the MetaSMT interface
> (untested) and I am currently working on native Z3 support.
>
> > 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.
>
> KLEE supports emission of the constraints in its own custom language
> (KQuery) and as SMT-LIBv2.
>
> HTH,
> Dan.
>



-- 


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