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 <d...@su-root.co.uk
<mailto:d...@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@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
