Hi Martin, Thanks for your reply. I'm interested in giving a patch to improve the situation, and I would like to try.
Here is my idea: First, I think we could update min-distance-to-uncovered dynamically when we need, such as there are no candidate state covering new instruction and need to be decided which state should be selected. So that we needn't update periodically, instead more effectively. Second, We could just calculate min-distance-to-uncovered for candidate instructions(The pc of candidate states) using Dijkstra's algorithm rather than iterating all instructions. In this way, we may decrease the cost of updating. Is my idea reasonable? Thanks and Cheers, Chengyu 2016-11-21 21:13 GMT+08:00 Martin Nowack <martin_now...@tu-dresden.de>: > Hi Chengyu, > > On 18 Nov 2016, at 15:16, Chengyu Zhang <dale.chengyu.zh...@gmail.com> > wrote: > > > > But I have a question that why KLEE set uncovered-update interval > default to 30 ticks rather than every time we do stepInstruction function? > > Is it because of low efficiency or other reasons? > > > > Well, the current implementation is quite costly, therefore the high value > of 30s. > This might be less of a problem with older machines but becomes more > problematic with newer ones, > as they number of instructions per second might be much higher. So you > update less often and might > work more often with outdated information. > So you should vary that number according to your needs. > > (Of course, patches, which improve that situation are always welcome ;) ) > > Cheers, > Martin > > > > Best regards, > > Chengyu > > > > 2016-11-02 18:00 GMT+08:00 Chengyu Zhang <dale.chengyu.zh...@gmail.com>: > > Hi all, > > > > I saw the md2u(Min-Dist-to-Uncovered) search heuristic in KLEE. > > In my opinion, md2u is the strategy that when selecting a state KLEE > aways consider about > > the states have the minimum distance to uncovered part of the code. I > read the source code > > of the MinDistToUncovered, but I'm still confused about the implement of > computeMinDistToUncovered function. > > > > So I have two questions: > > > > 1. If someone could give the algorithm description about how to compute > the minimum distance to uncovered part in KLEE or explain the implement of > computeMinDistToUncovered function in KLEE. And if I could compute the > distance between two instructions in KLEE. > > > > 2. What's the difference between CovNew and MD2U search heuristic ? > > > > Thanks a lot. > > Chengyu Zhang > > > > -- > > 张枨宇 Chengyu Zhang > > East China Normal University > > School of Computer Science and Software Engineering > > Tel: 18685412181 > > Mail: dale.chengyu.zh...@gmail.com > > > > > > > > -- > > 张枨宇 Chengyu Zhang > > East China Normal University > > School of Computer Science and Software Engineering > > Tel: 18685412181 > > Mail: dale.chengyu.zh...@gmail.com > > _______________________________________________ > > klee-dev mailing list > > klee-dev@imperial.ac.uk > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > --------------------------------------------------- > Martin Nowack > Research Assistant > > Technische Universität Dresden > Computer Science > Institute of Systems Architecture > Systems Engineering > 01062 Dresden > > Phone: +49 351 463 39608 > Email: martin_now...@tu-dresden.de > ---------------------------------------------------- > > -- 张枨宇 Chengyu Zhang East China Normal University School of Computer Science and Software Engineering Tel: +86 18685412181 Mail: dale.chengyu.zh...@gmail.com
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev