[klee-dev] Generate all solutions

[Sylvain Gault]

I have the feeling this solution is interesting but I don't understand
what happen for klee.

Sylvain Gault

On Thu, Sep 11, 2014 at 07:54:10PM -0700, Daniel Dunbar wrote:
> One "hack" to do this is to simply loop over all of bytes of the symbolic
> variable, and test each bit in them (you probably can't let the optimizer run
> on this code though, as it will figure out what is happening and remove it).
> For example:
> --
> #include <stdio.h>
> #include <klee/klee.h>
> 
> signed char concretizeByte(signed char input) {
>   unsigned char result = 0;
>   for (int i = 0; i != 8; ++i) {
>     if (input & (1<<i))
>       result |= 1<<i;
>   }
>   return result;
> }
> 
> int main() {
>   signed char x, y;
>   klee_make_symbolic(&x, sizeof(x), "x");
>   klee_make_symbolic(&y, sizeof(y), "y");
> 
>   if (56 * x + 72 * y == 40) {
>     printf("56 * (%d) + 72 * (%d) == 40\n", concretizeByte(x),
>            concretizeByte(y));
>   }
> 
>   return 0;
> }
> --
> will produce all possible solutions to the Diophantine equation 56 * x + 72 * y
> = 40.
> 
> This probably won't be fast. :)
> 
>  - Daniel
> 
> 
> On Sat, Aug 2, 2014 at 2:34 PM, Sylvain Gault <sylvain.gault at inria.fr> wrote:
> 
>     Hello,
> 
>     I would like to use klee as a front-end to an SMT solver. Basically,
>     what I currently do is:
>     - declare input as symbolic;
>     - write the computation in C;
>     - test whether the output is the one I want with an "if";
>     - make klee find an input that activate the "true" branch of the if.
> 
>     And it works quite well, it produce a solution.
>     But then I would like to obtain all the input assignments that would
>     activate that same path.
> 
>     Is there an easy way to do this?
>     I have the feeling that a hack-ish way to do this would be to get the
>     query to kleaver that activate that path (I think I saw an option for
>     that) and feed it repetidely to kleaver (or another SMT solver), each
>     time adding a clause negating the previous solutionS.
> 
>     I think this is a hackish solution because the solver would probably
>     make the same computation over and over again. While outputing the
>     solution and backtracking to find the next one directly would probably
>     be a lot more efficient. But I may be wrong.
> 
>     Thanks in advance.
> 
>     Regards,
>     Sylvain Gault
> 
>     _______________________________________________
>     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