Query: Klee behavior with pointer de-referencing

[Sandeep]

Hello All,

Please consider the following program.

The intension of the program is to let KLEE choose a value of x so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.

Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)


Can anybody please give me some insight.

int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;

int **ptr = array + x;

int* temp = *ptr;

if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}


int main() {
int x;

klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}

[Cristian Cadar]

I only had a brief look at your code, but it looks like you are storing
the addresses of the x_i variables into the array, which is likely not
what you intended.

Cristian

Post by Sandeep
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Pablo González de Aledo]

I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.

May be the next code is simpler, and still explains the issue.

int main() {
int a;
int array[] = {1,2,3,4,5};

klee_make_symbolic(&a, sizeof(a), "a");

if(array[a] == 3)
return 0;
else
return 1;
}

Why does Klee generate 17 solutions when only one is possible (a == 2) ?

Thanks.

Post by Cristian Cadar
I only had a brief look at your code, but it looks like you are storing
the addresses of the x_i variables into the array, which is likely not what
you intended.
Cristian

Post by Sandeep
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
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

[Cristian Cadar]

See http://www.mail-archive.com/klee-dev-AQ/***@public.gmane.org/msg00891.html

Cristian

Post by Pablo González de Aledo
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a == 2) ?
Thanks.
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x,
sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Sandeep]

Hello Cristian,
I am the original author of the code that you looked at.

Let me explain my intention of the code (pasted below).

I am intentionally storing the addresses of xi's in a array of pointers.
Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored
as all possible values of the symbolic variable x will make
*temp > 0.

int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;

int **ptr = array + x;

int* temp = *ptr;

if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;

klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4));

return foo(x,10,20,30,40);
}

But Klee is reporting three paths.

Also ktest-tool gives the following information:

ktest file : 'klee-last/test000002.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 2

ktest file : 'klee-last/test000003.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3

ktest file : 'klee-last/test000001.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1

Can you please explain why I am getting this result.

With Thanks
Sandeep

Post by Cristian Cadar
Cristian

Post by Pablo González de Aledo
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a == 2) ?
Thanks.
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x,
sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<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

[Paul Marinescu]

As Cristian pointed in the previous reply, the answer lies in object resolution. klee does not report 3 paths, it reports 3 possible executions, all of which follow the same path. What differs between these 3 executions is the value of ptr, i.e. the object it points to.

Paul

Post by Sandeep
Hello Cristian,
I am the original author of the code that you looked at.
Let me explain my intention of the code (pasted below).
I am intentionally storing the addresses of xi's in a array of pointers. Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored as all possible values of the symbolic variable x will make
*temp > 0.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4));
return foo(x,10,20,30,40);
}
But Klee is reporting three paths.
ktest file : 'klee-last/test000002.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 2
ktest file : 'klee-last/test000003.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3
ktest file : 'klee-last/test000001.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
Can you please explain why I am getting this result.
With Thanks
Sandeep

Post by Cristian Cadar
Cristian

Post by Pablo González de Aledo
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a == 2) ?
Thanks.
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to
happen. But
in addition it is reporting two other paths for x = 1 and x =2, despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<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

--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[Cristian Cadar]

Indeed. You have a double-dereference there, and KLEE cannot reason
symbolically about this, so it's forking into all possible cases
(alternatively it could choose only one option). There is a discussion
about double-dereferences in the paper describing KLEE's predecessor EXE
(http://www.doc.ic.ac.uk/~cristic/papers/exe-tissec-08.pdf).

Cristian

Post by Paul Marinescu
As Cristian pointed in the previous reply, the answer lies in object
resolution. klee does not report 3 paths, it reports 3 possible
executions, all of which follow the same path. What differs between
these 3 executions is the value of ptr, i.e. the object it points to.
Paul

Post by Sandeep
Hello Cristian,
I am the original author of the code that you looked at.
Let me explain my intention of the code (pasted below).
I am intentionally storing the addresses of xi's in a array of
pointers. Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored
as all possible values of the symbolic variable x will make
*temp > 0.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4));
return foo(x,10,20,30,40);
}
But Klee is reporting three paths.
ktest file : 'klee-last/test000002.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 2
ktest file : 'klee-last/test000003.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3
ktest file : 'klee-last/test000001.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
Can you please explain why I am getting this result.
With Thanks
Sandeep

Post by Cristian Cadar
Cristian

