[klee-dev] how klee_set_forking works exactly?

[Sunha Ahn]

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
>
>
-------------- next part --------------
HTML attachment scrubbed and removed