See: http://llvm.org/viewvc/llvm-project/klee/trunk/lib/Core/Executor.cpp?annotate=178759 inside Executor::fork(). Line 704 is the path followed when forking is disabled, note it is only reached when both paths are feasible.
The feasibility of a path is checked using the constrain solver and the current path constraints on the symbolic expressions. - Daniel On Wed, Jul 3, 2013 at 11:06 AM, Sunha Ahn <[email protected]> wrote: > 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 > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
