Hi Alberto, KLEE prints the number of tests and paths at the end of its run, but this is not shown in your log. With the options that you provided KLEE with (-only-replay-seeds) and with only one seed (png-files-download.bout), I expect the number of paths to be 1, in which case only one path is traversed. Best, Andrew
Sent from Yahoo Mail on Android On Sat, Oct 20, 2018 at 6:30 PM, Alberto Barbaro<[email protected]> wrote: Hi Andrew,Thanks a lot. I understand now, so it would follow all the paths because the input is symbolic. In my mind I would like to have a searcher that would follow only and only one path with symbolic data. This path should be generated with a concrete file. This is I'm working on a searcher but I cannot do it properly for now. Thanks On Sat, Oct 20, 2018, 09:58 Andrew Santosa <[email protected]> wrote: 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 <[email protected]> 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@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@a8a6399e6799:~/seeds$ ../target/libpng-1.6.35/contrib/examples/pngpixel 1 1 ../images/png-files-download.png RGBA 255 255 255 255klee@a8a6399e6799:~/seeds$ What am I missing? :) Thanks for your help! Alberto Il giorno mar 16 ott 2018 alle ore 14:27 Alberto Barbaro <[email protected]> ha scritto: Thanks I'll try that one later :) On Tue, Oct 16, 2018, 14:08 Sang Phan <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 <[email protected]> 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 [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
