[klee-dev] Choosing the concrete values and getting the symbolic constraints

[Thuan Pham]

Hi Jason,
What you want can be achieved by using concolic execution or using seed
mode in KLEE. The default mode of KLEE is symbolic execution.
For concolic execution, you can try ZESTI or S2E. For seed mode in KLEE,
you need somehow convert your concrete input to a .ktest file so KLEE can
read it.

The two approaches you tried should not work. First approach will result in
a constraint Phi ^ (x==value) where Phi is the path constraints so the
result is always x=value as you got or unsatisfiable. The second one also
does not work because by writing a concrete value to a symbolic variable,
you will write concrete value to the memory area allocated for this
variable in the symbolic memory model of KLEE -> that memory area will not
be symbolic anymore, it is concrete.
Hope it will helps,
Thuan

On Mon, Dec 12, 2016 at 8:33 PM, Papapanagiotakis-Bousy, Iason <
iason.papapanagiotakis-bousy.15 at ucl.ac.uk> wrote:

> Hi everyone,
>
>
> I would like to know how could I specify the concrete values chosen by
> KLEE to execute.
>
> Instead of the normal mode of KLEE I would like to be able to choose a
> value (I am interested only in integers and assume for simplification that
> there is only one symbolic variable in the program) and execute the program
> in KLEE with that value and record the symbolic constraints encountered.
>
>
> I've tried the following two approaches:
> 1) using klee_assume(x==the_value_of_my_choice)
>
> this does not seem to work as the only constraint that is generated in
> kquery is the one I've given to klee_assume.
>
>
> 2) assigning a value to the symbolic variable
>
> int x;
>
> klee_make_symbolic(&x, sizeof(x), "x");
>
> x=the_value_of_my_choice
>
> this does not seem to work either as the resulting kquery file has an
> empty query "(query [] false)".
>
>
> How could I pick the value used during concolic execution and get the
> symbolic constraints?
>
>
> Thank you in advance for your suggestions.
>
>
> Best regards,
>
> Jason
>
> _______________________________________________
> 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