Need to understand how klee

Discussion:

Need to understand how klee_assume() works

General Email

2013-11-11 14:27:30 UTC

Hello,

I have the following program and I want to create the set of test cases and their corresponding constraints that only satisfy the conditions included in the klee_assume() expression.

#include <klee/klee.h>

int main()
{
int c,d,e,f;
klee_make_symbolic(&c, sizeof(c), "c");
klee_make_symbolic(&d, sizeof(d), "d");
klee_make_symbolic(&e, sizeof(e), "e");
klee_make_symbolic(&f, sizeof(f), "f");

klee_assume((((c==2)||(d==1))&&((e>=2)||((f<600)&&(e>=1))))||(((c == 1)||(d == 0))&&((e>=3)||((f<600)&&(e>=2)))));

return 0;
}

When I run this program, klee gives me the following:

KLEE: output directory = "klee-out-14"
KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 242
KLEE: done: completed paths = 21
KLEE: done: generated tests = 9

My question is why only 9 tests are generated however there are 21 paths? And if klee generates tests for only satisfiable paths, why the message "KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)" is generated and what does it indicate?

As you notice I used the junction operators && and ||, are these operators the right ones to use? I guess I have some misunderstanding of the use of klee_assume() function, so can I have more explanation of its usage?

Thanks
AKhalil

Urmas Repinski

2013-11-11 14:59:07 UTC

Permalink

Hi, AKhalil.

I suggest to try instead of using of logical 'and - &&' and 'or - ||' use bitwise 'and - &' and 'or - |'.

Difference practically between them is following: if logical && is used , a && b as example, and if a is false, then whole expression is false and b is not checked at all.
If to use bitwise &, then second parameter is checked too.

Practically in this case there is no difference what form to use, but i have no idea how klee_assume() function exactly is implemented and it is safer to use bitwise 'and' and 'or' operators instead of logical ones.

There is no misunderstanding, simply i suggest to use safer condition form, try to replace &&-s with &-s, and ||-s with |-s.

