[prev in list] [next in list] [prev in thread] [next in thread]
List: klee-dev
Subject: Re: [klee-dev] Klee path statistics and merging options
From: RAJDEEP MUKHERJEE <rajdeep.mukherjee87 () gmail ! com>
Date: 2015-12-19 14:41:53
Message-ID: CAKsD1Vm7p_7VJx=niSxu2RrMG=HDzPcpnSLS=eb+yz2YLCJUwQ () mail ! gmail ! com
[Download RAW message or body]
[Attachment #2 (multipart/alternative)]
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@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@imperial.ac.uk <klee-dev-bounces@imperial.ac.uk>
> on behalf of RAJDEEP MUKHERJEE <rajdeep.mukherjee87@gmail.com>
> *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/
<http://cse.iitkgp.ac.in/~rajmukh/#research>
[Attachment #5 (text/html)]
<div dir="ltr"><br><div>Hi,</div><div><br></div><div>Many thanks for your reply. I \
have few follow-up questions. It would be great</div><div>if you could help \
understand these queries:</div><div><br></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">1> </span><span \
style="color:rgb(0,0,0);font-family:Tahoma">I used klee-stats (eg. klee-stats \
--print-all klee-last) to see the statistics, but it does </span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma">not report any stats about the number \
</span><span style="color:rgb(0,0,0);font-family:Tahoma">of feasible and infeasible \
paths in the program ?</span></div><div><br></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">When I run Klee on a \
program, the statistics dumped looks like as follows.</span><br \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">KLEE: done: total \
instructions = 272667</span><br \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">KLEE: done: completed \
paths = 1</span><br style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">KLEE: done: generated \
tests = 1</span><br style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><br></span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">Is the number of completed \
paths same as number of feasible paths in the program ?</span><br \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><br></div><div>2> Does \
Klee invoke a SAT query at every branch point in the program by default to determine \
</div><div>the eager infeasibility of a path ? Or is there other heuristics to \
selectively chose branch points ?</div><div><br></div><div>3> <span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">Does Klee support SAT \
solvers in the backend like MiniSAT etc ? I believe that the default SMT solver \
</span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">used is STP</span><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">. The follow-up to this \
question is that</span><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"> are</span><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"> </span><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">there options to dump the \
path-constraints </span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">in DIMACS format to use \
with a SAT solver.</span><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"> </span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><br></span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">Many thanks in advance. \
</span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px"><br></span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">Best \
regards,</span></div><div><span \
style="color:rgb(0,0,0);font-family:Tahoma;font-size:13px">Rajdeep</span></div><div><br></div><div><br></div><div><br></div><div \
class="gmail_extra"><br><div class="gmail_quote">On Sat, Dec 19, 2015 at 11:23 AM, \
Carril Rodriguez, Luis Manuel (IPD) <span dir="ltr"><<a \
href="mailto:luis.rodriguez@kit.edu" \
target="_blank">luis.rodriguez@kit.edu</a>></span> wrote:<br><blockquote \
class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc \
solid;padding-left:1ex">
<div dir="ltr" style="font-size:12pt;color:#000000;background-color:#ffffff;font-family:Calibri,Arial,Helvetica,sans-serif">
<p>Hi,</p>
<p> about the slicing this work could interest you: </p>
<p><a href="http://www.fi.muni.cz/~xstrejc/publications/tacas2013preprint.pdf" \
target="_blank">http://www.fi.muni.cz/~xstrejc/publications/tacas2013preprint.pdf</a></p>
<p><br>
</p>
<p> Basically they have a llvm pass that perform the program slicing before \
running it under KLEE, reducing effectively the search space.</p> <p><br>
</p>
<p>Cheers</p>
<p>Luis M.<br>
</p>
<p><br>
</p>
<div style="color:rgb(33,33,33)">
<hr style="display:inline-block;width:98%">
<div dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" \
color="#000000"><b>From:</b> <a href="mailto:klee-dev-bounces@imperial.ac.uk" \
target="_blank">klee-dev-bounces@imperial.ac.uk</a> <<a \
href="mailto:klee-dev-bounces@imperial.ac.uk" \
target="_blank">klee-dev-bounces@imperial.ac.uk</a>> on behalf of RAJDEEP \
MUKHERJEE <<a href="mailto:rajdeep.mukherjee87@gmail.com" \
target="_blank">rajdeep.mukherjee87@gmail.com</a>><br> <b>Sent:</b> 17 December \
2015 03:08<br> <b>To:</b> <a href="mailto:klee-dev@imperial.ac.uk" \
target="_blank">klee-dev@imperial.ac.uk</a><br> <b>Subject:</b> [klee-dev] Klee path \
statistics and merging options</font> <div> </div>
</div><div><div class="h5">
<div>
<div dir="ltr">
<div><br>
</div>
<p style="margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px;margin-top:0px!important"> Hi,</p>
<p style="margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px;margin-top:0px!important"> I have the \
following queries regarding Klee. I would really appreciate any help.</p> <p \
style="margin-top:0px;margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px"> 1> How to obtain the following \
statistics from Klee:<br> A> Total number of feasible paths, <br>
B> Total number of infeasible paths,<br>
C> Total number of paths in the program.<br>
D> Total number of solver queries and<br>
E> Total time spent in solver </p>
<p style="margin-top:0px;margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px"> 2> Does Klee perform any state \
merging or path-merging ? What option to use for this ?</p> <p \
style="margin-top:0px;margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px"> 3> Does Klee perform property driven \
slicing before it begins symbolic execution ?</p> <p \
style="margin-top:0px;margin-bottom:16px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px"> Many thanks in advance.</p>
<p style="margin-top:0px;color:rgb(51,51,51);font-family:'Helvetica \
Neue',Helvetica,'Segoe UI',Arial,freesans,sans-serif,'Apple Color \
Emoji','Segoe UI Emoji','Segoe UI \
Symbol';font-size:14px;line-height:22px;margin-bottom:0px!important"> Best,<br>
Rajdeep</p>
<div><br>
</div>
-- <br>
<div>
<div dir="ltr"><br>
<br>
<br>
</div>
</div>
</div>
</div>
</div></div></div>
</div>
</blockquote></div><br><br clear="all"><div><br></div>-- <br><div \
class="gmail_signature"><div dir="ltr"><div><br><br>Thank You<br></div><div>Rajdeep \
Mukherjee</div> <div>D.Phil Student, <br>
</div><div>Dept. of Computer Science,</div>
<div> </div>
<div>University of Oxford<br>Mob. :- 07405100369<br></div>
<div>Webpage :- <a href="http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/" \
target="_blank">http://www.cs.ox.ac.uk/people/rajdeep.mukherjee/</a><a \
href="http://cse.iitkgp.ac.in/~rajmukh/#research" target="_blank"></a></div> <div> \
</div> <div> </div></div></div>
</div></div>
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
[prev in list] [next in list] [prev in thread] [next in thread]
Configure |
About |
News |
Add a list |
Sponsored by KoreLogic