[klee-dev] Guided Search - Help

[Sang Phan]

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
>
-------------- next part --------------
HTML attachment scrubbed and removed