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

[Alberto Barbaro]

Hi,
I was able to create a new Searcher called Guided where I have implemented
my selectState() and updateStates(). The problem I have now is to identify
what state I should return  in select selectState() and how to remove all
the other states(). I guessed that with symbolic input when and if is
encountered 2 states are returned, the first should be the false branch
instead the second should be the true branch. Am I right? At this point
should I terminate the other state?

Thanks for your time.

A

2018-03-18 20:43 GMT+00:00 Alberto Barbaro <barbaro.alberto at gmail.com>:

> Thanks I'll do, do you think my approach is correct or should I do it on a
> different way? How would you approach it?
>
> Thanks
>
> 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
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed