[klee-dev] Why no BFS?

[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

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.marinescu at imperial.ac.uk <mailto:paul.marinescu at 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 at imperial.ac.uk <mailto:klee-dev at 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 at imperial.ac.uk <mailto:klee-dev at 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.