Generate multiple concrete inputs to cover each path‏

[jiaquan]

Hello All,
I would like to know if it's possible to generate multiple concrete inputs/tests to cover each path of a test program, with or without modifying KLEE's source code.
I'm new to KLEE and have just gone through the tutorials on klee.llvm.org. In my experience, I noticed that KLEE only produces one concrete input/test for each path of a test program.
I'm wondering if there's a command line option to let KLEE produce more than one concrete input/test per path? If not, is there another way to achieve this?
On top of my head, the options are:
A. Rerun KLEE multiple times to get different sets of inputs/tests. I have tried this, but I could only see the same inputs/tests getting repeated over and over again. Is there a way to let KLEE generate randomized inputs/tests across different runs?
B. Dump all symbolic inputs/tests generated by KLEE to a file and parse it myself. Is there a command line switch to make such a dump?
C. Re-write KLEE's code that converts a symbolic input to a concrete input. If I have to do this, which part of the code should I look into?
Your help would be greatly appreciated!
Regards,Charlie

[Daniel Liew]

I think option B might be the easiest. You could try this after
generating all test cases.

1. Get a satisfying assignment for the constraints by running a
constraint solver on the constraints
2. If a satisfying assignment is found add an assertion that the
satisfying assignment is not the answer you just got. If no satisfying
assignment is found you've found all possible assignments and you can
STOP.

e.g. This adds an assertions (SMT-LIBv2 language) that the bitvector
array named "array_name" does not have first two bytes equal to all
ones.

(assert (not (= (select array_name (_ bv0 32) ) 0xff) )
(assert (not (= (select array_name (_ bv1 32) ) 0xff) )

3. Repeat

KLEE can output constraints for test cases in two formats: kQuery and
SMT-LIBv2. My advise would be to use the SMT-LIBv2 format because more
solvers are available and kleaver (the constraint solver for kQuery
files) is buggy and confusing (uses validity instead of
satisfiability).

To do this run KLEE with --write-smt2s . Note you can use the options

--smtlib-human-readable
--smtlib-use-let-expressions
--smtlib-display-constants

to tweak the output generated by the --write-smt2s flag.


If you wanted to automate this process and you know python, Z3 might
be a good choice of constraint because it has a python API.

Hope this helps.

Thanks,
Dan Liew.

Post by jiaquan
Hello All,
I would like to know if it's possible to generate multiple concrete
inputs/tests to cover each path of a test program, with or without modifying
KLEE's source code.
I'm new to KLEE and have just gone through the tutorials on klee.llvm.org.
In my experience, I noticed that KLEE only produces one concrete input/test
for each path of a test program.
I'm wondering if there's a command line option to let KLEE produce more than
one concrete input/test per path? If not, is there another way to achieve
this?
A. Rerun KLEE multiple times to get different sets of inputs/tests. I have
tried this, but I could only see the same inputs/tests getting repeated over
and over again. Is there a way to let KLEE generate randomized inputs/tests
across different runs?
B. Dump all symbolic inputs/tests generated by KLEE to a file and parse it
myself. Is there a command line switch to make such a dump?
C. Re-write KLEE's code that converts a symbolic input to a concrete input.
If I have to do this, which part of the code should I look into?
Your help would be greatly appreciated!
Regards,
Charlie