[klee-dev] Guided Search - Help

Sat Oct 20 09:58:34 BST 2018

 Hi Alberto,
Please keep in mind that, although KLEE still tries to follow the seed's path, the state it maintains is no longerthe concrete state, but the symbolic state. So, the symbolic file A no longer contains a concrete RGB value at coordinate(1, 1), but instead a symbolic value. By looking at the log you sent, especially the following lines, this symbolic value couldhave been concretized by KLEE into a value you were not expecting. 
 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)
Best,Andrew    On Saturday, 20 October 2018, 1:51:56 AM GMT+8, Alberto Barbaro <barbaro.alberto at gmail.com> wrote:  

 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 89760KLEE: NOTE: Using klee-uclibc : /usr/local/lib/x86_64-linux-gnu/klee/runtime/klee-uclibc.bcaKLEE: NOTE: Using POSIX model: /usr/local/lib/x86_64-linux-gnu/klee/runtime/libkleeRuntimePOSIX.bcaKLEE: output directory is "/home/klee/seeds/../target/libpng-1.6.35/contrib/examples/klee-out-41"KLEE: Using STP solver backendKLEE: WARNING: undefined reference to function: floorKLEE: WARNING: undefined reference to function: modfKLEE: WARNING: undefined reference to function: powKLEE: KLEE: using 1 seeds
KLEE: 1 seeds remaining over: 1 statesKLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 147249744) at /home/klee/klee-gen-bout/runtime/POSIX/fd.c:980KLEE: 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 modelKLEE: WARNING ONCE: flushing 8192 bytes on read, may be slow and/or crash: MO504[8192] allocated at global:crc_tableKLEE: 1 seeds remaining over: 1 statesKLEE: 1 seeds remaining over: 1 statesKLEE: 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 constraintKLEE: WARNING ONCE: calling external: floor(4621195801218788662) at /home/klee/target/libpng-1.6.35/png.c:3375KLEE: 1 seeds remaining over: 1 statesKLEE: 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 255klee 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-devI 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:file2 - Inside my searcher create a map from instruction.txt so I know which is the next instruction3 - 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 state5 - 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 timeAlberto
[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

_______________________________________________
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