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

[Lei Zhang]

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