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
On 23/04/13 13:45, Paul Marinescu wrote:
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
On 23/04/13 12:58, Loi Luu wrote:
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
<paul.marine...@imperial.ac.uk <mailto:paul.marine...@imperial.ac.uk>>
wrote:
Hello Loi,
DFS is not the default searcher for a few months now. What results
do you get with no --search argument?
Paul
On 23/04/13 12:03, Loi Luu wrote:
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.
_________________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk <mailto:klee-dev@imperial.ac.uk>
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
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
