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 <[email protected]>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 >>> <[email protected] >>> <mailto:paul.marinescu@**imperial.ac.uk<[email protected]> >>> >> >>> 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 >>> [email protected] >>> <mailto:[email protected].**uk<[email protected]> >>> > >>> >>> 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 >>> [email protected] >>> <mailto:[email protected].**uk<[email protected]> >>> > >>> >>> 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 >> [email protected] >> https://mailman.ic.ac.uk/**mailman/listinfo/klee-dev<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev> >> > > ______________________________**_________________ > klee-dev mailing list > [email protected] > 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
