[klee-dev] Questions about cex and klee_assume()

[Lei Zhang]

Thanks a lot for the answer!

I think I get your idea. By "given by the context", you mean that we want
to interpret p1->f2 as an unsigned int. And we want it to be less than 10U.
These two together determines the bytes referenced by p1->f2 can only be in
the range [0, 10). Latter we can make other pointers pointing to the same
bytes and enforce more constraints. It all depends on how you interpret it.

Yes, I lost a dereference in my example. Thanks for reminding!


On Mon, Jan 13, 2014 at 9:51 PM, Paul Marinescu <
paul.marinescu at imperial.ac.uk> wrote:

> In KLEE, symbolic data carries no notion of signedness with it. Signedness
> is given by the context, so 'klee_assume(p1->f2 < 10U)' means that the
> bytes referenced by p1->f2, interpreted as typeof(p1->f2), should be less
> than 10U. You may very well add another constraint where the same bytes are
> interpreted as a signed type.
>
> One last thing: your klee_make_symbolic should probably
> read klee_make_symbolic(f, 1000);
>
> Paul
>
> On 13 Jan 2014, at 01:11, Lei Zhang <antiagainst at gmail.com> wrote:
>
> Thanks for the answer, Paul!
>
> BTW, would you mind tell me how the signed/unsigned type is handled in
> klee? For example,
>
> struct A {
>   int f1;  // 4 bytes
>   unsigned f2;  // 4 byte
>   bool f3[10];  // 10 bytes
> };
>
> void *f = malloc(1000);
> klee_make_symbolic(f, sizeof(f));
> struct A *p1 = (struct A *) f;
> klee_assume(p1->f2 < 10U);
>     // will this make sure that f2 is greater than or equal to 0
> automatically?
>
> For the above case, f2 is only explicitly forced to be less than 10.
> However, since f2 is an unsigned int, it should be greater than or equal to
> 0. Will >= 0 be automatically enforced? Or, the 5th-8th byte of f can be
> combined to represent a negative number (with the most significant bit as
> 1, which is interpreted as a very large number for unsigned int)?
>
>
> On Sun, Jan 12, 2014 at 11:48 AM, Paul Marinescu <
> paul.marinescu at imperial.ac.uk> wrote:
>
>> The answer is indeed yes to both questions.
>>
>> Regarding the origin of the term 'counterexample', it's likely related to
>> the fact that a that a solution from KLEE's point of view is a
>> counterexample from STP's point of view (because STP decides validity while
>> KLEE looks for satisfiability).
>>
>> Paul
>>
>> On 12 Jan 2014, at 02:51, Lei Zhang <antiagainst at gmail.com> wrote:
>>
>> Hi All,
>>
>> I am reading KLEE's source code in order to add some functionalities for
>> it. After struggling with the details for a long time, I still have
>> difficulties with the following questions. Can somebody shed light on it?
>> Any explanation will be highly appreciated. Thanks!
>>
>> 1) Lots of places use "counter example (cex)" as parts of the names. For
>> me, counter examples mean instances that disprove a statement. However,
>> from my understanding of the code, couter examples just mean "some
>> assignments that satisfy a set of constraints" or "no solution", which is
>> quite the opposite. If this is actually the case, why is the misleading
>> "counter example" used? Maybe it is better to change it?
>>
>> Besides, klee_prefer_cex() only gives "preference" of the argument
>> constraint without forcing it (meaning test cases violate the constraint
>> can also be generated), while klee_assume() forces the argument constraint
>> to be true. Is this right?
>>
>> 2) If I first klee_make_symbolic() a large range of memory, and then
>> doing lots of pointer calculation and klee_assume(), will this actually
>> enforce the constraints on the underlying memory? For example, for the
>> following code,
>>
>> struct A {
>>   int f1;  // 4 bytes
>>   bool f2;  // 1 byte
>>   bool f3[10];  // 10 bytes
>> };
>>
>> void *f = malloc(1000);
>> klee_make_symbolic(f, sizeof(f));
>> struct A *p1 = (struct A *) f;
>> klee_assume(p1->f2 == 0);
>>     // will this make the 5th byte of f to be 0?
>> struct A *p2 = (struct A *) ( (char *) f + sizeof(struct A) + 3 );
>> klee_assume(p2->f3[0] == 1);
>>     // will this make the (15 + 3 + 6)th byte of f to be 1?
>>
>> By working through how the code handles the statements, I think the
>> answer to the above question are both yes. But my code just does not behave
>> as I expected. So I just need to double check my understanding.
>>
>> Thanks in advance!
>>
>> --
>> Best regards,
>> Lei Zhang
>>  _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>>
>
>
> --
> Best regards,
> Lei Zhang
>
>
>


-- 
Best regards,
Lei Zhang
-------------- next part --------------
HTML attachment scrubbed and removed