[klee-dev] how klee_set_forking works exactly?

[Daniel Dunbar]

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 <sahn at princeton.edu> 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 <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
>>
>>
>
> _______________________________________________
> 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