Post by Pablo González de Aledo
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a == 2) ?
Thanks.
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to
happen. But
in addition it is reporting two other paths for x = 1 and x =2,
despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x,
sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<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

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
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

[Sandeep Dasgupta]

Thanks a lot Cristian. Appreciate your help.

Indeed. You have a double-dereference there, and KLEE cannot reason
symbolically about this, so it's forking into all possible cases
(alternatively it could choose only one option). There is a
discussion about double-dereferences in the paper describing KLEE's
predecessor EXE
(http://www.doc.ic.ac.uk/~cristic/papers/exe-tissec-08.pdf).
Cristian

Post by Paul Marinescu
As Cristian pointed in the previous reply, the answer lies in object
resolution. klee does not report 3 paths, it reports 3 possible
executions, all of which follow the same path. What differs between
these 3 executions is the value of ptr, i.e. the object it points to.
Paul

Post by Sandeep
Hello Cristian,
I am the original author of the code that you looked at.
Let me explain my intention of the code (pasted below).
I am intentionally storing the addresses of xi's in a array of
pointers. Also I am constraining x to take values 1,2 and 3.
My expectation is that only one path of the if condition got explored
as all possible values of the symbolic variable x will make
*temp > 0.
int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4));
return foo(x,10,20,30,40);
}
But Klee is reporting three paths.
ktest file : 'klee-last/test000002.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 2
ktest file : 'klee-last/test000003.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3
ktest file : 'klee-last/test000001.ktest'
args : ['kleetest_5.o']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
Can you please explain why I am getting this result.
With Thanks
Sandeep

Post by Cristian Cadar
Cristian

Post by Pablo González de Aledo
I'm sorry, I'm not the original author but I've faced the same problem
before and I also don't understand why Klee does what it does.
May be the next code is simpler, and still explains the issue.
int main() {
int a;
int array[] = {1,2,3,4,5};
klee_make_symbolic(&a, sizeof(a), "a");
if(array[a] == 3)
return 0;
else
return 1;
}
Why does Klee generate 17 solutions when only one is possible (a == 2) ?
Thanks.
I only had a brief look at your code, but it looks like you are
storing the addresses of the x_i variables into the array, which is
likely not what you intended.
Cristian
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x
so that
the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to
happen. But
in addition it is reporting two other paths for x = 1 and x =2,
despite
of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path
(as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int
x3, int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x,
sizeof(x), "x");
klee_assume((x > 0) & (x <
4)); // To
allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<https://mailman.ic.ac.uk/mailman/listinfo/klee-dev>
_________________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/__mailman/listinfo/klee-dev
<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

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science
_______________________________________________
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

[Sandeep]

Hello Tomasz,
Thanks a lot for the try.

As you said the test case that you are getting is for failed external
assert call.
But what is expected in this case is *one *testcase for the path
(*temp > 0) (as all values of the symbolic variable x will suggest that
path only).

Can you please add #include<assert.h> and run it again. (I am also
getting the same behavior if I omit #include<assert.h> ).


Thanks
Sandeep

Hi Sandeep,
tk2512:/data/temp$ /data/temp/klee/Release+Asserts/bin/klee test.bc
KLEE: output directory = "klee-out-4"
KLEE: WARNING: undefined reference to function: assert
KLEE: WARNING ONCE: calling external: assert(1)
KLEE: ERROR: /data/temp/test.c:13: failed external call: assert
KLEE: NOTE: now ignoring this error at this location
KLEE: done: total instructions = 69
KLEE: done: completed paths = 3
KLEE: done: generated tests = 1
1 test file is generated (this is for failed external call assert and
ktest-tool --write-ints test000001.ktest
ktest file : 'test000001.ktest'
args : ['test.bc']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
Best regards,
Tomek
Date: Wednesday, 18 December 2013 20:29
Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing
Thanks a lot Tomasz.
I two believe that only two paths should get reported. But I am
getting 3 (with one abort)
Can you please confirm the number of paths that you are getting with
the following call to foo
return foo(x,10,20,30,40);
I believe it is just 1 in your case.
Thanks
Sandeep

Hello Sandeep,
It seems to me that both paths are possible here.
We first constraint x to be 1, 2 or 3 by doing klee_assume((x > 0) &
(x < 4)).
Then we will have the following values for the corresponding indices
in the “array”,
array[1] == 20
array[2] == 30
array[3] == -1
Both: array[1] and array[2] will exercise the path leading to
assert(1), because their values are greater than 0.
On the other hand, array[3] will exercise the path leading to
assert(0), because its value is –1.
I’ve run the test on the current latest version of KLEE and two
ktest-tool --write-ints test000001.ktest
ktest file : 'test000001.ktest'
args : ['test.bc']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 1
ktest-tool --write-ints test000002.ktest
ktest file : 'test000002.ktest'
args : ['test.bc']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: 3
The first file corresponds to the path exercised by value 20 of
array[1] (x == 1, which transforms to array[1]).
The second file corresponds to the path exercised by value –1 of
array[3] (x == 3, which transforms to array[3]).
Hope that helps,
Best regards
Tomek
Date: Wednesday, 18 December 2013 06:39
Subject: [klee-dev] Query: Klee behavior with pointer de-referencing
Hello All,
Please consider the following program.
The intension of the program is to let KLEE choose a value of x so
that the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen.
But in addition it is reporting two other paths for x = 1 and x =2,
despite of the fact that there are only 2 possible paths.
Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the
path (*temp > 0) is not feasible for any value of x)
Can anybody please give me some insight.
int foo(int x, int x1, int x2, int x3,
int x4) {
int **array = (int **)
malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;
int **ptr = array + x;
int* temp = *ptr;
if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}
int main() {
int x;
klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4)); //
To allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}
--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

