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 <[email protected]>:
> 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: [email protected]
>
--
张枨宇 Chengyu Zhang
East China Normal University
School of Computer Science and Software Engineering
Tel: 18685412181
Mail: [email protected]
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
