[klee-dev] Generate all solutions

[Daniel Dunbar]

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
>
-------------- next part --------------
HTML attachment scrubbed and removed