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

[Alberto Barbaro]

Thanks Martin,
I think tipically within the update function all the states within the
'removedStates' vector are removed from the 'states' variable so I thought
I should do the same in my case.

If in other cases states are added I think my approach to remove or add
states depending on the condition described in the .path file it would not
work. Are you happy to describe an approach that I should use for creating
this kind of searcher?

Just to clarify, I have a ,path file with 0's and 1's because a program was
executed with a real input file as parameter and now I would like to
execute again the same program but with symbolic input and be able to
follow exactly the same path had before.

Thanks


On Wed, May 2, 2018, 22:11 Nowack, Martin <m.nowack at imperial.ac.uk> wrote:

> Hi Alberto,
>
> The function `selectState()` returns the state you would like KLEE to work
> on next.
> So this always only one state.
>
> 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>
> 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> 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
>> > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>> >
>>
>> _______________________________________________
>> klee-dev mailing list
>> 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
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed