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

[Paul Marinescu]

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

On 11 Nov 2013, at 21:58, General Email <general_mail2011 at yahoo.com> wrote:

> 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
> 
> 
> 
> 
> On Monday, November 11, 2013 7:51 AM, Paul Marinescu <paul.marinescu at imperial.ac.uk> wrote:
> 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
> 
> >
> 
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
> 
> 

-------------- next part --------------
HTML attachment scrubbed and removed