[klee-dev] Generate all solutions

[Kuchta, Tomasz]

Hi Sylvain, 

Regarding your question from the first e-mail - as far as I know there is
no easy way to get all possible values, except
for adding inequalities to the set of constraints, but if there exists one
I would be happy to learn about that.
One possible issue related to this problem is when you have non-monotonic
range of values, let¹s say 1..2 and 5..10 are SAT.

If I understand Daniel¹s example (which is very nice) correctly, what
happens is:
1. You mark variables x and y as symbolic

2. In concretizeByte function you iterate over all bits of the input
parameter (which is a symbolic single byte char); this is done in the
loop, by retrieving value of each bit through a bit mask

3. Since the input parameter ³input² to the function concretizeByte is
symbolic, ³if² statement inside the function will cause forking: ³then²
side will be for a given bit being ³1², ³else² side will be for a given
bit being ³0²; in order to fork, we need to call the solver to know
whether the other side of the branch is feasible

4. Since we iterate over all bits of a variable and fork at each bit, what
you get as a result are all possible combinations of 0s and 1s (see point
5)

5. Important part here is that before we call concretizeByte there is an
³if² statement inside ³main² that already puts some constraints on ³x² and
³y², so in concretizeByte not all combinations of bits will be possible

HTH,

Best regards,
Tomek

On 12/09/2014 05:12, "Sylvain Gault" <sylvain.gault at inria.fr> wrote:

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: winmail.dat
Type: application/ms-tnef
Size: 6030 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20140912/4836b88b/attachment.bin>