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

[Papapanagiotakis-Bousy, Iason]

Hi Thuan,


Thank you for pointing me to those two tools. Are you aware if there is any documentation for ZESTI ?


Regards,

Jason

________________________________
From: thuanpv.nus at gmail.com <thuanpv.nus at gmail.com> on behalf of Thuan Pham <thuanpv at comp.nus.edu.sg>
Sent: 14 December 2016 10:23:41
To: Papapanagiotakis-Bousy, Iason
Cc: klee-dev at imperial.ac.uk
Subject: Re: [klee-dev] Choosing the concrete values and getting the symbolic constraints

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<mailto: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<mailto:klee-dev at imperial.ac.uk>
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev


-------------- next part --------------
HTML attachment scrubbed and removed