Discussion:
Why no BFS?
Loi Luu
2013-04-23 11:03:52 UTC
Permalink
Dear all,

I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in some cases
and equally good in almost all cases than that of DFS.

For example, in the *stat *in coreutils 6.11:
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 | 29019 |
1.49 | 0 | 0 | 0.00 | 26.64 |
26.64 | 26.47 | 1 | 15 | 1.37
| 0.00 |

with --search=dfs

| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last | 15356 | 0.03 | 7.12 | 4.24 | 29019 |
1.90 | 0 | 0 | 0.00 | 26.61 |
26.61 | 26.46 | 1 | 15 | 1.75 |
0.00 |


The difference of state space is pretty small, so is there any reason that
BFS is not included in Klee?

Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Paul Marinescu
2013-04-23 11:33:47 UTC
Permalink
Hello Loi,
DFS is not the default searcher for a few months now. What results do
you get with no --search argument?

Paul
Post by Loi Luu
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in some cases
and equally good in almost all cases than that of DFS.
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 | 29019 |
1.49 | 0 | 0 | 0.00 | 26.64
| 26.64 | 26.47 | 1 | 15
| 1.37 | 0.00 |
with --search=dfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last | 15356 | 0.03 | 7.12 | 4.24 | 29019 |
1.90 | 0 | 0 | 0.00 | 26.61
| 26.61 | 26.46 | 1 | 15 |
1.75 | 0.00 |
The difference of state space is pretty small, so is there any reason
that BFS is not included in Klee?
Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Loi Luu
2013-04-23 11:58:31 UTC
Permalink
Hello Paul,

I got this one:

| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount | TSolver(%)
| States | maxStates | avgStates | Mem(MB) | maxMem(MB) | avgMem(MB) |
Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last | 15428 | 0.03 | 7.12 | 4.24 | 29019 |
2.36 | 0 | 0 | 0.00 | 26.62 | 26.62
| 26.47 | 1 | 15 | 2.19 |
0.00 |

This is still not as good as BFS result. And I want to emphasis again the
question is why no BFS?

Thanks,



On Tue, Apr 23, 2013 at 6:33 PM, Paul Marinescu <
Post by Paul Marinescu
Hello Loi,
DFS is not the default searcher for a few months now. What results do you
get with no --search argument?
Paul
Post by Loi Luu
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in some cases
and equally good in almost all cases than that of DFS.
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------**------------------------------**
------------------------------**------------------------------**
------------------------------**------------------------------**----
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 | 29019 |
1.49 | 0 | 0 | 0.00 | 26.64
| 26.64 | 26.47 | 1 | 15
| 1.37 | 0.00 |
with --search=dfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------**------------------------------**
------------------------------**------------------------------**
------------------------------**------------------------------**--
| klee-last | 15356 | 0.03 | 7.12 | 4.24 | 29019 |
1.90 | 0 | 0 | 0.00 | 26.61
| 26.61 | 26.46 | 1 | 15 |
1.75 | 0.00 |
The difference of state space is pretty small, so is there any reason
that BFS is not included in Klee?
Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Paul Marinescu
2013-04-23 12:45:01 UTC
Permalink
Hello Loi,
In general, given limited resources, BFS will only explore shallow
states (parsing inputs), while ideally you want to explore the whole
program.

The stats that you get are a bit dodgy. The fact that you explore the
entire state space with respect to the symbolic input chosen (are you
using any symbolic input?), but you get different #Inst and Cov% with
your BFS searcher doesn't make sense.

Finally, stats for a 0.04s execution are not representative for symbolic
execution. Use 1h runs for a compelling comparison.

Paul
Post by Loi Luu
Hello Paul,
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last | 15428 | 0.03 | 7.12 | 4.24 | 29019 |
2.36 | 0 | 0 | 0.00 | 26.62 |
26.62 | 26.47 | 1 | 15 |
2.19 | 0.00 |
This is still not as good as BFS result. And I want to emphasis again
the question is why no BFS?
Thanks,
On Tue, Apr 23, 2013 at 6:33 PM, Paul Marinescu
Hello Loi,
DFS is not the default searcher for a few months now. What results
do you get with no --search argument?
Paul
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in some cases
and equally good in almost all cases than that of DFS.
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__----
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 |
29019 |
1.49 | 0 | 0 | 0.00 | 26.64
| 26.64 | 26.47 | 1 | 15
| 1.37 | 0.00 |
with --search=dfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__--
| klee-last | 15356 | 0.03 | 7.12 | 4.24 |
29019 |
1.90 | 0 | 0 | 0.00 |
26.61
| 26.61 | 26.46 | 1 | 15
|
1.75 | 0.00 |
The difference of state space is pretty small, so is there any reason
that BFS is not included in Klee?
Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Cristian Cadar
2013-04-23 12:58:01 UTC
Permalink
Hi Loi,

There is not reason not to have BFS in KLEE, and we would be happy to
add support for this: just send your patch for review to the
klee-commits mailing list.

This was never a priority because, as Paul mentioned, KLEE has more
advanced heuristics, including one that actively favors uncovered code.
For a proper comparison, you should run more benchmarks for a longer
amount of time, as Paul suggested (and also make sure you eliminate any
significant sources of non-determinism).

