[klee-dev] Seeding KLEE with a concrete input

[Super Zhang]

I ever used both methods as Paul mentioned.

zesti is cool, it could automatically use your concrete command line
parameters as search seeds. But you need to use zesti code base:).

For the second method, you could use gen-random-bout tool(under the same
folder of your klee binary, source code
location: tools/gen-random-bout/gen-random-bout.cpp)
for example, you could generate a random ktest file with this command line:
gen-random-bout 100 --sym-args 0 2 2 --sym-files 1 8
check the generated file.bout under the current folder.

For your specific purpose, you could just copy KTest.h and KTest.cpp file
out of klee project and make a standalone program to convert your concrete
inputs into ktest files to feed klee with the command line option
--seed-out. Still, gen-random-bout.cpp will be a great example for how to
do this.

Chaoqiang

Super




On Thu, Nov 14, 2013 at 6:03 AM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> There's no easy way to do it as far as I know. We did this, among others,
> in ZESTI (http://srg.doc.ic.ac.uk/projects/zesti/) but it required
> changes to code.
>
> If you only want to use KLEE, the 'easiest' way to do it would be to
> somehow create a ktest file corresponding to your concrete input and then
> use it as a seed for KLEE - there's a command line argument for that. You
> probably need to make sure that the symbolic objects are created by KLEE in
> the same order as they appear in the ktest file (i.e. via --sym-args or
> klee_make_symbolic). I've never tried this though and can't guarantee it.
>
> Paul
>
> > On 14 Nov 2013, at 02:52, Vijay Ganesh <hellovijay at gmail.com> wrote:
> >
> > Hi,
> >
> > I want to seed KLEE with a concrete input, i.e., I only care about the
> symbolic expression corresponding to the path taken by the program on a
> concrete input. How can I force KLEE to just produce that one path
> constraint?
> >
> > Cheers,
> > Vijay.
> > _______________________________________________
> > 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