[klee-dev] Need to understand how klee_assume() works

[Paul Marinescu]

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

On 11/11/13 14:59, Urmas Repinski wrote:
> 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 at yahoo.com
> To: klee-dev at imperial.ac.uk
> 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?
>
> Thanks
> AKhalil
>
>
>
> _______________________________________________ klee-dev mailing list
> klee-dev at imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>