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

[Cristian Cadar]

Hi, there is some documentation for ZESTI at 
https://srg.doc.ic.ac.uk/projects/zesti/.  Unfortunately, the project is 
not maintained anymore.

Best,
Cristian

On 14/12/2016 12:46, Papapanagiotakis-Bousy, Iason wrote:
> 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
>     <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
>