[klee-dev] Guided Search - Help
Alberto Barbaro
barbaro.alberto at gmail.com
Fri Oct 19 18:51:26 BST 2018
Hi all,
I think we are getting there but I'm still missing something. So I was able
to generate pngpixel.bc and successfully use it. My next step was to
generate the seed an I used the following command:
gen-bout --sym-file ../images/png-files-download.png && mv file.bout
png-files-download.bout
Now, as suggested, I have used that seed with klee:
klee at a8a6399e6799:~/seeds$ time klee -only-seed
-seed-out=png-files-download.bout -only-replay-seeds --posix-runtime
-libc=uclibc ../target/libpng-1.6.35/contrib/examples/pngpixel.bc 1 1 A
--sym-files 1 89760
KLEE: NOTE: Using klee-uclibc :
/usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bca
KLEE: NOTE: Using POSIX model:
/usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bca
KLEE: output directory is
"/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41"
KLEE: Using STP solver backend
KLEE: WARNING: undefined reference to function: floor
KLEE: WARNING: undefined reference to function: modf
KLEE: WARNING: undefined reference to function: pow
KLEE: KLEE: using 1 seeds
KLEE: 1 seeds remaining over: 1 states
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at
/home/klee/klee-gen-bout/runtime/POSIX/fd.c:980
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: Alignment of memory from call "malloc" is not modelled.
Using alignment of 8.
KLEE: WARNING ONCE: ioctl: (TCGETS) symbolic file, incomplete model
KLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash:
MO504[8192] allocated at global:crc_table
KLEE: 1 seeds remaining over: 1 states
KLEE: 1 seeds remaining over: 1 states
KLEE: WARNING ONCE: silently concretizing (reason: floating point)
expression (Select w32 (Slt 4294967295
N0:(Or w32 (Or w32 (Or w32 (Shl w32 (ZExt w32 (Read w8 55
A-data))
16)
(Shl w32 (ZExt w32 (Read w8 54
A-data))
24))
(Shl w32 (ZExt w32 (Read w8 56 A-data))
8))
(ZExt w32 (Read w8 57 A-data))))
N0
4294967295) to value 541597261
(/home/klee/target/libpng-1.6.35/png.c:3371)
KLEE: WARNING: seeds patched for violating constraint
KLEE: WARNING ONCE: calling external: floor(4621195801218788662) at
/home/klee/target/libpng-1.6.35/png.c:3375
KLEE: 1 seeds remaining over: 1 states
KLEE: WARNING ONCE: calling external: vprintf(146758144, 154438432) at
/home/klee/klee_build/klee-uclibc/libc/stdio/fprintf.c:35
libpng warning: ����: gamma value does not match sRGB
>From my initial understanding now klee should follow only one path but i
feel that is not the case because at this point the input is symbolic so it
would follow all the paths.. I'm a bit confused at the moment.
Just to clarify, the expect output should be:
klee at a8a6399e6799:~/seeds$
../target/libpng-1.6.35/contrib/examples/pngpixel 1 1
../images/png-files-download.png
RGBA 255 255 255 255
klee at a8a6399e6799:~/seeds$
What am I missing? :)
Thanks for your help!
Alberto
Il giorno mar 16 ott 2018 alle ore 14:27 Alberto Barbaro <
barbaro.alberto at gmail.com> ha scritto:
> 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
More information about the klee-dev
mailing list