[klee-dev] Generate all solutions
Sylvain Gault
sylvain.gault at inria.fr
Mon Oct 6 03:27:50 BST 2014
Thanks for the explanation, and sorry for the late reply.
It was just not clear to me when the solver is actually called and what
it computes.
So, what I understand is that the solver is called every time there is a
conditional branching, and it just test for the feasability of both
branches. It doesn't provide a value for a symbolic input when the
solution is unique, it doesn't provide additional constraints for the
symbolic values (no constraint propagation).
It may, however, provide an example input when the program terminate or
when an error is encountered.
And the way concretizeByte work is that it may fork for every bit, thus
making a maximum of 256 subprocess, one for every possible value of the
byte. And that's why all the solutions should be printed. And the solver
is called before forking so that it doesn't fork if one process would
explore an unfeasible path. Right?
So it should theoretically only create as many process as the number of
solutions. Right?
Also, I should be able to write x = concretizeByte(x), isn't it?
I'm testing this right now, it seems to work, but is still very slow.
I guess it's the repeated invocations of the solver that takes some time
to do similar computations each time. That being said, compiling with
-O1 helps.
Sylvain
On Fri, Sep 12, 2014 at 07:11:38AM +0000, Kuchta, Tomasz wrote:
> 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
>
More information about the klee-dev
mailing list