[klee-dev] Guided Search - Help

[Alberto Barbaro]

Thanks I'll try that one later :)

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

> You need to pass -allow-seed-extension (or -allow-seed-truncation) when
> the seed is shorter (or longer) than the symbolic file
>
> On Tue, Oct 16, 2018 at 12:38 AM Alberto Barbaro <
> barbaro.alberto at gmail.com> wrote:
>
>> 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