[klee-dev] Guided Search - Help

[Alberto Barbaro]

Hi Andrew,
Thanks for your email and PR. So I tested gen-bout on a simple project
called first that prints a different message depending on the first byte of
file passed as a parameter. I think I did it properly because at the end I
had the file.bout file. At this point I was able to use klee-replay with it
and have the same stdout. Now I don't know how to use file.bout as a seed.
Are you happy to show me a simple example please? I would like to able to
use it in conjunction with a new searcher in order to 'execute,' queries at
runtime on the code.

Thanks a lot!

Alberto


On Mon, Oct 15, 2018, 01:19 Andrew Santosa <asantosa1999 at gmail.com> wrote:

> Hi Alberto,
>
> Thank you for describing your problem. I had submitted this PR some while
> ago:
> https://github.com/klee/klee/pull/956
>
> Basically I would use gen-bout implemented in the PR to create a ktest
> file using concrete inputs, then use the ktest file as a seed. In this way,
> all inputs will be symbolic, yet the path is the one that would have been
> executed using the concrete inputs.
>
> Best,
> Andrew
>
> On Sun, Oct 14, 2018 at 8:25 PM, 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