[klee-dev] Generate all solutions
Kuchta, Tomasz
t.kuchta12 at imperial.ac.uk
Mon Oct 6 06:21:11 BST 2014
Hi Sylvain,
On 06/10/2014 03:27, "Sylvain Gault" <sylvain.gault at inria.fr> wrote:
>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?
One note: the term “fork” in KLEE means that you create new
ExecutionState, which is a representation
of a certain execution path (it contains a “snapshot” of program state for
that path). KLEE doesn’t spawn
a new processes for each path when forking (new process can, however, be
spawned for a call to the solver, AFAIK).
Yes, as far as I know paths are checked for feasibility to avoid going
into a path
that would not be possible in any concrete execution. I think that whether
the actual solver is called or
not might depend on a certain situation - for example you can have some
sort of results caching that could
prevent from calling the solver or you could have a trivial branch point,
that is uni-directional (so it’s a branch
instruction which only performs a jump).
Also I think that you can have solver calls that are not obvious from the
source code - for example a check for division by zero
has an “if” statement; solver chain can also be invoked when performing
memory operations.
>
>So it should theoretically only create as many process as the number of
>solutions. Right?
Yes, it should explore paths for the possible executions. Please note that
in general for large programs and when
much data is marked as symbolic, exploring all the paths might not be
possible in practice due to the path explosion problem.
You may want to try klee-stats tool that also prints some query statistics.
>
>Also, I should be able to write x = concretizeByte(x), isn't it?
It seems to me that after this call x will stop being symbolic, because it
will be assigned a concrete value in the function.
>
>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
>
HTH,
Best regards,
Tomek
>
>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
>>
>
>_______________________________________________
>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: 7870 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20141006/87471575/attachment.bin>
More information about the klee-dev
mailing list