Dear David, or who knows well about the KLEE source code. Can you please point out the source code where (1) KLEE randomly chooses which part of the branch to explore when klee_set_forking(0) is disabled? Also, (2) when the klee_set_forking is disabled and one branch is not feasible, KLEE execute the feasible branch instead of randomly choose one of those two branches. Can you please point out the code how KLEE tests and knows if the (infeasible branch) is infeasible?
I would like to see the source code part which implementes (1) and (2). Thanks for your help! Best regards, Sunha. 2013/6/21 David Ramos <[email protected]> > Yes. Otherwise, it would be exploring infeasible paths, which would be > unsound and could generate false positives. > > On Jun 21, 2013, at 1:39 PM, Sunha Ahn <[email protected]> wrote: > > Hi, David. > > Thanks! I got it. May I ask one more question? I guess you mean if one of > the branches is not feasible, KLEE will choose the feasible branch then? > > Thanks, > Sunha. > > > 2013/6/21 David Ramos <[email protected]> > >> Sunha, >> >> KLEE only chooses a random branch if both branch targets are feasible. >> Your call to klee_assume() constrains the value of 'x' so that only one of >> those branch targets is feasible in each of your examples. >> >> -David >> >> On Jun 21, 2013, at 1:23 PM, Sunha Ahn <[email protected]> wrote: >> >> Hi, Daniel. >> Thanks for the reply! >> >> However, I feel like it might not be totally random. >> >> For example, >> >> ---- >> int x; >> klee_make_symbolic(&x, sizeof(x), "x"); >> klee_assume(x>0); >> klee_set_forking(0); >> >> if(x<=0){ >> printf("1\n"); >> }else{ >> printf("2\n"); >> } >> ----- >> >> In this case, KLEE chooses the false path and prints "2". >> >> ---- >> int x; >> klee_make_symbolic(&x, sizeof(x), "x"); >> klee_assume(x>0); >> klee_set_forking(0); >> >> if(x>0){ >> printf("1\n"); >> }else{ >> printf("2\n"); >> } >> ----- >> >> In this case, KLEE chooses the true path and prints "1". >> >> Does it chooses totally randomly? Seems like it knows some information. >> >> Thanks a lot! >> >> Best regards, >> Sunha. >> >> >> >> 2013/6/21 Daniel Dunbar <[email protected]> >> >>> If I recall correctly, KLEE will just randomly (based on a fixed seed, >>> though) choose a path when forking is disabled. >>> >>> - Daniel >>> >>> >>> On Fri, Jun 21, 2013 at 12:01 PM, Sunha Ahn <[email protected]> wrote: >>> >>>> Hi, all. >>>> >>>> I would like to know how exactly klee_set_forking works. >>>> >>>> It seems like that, after klee_set_forking(0);, a branch controlled by >>>> a symbolic variable is not forked with both true/false sides any more. >>>> However, it still picks either one of the branch. I do not understand how >>>> they pick when the symbolic variable is still symbolic. >>>> >>>> For example, >>>> >>>> 1: int x; >>>> 2: klee_make_symbolic(&x, sizeof(x), "x"); >>>> 3: klee_assume(x>0); >>>> 4: klee_assume(x<10); >>>> 5: klee_set_forking(0); >>>> 6: >>>> 7: if(x>5){ >>>> 8: printf("1\n"); >>>> 9: }else{ >>>> 10: printf("2\n"); >>>> 11: } >>>> >>>> >>>> Here, it prints "2". >>>> At line 6, x is still symbolic, i.e. the value x can be either less >>>> than 5 or greater than 5. I do not understand how they choose the false >>>> branch. >>>> >>>> >>>> Besides this example, I would appreciate any explanation on how >>>> klee_set_forking works. >>>> >>>> >>>> I always appreciate that you answer my questions! >>>> >>>> Many many thanks, >>>> Sunha. >>>> >>>> _______________________________________________ >>>> klee-dev mailing list >>>> [email protected] >>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>>> >>>> >>> >>> _______________________________________________ >>> klee-dev mailing list >>> [email protected] >>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >>> >>> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> >> >> _______________________________________________ >> klee-dev mailing list >> [email protected] >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
