Questions about cex and klee

Discussion:

Questions about cex and klee_assume()

Lei Zhang

2014-01-12 02:51:49 UTC

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

Paul Marinescu

2014-01-12 16:48:52 UTC

Permalink

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

Post by 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
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Lei Zhang

2014-01-13 01:11:54 UTC

Permalink

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 <

Post by Paul Marinescu
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

--
Best regards,
Lei Zhang

Paul Marinescu

2014-01-14 02:51:25 UTC

Permalink

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

Post by 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)?
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

--
Best regards,
Lei Zhang

Lei Zhang

2014-01-14 21:25:29 UTC

Permalink

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 <

Post by Paul Marinescu
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
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 <

Post by Paul Marinescu
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
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

--
Best regards,
Lei Zhang