Re: [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 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/


___
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

Re: [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  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/

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Klee path statistics and merging options

[Dan Liew]

> 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.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Klee path statistics and merging options

[Carril Rodriguez, Luis Manuel (IPD)]

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-boun...@imperial.ac.uk  on 
behalf of RAJDEEP MUKHERJEE 
Sent: 17 December 2015 03:08
To: klee-dev@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

--



___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [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.rodrig...@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-boun...@imperial.ac.uk 
> on behalf of RAJDEEP MUKHERJEE 
> *Sent:* 17 December 2015 03:08
> *To:* klee-dev@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/

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Re: [klee-dev] Klee path statistics and merging options

[Dan Liew]

Hi,

On 17 December 2015 at 02:08, RAJDEEP MUKHERJEE
 wrote:
>
> 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

Use the ``klee-stats`` tool tool on an output directory (e.g.
``klee-last``) produced by KLEE after it has finished executing.

> 2> Does Klee perform any state merging or path-merging ? What option to use
> for this ?

Not by default. There is experimental support for merging paths with
the ``klee_merge()`` special function but I've never used it.

> 3> Does Klee perform property driven slicing before it begins symbolic
> execution ?

Technically I think running an optimisation that the LLVM optimiser
considers remove dead code could be considered a form of program
slicing
but that's probably not what you mean by "property driven slicing" in
which case the answer is probably no.

Dan.

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev