[klee-dev] Why no BFS?
Loi Luu
loi.luuthe at gmail.com
Tue Apr 23 14:37:13 BST 2013
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,
On Tue, Apr 23, 2013 at 7:58 PM, Cristian Cadar <c.cadar at imperial.ac.uk>wrote:
>
> 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@**imperial.ac.uk<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<klee-dev at imperial.ac.uk>
>>> >
>>> 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
>>> klee-dev at imperial.ac.uk <mailto:klee-dev at imperial.ac.**uk<klee-dev at imperial.ac.uk>
>>> >
>>> 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
>> 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
> 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.
-------------- next part --------------
HTML attachment scrubbed and removed
More information about the klee-dev
mailing list