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 longer > the 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 could > have 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 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@a8a6399e6799:~/seeds$ > ../target/libpng-1.6.35/contrib/examples/pngpixel 1 1 > ../images/png-files-download.png > RGBA 255 255 255 255 > klee@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-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 <[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: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 > [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
