[klee-dev] how klee_set_forking works exactly?

[David Ramos]

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

-------------- next part --------------
HTML attachment scrubbed and removed