Re: [klee-dev] obtain distance to a particular instruction

2019-08-28 Thread Nowack, Martin
Hi Qiao,

Currently, there is no direct support for this.
But, to hack it - under the assumption you don’t need the coverage-guided 
searcher - you can modify the `StatsTracker::computeReachableUncovered` 
function 
(https://github.com/klee/klee/blob/8a531bf8f276274b146dbb245293b06d31dfaef4/lib/Core/StatsTracker.cpp#L805).

You can update the `sm.setIndexedValue(…)` and replace `isa(inst)` 
(https://github.com/klee/klee/blob/8a531bf8f276274b146dbb245293b06d31dfaef4/lib/Core/StatsTracker.cpp#L875)
 with the check for your target instruction. Still, this will used for distance 
calculation for all states.

Hope that helps,

Martin

On 10. Aug 2019, at 04:44, Qiao Kang 
mailto:qiaokang1...@gmail.com>> wrote:

Hi,

If I understand correctly, KLEE can use MinDistToUncovered as a weight to 
prioritize execution state which is closet to an uncovered instruction. What if 
I want to prioritize the state which is closet to a particular instruction 
(say, the instruction at line X), instead of an uncovered one?

One way in my mind is to obtain the distance between the state and the target 
instruction. Is there such an API in KLEE that can help compute this dist?

Thanks,
Qiao
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


[klee-dev] obtain distance to a particular instruction

2019-08-09 Thread Qiao Kang
Hi,

If I understand correctly, KLEE can use MinDistToUncovered as a weight to
prioritize execution state which is closet to an uncovered instruction.
What if I want to prioritize the state which is closet to a particular
instruction (say, the instruction at line X), instead of an uncovered one?

One way in my mind is to obtain the distance between the state and the
target instruction. Is there such an API in KLEE that can help compute this
dist?

Thanks,
Qiao
___
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev