[klee-dev] how klee_set_forking works exactly?

[David Ramos]

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