[klee-dev] Guided Search - Help
Alberto Barbaro
barbaro.alberto at gmail.com
Sun Oct 21 07:58:15 BST 2018
Hi Andrew,
I checked again and the number of completed of paths is not set to 1. Even
after few seconds it is set to 4. In my opinion this is due to the fact
that the input is symbolic so in case of an if with symbolic path, as
expected, multiple paths may be followed. Isn't it?
This is why my main goal is to have a searcher that follows specifically
one path based on the image passed to pngpixel in the first instance. I'm
working on it but for now it does not work properly.
Thanks
Il giorno sab 20 ott 2018 alle ore 16:16 Andrew Santosa <
asantosa1999 at gmail.com> ha scritto:
> 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
> <https://go.onelink.me/107872968?pid=InProduct&c=Global_Internal_YGrowth_AndroidEmailSig__AndroidUsers&af_wl=ym&af_sub1=Internal&af_sub2=Global_YGrowth&af_sub3=EmailSignature>
>
> On Sat, Oct 20, 2018 at 6:30 PM, Alberto Barbaro
> <barbaro.alberto at gmail.com> 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 <asantosa1999 at gmail.com> 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 <
> 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 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
>
> _______________________________________________
> 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