[klee-dev] Klee path statistics and merging options

[Cristian Cadar]

Hi Rajdeep, in dynamic symbolic execution, only a subset of paths are 
usually explored.  The number of completed paths is just the number of 
feasible paths successfully explored by KLEE in the given time budget. 
You might want to refer to the EXE and KLEE papers for more details on 
how this variant of symbolic execution works.

Cristian

On 06/01/16 05:44, RAJDEEP MUKHERJEE wrote:
>
> 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
> <mailto: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>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>