[klee-dev] Why no BFS?

Tue Apr 23 13:58:01 BST 2013

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.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.
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev