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" <[email protected]> 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 <[email protected]> >>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 >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> > >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > >_______________________________________________ >klee-dev mailing list >[email protected] >https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
<<attachment: winmail.dat>>
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
