how klee_set_forking works exactly?

Discussion:

Sunha Ahn

2013-06-21 19:01:12 UTC

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.

Daniel Dunbar

2013-06-21 19:30:31 UTC

Permalink

If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.

- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Sunha Ahn

2013-06-21 20:23:54 UTC

Permalink

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.

Post by Daniel Dunbar
If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.
- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

David Ramos

2013-06-21 20:27:20 UTC

Permalink

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

Post by Sunha Ahn
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.
If I recall correctly, KLEE will just randomly (based on a fixed seed, though) choose a path when forking is disabled.
- Daniel
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Sunha Ahn

2013-06-21 20:39:33 UTC

Permalink

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.

Post by 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
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.

Post by Daniel Dunbar
If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.
- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

David Ramos

2013-06-21 20:41:41 UTC

Permalink

Yes. Otherwise, it would be exploring infeasible paths, which would be unsound and could generate false positives.

Post by 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.
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

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Sunha Ahn

2013-07-03 18:06:06 UTC

Permalink

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.

Post by David Ramos
Yes. Otherwise, it would be exploring infeasible paths, which would be
unsound and could generate false positives.
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.

Post by Daniel Dunbar
If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.
- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Daniel Dunbar

2013-07-03 18:11:20 UTC

Permalink

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

Post by Sunha Ahn
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.

Post by Daniel Dunbar
If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.
- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Sunha Ahn

2013-06-21 20:42:55 UTC

Permalink

Thanks! it helped a lot!

Best regards,
Sunha.

Post by David Ramos
Yes. Otherwise, it would be exploring infeasible paths, which would be
unsound and could generate false positives.
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.

Post by Daniel Dunbar
If I recall correctly, KLEE will just randomly (based on a fixed seed,
though) choose a path when forking is disabled.
- Daniel

Post by Sunha Ahn
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);
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev