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

[Lei Zhang]

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
-------------- next part --------------
HTML attachment scrubbed and removed