--
*With Thanks and Regards,*
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science

[Kuchta, Tomasz]

Hi Sandeep,

I’ve checked the program with added #include <assert.h> on the latest KLEE.

This is the result that I get:


klee test.bc

KLEE: output directory = "klee-out-5"


KLEE: done: total instructions = 102

KLEE: done: completed paths = 3

KLEE: done: generated tests = 3


This time 3 test cases were created:


ktest-tool --write-ints test000001.ktest

ktest file : 'test000001.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 1


ktest file : 'test000002.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 2


ktest-tool --write-ints test000003.ktest

ktest file : 'test000003.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 3


Please find the source file that I’ve used attached.

I am definitely not an expert, but taking the archive thread mentioned by Cristian (http://www.mail-archive.com/klee-dev-AQ/***@public.gmane.org/msg00891.html) as a hint,
I can guess that this behaviour might be caused by the object resolution.

The variable “x” is symbolic and it is constrained to be 1,2 or 3. We create the “temp” pointer by offsetting the array pointer by the symbolic
offset “x”. Since “x” is symbolic, now “temp” can point to one of three different memory objects: array[1], array[2] or array[3].
I guess this is the reason why we do get 3 executions here.

You may want to take a look at Executor::executeMemoryOperation.

To make a quick test I’ve added a printout in this part of the function:


ExecutionState *unbound = &state;



for (ResolutionList::iterator i = rl.begin(), ie = rl.end(); i != ie; ++i) {

klee_message(“resolution list”); // <<<< added by me


And when I executed the program once more, I got:


klee test.bc

KLEE: output directory = "klee-out-7"

KLEE: resolution list

KLEE: resolution list

KLEE: resolution list


KLEE: done: total instructions = 102

KLEE: done: completed paths = 3

KLEE: done: generated tests = 3

The added message is appearing thee times, which means that we have three possible objects that the pointer can point at.
In the code just below the mentioned fragment, we have a line calling “fork” function, which essentially means creating an alternative execution path.

I might be wrong, but my guess would be that we have three test cases here, because the pointer that we create using the constrained symbolic value ‘x’ can be pointing at three different memory
objects.

Hope that helps.

Tomek


From: Sandeep <sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org<mailto:sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org>>
Date: Wednesday, 8 January 2014 16:58
To: "Kuchta, Tomasz" <t.kuchta12-AQ/***@public.gmane.org<mailto:***@imperial.ac.uk>>, klee-dev <klee-dev-AQ/***@public.gmane.org<mailto:klee-dev-AQ/***@public.gmane.org>>
Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing

Hello Tomasz,
Thanks a lot for the try.

As you said the test case that you are getting is for failed external assert call.
But what is expected in this case is one testcase for the path (*temp > 0) (as all values of the symbolic variable x will suggest that path only).

Can you please add #include<assert.h> and run it again. (I am also getting the same behavior if I omit #include<assert.h> ).


Thanks
Sandeep

On 12/18/2013 3:53 PM, Kuchta, Tomasz wrote:
Hi Sandeep,

For foo (x, 10, 20, 30, 40) the result is the following:


tk2512:/data/temp$ /data/temp/klee/Release+Asserts/bin/klee test.bc

KLEE: output directory = "klee-out-4"

KLEE: WARNING: undefined reference to function: assert

KLEE: WARNING ONCE: calling external: assert(1)

KLEE: ERROR: /data/temp/test.c:13: failed external call: assert

KLEE: NOTE: now ignoring this error at this location


KLEE: done: total instructions = 69

KLEE: done: completed paths = 3

KLEE: done: generated tests = 1


1 test file is generated (this is for failed external call assert and x == 1):


ktest-tool --write-ints test000001.ktest

ktest file : 'test000001.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 1

Best regards,

Tomek

From: Sandeep <sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org<mailto:sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org>>
Date: Wednesday, 18 December 2013 20:29
To: "Kuchta, Tomasz" <t.kuchta12-AQ/***@public.gmane.org<mailto:***@imperial.ac.uk>>, "klee-dev-bounces-AQ/***@public.gmane.org<mailto:klee-dev-***@imperial.ac.uk>" <klee-dev-bounces-AQ/***@public.gmane.org<mailto:klee-dev-***@imperial.ac.uk>>
Subject: Re: [klee-dev] Query: Klee behavior with pointer de-referencing

Thanks a lot Tomasz.
I two believe that only two paths should get reported. But I am getting 3 (with one abort)

Can you please confirm the number of paths that you are getting with the following call to foo

return foo(x,10,20,30,40);

I believe it is just 1 in your case.


Thanks
Sandeep



On 12/18/2013 01:41 AM, Kuchta, Tomasz wrote:
Hello Sandeep,

It seems to me that both paths are possible here.
We first constraint x to be 1, 2 or 3 by doing klee_assume((x > 0) & (x < 4)).
Then we will have the following values for the corresponding indices in the “array”,
if we call foo() with arguments x1 = 10, x2 = 20, x3 = 30, x4 = -1:

array[1] == 20
array[2] == 30
array[3] == -1

Both: array[1] and array[2] will exercise the path leading to assert(1), because their values are greater than 0.
On the other hand, array[3] will exercise the path leading to assert(0), because its value is –1.

I’ve run the test on the current latest version of KLEE and two *.ktest files were created:


ktest-tool --write-ints test000001.ktest

ktest file : 'test000001.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 1


ktest-tool --write-ints test000002.ktest

ktest file : 'test000002.ktest'

args : ['test.bc']

num objects: 1

object 0: name: 'x'

object 0: size: 4

object 0: data: 3


The first file corresponds to the path exercised by value 20 of array[1] (x == 1, which transforms to array[1]).

The second file corresponds to the path exercised by value –1 of array[3] (x == 3, which transforms to array[3]).


Hope that helps,

Best regards

Tomek

From: Sandeep <sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org<mailto:sdasgup3-nzINlOoChub2fBVCVOL8/***@public.gmane.org>>
Date: Wednesday, 18 December 2013 06:39
To: klee-dev <klee-dev-AQ/***@public.gmane.org<mailto:klee-dev-AQ/***@public.gmane.org>>
Subject: [klee-dev] Query: Klee behavior with pointer de-referencing

Hello All,

Please consider the following program.

The intension of the program is to let KLEE choose a value of x so that the path (*temp <= 0) is explored and
KLEE is able to figure out the value of x (= 3) for that to happen. But in addition it is reporting two other paths for x = 1 and x =2, despite of the fact that there are only 2 possible paths.

Also to add, if I call foo with
foo(x, 10,20,30,40)
then KLEE report 3 paths (for x = 1 ,2 ,3 ) instead of 1 path (as the path (*temp > 0) is not feasible for any value of x)


Can anybody please give me some insight.

int foo(int x, int x1, int x2, int x3, int x4) {
int **array = (int **) malloc(4*sizeof(int *));
array[0] = &x1;
array[1] = &x2;
array[2] = &x3;
array[3] = &x4;


int **ptr = array + x;

int* temp = *ptr;

if(*temp > 0) {
assert(1);
} else {
assert(0);
}
return *temp;
}


int main() {
int x;

klee_make_symbolic(&x, sizeof(x), "x");
klee_assume((x > 0) & (x < 4)); // To allow valid memory access on 'array'
return foo(x,10,20,30,-1);
}



--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science


--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science


--
With Thanks and Regards,
Sandeep Dasgupta
Graduate ( PhD ) in Computer Science
Room : 1218 Siebel Center for Computer Science