Best,
Cristian
Post by Paul Marinescu
Hello Loi,
In general, given limited resources, BFS will only explore shallow
states (parsing inputs), while ideally you want to explore the whole
program.
The stats that you get are a bit dodgy. The fact that you explore the
entire state space with respect to the symbolic input chosen (are you
using any symbolic input?), but you get different #Inst and Cov% with
your BFS searcher doesn't make sense.
Finally, stats for a 0.04s execution are not representative for symbolic
execution. Use 1h runs for a compelling comparison.
Paul
Post by Loi Luu
Hello Paul,
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
| klee-last | 15428 | 0.03 | 7.12 | 4.24 | 29019 |
2.36 | 0 | 0 | 0.00 | 26.62 |
26.62 | 26.47 | 1 | 15 |
2.19 | 0.00 |
This is still not as good as BFS result. And I want to emphasis again
the question is why no BFS?
Thanks,
On Tue, Apr 23, 2013 at 6:33 PM, Paul Marinescu
Hello Loi,
DFS is not the default searcher for a few months now. What results
do you get with no --search argument?
Paul
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in some cases
and equally good in almost all cases than that of DFS.
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__----
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 |
29019 |
1.49 | 0 | 0 | 0.00 |
26.64
| 26.64 | 26.47 | 1 | 15
| 1.37 | 0.00 |
with --search=dfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__------------------------------__--
| klee-last | 15356 | 0.03 | 7.12 | 4.24 |
29019 |
1.90 | 0 | 0 | 0.00 |
26.61
| 26.61 | 26.46 | 1 | 15
|
1.75 | 0.00 |
The difference of state space is pretty small, so is there any reason
that BFS is not included in Klee?
Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Loi Luu
2013-04-23 13:37:13 UTC
Permalink
Thank you Cristian and Paul,

@Cristian: Could you please tell me how to send you my patch? I just
subscribed to klee-commits mailing list and dont know where to go from
there.

Thanks,
Post by Cristian Cadar
Hi Loi,
There is not reason not to have BFS in KLEE, and we would be happy to add
support for this: just send your patch for review to the klee-commits
mailing list.
This was never a priority because, as Paul mentioned, KLEE has more
advanced heuristics, including one that actively favors uncovered code.
For a proper comparison, you should run more benchmarks for a longer
amount of time, as Paul suggested (and also make sure you eliminate any
significant sources of non-determinism).
Best,
Cristian
Post by Paul Marinescu
Hello Loi,
In general, given limited resources, BFS will only explore shallow
states (parsing inputs), while ideally you want to explore the whole
program.
The stats that you get are a bit dodgy. The fact that you explore the
entire state space with respect to the symbolic input chosen (are you
using any symbolic input?), but you get different #Inst and Cov% with
your BFS searcher doesn't make sense.
Finally, stats for a 0.04s execution are not representative for symbolic
execution. Use 1h runs for a compelling comparison.
Paul
Post by Loi Luu
Hello Paul,
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------**------------------------------**
------------------------------**------------------------------**
------------------------------**------------------------------**--
| klee-last | 15428 | 0.03 | 7.12 | 4.24 | 29019 |
2.36 | 0 | 0 | 0.00 | 26.62 |
26.62 | 26.47 | 1 | 15 |
2.19 | 0.00 |
This is still not as good as BFS result. And I want to emphasis again
the question is why no BFS?
Thanks,
On Tue, Apr 23, 2013 at 6:33 PM, Paul Marinescu
Hello Loi,
DFS is not the default searcher for a few months now. What results
do you get with no --search argument?
Paul
Dear all,
I just added bfs-searcher to klee and make some comparisons between DFS
(which is default searcher now) and BFS. Surprisingly, the result for
branch coverage and instruction coverage of BFS are better in
some cases
and equally good in almost all cases than that of DFS.
with --search=bfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------**__----------------------------**
--__--------------------------**----__------------------------**
------__----------------------**--------__--------------------**
----------__----
| klee-out-10 | 21801 | 0.04 | 15.34 | 9.99 |
29019 |
1.49 | 0 | 0 | 0.00 |
26.64
| 26.64 | 26.47 | 1 | 15
| 1.37 | 0.00 |
with --search=dfs
| Path | Instrs | Time(s) | ICov(%) | BCov(%) | ICount |
TSolver(%) | States | maxStates | avgStates | Mem(MB) | maxMem(MB) |
avgMem(MB) | Queries | AvgQC | Tcex(%) | Tfork(%) |
------------------------------**__----------------------------**
--__--------------------------**----__------------------------**
------__----------------------**--------__--------------------**
----------__--
| klee-last | 15356 | 0.03 | 7.12 | 4.24 |
29019 |
1.90 | 0 | 0 | 0.00 |
26.61
| 26.61 | 26.46 | 1 | 15
|
1.75 | 0.00 |
The difference of state space is pretty small, so is there any reason
that BFS is not included in Klee?
Thanks,
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
______________________________**___________________
klee-dev mailing list
https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev>
<https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
______________________________**___________________
klee-dev mailing list
https://mailman.ic.ac.uk/__**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev>
<https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
______________________________**_________________
klee-dev mailing list
https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
--
Loi, Luu The (Mr.)
University of Engineering and Technology, Vietnam National University,
Hanoi.
Continue reading on narkive:
Loading...