[klee-dev] how klee_set_forking works exactly?

[Sunha Ahn]

Thanks! it helped a lot!

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