[klee-dev] The algorithm of Min-Dist-to-Uncovered Searcher

[Chengyu Zhang]

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_nowack at tu-dresden.de>:

> Hi Chengyu,
> > On 18 Nov 2016, at 15:16, Chengyu Zhang <dale.chengyu.zhang at 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.zhang at 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.zhang at gmail.com
> >
> >
> >
> > --
> > 张枨宇   Chengyu Zhang
> > East China Normal University
> > School of Computer Science and Software Engineering
> > Tel: 18685412181
> > Mail: dale.chengyu.zhang at gmail.com
> > _______________________________________________
> > klee-dev mailing list
> > klee-dev at 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_nowack at tu-dresden.de
> ----------------------------------------------------
>
>


-- 
张枨宇   Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: +86 18685412181
Mail: dale.chengyu.zhang at gmail.com
-------------- next part --------------
HTML attachment scrubbed and removed