[klee-dev] how klee_set_forking works exactly?

[Sunha Ahn]

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 <daramos at stanford.edu>

> 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 <sahn at princeton.edu> 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 <daramos at stanford.edu>
>
>> 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 <sahn at princeton.edu> 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 <daniel at zuster.org>
>>
>>> 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 <sahn at princeton.edu> 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
>>>> 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
>>
>>
>>
>> _______________________________________________
>> 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