[klee-dev] Guided Search - Help

[Alberto Barbaro]

Hi Andrew and Sang,
Thanks a lot for your explanation. I tried and I think we are getting there.

@Andrew: so as you suggested I tried klee -seed-out=file.bout first.bc
-only-seed A -sym-files 1 10. Now klee is complaining about the different
file size. When I generated the file.bout of course the file was just 1
byte, now I would like to use a symbolic file. Can you suggest me how to
solve my problem please?

@Sang: I'll have a look and try to use it and get back to you.

Once I solved this problem I'll try to create a PR so next time should be
easier for all of us.

Thanks again


On Tue, Oct 16, 2018, 00:50 Sang Phan <phanquocsang at gmail.com> wrote:

> Hi Alberto,
>
> What you described is called concolic execution (
> https://en.wikipedia.org/wiki/Concolic_testing)
> So the easiest way is to use an existing concolic execution engine, and
> you will have what you want out-of-the-box.
>
> KLEE had a concolic execution engine, called ZESTI, but it is no longer
> supported. You may want to try Crete, it is based on KLEE, but maintained
> by a different group.
> https://github.com/SVL-PSU/crete-dev
> I have not checked it.
>
> KLEE can be run with (concrete) seeds, and when there is only one seed, it
> is somewhat similar to concolic execution. But you need to:
> + tell KLEE that you only want to run seed (-only-seed) and you only want
> to replay seeds (-only-replay-seeds), and
> + re-start KLEE for each run of each seed.
>
> Cheers,
> Sang
>
> On Sun, Oct 14, 2018 at 5:25 AM Alberto Barbaro <barbaro.alberto at gmail.com>
> wrote:
>
>> Hi all,
>> I have already asked this in the past and received few suggestions but I
>> was not able to do it. I'm trying to test pngpixel[1] that takes as input
>> an image file. My goal is to execute pngpixel with a real file and
>> subsequently execute pngpixel with a symbolic file and follow the path
>> followed by the first execution.I would like to describe my approach so
>> before spending to much time on it and I can understand if I'm doing it
>> right or not :)
>>
>> 1 - Execute pngpixel enabling -debug-print-instructions=src:file
>> 2 - Inside my searcher create a map from instruction.txt so I know which
>> is the next instruction
>> 3 - Inside the update() function for my searcher, get the current
>> instruction, get the next instruction,
>> 4 - Check for each state in addedStates if the next instruction would be
>> execute at the next step in the state
>> 5 - If yes add the state using state.push_back(state) else remove the
>> state ( adding the state to removedStates? )
>>
>> I'm sure this flow is not optimized but at least is it correct? How would
>> you approach this problem?
>>
>> Thanks for your time
>> Alberto
>>
>> [1]
>> https://github.com/fcoulombe/libpng/blob/master/contrib/examples/pngpixel.c
>> _______________________________________________
>> 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