Urmas Repinski.
Date: Mon, 11 Nov 2013 06:27:30 -0800
From: general_mail2011-/***@public.gmane.org
To: klee-dev-AQ/***@public.gmane.org
Subject: [klee-dev] Need to understand how klee_assume() works

Hello,
I have the following program and I want to create the set of test cases and their corresponding constraints that only satisfy the conditions included in the klee_assume() expression.
#include <klee/klee.h>

int main()
{
int c,d,e,f;
klee_make_symbolic(&c, sizeof(c), "c");
klee_make_symbolic(&d, sizeof(d), "d");
klee_make_symbolic(&e, sizeof(e), "e");
klee_make_symbolic(&f, sizeof(f), "f");

klee_assume((((c==2)||(d==1))&&((e>=2)||((f<600)&&(e>=1))))||(((c == 1)||(d == 0))&&((e>=3)||((f<600)&&(e>=2)))));

return 0;}
When I run this program, klee gives me the following:
KLEE: output directory = "klee-out-14"
KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 242
KLEE: done: completed paths = 21
KLEE: done: generated tests = 9
My question is why only 9 tests are generated however there are 21 paths? And if klee generates tests for only satisfiable paths, why the message "KLEE: ERROR: /home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid klee_assume call (provably false)" is generated and what does it indicate?
As you notice I used the junction operators && and ||, are these operators the right ones to use? I guess I have some misunderstanding of the use of klee_assume() function, so can I have more explanation of its usage?
ThanksAKhalil

Paul Marinescu

2013-11-11 15:50:40 UTC

Permalink

Hello,
1. You may replace && with & as suggested if all operands are boolean
values and have no side-effects. This can work well in most scenarios.
See below to understand why.

2. The tricky part in your example is not about klee_assume, but how it
interacts with the code generated by the compiler. Consider the simpler
code below:

int b = (((c==2)||(d==1)));
klee_assume(b && "b cannot be true");

which produces a similar output:

KLEE: output directory = "klee-out-0"
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 53
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

The code gets compiled to

if (c == 2) {
b = 1;
} else if (d == 1) {
b = 1;
} else {
b = 0;
}

klee_assume(b && "b cannot be true");

Since there are 3 paths and all are feasible, klee_assume will be called
3 times with trivial arguments

klee_assume(1)
klee_assume(1)
klee_assume(0)

The first two paths go further while the 3rd is terminated, which is
pretty much what is intended. Ideally the paths which satisfy the assume
would be merged, but that's a different story and klee has only some
experimental support for it.

Regarding your other question (21 paths vs 9 test cases), that's because
by default klee generates a single test case per error. Use
--emit-all-errors to get all the test cases.

Paul

Post by Urmas Repinski
Hi, AKhalil.
I suggest to try instead of using of logical 'and - &&' and 'or - ||'
use bitwise 'and - &' and 'or - |'.
Difference practically between them is following: if logical && is used
, a && b as example, and if a is false, then whole expression is false
and b is not checked at all.
If to use bitwise &, then second parameter is checked too.
Practically in this case there is no difference what form to use, but i
have no idea how klee_assume() function exactly is implemented and it is
safer to use bitwise 'and' and 'or' operators instead of logical ones.
There is no misunderstanding, simply i suggest to use safer condition
form, try to replace &&-s with &-s, and ||-s with |-s.
Urmas Repinski.
------------------------------------------------------------------------
Date: Mon, 11 Nov 2013 06:27:30 -0800
Subject: [klee-dev] Need to understand how klee_assume() works
Hello,
I have the following program and I want to create the set of test cases
and their corresponding constraints that only satisfy the conditions
included in the klee_assume() expression.
#include <klee/klee.h>
int main()
{
int c,d,e,f;
klee_make_symbolic(&c, sizeof(c), "c");
klee_make_symbolic(&d, sizeof(d), "d");
klee_make_symbolic(&e, sizeof(e), "e");
klee_make_symbolic(&f, sizeof(f), "f");
klee_assume((((c==2)||(d==1))&&((e>=2)||((f<600)&&(e>=1))))||(((c ==
1)||(d == 0))&&((e>=3)||((f<600)&&(e>=2)))));
return 0;
}
KLEE: output directory = "klee-out-14"
invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 242
KLEE: done: completed paths = 21
KLEE: done: generated tests = 9
My question is why only 9 tests are generated however there are 21
paths? And if klee generates tests for only satisfiable paths, why the
/home/pgbovine/klee/examples/exploringAssume/t1.c:12: invalid
klee_assume call (provably false)" is generated and what does it indicate?
As you notice I used the junction operators && and ||, are these
operators the right ones to use? I guess I have some misunderstanding of
the use of klee_assume() function, so can I have more explanation of its
usage?
Thanks
AKhalil
_______________________________________________ klee-dev mailing list
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Paul Marinescu

2013-11-11 22:07:38 UTC

Permalink

As said before, klee is only exploring those paths which satisfy the condition. If you're referring to output files, ignore the tests which have an .user.err extension.

Paul

Thank you Paul for your prompt response.
What if I'm interested only in getting the feasible paths that satisfy the condition ((c==2)||(d==1)), i.e., in the paths that are evaluated to true. How can I achieve this (if possible)?
Thanks,
AKhalil
Hello,
1. You may replace && with & as suggested if all operands are boolean
values and have no side-effects. This can work well in most scenarios.
See below to understand why.
2. The tricky part in your example is not about klee_assume, but how it
interacts with the code generated by the compiler. Consider the simpler
int b = (((c==2)||(d==1)));
klee_assume(b && "b cannot be true");
KLEE: output directory = "klee-out-0"
KLEE: ERROR: invalid klee_assume call (provably false)
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 53
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3
The code gets compiled to
if (c == 2) {
b = 1;
} else if (d == 1) {
b = 1;
} else {
b = 0;
}
klee_assume(b && "b cannot be true");
Since there are 3 paths and all are feasible, klee_assume will be called
3 times with trivial arguments
klee_assume(1)
klee_assume(1)
klee_assume(0)
The first two paths go further while the 3rd is terminated, which is
pretty much what is intended. Ideally the paths which satisfy the assume
would be merged, but that's a different story and klee has only some
experimental support for it.
Regarding your other question (21 paths vs 9 test cases), that's because
by default klee generates a single test case per error. Use
--emit-all-errors to get all the test cases.
Paul