[klee-dev] How to introduce the "Exploration Technique" concept

[Nowack, Martin]

Hi Alberto,

The function `selectState()` returns the state you would like KLEE to work on next.
So this is always only one state maximum.

The update function is KLEE’s callback to your searcher to inform you which states have been added or removed.

But, you should not make any assumption on the order of states coming in nor how many states you will have.
Forking of states can happen at different positions not only the branch instruction.

The only information you can currently consider as exact is the one you get from the state itself: e.g. the old
instruction pointer and the new instruction pointer, but of course there is much more there.

Hope that helps you a bit further.

Best,
Martin

On 2. May 2018, at 20:16, Alberto Barbaro <barbaro.alberto at gmail.com<mailto:barbaro.alberto at gmail.com>> wrote:

Hi all,
thanks for the answer. I was able to create another searcher called "guided" that should do what i want but I have problem for now. From my understanding the crucial function to implement are: update and selectState.

I think in the selectState function I should return *states[0] or *states[1] depending if in the condition is false or true. I'm not sure that the first state represents the false condition so please let me know if I'm wrong. Instead, within the update function I should remove all the states apart states[0] or states[1] depending on the content of the file again.

Unfortunately I'm not sure that if my idea is correct. Can someone let me know what I'm missing and maybe give me an example?

Thanks
Alberto

On Sun, Mar 18, 2018, 19:31 Cristian Cadar <c.cadar at imperial.ac.uk<mailto:c.cadar at imperial.ac.uk>> wrote:
My recommendation is to implement such an exploration technique as an
independent search heuristic.  The bar for changing the core of KLEE is
much higher, as it affects all users.

Best,
Cristian

On 18/03/2018 17:41, Alberto Barbaro wrote:
> Hi,
> I'm working on a possible PULL request that would allow to execute a
> project but excluding paths based on a .path previously generated using
> KLEE. Doing so it would be possible to have some sort of "exploration
> technique" that would help to follow specific paths.
>
> I think, after having generated the .path file, it would be possible to
> do so amending Executor.cpp main switch for the Instruction::Br case.
> I'm able to keep track of the "index" for the current branch so I would
> check cond.get().isTrue() comparing with value on line "index". At this
> point I'm not sure how to skip a branch ( I cannot use exit(0) like
> klee_silent_exit I think ). Should I just modify the if for the "br"
> branch of the switch?
>
> Thanks for any suggesiton,
> A
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>

_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

-------------- next part --------------
HTML attachment scrubbed and removed