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

[Chengyu Zhang]

Hi all,

     After reading the source code, I have figured out how MD2U strategy
works.
     The main idea of MD2U strategy is :
          Init every uncovered instruction min-distance-to-uncovered value
to 1, every covered instruction min-distance-to-uncovered value to 0;
          Iterate each instruction, inherit min-distance-to-uncovered value
from it's successor, until no more min-distance-to-uncovered value have
changed.
          Then we can get the min-distance-to-uncovered for every
instruction.

    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?

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
-------------- next part --------------
HTML attachment scrubbed and removed